\begin{frame}[t]{Model Infiniteness is Undefinable by a Single Formula} \begin{block}{Corollary} There is \alert{no} sentence\/ $\bform$ such that for all $\model{\amodel}$: \begin{talign}\tag{$\star$}\label{eq:bform:defines:infiniteness} \model{\amodel} \satisfies \bform \;\;\iff\;\; \text{\normalfont $\model{\amodel}$ has an \alert{infinite} domain} \end{talign} \end{block}\pause{} \begin{proof} \dm{Suppose that there exists} a sentence $\bform$ such that \eqref{eq:bform:defines:infiniteness} holds. \pause\medskip Then we find that \alert{$\formula{\lognot{\bform}}$} actually defines \alert{model finiteness}: \begin{talign} \mpause[1]{\model{\amodel} \satisfies \formula{\lognot{\bform}}} \;\; & \mpause{ \Longleftrightarrow\;\; \text{not: } \model{\amodel} \satisfies \bform } \\ \;\; & \mpause{ \Longleftrightarrow\;\; \text{not: } \text{$\model{\amodel}$ has an \alert{infinite} domain} } \\ \;\; & \mpause{ \Longleftrightarrow\;\; \text{$\model{\amodel}$ has a \alert{finite} domain} } \end{talign} \updatepause We know that such sentence does not exist. \pause\medskip We conclude that the \alert{assumption} was \alert{wrong}. \end{proof} \end{frame}