You are here
Homededuction theorem holds for intuitionistic propositional logic
Primary tabs
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.
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$.
The proof is very similar to that of the classical propositional logic, given here, 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 $\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. ∎
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)
Mathematics Subject Classification
03F55 no label found03B20 no label found Forums
 Planetary Bugs
 HS/Secondary
 University/Tertiary
 Graduate/Advanced
 Industry/Practice
 Research Topics
 LaTeX help
 Math Comptetitions
 Math History
 Math Humor
 PlanetMath Comments
 PlanetMath System Updates and News
 PlanetMath help
 PlanetMath.ORG
 Strategic Communications Development
 The Math Pub
 Testing messages (ignore)
 Other useful stuff
 Corrections