# deduction theorem holds for intuitionistic propositional logic

###### Theorem 1.

If $\Delta,A\vdash_{i}B$, where $\Delta$ is a set of wff’s of the intuitionistic propositional logic, then $\Delta\vdash_{i}A\to B$.

###### Proof.

There are two main cases to consider:

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

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

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

• Now, suppose that

 $A_{1},\ldots,A_{n}$

is a deduction of $B$ from $\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\geq 3$. If $n=3$, then $C$ and $C\to B$ are either axioms or in $\Delta\cup\{A\}$.

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

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

 $\displaystyle\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)),$ $\displaystyle(A\to(C\to B))\to(A\to B),A\to B$

is a deduction of $A\to B$ from $\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 $\Delta$, then $\Delta\vdash_{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, $\Delta\vdash_{i}A\to(A_{k}\to B)$. Likewise, a subsequence of $\mathcal{E}$ is a deduction of $A_{k}$, so by induction, $\Delta\vdash_{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 $\Delta\vdash_{i}A\to B$ as required.

In both cases, $\Delta\vdash_{i}A\to B$, and the proof is complete    . ∎

## References

• 1 J. W. Robbin, Mathematical Logic, A First Course, Dover Publication (2006)
Title deduction theorem holds for intuitionistic propositional logic DeductionTheoremHoldsForIntuitionisticPropositionalLogic 2013-03-22 19:31:32 2013-03-22 19:31:32 CWoo (3771) CWoo (3771) 21 CWoo (3771) Theorem msc 03F55 msc 03B20 AxiomSystemForIntuitionisticLogic