The Deduction Theorem and Soundness

Proof. (a) \(\vdash(\psi\to\chi)\to(\varphi\to(\psi\to\chi))\) by (L1), and \(\vdash(\varphi\to(\psi\to\chi))\to((\varphi\to\psi)\to(\varphi\to\chi))\) by (L2). Chain the two with HS (Proposition 8.36).

(b) From \(\Gamma\vdash\varphi\to(\psi\to\chi)\), (L2) and MP give \(\Gamma\vdash(\varphi\to\psi)\to(\varphi\to\chi)\). By (L1), \(\vdash\psi\to(\varphi\to\psi)\), so \(\Gamma\vdash\psi\to(\varphi\to\psi)\) by Proposition 8.35(b). HS gives \(\Gamma\vdash\psi\to(\varphi\to\chi)\).

(c) Apply (b) to (a): the two antecedents \(\psi\to\chi\) and \(\varphi\to\psi\) change places.

(d) From \(\Gamma\vdash\varphi\to(\varphi\to\psi)\), (L2) and MP give \(\Gamma\vdash(\varphi\to\varphi)\to(\varphi\to\psi)\). By Example 8.27 and Proposition 8.35(b), \(\Gamma\vdash\varphi\to\varphi\). MP gives \(\Gamma\vdash\varphi\to\psi\). □

Proof. (a) By (L1), \(\vdash\neg\varphi\to(\neg\psi\to\neg\varphi)\), and by (L3), \(\vdash(\neg\psi\to\neg\varphi)\to(\varphi\to\psi)\). HS gives (a). (b) follows from (a) by swapping the antecedents, Lemma 9.4(b).

(c) We use (a) with \(\neg\varphi\) in place of \(\varphi\) and \(\neg\neg\neg\varphi\) in place of \(\psi\). Line 2 is (L3) with \(\varphi:=\neg\neg\varphi\) and \(\psi:=\varphi\).

(d) Line 1 is (L3) with \(\varphi:=\varphi\) and \(\psi:=\neg\neg\varphi\). Line 2 is (c) for the formula \(\neg\varphi\).

(e) The idea: from \(\varphi\to\psi\) we go to \(\neg\neg\varphi\to\neg\neg\psi\), and then (L3) turns this around.

Line 8 is (L3) with \(\varphi:=\neg\psi\) and \(\psi:=\neg\varphi\).

(f) Line 1 is (a) with \(\psi:=\neg(\neg\varphi\to\varphi)\); line 4 is (L3) with \(\varphi:=\neg\varphi\to\varphi\) and \(\psi:=\varphi\).

(g) From \(\varphi\to\chi\) we get \(\neg\chi\to\neg\varphi\) by (e); together with \(\neg\varphi\to\chi\) this gives \(\neg\chi\to\chi\), and (f) turns this into \(\chi\).

Line 5 is Lemma 9.4(a) with \(\varphi:=\neg\varphi\to\chi\), \(\psi:=\neg\chi\to\chi\) and \(\chi:=\chi\). □

Throughout, \(\vdash\) is \(\vdash_3\).

(L8) \(\psi\to(\varphi\vee\psi)\) is short for \(\psi\to(\neg\varphi\to\psi)\), an instance of (L1) (Example 9.2(d)).

(L7) \(\varphi\to(\varphi\vee\psi)\) is short for \(\varphi\to(\neg\varphi\to\psi)\), which is Lemma 9.5(b).

(L4) \((\varphi\wedge\psi)\to\varphi\) is short for \(\neg(\varphi\to\neg\psi)\to\varphi\). Line 2 is Lemma 9.5(e) with \(\varphi:=\neg\varphi\) and \(\psi:=\varphi\to\neg\psi\).

(L5) \((\varphi\wedge\psi)\to\psi\) is short for \(\neg(\varphi\to\neg\psi)\to\psi\). Line 1 is (L1) with \(\varphi:=\neg\psi\) and \(\psi:=\varphi\).

(L6) \(\varphi\to(\psi\to(\varphi\wedge\psi))\) is short for \(\varphi\to(\psi\to\neg(\varphi\to\neg\psi))\).

Line 2 moves the antecedent \(\varphi\to\neg\psi\) of line 1 behind \(\varphi\). Line 3 is Lemma 9.5(e) with \(\varphi:=\varphi\to\neg\psi\) and \(\psi:=\neg\psi\).

(L9) \((\varphi\to\chi)\to((\psi\to\chi)\to((\varphi\vee\psi)\to\chi))\) is short for \((\varphi\to\chi)\to((\psi\to\chi)\to((\neg\varphi\to\psi)\to\chi))\). The idea: from \(\neg\varphi\to\psi\) and \(\psi\to\chi\) we get \(\neg\varphi\to\chi\), and Lemma 9.5(g) combines it with \(\varphi\to\chi\).

