30/155
\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}