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 (whose deduction can be found here (http://planetmath.org/AxiomSystemForPropositionalLogic)).
Proof.
Suppose is a deduction of from . We want to find a deduction of from . There are two main cases to consider:
-
•
If is an axiom or in , then
is a deduction of from , where is obtained by modus ponens applied to and the axiom . So .
-
•
If is obtained from and by modus ponens. Then , say, is . We use induction on the length of the deduction of . Note that . If , then the first two formulas are and .
-
–
If is , then is either an axiom or in . So , which is just , is a deduction of from .
-
–
If is , then is either an axiom or in , and
is a deduction of from , where is a deduction of , followed by two axiom instances, followed by , followed by results of two applications of modus ponens.
-
–
If both and are either axioms are in , then
is a deduction of from .
Next, assume the deduction of has length . A subsequence of is a deduction of from . This deduction has length less than , so by induction,
and therefore by , an axiom instance, and modus ponens,
Likewise, a subsequence of is a deduction of , so by induction, . Therefore, an application of modus ponens gives us .
-
–
In both cases, and we are done. ∎
We record two corollaries:
Corollary 1.
(Proof by Contradiction). If , then .
Proof.
From , we have by the deduction theorem. Since , the result follows. ∎
Corollary 2.
(Proof by Contrapositive). If , then .
Proof.
If , then by the deduction thereom, and therefore 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 | 2013-03-22 19:13:42 |
Last modified on | 2013-03-22 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 |