\begin{frame}{Models in Predicate Logic with Equality} \begin{block}{} \emph{Truth} of a formula $\formula{\aform}$ in a model $\model{\amodel}$ with universe $\model{\adomain}$ {\it with respect to environment $\saluf$} is defined by induction on the structure of $\formula{\aform}$: \medskip Atomic formulas: \begin{itemize}\setlength{\itemsep}{0.4ex} \item $\model{\amodel} \satisfieslookup{\saluf} \formula{\narypredsynvar{P}{\ateri{1},\ldots,\ateri{n}}} \;\iff\; \tuple{\interpretin{\formula{\ateri{1}}}{\model{\amodel},\saluf}, \ldots, \interpretin{\formula{\ateri{n}}}{\model{\amodel},\saluf}} \in \interpretin{\snarypredsynvar{P}}{\model{\amodel}} $ \mpause[1]{ \item$\model{\amodel} \satisfieslookup{\saluf} \formula{\equalto{\ateri{1}}{\ateri{2}}} \iff \pair{ \intin{\formula{\ateri{1}}}{\model{\amodel},\saluf} }{ \intin{\formula{\ateri{2}}}{\model{\amodel},\saluf} } \in {\intin{\sequalto}{\model{\amodel}}} \iff \intin{\formula{\ateri{1}}}{\model{\amodel},\saluf} = \intin{\formula{\ateri{2}}}{\model{\amodel},\saluf}$ } \end{itemize} \smallskip Logic connectives: \begin{itemize}\setlength{\itemsep}{0.4ex} \item $\model{\amodel} \satisfieslookup{\saluf} \formula{\lognot{\aform}} \;\iff\; \model{\amodel} \satisfiesnotlookup{\saluf} \formula{\aform}$ \item $\model{\amodel} \satisfieslookup{\saluf} \formula{\logand{\aform}{\bform}} \;\iff\; \model{\amodel} \satisfieslookup{\saluf} \formula{\aform} \;\text{ and }\; \model{\amodel} \satisfieslookup{\saluf} \formula{\bform}$ \item $\model{\amodel} \satisfieslookup{\saluf} \formula{\logor{\aform}{\bform}} \;\iff\; \model{\amodel} \satisfieslookup{\saluf} \formula{\aform} \;\text{ or }\; \model{\amodel} \satisfieslookup{\saluf} \formula{\bform}$ \item $\model{\amodel} \satisfieslookup{\saluf} \formula{\logimp{\aform}{\bform}} \;\iff\; (\text{if }\; \model{\amodel} \satisfieslookup{\saluf} \formula{\aform} \;\text{ then }\; \model{\amodel} \satisfieslookup{\saluf} \formula{\bform} )$ \end{itemize} \smallskip Quantifiers: \begin{itemize}\setlength{\itemsep}{0.4ex} \item $\model{\amodel} \satisfieslookup{\saluf} \formula{\forallst{x}{\,\aform}} \;\iff\; \text{for all $\forestgreen{a} \in \model{\adomain}$ it holds: } \model{\amodel} \satisfieslookup{\saluf\alert{[x\mapsto \forestgreen{a}]}} \formula{\aform}$ \item $\model{\amodel} \satisfieslookup{\saluf} \formula{\existsst{x}{\,\aform}} \;\iff\; \text{for some $\forestgreen{a} \in \model{\adomain}$ it holds: } \model{\amodel} \satisfieslookup{\saluf\alert{[x\mapsto \forestgreen{a}]}} \formula{\aform} $ \end{itemize} \end{block} \end{frame}