% Part: first-order-logic
% Chapter: natural-deduction
% Section: soundness

\documentclass[../../../include/open-logic-section]{subfiles}

\begin{document}

\iftag{FOL}
      {\olfileid{fol}{ntd}{sou}}
      {\olfileid{pl}{ntd}{sou}}
      
\olsection{Soundness}

\begin{explain}
!!^a{derivation} system, such as natural deduction, is \emph{sound}
if it cannot !!{derive} things that do not actually follow.  Soundness is
thus a kind of guaranteed safety property for !!{derivation} systems.
Depending on which proof theoretic property is in question, we would
like to know for instance, that
\begin{enumerate}
\item every !!{derivable} !!{sentence} is \iftag{FOL}{valid}{a tautology};
\item if !!a{sentence} is !!{derivable} from some others, it is also a
  consequence of them;
\item if a set of !!{sentence}s is inconsistent, it is unsatisfiable.
\end{enumerate}
These are important properties of !!a{derivation} system. If any of
them do not hold, the !!{derivation} system is deficient---it would
!!{derive} too much.  Consequently, establishing the soundness of a
!!{derivation} system is of the utmost importance.
\end{explain}

\begin{thm}[Soundness]
\ollabel{thm:soundness}
If $!A$ is !!{derivable} from the !!{undischarged} assumptions
$\Gamma$, then $\Gamma \Entails !A$.
\end{thm}

\begin{proof}
Let $\delta$ be !!a{derivation} of $!A$. We proceed by
induction on the number of inferences in~$\delta$.

For the induction basis we show the claim if the number of inferences
is~$0$. In this case, $\delta$ consists only of a single
!!{sentence}~$!A$, i.e., an assumption. That assumption is
!!{undischarged}, since assumptions can only be !!{discharged} by
inferences, and there are no inferences.  So, any
\iftag{FOL}{!!{structure}~$\Struct{M}$}{!!{valuation}~$\pAssign{v}$}
that satisfies all of the !!{undischarged} assumptions of the proof
also satisfies~$!A$.

Now for the inductive step. Suppose that $\delta$ contains~$n$
inferences. The premise(s) of the lowermost inference are !!{derive}d
using sub-!!{derivation}s, each of which contains fewer than~$n$
inferences.  We assume the induction hypothesis: The premises of the
lowermost inference follow from the !!{undischarged} assumptions of
the sub-!!{derivation}s ending in those premises.  We have to show
that the conclusion~$!A$ follows from the !!{undischarged} assumptions
of the entire proof.

We distinguish cases according to the type of the lowermost inference.
First, we consider the possible inferences with only one premise.

\begin{enumerate}
\item Suppose that the last inference is \Intro{\lnot}: The
  !!{derivation} has the form
  \begin{prooftree}
    \AxiomC{$\Gamma, \Discharge{!A}{n}$}
    \RightLabel{$\delta_1$}
    \DeduceC{$\lfalse$}
    \DischargeRule{\Intro{\lnot}}{n}
    \UnaryInfC{$\lnot !A$}
  \end{prooftree}
  By inductive hypothesis, $\lfalse$ follows from the !!{undischarged}
  assumptions $\Gamma \cup \{!A\}$ of~$\delta_1$. Consider
  \iftag{FOL}{!!a{structure}~$\Struct{M}$}{!!a{valuation}~$\pAssign{v}$}. We
  need to show that, if $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$, then
  $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\lnot !A}$. Suppose for reductio
  that $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$, but
  $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{\lnot !A}$, i.e.,
  $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$. This would mean that
  $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma \cup \{!A\}}$. This is
  contrary to our inductive hypothesis. So,
  $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\lnot !A}$.

