2.5.11: Soundness

\(\def\Assign#1#2{ { #1^{\Struct{#2}} } }\)
\(\def\Atom#1#2{ { \mathord{#1}(#2) } }\)
\(\def\Bin{ {\mathbb{B}} }\)
\(\def\cardeq#1#2{ { #1 \approx #2 } }\)
\(\def\cardle#1#2{ { #1 \preceq #2 } }\)
\(\def\cardless#1#2{ { #1 \prec #2 } }\)
\(\def\cardneq#1#2{ { #1 \not\approx #2 } }\)
\(\def\comp#1#2{ { #2 \circ #1 } }\)
\(\def\concat{ { \;\frown\; } }\)
\(\def\Cut{ { \text{Cut} } }\)
\(\def\Discharge#1#2{ { [#1]^#2 } }\)
\(\def\DischargeRule#1#2{ { \RightLabel{#1}\LeftLabel{\scriptsize{#2} } } }\)
\(\def\dom#1{ {\operatorname{dom}(#1)} }\)
\(\def\Domain#1{ {\left| \Struct{#1} \right|} }\)
\(\def\Elim#1{ { {#1}\mathrm{Elim} } }\)
\(\newcommand{\Entails}{\vDash}\)
\(\newcommand{\EntailsN}{\nvDash}\)
\(\def\eq[#1][#2]{ { #1 = #2 } }\)
\(\def\eqN[#1][#2]{ { #1 \neq #2 } }\)
\(\def\equivclass#1#2{ { #1/_{#2} } }\)
\(\def\equivrep#1#2{ { [#1]_{#2} } }\)
\(\def\Exchange{ { \text{X} } }\)
\(\def\False{ { \mathbb{F} } }\)
\(\def\FalseCl{ { \lfalse_C } }\)
\(\def\FalseInt{ { \lfalse_I } }\)
\(\def\fCenter{ { \,\Sequent\, } }\)
\(\def\fdefined{ { \;\downarrow } }\)
\(\def\fn#1{ { \operatorname{#1} } }\)
\(\def\Frm[#1]{ {\operatorname{Frm}(\Lang #1)} }\)
\(\def\fundefined{ { \;\uparrow } }\)
\(\def\funimage#1#2{ { #1[#2] } }\)
\(\def\funrestrictionto#1#2{ { #1 \restriction_{#2} } }\)
\(\newcommand{\ident}{\equiv}\)
\(\newcommand{\indcase}[2]{#1 \ident #2\text{:}}\)
\(\newcommand{\indcaseA}[2]{#1 \text{ is atomic:}}\)
\(\def\indfrm{ { A } }\)
\(\def\indfrmp{ { A } }\)
\(\def\joinrel{\mathrel{\mkern-3mu}}\)
\(\def\lambd[#1][#2]{\lambda #1 . #2}\)
\(\def\Lang#1{ { \mathcal{#1} } }\)
\(\def\LeftR#1{ { {#1}\mathrm{L} } }\)
\(\def\len#1{ {\operatorname{len}(#1)} }\)
\(\def\lexists#1#2{ { \exists #1\, #2 } }\)
\(\def\lfalse{ {\bot} }\)
\(\def\lforall#1#2{ { \forall#1\, #2 } }\)
\(\newcommand{\lif}{\rightarrow}\)
\(\newcommand{\liff}{\leftrightarrow}\)
\(\def\Log#1{ { \mathbf{#1} } }\)
\(\def\ltrue{ {\top} }\)
\(\def\Id#1{ {\operatorname{Id}_#1} }\)
\(\def\Int{ {\mathbb{Z}} }\)
\(\def\Intro#1{ { {#1}\mathrm{Intro} } }\)
\(\def\mModel#1{ { \mathfrak{#1} } }\)
\(\newcommand{\mSat}[3][{}]{\mModel{#2}{#1}\Vdash{#3}}\)
\(\newcommand{\mSatN}[3][{}]{\mModel{#2}{#1}\nVdash{#3}}\)
\(\def\Nat{ {\mathbb{N}} }\)
\(\def\nicefrac#1#2{ {{}^#1/_#2} }\)
\(\def\num#1{ { \overline{#1} } }\)

\(\def\ran#1{ {\operatorname{ran}(#1)} }\)
\(\newcommand{\Obj}[1]{\mathsf{#1}}\)
\(\def\Rat{ {\mathbb{Q}} }\)
\(\def\Real{ {\mathbb{R}} }\)
\(\def\RightR#1{ { {#1}\mathrm{R} } }\)
\(\def\Part#1#2{ { \Atom{\Obj P}{#1, #2} } }\)
\(\def\pto{ { \hspace{0.1 cm}\to\hspace{-0.44 cm}\vcenter{\tiny{\hbox{|}}}\hspace{0.35 cm} } }\)
\(\def\PosInt{ {\mathbb{Z}^+} }\)
\(\def\Pow#1{ {\wp(#1)} }\)
\(\newcommand{\Proves}{\vdash}\)
\(\newcommand{\ProvesN}{\nvdash}\)
\(\def\Relbar{\mathrel{=}}\)
\(\newcommand{\Sat}[3][{}]{\Struct{#2}{#1}\vDash{#3}}\)
\(\newcommand{\SatN}[3][{}]{\Struct{#2}{#1}\nvDash{#3}}\)
\(\newcommand{\Sequent}{\Rightarrow}\)
\(\def\Setabs#1#2{ { \{#1:#2\} } }\)
\(\newcommand{\sFmla}[2]{#1\,#2}\)
\(\def\Struct#1{ {#1} }\)
\(\def\subst#1#2{ { #1/#2 } }\)
\(\def\Subst#1#2#3{ { #1[\subst{#2}{#3}] } }\)
\(\def\TMblank{ { 0 } }\)
\(\newcommand{\TMendtape}{\triangleright}\)
\(\def\TMleft{ { L } }\)
\(\def\TMright{ { R } }\)
\(\def\TMstay{ { N } }\)
\(\def\TMstroke{ { 1 } }\)
\(\def\TMtrans#1#2#3{ { #1,#2,#3 } }\)
\(\def\Trm[#1]{ {\operatorname{Trm}(\Lang #1)} }\)
\(\def\True{ { \mathbb{T} } }\)
\(\newcommand{\TRule}[2]{#2#1}\)
\(\def\tuple#1{ {\langle #1 \rangle} }\)
\(\newcommand{\Value}[3][\,]{\mathrm{Val}_{#1}^{#3}(#2)}\)
\(\def\Var{ { \mathrm{Var} } }\)
\(\newcommand{\varAssign}[3]{#1 \sim_{#3} #2}\)
\(\def\Weakening{ { \text{W} } }\)

A derivation system, such as natural deduction, is 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

1. every derivable sentence is valid;
2. if a sentence is derivable from some others, it is also a consequence of them;
3. if a set of sentences is inconsistent, it is unsatisfiable.

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.

Theorem \(\PageIndex{1}\): Soundness

If \(A\) is derivable from the undischarged assumptions \(\Gamma\), then \(\Gamma \Entails A\).

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 structure \(\Struct{M}\) 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 derived using sub-derivations, 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-derivations 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.

1. Suppose that the last inference is \(\Intro{\lnot}\): The derivation has the form

   

   By inductive hypothesis, \(\lfalse\) follows from the undischarged assumptions \(\Gamma \cup \{A\}\) of \(\delta_1\). Consider a structure \(\Struct{M}\). We need to show that, if \(\Sat{M}{\Gamma}\), then \(\Sat{M}{\lnot A}\). Suppose for reductio that \(\Sat{M}{\Gamma}\), but \(\SatN{M}{\lnot A}\), i.e., \(\Sat{M}{A}\). This would mean that \(\Sat{M}{\Gamma \cup \{A\}}\). This is contrary to our inductive hypothesis. So, \(\Sat{M}{\lnot A}\).

2. 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:

   

   By inductive hypothesis, \(A \land B\) follows from the undischarged assumptions \(\Gamma\) of \(\delta_1\). Consider a structure \(\Struct{M}\). We need to show that, if \(\Sat{M}{\Gamma}\), then \(\Sat{M}{A}\). Suppose \(\Sat{M}{\Gamma}\). By our inductive hypothesis (\(\Gamma \Entails A \land B\)), we know that \(\Sat{M}{A \land B}\). By definition, \(\Sat{M}{A \land B}\) iff \(\Sat{M}{A}\) and \(\Sat{M}{B}\). (The case where \(B\) is inferred from \(A \land B\) is handled similarly.)

3. 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

   

   By inductive hypothesis, \(A\) follows from the undischarged assumptions \(\Gamma\) of \(\delta_1\). Consider a structure \(\Struct{M}\). We need to show that, if \(\Sat{M}{\Gamma}\), then \(\Sat{M}{A \lor B}\). Suppose \(\Sat{M}{\Gamma}\); then \(\Sat{M}{A}\) since \(\Gamma \Entails A\) (the inductive hypothesis). So it must also be the case that \(\Sat{M}{A \lor B}\). (The case where \(A \lor B\) is inferred from \(B\) is handled similarly.)

4. The last inference is \(\Intro{\lif}\): \(A \lif B\) is inferred from a subproof with assumption \(A\) and conclusion \(B\), i.e.,

   

   By inductive hypothesis, \(B\) follows from the undischarged assumptions of \(\delta_1\), i.e., \(\Gamma \cup \{A\} \Entails B\). Consider a structure \(\Struct{M}\). 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 structure \(\Struct{M}\), \(\Sat{M}{\Gamma}\) but \(\SatN{M}{A \lif B}\). So, \(\Sat{M}{A}\) and \(\SatN{M}{B}\). But by hypothesis, \(B\) is a consequence of \(\Gamma \cup \{A\}\), i.e., \(\Sat{M}{B}\), which is a contradiction. So, \(\Gamma \Entails A \lif B\).

5. The last inference is \(\FalseInt\): Here, \(\delta\) ends in

   

   By induction hypothesis, \(\Gamma \Entails \lfalse\). We have to show that \(\Gamma \Entails A\). Suppose not; then for some \({\Struct{M}}\) we have \(\Sat{M}{\Gamma}\) and \(\SatN{M}{A}\). But we always have \(\SatN{M}{\lfalse}\), so this would mean that \(\Gamma \EntailsN \lfalse\), contrary to the induction hypothesis.

6. The last inference is \(\FalseCl\): Exercise.
7. The last inference is \(\Intro{\lforall{}{}}\): Then \(\delta\) has the form

   

   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[,s]{M}{A(x)}\) (Proposition 5.12.4). Since \(\Gamma\) consists entirely of sentences, \(\Sat[,s]{M}{B}\) for all \(B \in \Gamma\) by Definition 5.11.4. 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 Corollary 5.13.1. Since \(\Gamma \Entails A(a)\), \(\Sat{M'}{A(a)}\). Since \(A(a)\) is a sentence, \(\Sat[,s]{M'}{A(a)}\) by Proposition 5.12.3. \(\Sat[,s]{M'}{A(x)}\) iff \(\Sat{M'}{A(a)}\) by Proposition 5.13.3 (recall that \(A(a)\) is just \(\Subst{A(x)}{a}{x}\)). So, \(\Sat[,s]{M'}{A(x)}\). Since \(a\) does not occur in \(A(x)\), by Proposition 5.13.1, \(\Sat[,s]{M}{A(x)}\). But \(s\) was an arbitrary variable assignment, so \(\Sat{M}{\lforall{x}{A(x)}}\).

8. The last inference is \(\Intro{\lexists{}{}}\): Exercise.
9. The last inference is \(\Elim{\forall}\): Exercise.

Now let’s consider the possible inferences with several premises: \(\Elim{\lor}\), \(\Intro{\land}\), \(\Elim{\lif}\), and \(\Elim{\lexists{}{}}\).

1. The last inference is \(\Intro{\land}\). \(A \land B\) is inferred from the premises \(A\) and \(B\) and \(\delta\) has the form

   

   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 a structure \(\Struct{M}\) with \(\Sat{M}{\Gamma_1 \cup \Gamma_2}\). Since \(\Sat{M}{\Gamma_1}\), it must be the case that \(\Sat{M}{A}\) as \(\Gamma_1 \Entails A\), and since \(\Sat{M}{\Gamma_2}\), \(\Sat{M}{B}\) since \(\Gamma_2 \Entails B\). Together, \(\Sat{M}{A \land B}\).

2. The last inference is \(\Elim{\lor}\): Exercise.
3. The last inference is \(\Elim{\lif}\). \(B\) is inferred from the premises \(A \lif B\) and \(A\). The derivation \(\delta\) looks like this:

   

   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 a structure \(\Struct{M}\). We need to show that, if \(\Sat{M}{\Gamma_1 \cup \Gamma_2}\), then \(\Sat{M}{B}\). Suppose \(\Sat{M}{\Gamma_1 \cup \Gamma_2}\). Since \(\Gamma_1 \Entails A \lif B\), \(\Sat{M}{A \lif B}\). Since \(\Gamma_2 \Entails A\), we have \(\Sat{M}{A}\). This means that \(\Sat{M}{B}\) (For if \(\SatN{M}{B}\), since \(\Sat{M}{A}\), we’d have \(\SatN{M}{A \lif B}\), contradicting \(\Sat{M}{A \lif B}\)).

4. The last inference is \(\Elim{\lnot}\): Exercise.
5. The last inference is \(\Elim{\lexists{}{}}\): Exercise.

◻

Problem \(\PageIndex{1}\)

Complete the proof of Theorem \(\PageIndex{1}\).

Corollary \(\PageIndex{1}\)

If \(\Proves A\), then \(A\) is valid.

Corollary \(\PageIndex{2}\)

If \(\Gamma\) is satisfiable, then it is consistent.

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 Theorem \(\PageIndex{1}\), any structure \(\Struct{M}\) that satisfies \(\Gamma\) must satisfy \(\lfalse\). Since \(\SatN{M}{\lfalse}\) for every structure \(\Struct{M}\), no \(\Struct{M}\) can satisfy \(\Gamma\), i.e., \(\Gamma\) is not satisfiable. ◻