\begin{frame}[t]{Model Finiteness is Undefinable (Set of Formulas)} \begin{block}{Theorem (Finiteness is Undefinable)} There is \alert{no} set of formulas\/ $\asetforms$ such that for all $\model{\amodel}\,$: %, $\saluf\,$: \begin{talign}\label{eq:bform:defines:finiteness}\tag{$\star$} \model{\amodel} \satisfies \asetforms \;\;\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 a set \alert{$\asetforms$} expresses finiteness in the sense \eqref{eq:bform:defines:finiteness}. \pause\medskip Consider the set $\bsetforms \;\; = \;\; \alert{\asetforms} \:\cup\: \setexp{ \aformi{2},\, \aformi{3},\, \aformi{4},\, \ldots }$. \pause\medskip \mediumblue{(B)} The set $\bsetforms$ is \emph{inconsistent}\malt[1]{: \begin{itemize}\setlength{\itemsep}{0pt} \item $\model{\amodel} \satisfies \alert{\asetforms}$ $\iff$ $\amodel$ is finite \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[1]{: \begin{itemize}\setlength{\itemsep}{0pt} \item Let $\forestgreen{n_0}$ be the largest number such that $\aformi{\forestgreen{n_0}} \in \bsetformsi{0}$. \item Take a model $\model{\amodel}$ with $\forestgreen{n_0}$ elements. \item Then $\model{\amodel} \satisfies \aformi{n}$ for all $\aformi{n}\in\bsetformsi{0}$, and $\model{\amodel} \satisfies \alert{\asetforms}$. Thus $\model{\amodel} \satisfies \bsetformsi{0}$. \end{itemize} }{.} \updatepause\bigskip A set $\bsetforms$ with \mediumblue{(B)} and \mediumblue{(C)} {contradicts} the {compactness theorem}. \medskip The problem must be assumption~\mediumblue{(A)}. \medskip Hence \emph{there cannot be such a set of formulas $\alert{\asetforms}$}. \end{overlayarea} \end{block} \vspace{10cm} \end{frame}