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