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 $\mathrm{\Delta }\mathrm{,}A{\mathrm{⊢}}_{i}B$, where $\mathrm{\Delta }$ is a set of wff’s of the intuitionistic propositional logic, then $\mathrm{\Delta }{\mathrm{⊢}}_{i}A\mathrm{\to }B$.

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 $B$. In fact, the proof is simpler as only two axiom schemas are used: $A\to (B\to A)$ and $(A\to B)\to ((A\to (B\to C))\to (A\to C))$.

Proof.

There are two main cases to consider:

• If $B$ is an axiom or in $\mathrm{\Delta }\cup \{A\}$, then

  $$B,B\to (A\to B),A\to B$$

  is a deduction of $A\to B$ from $\mathrm{\Delta }$, where $A\to B$ is obtained by modus ponens applied to $B$ and the axiom $B\to (A\to B)$. So $\mathrm{\Delta }{⊢}_{i}A\to B$.

• Now, suppose that

  $$A_1,\mathrm{\dots },A_n$$

  is a deduction of $B$ from $\mathrm{\Delta }\cup \{A\}$, with $B$ obtained from earlier formulas by modus ponens.

  We use induction on the length $n$ of deduction of $B$. Note that $n\ge 3$. If $n=3$, then $C$ and $C\to B$ are either axioms or in $\mathrm{\Delta }\cup \{A\}$.

  • If $C$ is $A$, then $C\to B$ is either an axiom or in $\mathrm{\Delta }$. So $\mathrm{\Delta }{⊢}_{i}A\to B$.

  • If $C\to B$ is $A$, then $C$ is either an axiom or in $\mathrm{\Delta }$. Then

    ${ℰ}_0,C\to (A\to C),C,A\to C,(A\to C)\to ((A\to (C\to B))\to (A\to B)),$

    $(A\to (C\to B))\to (A\to B),A\to B$

    is a deduction of $A\to B$ from $\mathrm{\Delta }$, where ${ℰ}_0$ is a deduction of the theorem $A\to A$, followed by an axiom instance, then $C$, 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 $(A\to A)\to (A\to B)$.

  • If $C$ and $C\to B$ are axioms or in $\mathrm{\Delta }$, then $\mathrm{\Delta }{⊢}_{i}A\to B$ based on the deduction $C,C\to B,B,B\to (A\to B),A\to B$.

  Next, assume there is a deduction $ℰ$ of $B$ of length $n>3$. So one of the earlier formulas is $A_k\to B$, and a subsequence of $ℰ$ is a deduction of $A_k\to B$, which has length less than $n$, and therefore by induction, $\mathrm{\Delta }{⊢}_{i}A\to (A_k\to B)$. Likewise, a subsequence of $ℰ$ is a deduction of $A_k$, so by induction, $\mathrm{\Delta }{⊢}_{i}A\to A_k$. With the axiom instance $(A\to A_k)\to ((A\to (A_k\to B))\to (A\to B))$, and two applications of modus ponens, we get $\mathrm{\Delta }{⊢}_{i}A\to B$ as required.

In both cases, $\mathrm{\Delta }{⊢}_{i}A\to B$, 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.

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