\begin{frame}{Reminder: Model Cardinality} Define $\aformi{n}$ for $n\in\nat$ with $n \ge 2$: \begin{talign} \aformi{n} \;=\; \displaystyle\formula{\existsst{x_1}{\ldots\existsst{x_{n}}{ \bigwedge_{1\le i < j\le n} \notequalto{x_i}{x_j} }}} \end{talign} Define $\bformi{n}$ for $n \in \nat$ with $n \ge 1$: \begin{talign} \bformi{n} \;=\; \displaystyle\formula{ \forallst{x_1}{\ldots\forallst{x_{n+1}}{ \bigvee_{1\le i < j\le n} \equalto{x_i}{x_j} }}} \end{talign} \begin{proposition} For all models $\model{\amodel}$ and all $\forestgreen{n}\ge 2$ it holds: \begin{enumerate}[(i)] \item $\model{\amodel} \satisfies \aformi{\forestgreen{n}} \;\;\Longleftrightarrow\;\; \text{$\model{\adomain}$ has \alert{at least} $\forestgreen{n}$ elements}$ (i.e.\ $\cardinality{\model{\adomain}} \ge \forestgreen{n}$) \item $\model{\amodel} \satisfies \bformi{\forestgreen{n}} \;\;\Longleftrightarrow\;\; \text{$\model{\adomain}$ has \alert{at most} $\forestgreen{n}$ elements}$ (i.e.\ $\cardinality{\model{\adomain}} \le \forestgreen{n}$) \item $\model{\amodel} \satisfies \formula{\aformi{\forestgreen{n}} \logandinf \bformi{\forestgreen{n}}} \;\;\Longleftrightarrow\;\; \text{$\model{\adomain}$ has \alert{precisely} $\forestgreen{n}$ elements}$ ($\cardinality{\model{\adomain}} = \forestgreen{n}$) \end{enumerate} \end{proposition} \end{frame}