\begin{frame}[t]{Correctness Theorem}
  \begin{block}{Theorem (Correctness of $\sderives$ with respect to $\ssatisfies$)}
    For all formulas\/ $\aform$, and every set\/ $\asetforms$ of formulas:
    \begin{talign}
      \asetforms \derives \aform \;\;\;\Longrightarrow\;\;\; \asetforms \satisfies \aform  
    \end{talign}
  \end{block}
  \pause\medskip
  
  Reformulation and explanation:
  \pause

  \begin{goal}{}
    If there is a natural deduction derivation of $\aform$ from $\asetforms$,
    then there is no model $\model{\amodel}$
    in which all formulas of $\asetforms$ are true, but $\aform$ is false.
  \end{goal}
  \pause

  \begin{goal}{}
    The derivation rules are \emph{correct} in this sense:
    It is \alert{not possible} to derive
    a \alert{false} conclusion $\aform$
    from \alert{true} premises $\asetforms$.
  \end{goal}
  \pause
  
  \begin{goal}{}
    Truth in a model is preserved under making deductions.
  \end{goal}
  \pause\medskip

  Proof of the theorem: by \emph{induction on derivation lengths}.  
\end{frame}