\begin{frame}[t]{Model Infiniteness is Definable by Set of Formulas}  
  \begin{proposition}
    There is a set $\bsetforms$ of sentences such that for all $\model{\amodel}$:
    \begin{talign}
       \model{\amodel} \satisfies \bsetforms
       \;\;\Longleftrightarrow\;\;
       \text{\normalfont $\model{\amodel}$ has an \alert{infinite} domain}
    \end{talign}     
  \end{proposition}
  \pause

  \begin{proof}
    Let $\bsetforms = \setexp{ \aformi{2},\, \aformi{3},\, \aformi{4},\, \ldots }$
    where $\aformi{\forestgreen{n}}$ express `at least $\forestgreen{n}$ values'.
    \pause\medskip
    
    Then it holds for all models $\model{\amodel}$:
    \begin{talign}
      \model{\amodel} \satisfies \bsetforms
      \;\; & \mpause[1]{ \Longleftrightarrow\;\; 
                      \model{\amodel} \satisfies \aformi{\forestgreen{n}} \; \text{for all $\forestgreen{n}\ge 2$}}
      \\
      \;\; & \mpause{ \Longleftrightarrow\;\;
                      \text{$\model{\amodel}$ has at least $\forestgreen{n}$ values, for all $\forestgreen{n}  \in\nat$}}
      \\
      \;\; & \mpause{ \Longleftrightarrow\;\;
                      \text{$\model{\amodel}$ has infinitely many values}}
      \\
      \;\; & \mpause{ \Longleftrightarrow\;\;
                      \text{$\model{\amodel}$ has an infinite domain}}
    \end{talign}
  \end{proof}
\end{frame}