2.4 Useful Theorems, Lemmas and Metatheorems

The goal of this chapter is to prove the required lemmas so that we become able to prove two things: the Principle of Explosion and the Completeness Theorem. To do so, we'll prove some theorems, as well as some metatheorems. If you are familiar with programming, all metatheorems of this chapter can be viewed as macros, an abbreviation in the code that stands for other lines of code. In the same way, a metatheorem can be viewed as a shortcut to spare some lines of proof. You can also view them as additional rules of inference, procedures to derive a wff from other wffs.

To understand the proofs, you'll need to be able to consult, or even better, memorize the axioms \(A_1\), \(A_2\) and \(A_3\), as well as the Modus Ponens rule of inference:

• \(A_1\): \(\varphi\rightarrow(\psi\rightarrow\varphi)\)
• \(A_2\): \([\varphi\rightarrow(\psi\rightarrow\eta)]\rightarrow[(\varphi\rightarrow\psi)\rightarrow(\varphi\rightarrow\eta)]\)
• \(A_3\): \((\neg\varphi\rightarrow\neg\psi)\rightarrow(\psi\rightarrow\varphi)\)
• MP: \(\vdash\varphi\) and \(\vdash\varphi\rightarrow\psi\) \(\Rightarrow\) \(\vdash\psi\)

Now, without further ado, let the fun begin!

Implication Reflexivity Theorem: \(\varphi \rightarrow \varphi\)

∎

We shall denote the use of this theorem by (R).

Hypothetical Syllogism

The following theorems and metatheorem will be proven:

• (HS1): \((\psi \rightarrow \eta) \rightarrow [(\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \eta)]\)
• (HS2): \((\varphi \rightarrow \psi) \rightarrow [(\psi \rightarrow \eta) \rightarrow (\varphi \rightarrow \eta)]\)
• HS: \(\vdash\varphi \rightarrow \psi\) and \(\vdash\psi \rightarrow \eta\) \(\Rightarrow\) \(\vdash \varphi \rightarrow \eta\)

Proofs:

• (HS1):

	\(\vdash\)	\([\varphi\rightarrow(\psi\rightarrow\eta)]\rightarrow[(\varphi\rightarrow\psi)\rightarrow(\varphi\rightarrow\eta)]\)	: \(\varphi_0\)	// instance of \(A_2\)
	\(\vdash\)	\(([\varphi\rightarrow(\psi\rightarrow\eta)]\rightarrow[(\varphi\rightarrow\psi)\rightarrow(\varphi\rightarrow\eta)]) \rightarrow [(\psi \rightarrow \eta) \rightarrow ([\varphi\rightarrow(\psi\rightarrow\eta)]\rightarrow[(\varphi\rightarrow\psi)\rightarrow(\varphi\rightarrow\eta)])]\)	: \(\varphi_1\)	// instance of \(A_1\)
	\(\vdash\)	\((\psi \rightarrow \eta) \rightarrow ([\varphi\rightarrow(\psi\rightarrow\eta)]\rightarrow[(\varphi\rightarrow\psi)\rightarrow(\varphi\rightarrow\eta)])\)	: \(\varphi_2\)	// from \(\varphi_0\) and \(\varphi_1\) by MP
	\(\vdash\)	\([(\psi \rightarrow \eta) \rightarrow ([\varphi\rightarrow(\psi\rightarrow\eta)]\rightarrow[(\varphi\rightarrow\psi)\rightarrow(\varphi\rightarrow\eta)])] \rightarrow [((\psi \rightarrow \eta) \rightarrow (\varphi\rightarrow(\psi\rightarrow\eta))) \rightarrow ((\psi \rightarrow \eta) \rightarrow ((\varphi\rightarrow\psi)\rightarrow(\varphi\rightarrow\eta)))]\)	: \(\varphi_3\)	// instance of \(A_2\)
	\(\vdash\)	\(((\psi \rightarrow \eta) \rightarrow (\varphi\rightarrow(\psi\rightarrow\eta))) \rightarrow ((\psi \rightarrow \eta) \rightarrow ((\varphi\rightarrow\psi)\rightarrow(\varphi\rightarrow\eta)))\)	: \(\varphi_4\)	// from \(\varphi_2\) and \(\varphi_3\) by MP
	\(\vdash\)	\((\psi \rightarrow \eta) \rightarrow (\varphi\rightarrow(\psi\rightarrow\eta))\)	: \(\varphi_5\)	// instance of \(A_1\)
	\(\vdash\)	\((\psi \rightarrow \eta) \rightarrow ((\varphi\rightarrow\psi)\rightarrow(\varphi\rightarrow\eta))\)	: \(\varphi_6\)	// from \(\varphi_4\) and \(\varphi_5\) by MP