Line 3 is Lemma 9.4(c) with \(\varphi:=\neg\varphi\to\psi\), \(\psi:=\neg\varphi\to\chi\), \(\chi:=\chi\). □

(\(\Rightarrow\)) A deduction in the small system is also a deduction in the large system, because every instance of (L1), (L2), (L3) is allowed there.

(\(\Leftarrow\)) Let \(\psi_1,\dots,\psi_n\) be a deduction from \(\Gamma\) in the large system. We show by strong induction on \(i\) that \(\Gamma\vdash_3\psi_i\) for every \(i\le n\). Let \(i\le n\), and assume \(\Gamma\vdash_3\psi_j\) for all \(j<i\). There are four cases.

• \(\psi_i\) is an instance of (L1), (L2) or (L3). Then the one line \(\psi_i\) is a deduction in the small system, so \(\vdash_3\psi_i\), and \(\Gamma\vdash_3\psi_i\) by Proposition 8.35(b).
• \(\psi_i\) is an instance of (L4) to (L9). Then \(\vdash_3\psi_i\) by Lemma 9.6, and \(\Gamma\vdash_3\psi_i\) by Proposition 8.35(b).
• \(\psi_i\in\Gamma\). Then \(\Gamma\vdash_3\psi_i\) by Proposition 8.35(a).
• \(\psi_i\) follows by MP from \(\psi_j\) and \(\psi_k=\psi_j\to\psi_i\) with \(j,k<i\). By the induction hypothesis \(\Gamma\vdash_3\psi_j\) and \(\Gamma\vdash_3\psi_j\to\psi_i\), so \(\Gamma\vdash_3\psi_i\) by Proposition 8.35(c).

For \(i=n\) we get \(\Gamma\vdash_3\psi_n\). □

Proof. Each line \(\psi_i\) with \(i\le m\) is an axiom, a member of \(\Gamma\), or follows by MP from two lines before \(\psi_i\). Those lines are among \(\psi_1,\dots,\psi_m\), since MP only looks back. □

Proof. (\(\Leftarrow\)) Let \(\chi_1,\dots,\chi_n\) be a deduction of \(\varphi\to\psi\) from \(\Gamma\). It is also a deduction from \(\Gamma\cup\{\varphi\}\). Add two lines: \(\chi_{n+1}=\varphi\) (assump.) and \(\chi_{n+2}=\psi\) (\(n,n+1\) MP). This is a deduction of \(\psi\) from \(\Gamma\cup\{\varphi\}\).

(\(\Rightarrow\)) We prove by strong induction on \(n\ge1\): for every formula \(\psi\), if \(\psi_1,\dots,\psi_n\) is a deduction of \(\psi\) from \(\Gamma\cup\{\varphi\}\), then \(\Gamma\vdash\varphi\to\psi\).

Base case, \(n=1\). The deduction is the single line \(\psi_1=\psi\), so \(\psi\) is an axiom or a member of \(\Gamma\cup\{\varphi\}\).

• If \(\psi\) is an axiom or \(\psi\in\Gamma\), then this is a deduction from \(\Gamma\):

  1	\(\psi\)	(axiom or assump.)
  2	\(\psi\to(\varphi\to\psi)\)	(L1)
  3	\(\varphi\to\psi\)	(1,2 MP)

• If \(\psi=\varphi\), we need \(\Gamma\vdash\varphi\to\varphi\). This holds by Example 8.27 and Proposition 8.35(b).

Induction step. Let \(n\ge1\) and assume the statement for all lengths \(k\le n\). Let \(\psi_1,\dots,\psi_{n+1}\) be a deduction of \(\psi\) from \(\Gamma\cup\{\varphi\}\). If \(\psi\) is an axiom or a member of \(\Gamma\cup\{\varphi\}\), the argument of the base case works. Otherwise \(\psi\) follows by MP: there are \(i,j\le n\) with \(\psi_j=\psi_i\to\psi\).

