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 .
- •
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 is , then is either an axiom or in . Then
is a deduction of from , where is a deduction of the theorem
, followed by an axiom instance, then , then the result of modus ponens, then an axiom instance, and finally two applications of modus ponens. Note the second to the last formula is just .
- –
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)