\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}