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