By Lemma 9.8, \(\psi_1,\dots,\psi_i\) is a deduction of \(\psi_i\) from \(\Gamma\cup\{\varphi\}\) of length \(i\le n\), and \(\psi_1,\dots,\psi_j\) is a deduction of \(\psi_i\to\psi\) of length \(j\le n\). By the induction hypothesis, \[\Gamma\vdash\varphi\to\psi_i\qquad\text{and}\qquad\Gamma\vdash\varphi\to(\psi_i\to\psi).\] Write a deduction of \(\varphi\to\psi_i\) from \(\Gamma\) (\(m\) lines), then a deduction of \(\varphi\to(\psi_i\to\psi)\) from \(\Gamma\) (ending at line \(m'\)), and add three lines:

This is a deduction of \(\varphi\to\psi\) from \(\Gamma\). This completes the induction. □

Proof. By Theorem 9.7, \(\Gamma,\varphi\vdash_9\psi\) iff \(\Gamma,\varphi\vdash_3\psi\). By Theorem 9.9 this holds iff \(\Gamma\vdash_3\varphi\to\psi\), and by Theorem 9.7 again iff \(\Gamma\vdash_9\varphi\to\psi\). □

Proof. The value of an instance depends only on the values of the formulas that replace \(\varphi,\psi,\chi\). So it is enough to show that the scheme is true for every choice of values \(\mathrm T,\mathrm F\) of \(\varphi,\psi,\chi\). For each scheme we assume it is false and reach a contradiction.

(L1) \(\varphi\to(\psi\to\varphi)\) false needs \(\varphi=\mathrm T\) and \(\psi\to\varphi=\mathrm F\), so \(\varphi=\mathrm F\). Contradiction.

(L2) False needs \(\varphi\to(\psi\to\chi)=\mathrm T\) and \((\varphi\to\psi)\to(\varphi\to\chi)=\mathrm F\). The second gives \(\varphi\to\psi=\mathrm T\) and \(\varphi\to\chi=\mathrm F\), so \(\varphi=\mathrm T\), \(\chi=\mathrm F\), and then \(\psi=\mathrm T\). But then \(\varphi\to(\psi\to\chi)=\mathrm T\to(\mathrm T\to\mathrm F)=\mathrm F\). Contradiction.

(L3) False needs \(\neg\psi\to\neg\varphi=\mathrm T\) and \(\varphi\to\psi=\mathrm F\), so \(\varphi=\mathrm T\) and \(\psi=\mathrm F\). Then \(\neg\psi=\mathrm T\) and \(\neg\varphi=\mathrm F\), so \(\neg\psi\to\neg\varphi=\mathrm F\). Contradiction.

The other six in the same way:

Each line is a contradiction. □

Proof. If \([\![\psi]\!]_v=\mathrm F\), then \([\![\varphi\to\psi]\!]_v=\mathrm F\), because \([\![\varphi]\!]_v=\mathrm T\). □

Proof. Fix \(\Gamma\) and a valuation \(v\) that satisfies \(\Gamma\). We prove by strong induction on \(n\ge1\): if \(\psi_1,\dots,\psi_n\) is a deduction from \(\Gamma\), then \([\![\psi_n]\!]_v=\mathrm T\).

Base case, \(n=1\). The line \(\psi_1\) is an axiom or a member of \(\Gamma\). An axiom is a tautology by Lemma 9.15, so it is true under \(v\). A member of \(\Gamma\) is true under \(v\) because \(v\) satisfies \(\Gamma\).

Induction step. Let \(n\ge1\) and assume the statement for all deductions of length at most \(n\). Let \(\psi_1,\dots,\psi_{n+1}\) be a deduction from \(\Gamma\). If \(\psi_{n+1}\) is an axiom or a member of \(\Gamma\), it is true under \(v\), as in the base case. Otherwise there are \(i,j\le n\) with \(\psi_j=\psi_i\to\psi_{n+1}\). By Lemma 9.8, \(\psi_1,\dots,\psi_i\) and \(\psi_1,\dots,\psi_j\) are deductions from \(\Gamma\) of length at most \(n\). By the induction hypothesis \([\![\psi_i]\!]_v=\mathrm T\) and \([\![\psi_i\to\psi_{n+1}]\!]_v=\mathrm T\). By Lemma 9.16, \([\![\psi_{n+1}]\!]_v=\mathrm T\).

Now let \(\Gamma\vdash\varphi\), with a deduction \(\psi_1,\dots,\psi_n=\varphi\). We showed \([\![\varphi]\!]_v=\mathrm T\), and \(v\) was an arbitrary valuation that satisfies \(\Gamma\). So \(\Gamma\models\varphi\). □

Proof. Take \(\Gamma=\varnothing\) in Theorem 9.17. □

Proof. Let \(v\) satisfy \(\Gamma\), and suppose \(\Gamma\vdash\varphi\) and \(\Gamma\vdash\neg\varphi\). By the Soundness Theorem, \([\![\varphi]\!]_v=\mathrm T\) and \([\![\neg\varphi]\!]_v=\mathrm T\). But then \([\![\varphi]\!]_v=\mathrm F\). Contradiction. Every valuation satisfies \(\varnothing\). □