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)).
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 , 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:
(Proof by Contradiction). If , then .
From , we have by the deduction theorem. Since , the result follows. ∎
(Proof by Contrapositive). If , then .
If , then by the deduction thereom, and therefore by the deduction theorem again. ∎
- 1 J. W. Robbin, Mathematical Logic, A First Course, Dover Publication (2006)
|Title||deduction theorem holds for classical propositional logic|
|Date of creation||2013-03-22 19:13:42|
|Last modified on||2013-03-22 19:13:42|
|Last modified by||CWoo (3771)|
|Defines||proof by contradiction|
|Defines||proof by contrapositive|