Deduction theorem explanation

Question

Can someone please explain Deduction theorem in Logic. I am using the textbook "Mathematical Logic" for Tourlakis.

I can't understand it at all.

Answer 1

The statement is the reverse of modus ponens so to speak: If it is possible to deduce $B$ under the assumption that $A$ holds, then it is possible to deduce the single formula $A\to B$. But in contrast to modus ponens this is not an immediate rule of inference by itself, even though its result seems so obvious.

Answer 2

By way of example, suppose we want to establish that $(a \to (b \to c)) \to (b \to (a \to c))$ is provable, i.e. that

$$\vdash (a \to (b \to c)) \to (b \to (a \to c))$$

The deduction theorem states that this holds if the following holds:

$$(a \to (b \to c)) \vdash (b \to (a \to c))$$

That is, there is a proof of the original theorem if we can prove $(b \to (a \to c))$ using $(a \to (b \to c))$ as an assumption. Applying the theorem again, the above holds if

$$(a \to (b \to c)),\ b \vdash (a \to c)$$

Which in turn holds if

$$(a \to (b \to c)),\ b,\ a \vdash c$$

That is, the original theorem is provable (with no assumptions) if $c$ is provable with $a$, $b$ and $a \to (b \to c)$ as assumptions. This is easy to prove:

1. $(a \to (b \to c)),\ b,\ a \vdash a$ by assumption
2. $(a \to (b \to c)),\ b,\ a \vdash a \to (b \to c)$ by assumption
3. $(a \to (b \to c)),\ b,\ a \vdash b \to c$ by modus ponens on 1 and 2
4. $(a \to (b \to c)),\ b,\ a \vdash b$ by assumption
5. $(a \to (b \to c)),\ b,\ a \vdash c$ by modus ponens on 3 and 4.

To appreciate the usefulness of the deduction theorem, try to prove $(a \to (b \to c)) \to (b \to (a \to c))$ without using it.

So far, I have only shown (assuming that the deduction theorem is true) that $$(a \to (b \to c)) \to (b \to (a \to c))$$ is provable, but I haven't constructed such a proof.

The Wikipedia article has an algorithm for going from $\Gamma, H \vdash C$ to $\Gamma \vdash H \to C$, that is, for turning an assumption into a condition. Instead of proving $C$ given $H$, you can prove "if $H$ then $C$".

To construct a proof of $(a \to (b \to c)) \to (b \to (a \to c))$, use the proof of $c$ with assumptions to construct a proof of $a \to c$ with fewer assumptions, then a proof of $b \to (a \to c)$ with even fewer assumptions, and then a proof of $(a \to (b \to c)) \to (b \to (a \to c))$ with no assumptions.

Answer 3

You can see Stephen Cole Kleene, Mathematical Logic (1967).

It is not very "user friendly": other textbooks are better for beginning with mathematical logic, but it adopt a presentation of the proof system that is interesting.

Limit ourselfs for simplicity to propositional calculus (Chapter I, page 3-on): the book states an Hilbert-style proof system, based on a list of axioms [page 15]: from 1a to 10b, and a single rule of inference, the only primitive one : modus ponens [page 34].

Then he proves a set of "derived rules" [Theorem 13, page 44] that are the analogue of introduction and elimination rules of Natural Deduction.

Typically, we have a couple of rules (one for introduction and one for elimination) for every connective.

The couple of rules for $\rightarrow$ are :

$A,A \rightarrow B \vdash B \quad $ --- called $\rightarrow$-elimination; it is simply modus ponens

if $\Gamma , A \vdash B$, then $\Gamma \vdash A \rightarrow B \quad $ --- called $\rightarrow$-introduction; it is the Deduction Theorem [see Kleene, page 39].

The "derived rules" are proved via meta-theorems, i.e. we use an argument in the meta-theory showing that we can add them without causing troubles.

The proof of the Deduction Theorem amount to displaying a method that, whenever we are given a deduction of $B$ from the assumption $A$ and the set of assumptions $\Gamma$, we can "build" a new deduction of $A \rightarrow B$ from the set of assumptions $\Gamma$.

If we refer to George Tourlakis, Mathematical Logic (2008), we have a different set of axioms and two primitive rules of inference : Leibniz and Equanimity.

This is a different proof systems, but the general "mechanism" is the same : you can introduce derived rules, like Transitivity [page 47] and Equanimity + Leibniz Merged [page 57].

But the overall result is the same : we want that all different proof systems (Equational, Natural Deduction, Hilbert-style) are sound and complete, i.e. we want that each of them can prove all and only the tautologies.

Also in Tourlakis you have the Deduction Theorem : see page 81-on; can be useful to re-read at page 45 the Remark 1.4.10 (Theorem vs. Metatheorem).