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