2.5 Deduction Metatheorem

The Deduction Theorem states that \(\varphi \vdash \psi\ \Leftrightarrow\ \vdash \varphi \rightarrow \psi\)

• Proof of \(\quad\varphi \vdash \psi \quad\Leftarrow\quad \vdash \varphi \rightarrow \psi\quad\):

Assume that \(\vdash \varphi \rightarrow \psi\).

\(\varphi\)	\(\vdash\)	\(\varphi\)	: \(\varphi_0\)	// hypothesis
	\(\vdash\)	\(\varphi \rightarrow \psi\)	: \(\varphi_1\)	// assumption
\(\varphi\)	\(\vdash\)	\(\varphi \rightarrow \psi\)	: \(\varphi_1\)	// \(\vdash \varphi \rightarrow \psi \ \Rightarrow\ \varphi \vdash \varphi \rightarrow \psi\) * \(\qquad\longrightarrow\) this step may be omitted
\(\varphi\)	\(\vdash\)	\(\psi\)	: \(\varphi_2\)	// from \(\varphi_0\) and \(\varphi_1\) by MP

*: Indeed, if something can be proved without hypothesis, then adding hypothesis won't change the fact that it can be proved

• Proof of \(\quad\varphi \vdash \psi \quad\Rightarrow\quad \vdash \varphi \rightarrow \psi\quad\):

Assume that \(\varphi \vdash \psi\). That means that \(\psi\) is either trivial, i.e. it is either \(\varphi\), or an axiom/proved theorem of \(P_2\) (base cases), or it can be proved by MP from two wffs \(\psi_j\) and \(\psi_j \rightarrow \psi\) (inductive case).

Let the wffs \(\psi_0\) till \(\psi_n\), where \(\psi_n\) and \(\psi\) are the same, make up a formal proof for \(\psi\) from \(\varphi\). For all \(i\) from 0 till \(n\), we shall reach \(\psi_i\) with a sequence of formulas which ends with \(\varphi \rightarrow \psi_i\). By doing so for all \(\psi_i\), we shall eventually reach \(\varphi \rightarrow \psi_n\), which will prove the theorem.

• Base cases:
• If \(\psi_i\) is an axiom or a proved theorem of \(P_2\):

	\(\vdash\)	\(\psi_i\)	: \(\varphi_{i,0}\)	// \(\psi_i\) is an axiom or a proved theorem
	\(\vdash\)	\(\psi_i \rightarrow (\varphi \rightarrow \psi_i)\)	: \(\varphi_{i,1}\)	// instance of \(A_1\)
	\(\vdash\)	\(\varphi \rightarrow \psi_i\)	: \(\varphi_{i,2}\)	// from \(\varphi_{i,0}\) and \(\varphi_{i,1}\) by MP

• If \(\psi_i\) is \(\varphi\):

	\(\vdash\)	\(\varphi \rightarrow \varphi\)	: \(\varphi_{i,0}\)	// instance of Implication Reflexivity
	\(\vdash\)	\(\varphi \rightarrow \psi_i\)	: \(\varphi_{i,0}\)	// \(\psi_i\) is \(\varphi\)

• Inductive case: \(\psi_i\) is obtained by MP from \(\psi_j\) and \(\psi_j \rightarrow \psi_i\):

	\(\vdash\)	\(\varphi \rightarrow \psi_j\)	: \(\varphi_{i,0}\)	// induction hypothesis
	\(\vdash\)	\(\varphi \rightarrow (\psi_j \rightarrow \psi_i)\)	: \(\varphi_{i,1}\)	// induction hypothesis
	\(\vdash\)	\([\varphi \rightarrow (\psi_j \rightarrow \psi_i)] \rightarrow [(\varphi \rightarrow \psi_j) \rightarrow (\varphi \rightarrow \psi_i)]\)	: \(\varphi_{i,2}\)	// instance of \(A_2\)
	\(\vdash\)	\((\varphi \rightarrow \psi_j) \rightarrow (\varphi \rightarrow \psi_i)\)	: \(\varphi_{i,3}\)	// from \(\varphi_{i,1}\) and \(\varphi_{i,2}\) by MP
	\(\vdash\)	\(\varphi \rightarrow \psi_i\)	: \(\varphi_{i,4}\)	// from \(\varphi_{i,0}\) and \(\varphi_{i,3}\) by MP

∎

Whenever this theorem is invoked, we shall abbreviate its name as DT.

The main reason why \(A_1\) and \(A_2\) were chosen as the axioms of \(P_2\) is that they are designed to prove the Deduction Metatheorem. Just like the Hypothetical Syllogism Metatheorem, once you've proved it, proving theorems becomes easier, as you get a new tool that works as an additional inference rule, like Modus Ponens.

Examples of decompression

In case you are still a bit foggy about induction, I'll present two examples of theorems in which the Deduction Theorem is used and convert them into pure formal proofs, without its use.

Let's first illustrate the use of \(\varphi \vdash \psi\ \Leftarrow\ \vdash \varphi \rightarrow \psi\), by providing a trivial alternative proof of HS:

∎

To decompress this theorem, we follow the algorithm provided in the "\(\Leftarrow\)" direction of the proof the Deduction Theorem:

∎

This was easy, but now comes the interesting part. Let's illustrate the use of \(\varphi \vdash \psi\ \Rightarrow\ \vdash \varphi \rightarrow \psi\) with an alternative proof of (TR1):

∎

The Deduction Theorem was used twice, once for the hypothesis \(\neg\neg\varphi\) and another for the hypothesis \(\varphi \rightarrow \psi\). Let's first expand the proof for the first use of DT. To do so, we refer to the algorithm provided in the "\(\Rightarrow\)" direction of the proof the Deduction Theorem and draw the following tree:

The arrows mean "depends on"/"is proved by". Each node (\(\varphi_i\)) corresponds to an inductive case and is proved by two others (\(\varphi_j\) and \(\varphi_j \rightarrow \varphi_i\)) by MP, unless it is a leaf, which corresponds to a base case (i.e. an axiom instance, a proved theorem or a hypothesis). According to the proof of DT, for each node \(\varphi_i\), we shall prove \(\neg\neg\varphi \rightarrow \varphi_i\).

Before starting, notice that \(\varphi_3\) will become \(\neg\neg\varphi \rightarrow \varphi\), which is a direct instance of (DN1), so you won't actually need to prove it from \(\neg\neg\varphi \rightarrow \varphi_1\) and \(\neg\neg\varphi \rightarrow \varphi_2\). Thus, we can simplify the tree to

and spare some lines of proof. Furthermore, \(\neg\neg\varphi \rightarrow \varphi\) is simply \(\varphi_2\), so in the final decompressed proof, you'll be able to simply remove \(\varphi_3\), as well as \(\varphi_1\), which was used to prove \(\varphi_3\).

The first decompression step/the removal of the \(\neg\neg\varphi\) hypothesis goes as follows:

∎

To help you follow, notice which subproof/decompression each color corresponds to:

We were lucky, because the theorem length went from 11 lines up to a mere 16. Unfortunately, our luck is about to run out, as we're about to tackle the removal of the \(\varphi \rightarrow \psi\) hypothesis. Behold the dependency tree:

Work in progress, stay tuned!

Sources:

• Axiomatic proof of \(\vdash (a \rightarrow b) \rightarrow (\neg b \rightarrow \neg a)\) without using the deduction theoremBram28 (StackExchange user)
• Gödel's Theorems and Zermelo's AxiomsLorenz Halbeisen & Regula Krapf