\begin{frame}
  \frametitle{Correctness Theorem}

  \begin{goal}{Soundness / Correctness}
    \vspace{-1ex}
    \begin{talign}
      \phi_1,\ldots,\phi_n \;\vdash \; \psi 
      \quad\Rightarrow\quad 
      \phi_1,\ldots,\phi_n \;\models \; \psi 
    \end{talign}
  \end{goal}
  \pause\bigskip

  \begin{block}{Explanation}
    \pause
    In a slogan: everything derivable is true.
    \bigskip\pause
    
    If $\psi$ is syntactically derivable from $\phi_1,\ldots,\phi_n$,\\
    then every valuation that makes $\phi_1,\ldots,\phi_n$ true, makes $\psi$ true.
    \bigskip\pause
    
    Thus truth in a model (valuation) is preserved under derivation.
    \bigskip\pause

    The syntactic deduction rules are \emph{correct} in the sense that
    it is not possible to derive \emph{false conclusions} from \emph{true premises}.
  \end{block}
%             \mpause[1]{In a slogan: everything true is derivable.\\
%             {\small (Every semantical conclusion is also syntactically derivable.)}}
\end{frame}