5/183
\begin{frame}<10>[t]
\frametitle{Reminder: Semantical Entailment}

\begin{block}{Semantic entailment in propositional logic}
In \emph{propositional logic}: \alert{${\aformi{1},\ldots,\aformi{n}} \satisfies \bform$} means:
\smallskip

For all valuations $\saval$:
\begin{talign}
\aval{\formula{\aformi{1}}} = \True \,,
\ldots\,,\,
\aval{\formula{\aformi{n}}} = \True
\;\;\Longrightarrow\;\;
\aval{\formula{\bform}} = \True
\end{talign}
\end{block}
\pause\smallskip

\begin{block}{Semantic entailment in predicate logic}
In \emph{predicate logic}: \alert{${\aformi{1},\ldots,\aformi{n}} \satisfies \bform$} means:
\smallskip

For all models $\model{\amodel}$, and all environments~$\saluf\,$:
\begin{talign}
\model{\amodel} \satisfieslookup{\saluf} \aformi{1}\;,
\ldots\,,
\;\model{\amodel} \satisfieslookup{\saluf} \aformi{n}\;
\;\;\Longrightarrow\;\;
\model{\amodel} \satisfieslookup{\saluf} \bform
\end{talign}
\end{block}

In words: for all models $\model{\amodel}$, and all environments~$\saluf$ such that
\begin{center}
$\model{\amodel} \satisfieslookup{\saluf} \aformi{1}\;$
\text{ and }
\ldots
\text{ and }
$\;\model{\amodel} \satisfieslookup{\saluf} \aformi{n}\;$
\text{ hold,}
\end{center}
it also holds that $\model{\amodel} \satisfieslookup{\saluf} \bform\,$.%
\end{frame}

\theme{Logic Equivalence}