∎

• (HS2):

	\(\vdash\)	\((\psi \rightarrow \eta) \rightarrow ((\varphi\rightarrow\psi)\rightarrow(\varphi\rightarrow\eta))\)	: \(\varphi_0\)	// instance of (HS1)
	\(\vdash\)	\([(\psi \rightarrow \eta) \rightarrow ((\varphi\rightarrow\psi)\rightarrow(\varphi\rightarrow\eta))] \rightarrow [((\psi \rightarrow \eta) \rightarrow (\varphi\rightarrow\psi)) \rightarrow ((\psi \rightarrow \eta) \rightarrow (\varphi\rightarrow\eta))]\)	: \(\varphi_1\)	// instance of \(A_2\)
	\(\vdash\)	\(((\psi \rightarrow \eta) \rightarrow (\varphi\rightarrow\psi)) \rightarrow ((\psi \rightarrow \eta) \rightarrow (\varphi\rightarrow\eta))\)	: \(\varphi_2\)	// from \(\varphi_0\) and \(\varphi_1\) by MP
	\(\vdash\)	\((((\psi \rightarrow \eta) \rightarrow (\varphi\rightarrow\psi)) \rightarrow ((\psi \rightarrow \eta) \rightarrow (\varphi\rightarrow\eta))) \rightarrow [((\varphi \rightarrow \psi) \rightarrow ((\psi \rightarrow \eta) \rightarrow (\varphi\rightarrow\psi))) \rightarrow ((\varphi \rightarrow \psi) \rightarrow ((\psi \rightarrow \eta) \rightarrow (\varphi\rightarrow\eta)))]\)	: \(\varphi_3\)	// instance of (HS1)
	\(\vdash\)	\(((\varphi \rightarrow \psi) \rightarrow ((\psi \rightarrow \eta) \rightarrow (\varphi\rightarrow\psi))) \rightarrow ((\varphi \rightarrow \psi) \rightarrow ((\psi \rightarrow \eta) \rightarrow (\varphi\rightarrow\eta)))\)	: \(\varphi_4\)	// from \(\varphi_2\) and \(\varphi_3\) by MP
	\(\vdash\)	\((\varphi \rightarrow \psi) \rightarrow ((\psi \rightarrow \eta) \rightarrow (\varphi\rightarrow\psi))\)	: \(\varphi_5\)	// instance of \(A_1\)
	\(\vdash\)	\((\varphi \rightarrow \psi) \rightarrow ((\psi \rightarrow \eta) \rightarrow (\varphi\rightarrow\eta))\)	: \(\varphi_6\)	// from \(\varphi_4\) and \(\varphi_5\) by MP

∎

• HS:

	\(\vdash\)	\(\varphi \rightarrow \psi\)	: \(\varphi_0\)	// assumption
	\(\vdash\)	\(\psi \rightarrow \eta\)	: \(\varphi_1\)	// assumption
	\(\vdash\)	\((\varphi \rightarrow \psi) \rightarrow [(\psi \rightarrow \eta) \rightarrow (\varphi \rightarrow \eta)]\)	: \(\varphi_2\)	// instance of (HS2)
	\(\vdash\)	\((\psi \rightarrow \eta) \rightarrow (\varphi \rightarrow \eta)\)	: \(\varphi_3\)	// from \(\varphi_0\) and \(\varphi_2\) by MP
	\(\vdash\)	\(\varphi \rightarrow \eta\)	: \(\varphi_4\)	// from \(\varphi_1\) and \(\varphi_3\) by MP

∎

Lemmas:

The following lemmas will be proven:

• (L1): \(\varphi \rightarrow [(\varphi \rightarrow \psi) \rightarrow \psi]\)
• (L2): \(\neg\varphi \rightarrow (\varphi \rightarrow \psi)\)
• (L3): \((\neg\varphi \rightarrow \varphi) \rightarrow \varphi\)

Proofs:

