\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}