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 (A→ B), 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 A → B.
Proof:
The proof is by induction on the number of well-formed formulas, i, in the sequence B_{1}, B_{2}, ..., B_{n}, forming the deduction of B from Γ∪{A}. So, let us prove, by induction on i, that Γ A → B_{i} for 1≤i ≤n. [That is, Γ A→ (B_{1}, ...,B_{i}).]
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. B_{1} = 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→ B_{1}) from Γ.
1. | B_{1} | Axiom of L.. |
2. | B_{1} → (A → B_{1}) | Instance of Axiom A1. |
3. | A → B_{1} | From 1 and 2 by modus ponens. |
Hence, Γ A→ B_{1}
Case ii. When B_{1} ∈ Γ.
Then, the following deduction shows Γ A → B_{1}
1. | B_{1} | Member of the set Γ. |
2. | B_{1} → (A → B_{1}) | Instance of Axiom A1. |
3. | A → B_{1} | From 1 and 2 by modus ponens. |
Hence, Γ A→ B_{1}
Case iii. When B_{1} 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 B_{1} is A, we have A→ B_{1}, by the above deduction, and, therefore, Γ A→ B_{1}.
And this completes the base case i = 1.
2. Inductive Step: Assume that Γ A→ B_{k} 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. | B_{k} is an axiom in L. |
Case ii. | B_{k} in a member of Γ. |
Case iii. | B_{k} is A. |
Case iv. | B_{k} follows from some [previous] B_{j} and B_{m}, where j < k and B_{m} < k, and B_{m} has the form B_{j} → B_{k}. |
Now lets work on these four cases.
Case i. When B_{k} 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 B_{k} ∈ Γ. Again, this is the same as that of case ii in the Base Step.
Case iii. When B_{k} is A. Once again, this is the case iii in the Base Step.
Case iv. Here we say: since B_{k} 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 B_{j}] and (C → B_{k}) [or (B_{j} → B_{k})] 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} (C → B), and, applying the induction hypothesis, we have
Γ (A → C) and Γ (A → (C→ B)).
[Note that we have done with C instead of B_{j} and (C → B_{k}) instead of (B_{j} → B_{k}) - But you should do with B_{j} and (B_{j} → B_{k}) - Possible Extra Credit!]
The idea of deduction of (A → B_{k}) 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 → B_{k}) | |
l + 1 | (A → (C → B_{k})) → ((A → C) → (A → B_{k})) | Instance of Axiom 2. |
l + 2 | (A → C) → (A → B_{k}) | From l and l + 1by modus ponens. |
l + 3 | A → B_{k} | From k and l +2 by modus ponens. |
Therefore, Γ (A → B_{k}) 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 Γ (A → B), 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)