104/160
\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}