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

–
If $C\to B$ is $A$, then $C$ is either an axiom or in $\mathrm{\Delta}$. Then
${\mathcal{E}}_{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 ${\mathcal{E}}_{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}{\u22a2}_{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 $\mathcal{E}$ of $B$ of length $n>3$. So one of the earlier formulas is ${A}_{k}\to B$, and a subsequence^{} of $\mathcal{E}$ is a deduction of ${A}_{k}\to B$, which has length less than $n$, and therefore by induction, $\mathrm{\Delta}{\u22a2}_{i}A\to ({A}_{k}\to B)$. Likewise, a subsequence of $\mathcal{E}$ is a deduction of ${A}_{k}$, so by induction, $\mathrm{\Delta}{\u22a2}_{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}{\u22a2}_{i}A\to B$ as required.

–
In both cases, $\mathrm{\Delta}{\u22a2}_{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.
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  20130322 19:31:32 
Last modified on  20130322 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 