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