• (L1):

	\(\vdash\)	\([(\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi)] \rightarrow [((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \psi)]\)	: \(\varphi_0\)	// instance of \(A_2\)
	\(\vdash\)	\((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi)\)	: \(\varphi_1\)	// instance of (R)
	\(\vdash\)	\(((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \psi)\)	: \(\varphi_2\)	// from \(\varphi_0\) and \(\varphi_1\) by MP
	\(\vdash\)	\(\varphi \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi)\)	: \(\varphi_3\)	// instance of \(A_1\)
	\(\vdash\)	\(\varphi \rightarrow ((\varphi \rightarrow \psi) \rightarrow \psi)\)	: \(\varphi_4\)	// from \(\varphi_2\) and \(\varphi_3\) by HS

∎

• (L2):

	\(\vdash\)	\(\neg\varphi \rightarrow (\neg\psi \rightarrow \neg\varphi)\)	: \(\varphi_0\)	// instance of \(A_1\)
	\(\vdash\)	\((\neg\psi\rightarrow\neg\varphi)\rightarrow(\varphi\rightarrow\psi)\)	: \(\varphi_1\)	// instance of \(A_3\)
	\(\vdash\)	\(\neg\varphi \rightarrow (\varphi \rightarrow \psi)\)	: \(\varphi_2\)	// from \(\varphi_0\) and \(\varphi_1\) by HS

∎

• (L3):

	\(\vdash\)	\(\psi\)	: \(\varphi_0\)	// instance of any axiom schema or proved theorem
	\(\vdash\)	\(\neg\varphi \rightarrow (\varphi \rightarrow \neg\psi)\)	: \(\varphi_1\)	// instance of (L2)
	\(\vdash\)	\([\neg\varphi \rightarrow (\varphi \rightarrow \neg\psi)] \rightarrow [(\neg\varphi \rightarrow \varphi) \rightarrow (\neg\varphi \rightarrow \neg\psi)]\)	: \(\varphi_2\)	// instance of \(A_2\)
	\(\vdash\)	\((\neg\varphi \rightarrow \varphi) \rightarrow (\neg\varphi \rightarrow \neg\psi)\)	: \(\varphi_3\)	// from \(\varphi_1\) and \(\varphi_2\) by MP
	\(\vdash\)	\((\neg\varphi \rightarrow \neg\psi) \rightarrow (\psi \rightarrow \varphi)\)	: \(\varphi_4\)	// instance of \(A_3\)
	\(\vdash\)	\((\neg\varphi \rightarrow \varphi) \rightarrow (\psi \rightarrow \varphi)\)	: \(\varphi_5\)	// from \(\varphi_3\) and \(\varphi_4\) by HS
	\(\vdash\)	\(\psi \rightarrow [(\psi \rightarrow \varphi) \rightarrow \varphi]\)	: \(\varphi_6\)	// instance of (L1)
	\(\vdash\)	\((\psi \rightarrow \varphi) \rightarrow \varphi\)	: \(\varphi_7\)	// from \(\varphi_0\) and \(\varphi_6\) by MP
	\(\vdash\)	\((\neg\varphi \rightarrow \varphi) \rightarrow \varphi\)	: \(\varphi_8\)	// from \(\varphi_5\) and \(\varphi_7\) by HS

∎

(L3) is known as Clavius's law or Consequentia Mirabilis.

Double Negation Theorems

The following theorems will be proven:

• (DN1): \(\neg\neg\varphi \rightarrow \varphi\)
• (DN2): \(\varphi \rightarrow \neg\neg\varphi\)

Proofs:

• (DN1):

	\(\vdash\)	\(\psi\)	: \(\varphi_0\)	// instance of any axiom schema or proved theorem
	\(\vdash\)	\((\neg\neg\psi \rightarrow \neg\neg\varphi) \rightarrow (\neg\varphi \rightarrow \neg\psi)\)	: \(\varphi_1\)	// instance of \(A_3\)
	\(\vdash\)	\((\neg\varphi \rightarrow \neg\psi) \rightarrow (\psi \rightarrow \varphi)\)	: \(\varphi_2\)	// instance of \(A_3\)
	\(\vdash\)	\((\neg\neg\psi \rightarrow \neg\neg\varphi) \rightarrow (\psi \rightarrow \varphi)\)	: \(\varphi_3\)	// from \(\varphi_1\) and \(\varphi_2\) by HS
	\(\vdash\)	\(\neg\neg\varphi \rightarrow (\neg\neg\psi \rightarrow \neg\neg\varphi)\)	: \(\varphi_4\)	// instance of \(A_1\)
	\(\vdash\)	\(\neg\neg\varphi \rightarrow (\psi \rightarrow \varphi)\)	: \(\varphi_5\)	// from \(\varphi_3\) and \(\varphi_4\) by HS
	\(\vdash\)	\(\psi \rightarrow ((\psi \rightarrow \varphi) \rightarrow \varphi)\)	: \(\varphi_6\)	// instance of (L1)
	\(\vdash\)	\((\psi \rightarrow \varphi) \rightarrow \varphi\)	: \(\varphi_7\)	// from \(\varphi_0\) and \(\varphi_6\) by MP
	\(\vdash\)	\(\neg\neg\varphi \rightarrow \varphi\)	: \(\varphi_8\)	// from \(\varphi_5\) and \(\varphi_7\) by HS

∎

• (DN2):

	\(\vdash\)	\(\neg\neg\neg\varphi \rightarrow \neg\varphi\)	: \(\varphi_0\)	// instance of (DN1)
	\(\vdash\)	\((\neg\neg\neg\varphi \rightarrow \neg\varphi) \rightarrow (\varphi \rightarrow \neg\neg\varphi)\)	: \(\varphi_1\)	// instance of \(A_3\)
	\(\vdash\)	\(\varphi \rightarrow \neg\neg\varphi\)	: \(\varphi_2\)	// from \(\varphi_0\) and \(\varphi_1\) by MP

∎

Contraposition Theorems

The following theorems will be proven:

• (TR1): \((\varphi \rightarrow \psi) \rightarrow (\neg\psi \rightarrow \neg\varphi)\)
• (TR2): \((\neg\varphi \rightarrow \psi) \rightarrow (\neg\psi \rightarrow \varphi)\)
• (TR3): \((\varphi \rightarrow \neg\psi) \rightarrow (\psi \rightarrow \neg\varphi)\)

Proofs:

• (TR1):

	\(\vdash\)	\(\psi \rightarrow \neg\neg\psi\)	: \(\varphi_0\)	// instance of (DN2)
	\(\vdash\)	\((\psi \rightarrow \neg\neg\psi) \rightarrow [(\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \neg\neg\psi)]\)	: \(\varphi_1\)	// instance of (HS1)
	\(\vdash\)	\((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \neg\neg\psi)\)	: \(\varphi_2\)	// from \(\varphi_0\) and \(\varphi_1\) by MP
	\(\vdash\)	\(\neg\neg\varphi \rightarrow \varphi\)	: \(\varphi_3\)	// instance of (DN1)
	\(\vdash\)	\((\neg\neg\varphi \rightarrow \varphi) \rightarrow [(\varphi \rightarrow \neg\neg\psi) \rightarrow (\neg\neg\varphi \rightarrow \neg\neg\psi)]\)	: \(\varphi_4\)	// instance of (HS2)
	\(\vdash\)	\((\varphi \rightarrow \neg\neg\psi) \rightarrow (\neg\neg\varphi \rightarrow \neg\neg\psi)\)	: \(\varphi_5\)	// from \(\varphi_3\) and \(\varphi_4\) by MP
	\(\vdash\)	\((\varphi \rightarrow \psi) \rightarrow (\neg\neg\varphi \rightarrow \neg\neg\psi)\)	: \(\varphi_6\)	// from \(\varphi_2\) and \(\varphi_5\) by HS
	\(\vdash\)	\((\neg\neg\varphi \rightarrow \neg\neg\psi) \rightarrow (\neg\psi \rightarrow \neg\varphi)\)	: \(\varphi_7\)	// instance of \(A_3\)
	\(\vdash\)	\((\varphi \rightarrow \psi) \rightarrow (\neg\psi \rightarrow \neg\varphi)\)	: \(\varphi_8\)	// from \(\varphi_6\) and \(\varphi_7\) by HS

∎

• (TR2):

	\(\vdash\)	\(\psi \rightarrow \neg\neg\psi\)	: \(\varphi_0\)	// instance of (DN2)
	\(\vdash\)	\((\psi \rightarrow \neg\neg\psi) \rightarrow [(\neg\varphi \rightarrow \psi) \rightarrow (\neg\varphi \rightarrow \neg\neg\psi)]\)	: \(\varphi_1\)	// instance of (HS1)
	\(\vdash\)	\((\neg\varphi \rightarrow \psi) \rightarrow (\neg\varphi \rightarrow \neg\neg\psi)\)	: \(\varphi_2\)	// from \(\varphi_0\) and \(\varphi_1\) by MP
	\(\vdash\)	\((\neg\varphi \rightarrow \neg\neg\psi) \rightarrow (\neg\psi \rightarrow \varphi)\)	: \(\varphi_3\)	// instance of \(A_3\)
	\(\vdash\)	\((\neg\varphi \rightarrow \psi) \rightarrow (\neg\psi \rightarrow \varphi)\)	: \(\varphi_4\)	// from \(\varphi_2\) and \(\varphi_3\) by HS

∎

• (TR3):

	\(\vdash\)	\(\neg\neg\varphi \rightarrow \varphi\)	: \(\varphi_0\)	// instance of (DN1)
	\(\vdash\)	\((\neg\neg\varphi \rightarrow \varphi) \rightarrow [(\varphi \rightarrow \neg\psi) \rightarrow (\neg\neg\varphi \rightarrow \neg\psi)]\)	: \(\varphi_1\)	// instance of (HS2)
	\(\vdash\)	\((\varphi \rightarrow \neg\psi) \rightarrow (\neg\neg\varphi \rightarrow \neg\psi)\)	: \(\varphi_2\)	// from \(\varphi_0\) and \(\varphi_1\) by MP
	\(\vdash\)	\((\neg\neg\varphi \rightarrow \neg\psi) \rightarrow (\psi \rightarrow \neg\varphi)\)	: \(\varphi_3\)	// instance of \(A_3\)
	\(\vdash\)	\((\varphi \rightarrow \neg\psi) \rightarrow (\psi \rightarrow \neg\varphi)\)	: \(\varphi_4\)	// from \(\varphi_2\) and \(\varphi_3\) by HS

∎

(TR2) and (TR3) won't actually be required to prove the Completeness Theorem, nor the Principle of Explosion, but I've decided to include them to complete the set of contraposition theorems.

Lemmas:

The following lemmas will be proven:

• (L4): \(\varphi \rightarrow [\neg\psi \rightarrow \neg(\varphi \rightarrow \psi)]\)
• (L5): \((\varphi \rightarrow \psi) \rightarrow [(\neg\varphi \rightarrow \psi) \rightarrow \psi]\)

Proofs:

• (L4):

	\(\vdash\)	\(\varphi \rightarrow [(\varphi \rightarrow \psi) \rightarrow \psi]\)	: \(\varphi_0\)	// instance of (L1)
	\(\vdash\)	\(((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow (\neg\psi \rightarrow \neg(\varphi \rightarrow \psi))\)	: \(\varphi_1\)	// instance of (TR1)
	\(\vdash\)	\(\varphi \rightarrow (\neg\psi \rightarrow \neg(\varphi \rightarrow \psi))\)	: \(\varphi_2\)	// from \(\varphi_0\) and \(\varphi_1\) by HS

∎

• (L5):

	\(\vdash\)	\((\varphi \rightarrow \psi) \rightarrow (\neg\psi \rightarrow \neg\varphi)\)	: \(\varphi_0\)	// instance of (TR1)
	\(\vdash\)	\((\neg\psi \rightarrow \neg\varphi) \rightarrow [(\neg\varphi \rightarrow \psi) \rightarrow (\neg\psi \rightarrow \psi)]\)	: \(\varphi_1\)	// instance of (HS2)
	\(\vdash\)	\((\neg\psi \rightarrow \psi) \rightarrow \psi\)	: \(\varphi_2\)	// instance of (L3)
	\(\vdash\)	\(((\neg\psi \rightarrow \psi) \rightarrow \psi) \rightarrow [((\neg\varphi \rightarrow \psi) \rightarrow (\neg\psi \rightarrow \psi)) \rightarrow ((\neg\varphi \rightarrow \psi) \rightarrow \psi)]\)	: \(\varphi_3\)	// instance of (HS1)
	\(\vdash\)	\(((\neg\varphi \rightarrow \psi) \rightarrow (\neg\psi \rightarrow \psi)) \rightarrow ((\neg\varphi \rightarrow \psi) \rightarrow \psi)\)	: \(\varphi_4\)	// from \(\varphi_2\) and \(\varphi_3\) by MP
	\(\vdash\)	\((\neg\psi \rightarrow \neg\varphi) \rightarrow ((\neg\varphi \rightarrow \psi) \rightarrow \psi)\)	: \(\varphi_5\)	// from \(\varphi_1\) and \(\varphi_4\) by HS
	\(\vdash\)	\((\varphi \rightarrow \psi) \rightarrow ((\neg\varphi \rightarrow \psi) \rightarrow \psi)\)	: \(\varphi_6\)	// from \(\varphi_0\) and \(\varphi_5\) by HS

∎

Sources:

• A Novel Proof of Hypothetical Syllogism in a Hilbert-Style Calculuspwithee24 (Reddit user)
• Axiomatic system (logic)Wikipedia
• ContrapositionWikipedia
• Differential geometry reconstructedAlan U. Kennington
• Double negationWikipedia
• Gödel's Theorems and Zermelo's AxiomsLorenz Halbeisen & Regula Krapf
• Hypothetical syllogismWikipedia