\begin{frame}{Expressible Frame Properties}
  Definable frame properties in predicate logic and modal logic:  
  \vspace*{-2.25ex}
  \begin{flushleft}\hspace*{-4ex}
  \renewcommand{\arraystretch}{1.3}
  \begin{tabular}{|c|c|c|}
    \hline
    \emph{property}  &  \emph{predicate logic} with $\sequalto$  & \emph{modal logic} \\
    \hline\hline 
    \mpause[1]{reflexivity} 
      & \mpause{$\formula{\forallst{x}{\,\binpred{R}{x}{x}}}$} 
      & \mpause{$\formula{\logimp{\boxmod{p}}{p}}$}
    \\ \hline
    \mpause{symmetry}  
      & \mpause{$\formula{\forallst{x}{\forallst{y}{(\logimp{\binpred{R}{x}{y}}{\binpred{R}{y}{x}})}}}$}
      & \mpause{$\formula{\logimp{p}{\boxmod{\diamod{p}}}}$}
    \\ \hline
    \mpause{anti-symmetry}
      & \mpause{$\formula{\forallst{x}{\forallst{y}{(\logimp{(\logand{\binpred{R}{x}{y}}{{\binpred{R}{y}{x}}}}{\equalto{x}{y}})}}}$}
      & \mpause{$\xmark$}
    \\ \hline
    \mpause{$\cardinality{\text{frame}} \ge \forestgreen{n}$}
      & \mpause{$\aformi{\forestgreen{n}}$ (see later)}
      & \mpause{$\xmark$}
    \\ \hline
    \mpause{$\cardinality{\text{frame}} \le \forestgreen{n}$}
      & \mpause{$\bformi{\forestgreen{n}}$ (see later)}
      & \mpause{$\xmark$}
    \\ \hline
    \mpause{every world has} 
      & \mpause{\multirow{2}{*}{$\checkmark$}} 
      & \mpause{\multirow{2}{*}{$\xmark$}}
    \\[-1ex]
    \mpause[-2]{$\ge 2$ successors} & & 
    \\ \hline
    \mpause[+3]{McKinsey}
      & \mpause[+2]{\multirow{2}{*}{$\xmark$}} 
      & \mpause[-1]{\multirow{2}{*}{$\formula{\logimp{\boxmod{\diamod{p}}}{\diamod{\boxmod{p}}}}$}}
    \\[-1ex] 
    \mpause[-1]{formula} & & 
    \\ \hline
  \end{tabular}  
  \end{flushleft}
\end{frame}

\theme{Definability and Undefinability Results\\[1ex] for Model Cardinality}