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).
Theorem 1.
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 .
Proof.
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 .
-
•
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.
References
- 1 J. W. Robbin, Mathematical Logic, A First Course, Dover Publication (2006)
Title | deduction theorem holds for intuitionistic propositional logic |
---|---|
Canonical name | DeductionTheoremHoldsForIntuitionisticPropositionalLogic |
Date of creation | 2013-03-22 19:31:32 |
Last modified on | 2013-03-22 19:31:32 |
Owner | CWoo (3771) |
Last modified by | CWoo (3771) |
Numerical id | 21 |
Author | CWoo (3771) |
Entry type | Theorem |
Classification | msc 03F55 |
Classification | msc 03B20 |
Related topic | AxiomSystemForIntuitionisticLogic |