deduction theorem holds for intuitionistic propositional logic
In this entry, we show that the deduction theorem below holds for intuitionistic propositional logic. We use the axiom system provided in this entry (http://planetmath.org/AxiomSystemForIntuitionisticLogic).
If , where is a set of wff’s of the intuitionistic propositional logic, then .
The proof is very similar to that of the classical propositional logic, given here (http://planetmath.org/DeductionTheoremHoldsForClassicalPropositionalLogic), in that it uses induction on the length of the deduction of . In fact, the proof is simpler as only two axiom schemas are used: and .
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 .
Now, suppose that
is a deduction of from , with obtained from earlier formulas by modus ponens.
We use induction on the length of deduction of . Note that . If , then and are either axioms or in .
If is , then is either an axiom or in . So .
If and are axioms or in , then based on the deduction .
Next, assume there is a deduction of of length . So one of the earlier formulas is , and a subsequence of is a deduction of , which has length less than , and therefore by induction, . Likewise, a subsequence of is a deduction of , so by induction, . With the axiom instance , and two applications of modus ponens, we get as required.
In both cases, , and the proof is complete. ∎
Remark The deduction theorem can be used to prove the deduction theorem for the first and second order intuitionistic predicate logic.
- 1 J. W. Robbin, Mathematical Logic, A First Course, Dover Publication (2006)
|Title||deduction theorem holds for intuitionistic propositional logic|
|Date of creation||2013-03-22 19:31:32|
|Last modified on||2013-03-22 19:31:32|
|Last modified by||CWoo (3771)|