\begin{frame}[t] \frametitle{Semantical Entailment in Predicate Logic} \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}