\item The last inference is \Elim{\land}: There are two variants: $!A$
  or $!B$ may be inferred from the premise $!A \land !B$. Consider the
  first case. The !!{derivation}~$\delta$ looks like this:
  \begin{prooftree}
    \AxiomC{$\Gamma$}
    \RightLabel{$\delta_1$}
    \DeduceC{$!A \land !B$}
    \RightLabel{\Elim{\land}}
    \UnaryInfC{$!A$}
  \end{prooftree}
  By inductive hypothesis, $!A \land !B$ follows from the
  !!{undischarged} assumptions~$\Gamma$ of~$\delta_1$. Consider
  !!a{structure}~\iftag{FOL}{$\Struct{M}$}{$\pAssign{v}$}. We need to
  show that, if $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$, then
  $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$. Suppose
  $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$. By our inductive
  hypothesis ($\Gamma \Entails !A \land !B$), we know that
  $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A \land !B}$. By definition,
  $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A \land !B}$ iff
  $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$ and
  $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!B}$.  (The case where $!B$ is
  inferred from $!A \land !B$ is handled similarly.)
  
\item The last inference is \Intro{\lor}: There are two variants: $!A
  \lor !B$ may be inferred from the premise~$!A$ or the
  premise~$!B$. Consider the first case. The !!{derivation} has the form
  \begin{prooftree}
    \AxiomC{$\Gamma$}
    \RightLabel{$\delta_1$}
    \DeduceC{$!A$}
    \RightLabel{\Intro{\lor}}
    \UnaryInfC{$!A \lor !B$}
  \end{prooftree}
  By inductive hypothesis, $!A$ follows from the !!{undischarged}
  assumptions~$\Gamma$ of~$\delta_1$.  Consider
  \iftag{FOL}{!!a{structure}~$\Struct{M}$}{!!a{valuation}~$\pAssign{v}$}. We
  need to show that, if $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$, then
  $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A \lor !B}$. Suppose
  $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$; then
  $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$ since $\Gamma \Entails !A$ (the
  inductive hypothesis). So it must also be the case that
  $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A \lor !B}$.  (The case where $!A
  \lor !B$ is inferred from~$!B$ is handled similarly.)
  
\item The last inference is \Intro{\lif}: $!A \lif !B$ is inferred
  from a subproof with assumption~$!A$ and conclusion~$!B$, i.e.,
  \begin{prooftree}
    \AxiomC{$\Gamma, \Discharge{!A}{n}$}
    \RightLabel{$\delta_1$}
    \DeduceC{$!B$}
    \DischargeRule{\Intro{\lif}}{n}
    \UnaryInfC{$!A \lif !B$}
  \end{prooftree}
  By inductive hypothesis, $!B$ follows from the !!{undischarged}
  assumptions of~$\delta_1$, i.e., $\Gamma \cup \{!A\} \Entails
  !B$. Consider
  \iftag{FOL}{!!a{structure}~$\Struct{M}$}{!!a{valuation}~$\pAssign{v}$}. The
  !!{undischarged} assumptions of~$\delta$ are just $\Gamma$, since
  $!A$ is discharged at the last inference. So we need to show that
  $\Gamma \Entails !A \lif !B$.  For reductio, suppose that for some
  \iftag{FOL}{!!{structure}~$\Struct{M}$}{!!{valuation}~$\pAssign{v}$},
  $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$ but
  $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!A \lif !B}$. So,
  $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$ and
  $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!B}$. But by hypothesis, $!B$ is a
  consequence of $\Gamma \cup \{!A\}$, i.e.,
  $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!B}$, which is a contradiction. So,
  $\Gamma \Entails !A \lif !B$.

\item The last inference is \FalseInt: Here, $\delta$ ends in
  \begin{prooftree}
    \AxiomC{$\Gamma$}
    \RightLabel{$\delta_1$}
    \DeduceC{$\lfalse$}
    \RightLabel{\FalseInt}
    \UnaryInfC{$!A$}
  \end{prooftree}
  By induction hypothesis, $\Gamma \Entails \lfalse$. We have to show
  that $\Gamma \Entails !A$. Suppose not; then for
  some~$\iftag{FOL}{\Struct{M}}{\pAssign{v}}$ we have
    $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$ and
    $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!A}$. But we always have
    $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{\lfalse}$, so this would mean
    that $\Gamma \Entails/ \lfalse$, contrary to the induction
    hypothesis.

