The Deduction Theorem

In logic (as well as in mathematics), we deduce a proposition B on the assumption of some other proposition A and then conclude that the implication "If A then B" is true. This line of argument is justified for the formal axiomatic system by the following well-known theorem.

If Γ∪{A} B, then T (AB), where A and B are well-formed formulas and Γ is a set of well-formed formulas (possibly empty).

The other way of saying the same thing (perhaps more clearly):

If Γ, A B, then Γ A B. In particular (when Γ is empty), if A B, then AB.

Proof:

The proof is by induction on the number of well-formed formulas, i, in the sequence B1, B2, ..., Bn, forming the deduction of B from Γ∪{A}. So, let us prove, by induction on i, that Γ ABi for 1≤i ≤n. [That is, Γ A→ (B1, ...,Bi).]

1. Base Step: When  i = 1.

That is, for the base case suppose that this sequence has one member. Then, that member must be B itself (i.e. B1 = B), and so either B is axiom of formal axiomatic theory L or B is a member of a set Γ∪{A}. This means we have three sub cases in the base case.

Case i. When B1 is an axiom of L

Then, the following is a deduction of (A→ B1) from Γ.

 1 B1 Axiom of L.. 2 B1 → (A → B1) Instance of Axiom A1. 3 A → B1 From 1 and 2 by modus ponens.

Hence, Γ A B1

Case ii. When B1 ∈ Γ.

Then, the following deduction shows Γ A B1

 1 B1 Member of the set Γ. 2 B1 → (A → B1) Instance of Axiom A1. 3 A → B1 From 1 and 2 by modus ponens.

Hence, Γ A B1

Case iii. When B1 is A.

Then, the following deduction shows that A A.

 1 (A → ((A → A) → A)) → ((A → (A → A)) → (A → A)) Instance of Axiom A2. 2 (A → ((A → A) → A)) Instance of Axiom A1. 3 ((A → (A → A)) → (A → A)) From 1 and 2 by modus ponens. 4 (A → (A → A)) Instance of Axiom A1. 5 (A → A) From 3 and 4 by modus ponens.

So, A A.

Hence, when B1 is A, we have A B1, by the above deduction, and, therefore, Γ A B1.

And this completes the base case i = 1.

2. Inductive Step: Assume that Γ ABk for all k < i.

Now suppose that the deduction of B from Γ∪{A} is a sequence with n members, where n > 1, and that the proposition holds for all well-formed formulas C which can be deduced from Γ∪{A} via sequence with fewer than n members. This time we have following four sub-cases to consider:

 Case i. Bk is an axiom in L. Case ii. Bk in a member of Γ. Case iii. Bk is A. Case iv. Bk follows from some [previous] Bj and Bm, where j < k and Bm < k, and Bm has the form Bj → Bk.

Now lets work on these four cases.

Case i. When Bk is an axiom of L. This is the precisely the case i above in the base case. In the base case, we have shown that Γ (A → Bi).

Case ii. When Bk ∈ Γ. Again, this is the same as that of case ii in the Base Step.

Case iii. When Bk is A. Once again, this is the case iii in the Base Step.

Case iv. Here we say: since Bk is obtained from two previous well-formed formulas in the deduction by the application of modus ponens. These two well-formed formulas must have the form C [or Bj] and (CBk) [or (BjBk)] and each one can be deduced from Γ∪{A} by a sequence with fewer than n members [i.e. k < n]. We have Γ∪{A} C and Γ∪{A} (CB), and, applying the induction hypothesis, we have

Γ (AC)   and    Γ (A → (CB)).

[Note that we have done with C instead of Bj and (CBk) instead of (BjBk) - But you should do with Bj and (BjBk) - Possible Extra Credit!]

The idea of deduction of (ABk) from Γ is as follows:

 1. . Deduction . . of . . (A → C) . . from Γ . ___________________ k A → C Deduction k + 1 . of . . A → (C → Bk) . . from . . the set Γ . ___________________ l A → (C → Bk) l + 1 (A → (C → Bk)) → ((A → C) → (A → Bk)) Instance of Axiom 2. l + 2 (A → C) → (A → Bk) From l and l + 1by modus ponens. l + 3 A → Bk From k and l +2 by modus ponens.

Therefore, Γ (ABk) in all four cases.

Hence, by the principle of mathematical induction the given proposition holds whatever the number of well-formed formulas in the deduction of B from Γ∪{A}.

And this completes the proof.

Converse of the Deduction Theorem

The proof of the converse of the Deduction theorem is much more easier and (pleasant) than that of original proposition of the Deduction Theorem. The converse [of the original statement] is as follows:

If Γ (AB), then Γ∪{A} B, where A and B are well-formed formulas and Γ is a set of well-formed formulas (possibly empty).

Proof.

Given a deduction of A → B from Γ, our problem is to construct a deduction of B from Γ∪{A}.

 1. . Deduction . . of . . (A → B) . . from Γ k A → B __________________ k + 1 A Member of Γ∪{A} k + 2 B From k and k + 1 by modus ponens.

Hence, Γ∪{A} B.

And this completes the proof.

Application of the Deduction Theorem

To see the application of the Deduction Theorem, lets consider the rule 'hypothetical syllogism' as the example. We say that for any propositions A, B and C in the formal axiomatic theory L, we have

{(A → B), (B → C)} (A → C)

We write out the deduction as follows:

 1 (A → B) Hypothesis. 2 (B → C) Hypothesis. 3 A Hypothesis. 4 B From 1 and 3 by modus ponens. 5 C From 2 and 4 by modus ponens.

From the above deduction, we see that

A → B, B → C, A C

Now apply the Deduction Theorem and we have

A → B, B → C A → C

We conclude this section by stating two important corollaries (can easily be shown using above deduction.)

Corollary I. For any well-formed formulas A, B and C in the formal axiomatic theory L,

(A → B), (B → C) (A → C)

Corollary II. For any well-formed formulas A, B and C in the formal axiomatic theory L,

A → (A → B), B  (A → C)