# Deduction theorem explanation

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

I can't understand it at all.

• When I was struggling with Enderton's 'A Mathematical Introduction to Logic', I found Mordechai Ben-Ari's 'Mathematical Logic for Computer Science' extremely useful for self-learning. Jun 21, 2020 at 18:40

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.

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

• So how could i use the deduction theorem ? And What kind of questions can i get on the deduction theorem? Also i would be thankful if you explained 3.1 and 3.2 in Tourlakis. The material is very hard to understand. It would be good if you gave a summary of these two sections and how could i use them ? Feb 21, 2014 at 16:24
• @Tennisman -you can read this post and you can appreciate how much easier is to prove some results with the DT than without it ... Feb 22, 2014 at 8:27
• @Trismegistos - Thanks ! Feb 24, 2014 at 10:22

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.

• Bonus point for mentioning the conversion algorithm on Wikipedia! I've been looking for that for a day now, but didn't know how to search for it and finally found it now thanks to you! Apr 29, 2020 at 21:39