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