\item The last inference is \FalseCl: Exercise.

\iftag{FOL}{
\item The last inference is \Intro{\lforall}: Then $\delta$ has the form
  \begin{prooftree}
    \AxiomC{$\Gamma$}
    \RightLabel{$\delta_1$}
    \DeduceC{$!A(a)$}
    \RightLabel{\Intro{\lforall}}
    \UnaryInfC{$\lforall[x][!A(x)]$}
  \end{prooftree}
  The premise $!A(a)$ is a consequence of the !!{undischarged}
  assumptions $\Gamma$ by induction hypothesis.  Consider some
  structure, $\Struct{M}$, such that $\Sat{M}{\Gamma}$.  We need to
  show that $\Sat{M}{\lforall[x][!A(x)]}$. Since $\lforall[x][!A(x)]$
  is !!a{sentence}, this means we have to show that for every variable
  assignment~$s$, $\Sat{M}{!A(x)}[s]$
  (\olref[syn][ass]{prop:sat-quant}). Since $\Gamma$ consists entirely
  of sentences, $\Sat{M}{!B}[s]$ for all $!B \in \Gamma$ by
  \olref[syn][sat]{defn:satisfaction}.  Let $\Struct{M'}$ be like
  $\Struct{M}$ except that $\Assign{a}{M'} = s(x)$.  Since $a$ does
  not occur in~$\Gamma$, $\Sat{M'}{\Gamma}$ by
  \olref[syn][ext]{cor:extensionality-sent}. Since $\Gamma \Entails
  !A(a)$, $\Sat{M'}{!A(a)}$.  Since $!A(a)$ is !!a{sentence},
  $\Sat{M'}{!A(a)}[s]$ by
  \olref[syn][ass]{prop:sentence-sat-true}. $\Sat{M'}{!A(x)}[s]$ iff
  $\Sat{M'}{!A(a)}$ by \olref[syn][ext]{prop:ext-formulas} (recall
  that $!A(a)$ is just $\Subst{!A(x)}{a}{x}$). So,
  $\Sat{M'}{!A(x)}[s]$. Since $a$ does not occur in~$!A(x)$, by
  \olref[syn][ext]{prop:extensionality}, $\Sat{M}{!A(x)}[s]$. But $s$
  was an arbitrary variable assignment, so
  $\Sat{M}{\lforall[x][!A(x)]}$.
  
\item The last inference is \Intro{\lexists}: Exercise.

\item The last inference is \Elim{\forall}: Exercise.
}{}
\end{enumerate}

Now let's consider the possible inferences with several premises:
\Elim{\lor}, \Intro{\land}, \iftag{FOL}{\Elim{\lif}, and
  \Elim{\lexists}}{and \Elim{\lif}}.
\begin{enumerate}

\item The last inference is \Intro{\land}. $!A \land !B$ is inferred
  from the premises $!A$ and $!B$ and $\delta$ has the form
  \begin{prooftree}
    \AxiomC{$\Gamma_1$}
    \RightLabel{$\delta_1$}
    \DeduceC{$!A$}
    \AxiomC{$\Gamma_2$}
    \RightLabel{$\delta_2$}
    \DeduceC{$!B$}
    \RightLabel{\Intro{\land}}
    \BinaryInfC{$!A \land !B$}
  \end{prooftree}
  By induction hypothesis, $!A$ follows from the !!{undischarged}
  assumptions~$\Gamma_1$ of~$\delta_1$ and $!B$ follows from the
  !!{undischarged} assumptions~$\Gamma_2$ of~$\delta_2$. The
  !!{undischarged} assumptions of~$\delta$ are $\Gamma_1 \cup
  \Gamma_2$, so we have to show that $\Gamma_1 \cup \Gamma_2 \Entails
  !A \land !B$. Consider
  \iftag{FOL}{!!a{structure}~$\Struct{M}$}{!!a{valuation}~$\pAssign{v}$}
  with $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma_1 \cup \Gamma_2}$. Since
  $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma_1}$, it must be the case that
  $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$ as $\Gamma_1 \Entails !A$, and
  since $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma_2}$,
  $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!B}$ since $\Gamma_2 \Entails
  !B$. Together, $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A \land !B}$.
  
\item The last inference is \Elim{\lor}: Exercise.

\item The last inference is \Elim{\lif}. $!B$ is inferred from the
  premises $!A \lif !B$ and~$!A$. The !!{derivation}~$\delta$ looks like this:
  \begin{prooftree}
    \AxiomC{$\Gamma_1$}
    \RightLabel{$\delta_1$}
    \DeduceC{$!A \lif !B$}
    \AxiomC{$\Gamma_2$}
    \RightLabel{$\delta_2$}
    \DeduceC{$!A$}
    \RightLabel{\Elim{\lif}}
    \BinaryInfC{$!B$}
  \end{prooftree}
  By induction hypothesis, $!A \lif !B$ follows from the
  !!{undischarged} assumptions~$\Gamma_1$ of~$\delta_1$ and $!A$
  follows from the !!{undischarged} assumptions~$\Gamma_2$
  of~$\delta_2$. Consider
  \iftag{FOL}{!!a{structure}~$\Struct{M}$}{!!a{valuation}~$\pAssign{v}$}. We
  need to show that, if $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma_1 \cup
    \Gamma_2}$, then $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!B}$. Suppose
  $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma_1 \cup \Gamma_2}$. Since
  $\Gamma_1 \Entails !A \lif !B$, $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A
    \lif !B}$. Since $\Gamma_2 \Entails !A$, we have
  $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$. This means that
  $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!B}$ (For if
  $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!B}$, since
  $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$, we'd have
  $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!A \lif !B}$,
  contradicting~$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A \lif !B}$).

