You are here
Homededuction theorem holds for classical propositional logic
Primary tabs
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. To prove the theorem, we use the theorem schema $A\to A$ (whose deduction can be found here).
Proof.
Suppose $A_{1},\ldots,A_{n}$ is a deduction of $B$ from $\Delta\cup\{A\}$. We want to find a deduction of $A\to B$ from $\Delta$. There are two main cases to consider:

If $B$ is an axiom or in $\Delta\cup\{A\}$, then
$B,B\to(A\to B),A\to B$ is a deduction of $A\to B$ from $\Delta$, where $A\to B$ is obtained by modus ponens applied to $B$ and the axiom $B\to(A\to B)$. So $\Delta\vdash A\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\geq 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 $\Delta$. So $A\to B$, which is just $C\to B$, is a deduction of $A\to B$ from $\Delta$.

If $C\to B$ is $A$, then $C$ is either an axiom or in $\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 $\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 $\Delta$, then
$C,C\to B,B,B\to(A\to B),A\to B$ is a deduction of $A\to B$ from $\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 $\Delta\cup\{A\}$. This deduction has length less than $n$, so by induction,
$\Delta\vdash A\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,
$\Delta\vdash(A\to A_{i})\to(A\to B).$ Likewise, a subsequence of $\mathcal{E}$ is a deduction of $A_{i}$, so by induction, $\Delta\vdash A\to A_{i}$. Therefore, an application of modus ponens gives us $\Delta\vdash A\to B$.

In both cases, $\Delta\vdash A\to B$ and we are done. ∎
We record two corollaries:
Corollary 1.
(Proof by Contradiction). If $\Delta,A\vdash\perp$, then $\Delta\vdash\neg A$.
Proof.
From $\Delta,A\vdash\perp$, we have $\Delta\vdash A\to\perp$ by the deduction theorem. Since $\neg A\leftrightarrow\perp$, the result follows. ∎
Corollary 2.
(Proof by Contrapositive). If $\Delta,A\vdash\neg B$, then $\Delta,B\vdash\neg A$.
Proof.
If $\Delta,A\vdash\neg B$, then $\Delta,A,B\vdash\perp$ by the deduction thereom, and therefore $\Delta,B\vdash\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)
Mathematics Subject Classification
03F03 no label found03B99 no label found03B22 no label found Forums
 Planetary Bugs
 HS/Secondary
 University/Tertiary
 Graduate/Advanced
 Industry/Practice
 Research Topics
 LaTeX help
 Math Comptetitions
 Math History
 Math Humor
 PlanetMath Comments
 PlanetMath System Updates and News
 PlanetMath help
 PlanetMath.ORG
 Strategic Communications Development
 The Math Pub
 Testing messages (ignore)
 Other useful stuff
 Corrections