deduction theorem holds for classical propositional logic
In this entry, we prove that the deduction theorem holds for classical propositional logic. For the logic, we use the axiom system found in this entry (http://planetmath.org/AxiomSystemForPropositionalLogic). To prove the theorem, we use the theorem schema $A\to A$ (whose deduction^{} can be found here (http://planetmath.org/AxiomSystemForPropositionalLogic)).
Proof.
Suppose ${A}_{1},\mathrm{\dots},{A}_{n}$ is a deduction of $B$ from $\mathrm{\Delta}\cup \{A\}$. We want to find a deduction of $A\to B$ from $\mathrm{\Delta}$. There are two main cases to consider:

•
If $B$ is an axiom or in $\mathrm{\Delta}\cup \{A\}$, then
$$B,B\to (A\to B),A\to B$$ is a deduction of $A\to B$ from $\mathrm{\Delta}$, where $A\to B$ is obtained by modus ponens^{} applied to $B$ and the axiom $B\to (A\to B)$. So $\mathrm{\Delta}\u22a2A\to B$.

•
If $B$ is obtained from ${A}_{i}$ and ${A}_{j}$ by modus ponens. Then ${A}_{j}$, say, is ${A}_{i}\to B$. We use induction^{} on the length $n$ of the deduction of $B$. Note that $n\ge 3$. If $n=3$, then the first two formulas^{} are $C$ and $C\to B$.

–
If $C$ is $A$, then $C\to B$ is either an axiom or in $\mathrm{\Delta}$. So $A\to B$, which is just $C\to B$, is a deduction of $A\to B$ from $\mathrm{\Delta}$.

–
If $C\to B$ is $A$, then $C$ is either an axiom or in $\mathrm{\Delta}$, and
$${\mathcal{E}}_{0},(A\to A)\to ((A\to C)\to (A\to B)),C\to (A\to C),C,A\to C,A\to B$$ is a deduction of $A\to B$ from $\mathrm{\Delta}$, where ${\mathcal{E}}_{0}$ is a deduction of $A\to A$, followed by two axiom instances, followed by $C$, followed by results of two applications of modus ponens.

–
If both $C$ and $C\to B$ are either axioms are in $\mathrm{\Delta}$, then
$$C,C\to B,B,B\to (A\to B),A\to B$$ is a deduction of $A\to B$ from $\mathrm{\Delta}$.
Next, assume the deduction $\mathcal{E}$ of $B$ has length $n>3$. A subsequence of $\mathcal{E}$ is a deduction of ${A}_{i}\to B$ from $\mathrm{\Delta}\cup \{A\}$. This deduction has length less than $n$, so by induction,
$$\mathrm{\Delta}\u22a2A\to ({A}_{i}\to B),$$ and therefore by $(A\to ({A}_{i}\to B))\to ((A\to {A}_{i})\to (A\to B))$, an axiom instance, and modus ponens,
$$\mathrm{\Delta}\u22a2(A\to {A}_{i})\to (A\to B).$$ Likewise, a subsequence of $\mathcal{E}$ is a deduction of ${A}_{i}$, so by induction, $\mathrm{\Delta}\u22a2A\to {A}_{i}$. Therefore, an application of modus ponens gives us $\mathrm{\Delta}\u22a2A\to B$.

–
In both cases, $\mathrm{\Delta}\u22a2A\to B$ and we are done. ∎
We record two corollaries:
Corollary 1.
(Proof by Contradiction^{}). If $\mathrm{\Delta}\mathrm{,}A\mathrm{\u22a2}\mathrm{\u27c2}$, then $\mathrm{\Delta}\mathrm{\u22a2}\mathrm{\neg}\mathit{}A$.
Proof.
From $\mathrm{\Delta},A\u22a2\u27c2$, we have $\mathrm{\Delta}\u22a2A\to \u27c2$ by the deduction theorem^{}. Since $\mathrm{\neg}A\leftrightarrow \u27c2$, the result follows. ∎
Corollary 2.
(Proof by Contrapositive). If $\mathrm{\Delta}\mathrm{,}A\mathrm{\u22a2}\mathrm{\neg}\mathit{}B$, then $\mathrm{\Delta}\mathrm{,}B\mathrm{\u22a2}\mathrm{\neg}\mathit{}A$.
Proof.
If $\mathrm{\Delta},A\u22a2\mathrm{\neg}B$, then $\mathrm{\Delta},A,B\u22a2\u27c2$ by the deduction thereom, and therefore $\mathrm{\Delta},B\u22a2\mathrm{\neg}A$ by the deduction theorem again. ∎
Remark The deduction theorem for the classical propositional logic^{} can be used to prove the deduction theorem for the classical first and second order^{} predicate logic.
References
 1 J. W. Robbin, Mathematical Logic, A First Course, Dover Publication (2006)
Title  deduction theorem holds for classical propositional logic 

Canonical name  DeductionTheoremHoldsForClassicalPropositionalLogic 
Date of creation  20130322 19:13:42 
Last modified on  20130322 19:13:42 
Owner  CWoo (3771) 
Last modified by  CWoo (3771) 
Numerical id  23 
Author  CWoo (3771) 
Entry type  Theorem 
Classification  msc 03F03 
Classification  msc 03B99 
Classification  msc 03B22 
Related topic  AxiomSystemForPropositionalLogic 
Defines  proof by contradiction 
Defines  proof by contrapositive 