\begin{frame}[t]{Constraining Model Cardinality (with \alert{At Least})} We consider the following sentences $\aformi{n}$ for $n\in\nat$ with $n \ge 2$: \begin{itemize}\vspace*{0.5ex}\setlength{\itemsep}{0.75ex} \pause \item $\aformi{2} \;=\; \formula{\existsst{x_1}{\existsst{x_2}{\; \notequalto{x_1}{x_2} }}}$ \pause \item $\aformi{3} \;=\; \formula{\existsst{x_1}{\existsst{x_2}{\existsst{x_3}{( \notequalto{x_1}{x_2} \logandinf \notequalto{x_1}{x_3} \logandinf \notequalto{x_2}{x_3} )}}}}$ \pause \item \ldots \item $\aformi{n} \;=\; \displaystyle\formula{\existsst{x_1}{\ldots\existsst{x_{n}}{ \bigwedge_{1\le i < j\le n} \notequalto{x_i}{x_j} }}}$ \end{itemize} \pause\smallskip \begin{proposition} For all models $\model{\amodel}$ and all $n \ge 2$ the following statements hold: % \begin{enumerate}[(i)]\vspace*{0.5ex}\setlength{\itemsep}{0.75ex} \pause \item $\model{\amodel} \satisfies \aformi{n} \iff\pause \text{$\model{\adomain}$ has \alert{at least $n$} elements}$ (i.e.\ $\cardinality{\model{\adomain}} \ge n$) \pause \item $\model{\amodel} \satisfies \formula{\lognot{\aformi{n}}} \iff\pause \text{$\model{\adomain}$ has \alert{less than $n$} elements}$ (i.e.\ $\cardinality{\model{\adomain}} < n$) \pause \item $\model{\amodel} \satisfies \formula{\logand{\aformi{n}}{\lognot{\aformi{n+1}}}} \iff\pause \text{$\model{\adomain}$ has \alert{precisely $n$} elements}$ \\ \hspace*{\fill} (i.e.\ $\cardinality{\model{\adomain}} = n$) \end{enumerate} \end{proposition} \end{frame}