\begin{frame}[t]{Model Finiteness is Undefinable (Single Formula)} \begin{block}{Theorem (Finiteness is Undefinable)} There is \alert{no} sentence\/ $\bform$ such that for all $\model{\amodel}\,$: %, $\saluf\,$: \begin{talign}\label{eq:bform:defines:finiteness}\tag{$\star$} \model{\amodel} \satisfies \bform \;\;\Longleftrightarrow\;\; \text{\normalfont $\model{\amodel}$ has a \alert{finite} domain} \end{talign} \end{block} \pause \begin{block}{Proof} \begin{overlayarea}{\linewidth}{25ex}\vspace{-1ex}% \pause \mediumblue{(A)} Suppose sentence $\bform$ expresses finiteness in the sense \eqref{eq:bform:defines:finiteness}. \pause\medskip Consider the set \alert{$\bsetforms \;\; = \;\; \setexp{ \bform } \:\cup\: \setexp{ \aformi{2},\, \aformi{3},\, \aformi{4},\, \ldots }$}. \pause\medskip \mediumblue{(B)} The set $\bsetforms$ is \emph{inconsistent}\malt[3]{: \begin{itemize}\setlength{\itemsep}{0pt} \pause \item $\model{\amodel} \satisfies \bform$ $\iff$ $\amodel$ is finite \pause \item $\model{\amodel} \satisfies \setexp{ \aformi{2},\, \aformi{3},\, \aformi{4},\, \ldots }$ $\iff$ $\amodel$ is infinite \end{itemize} }{.} \updatepause\medskip \mediumblue{(C)} Yet every finite $\bsetformsi{0}\subseteq\bsetforms$ is \emph{consistent}\malt[4]{: \pause \begin{itemize}\setlength{\itemsep}{0pt} \item Let $\forestgreen{n_0}$ be the largest number such that $\aformi{\forestgreen{n_0}} \in \bsetformsi{0}$. \pause \item Take a model $\model{\amodel}$ with $\forestgreen{n_0}$ elements. \pause \item Then $\model{\amodel} \satisfies \aformi{n}$ for all $\aformi{n}\in\bsetformsi{0}$, and $\model{\amodel} \satisfies \bform$. \pause Thus $\model{\amodel} \satisfies \bsetformsi{0}$. \end{itemize} }{.} \updatepause\bigskip A set $\bsetforms$ with \mediumblue{(B)} and \mediumblue{(C)} \alert{contradicts} the \alert{compactness theorem}. \pause\medskip The problem must be assumption~\mediumblue{(A)}. \pause\medskip Hence \emph{there cannot be such a formula $\bform$}. \end{overlayarea} \end{block} \vspace{10cm} \end{frame}