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