\begin{frame}[t]{Interpreting Formulas with Equality} \examplemodel \bigskip \begin{itemize}\setlength{\itemsep}{0.4ex} \item $\model{\amodel} \malt[1]{\gray{\satisfiesblack}}{\satisfies} \formula{\existsst{x}{\exists{y}{\existsst{z}{(\logand{\notequalto{x}{y}}{\logand{\notequalto{x}{z}}{\notequalto{y}{z}}})}}}}$ \updatepause \item $\model{\amodel} \malt[1]{\gray{\satisfiesblack}}{\satisfiesnot} \formula{\forallst{x}{\forallst{y}{(\logimp{\logand{\unpred{\mediumblue{P}}{x}}{\unpred{\mediumblue{P}}{y}}}{\equalto{x}{y}})}}}$ \updatepause \item $\model{\amodel} \malt[1]{\gray{\satisfiesblack}}{\satisfies} \formula{\forallst{x}{\forallst{y}{(\logimp{\logand{\binpred{\black{R}}{x}{x}}{\binpred{\black{R}}{y}{y}}}{\equalto{x}{y}})}}}$ \updatepause \item $\model{\amodel} \malt[1]{\gray{\satisfiesblack}}{\satisfiesnot} \formula{\forallst{x}{(\logor{\binpred{\black{R}}{x}{\const{\orange{b}}}}{\binpred{\black{R}}{x}{\const{\forestgreen{c}}}})}}$ \updatepause \item $\model{\amodel} \malt[1]{\gray{\satisfiesblack}}{\satisfies} \formula{\forallst{x}{( \equalto{x}{\const{\orange{b}}} \logorinf \binpred{\black{R}}{x}{\const{\forestgreen{c}}} )}}$ \updatepause \item $\model{\amodel} \malt[1]{\gray{\satisfiesblack}}{\satisfies} \formula{\existsst{x}{\forallst{y}{(\equalto{y}{x} \logorinf \binpred{\black{R}}{x}{y})}}}$ \end{itemize} \end{frame} \theme{Model Cardinality}