\item The last inference is \Elim{\lnot}: Exercise.
  
\tagitem{FOL}{The last inference is \Elim{\lexists}: Exercise.}{}
\end{enumerate}
\end{proof}

\tagprob{FOL}
\begin{prob}
Complete the proof of \olref[fol][ntd][sou]{thm:soundness}.
\end{prob}
\tagendprob

\tagprob{notFOL}
\begin{prob}
Complete the proof of \olref[pl][ntd][sou]{thm:soundness}.
\end{prob}
\tagendprob

\begin{cor}
\ollabel{cor:weak-soundness}
If $\Proves !A$, then $!A$ is \iftag{FOL}{valid}{a tautology}.
\end{cor}

\begin{cor}
\ollabel{cor:consistency-soundness}
If $\Gamma$ is satisfiable, then it is consistent.
\end{cor}

\begin{proof}
We prove the contrapositive.  Suppose that $\Gamma$ is not consistent.
Then $\Gamma \Proves \lfalse$, i.e., there is !!a{derivation} of
$\lfalse$ from !!{undischarged} assumptions in~$\Gamma$. By
\olref{thm:soundness}, any
\iftag{FOL}{!!{structure}~$\Struct{M}$}{!!{valuation}~$\pAssign{v}$}
that satisfies $\Gamma$ must satisfy $\lfalse$.  Since
$\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{\lfalse}$ for every
\iftag{FOL}{!!{structure}~$\Struct{M}$}{!!{valuation}~$\pAssign{v}$},
no \iftag{FOL}{$\Struct{M}$}{$\pAssign{v}$} can satisfy $\Gamma$,
i.e., $\Gamma$ is not satisfiable.
\end{proof}

\end{document}