intuitionistic propositional logic is a subsystem of classical propositional logic
Suppose logical systems ${\mathcal{L}}_{1}$ and ${\mathcal{L}}_{2}$ share the same set $L$ of wellformed formulas (wff’s). Let ${F}_{1}$ be the set of all theorems^{} of ${\mathcal{L}}_{1}$, and ${F}_{2}$ the set of all theorems of ${\mathcal{L}}_{2}$. We say that ${\mathcal{L}}_{1}$ is a subsystem of ${\mathcal{L}}_{2}$ if ${F}_{1}\subseteq {F}_{2}$, and a proper subsystem if ${F}_{1}\subset {F}_{2}$.
In the subsequent discussion, PL${}_{c}$ stands for classical propositional logic^{}, and PL${}_{i}$ for intuitionistic propositional logic. We write PL${}_{i}\le $ PL${}_{c}$ to mean that PL${}_{i}$ is a subsystem of PL${}_{c}$, or $$ if it is proper.
Proposition 1.
PL$$ PL${}_{c}$.
Unless otherwise specified, $\u22a2A$ means the wff $A$ is a theorem of PL${}_{c}$.
Before proving this, we need the following facts about PL${}_{c}$:

1.
$\u22a2A$ and $\u22a2B$ iff $\u22a2A\wedge B$.

2.
$\u22a2A$ implies $\u22a2B$ iff $\u22a2A\to B$.

3.
$A\to B,B\to C\u22a2A\to C$

4.
$A\to B,\mathrm{\neg}A\to B\u22a2B$

5.
if $\mathrm{\Delta}\u22a2A$ and $\mathrm{\Gamma},A\u22a2B$, then $\mathrm{\Delta},\mathrm{\Gamma}\u22a2B$.
Proof.
The first two facts are proved http://planetmath.org/node/12533here, and the third is http://planetmath.org/node/12561here.
Fact 4 is equivalent^{} to $\u22a2(A\to B)\to ((\mathrm{\neg}A\to B)\to B)$ by the deduction theorem^{} twice. Use the theorem schemas $\u22a2(A\to B)\leftrightarrow (\mathrm{\neg}B\to \mathrm{\neg}A)$ and $\u22a2A\leftrightarrow \mathrm{\neg}\mathrm{\neg}A$ (law of double negation), and the substitution theorem twice, it is enough to show
$$\u22a2(\mathrm{\neg}B\to \mathrm{\neg}A)\to ((\mathrm{\neg}B\to A)\to \mathrm{\neg}\mathrm{\neg}B).$$ 
By the deduction theorem three times, it is enough to show $\mathrm{\neg}B\to \mathrm{\neg}A,\mathrm{\neg}B\to A,\mathrm{\neg}B\u22a2\u27c2$, which is provided by the deduction^{} $\mathrm{\neg}B\to \mathrm{\neg}A,\mathrm{\neg}B\to A,\mathrm{\neg}B,\mathrm{\neg}A,A,\u27c2$.
For the last fact, given deduction ${\mathcal{E}}_{1}$ of $A$ from $\mathrm{\Delta}$, and deduction ${\mathcal{E}}_{2}$ of $A\to B$ from $\mathrm{\Gamma}$, ${\mathcal{E}}_{1},{\mathcal{E}}_{2},B$ is a deduction of $B$ from $\mathrm{\Delta}\cup \mathrm{\Gamma}$. ∎
Proof.
Since in both systems, the only inference rule is modus ponens^{}, and theoremhood of wff’s is preserved by the inference rule (that is, if $\u22a2A$ and $\u22a2A\to B$, then $\u22a2B$), all we need to show is that every axiom of PL${}_{i}$ is a theorem of PL${}_{c}$.

1.
$A\to (B\to A)$. This is just an axiom schema^{} for PL${}_{c}$.

2.
$A\to (B\to A\wedge B)$.
$A,B,A\to \mathrm{\neg}B,\mathrm{\neg}B,\u27c2$ leads to $A,B,A\to \mathrm{\neg}B\u22a2\u27c2$. Applying the deduction theorem three times, we get $\u22a2A\to (B\to ((A\to \mathrm{\neg}B)\to \u27c2))$, or $\u22a2A\to (B\to A\wedge B)$.

3.
$A\wedge B\to A$ and $A\wedge B\to B$. See http://planetmath.org/node/12533here.

4.
$A\to A\vee B$.
$A,\mathrm{\neg}A,\u27c2,\u27c2\to B,B$ results in $A,\mathrm{\neg}A\u22a2B$, since $\u27c2\to B$ is a theorem. By applying the deduction theorem twice, we get $\u22a2A\to (\mathrm{\neg}A\to B)$, or $\u22a2A\to A\vee B$.

5.
$B\to A\vee B$.
Clearly, $B,\mathrm{\neg}A\u22a2B$. By the deduction theorem, $B\u22a2\mathrm{\neg}A\to B$, or $B\u22a2A\vee B$. By the deduction theorem again, $\u22a2B\to A\vee B$.

6.
$(A\to C)\to ((B\to C)\to (A\vee B\to C))$.
By fact 3, $A\to C,B\to C,\mathrm{\neg}A\to B\u22a2\mathrm{\neg}A\to C$. With fact 4: $A\to C,\mathrm{\neg}A\to C\u22a2C$, so $A\to C,B\to C,\mathrm{\neg}A\to B\u22a2C$ by fact 5. Now apply the deduction theorem 3 times.

7.
$(A\to B)\to ((A\to (B\to C))\to (A\to C))$.
From $A\to B,A\to (B\to C),A,B\to C,B,C$, we get $A\to B,A\to (B\to C),A\u22a2C$. Applying the deduction theorem three times, we have the result.

8.
$(A\to B)\to ((A\to \mathrm{\neg}B)\to \mathrm{\neg}A)$. This is just 7, where $C$ is $\u27c2$.

9.
$\mathrm{\neg}A\to (A\to B)$.
From $\mathrm{\neg}A,A\u22a2\u27c2$ and $\u27c2\u22a2B$, we get $\mathrm{\neg}A,A\u22a2B$ by fact 5, and the result follows with two applications of the deduction theorem.
Since $A\vee \mathrm{\neg}A$ is a theorem of PL${}_{c}$ and not of PL${}_{i}$ (see http://planetmath.org/node/12493here), we conclude that PL${}_{i}$ is a proper subsystem of PL${}_{c}$. ∎
Remarks.

1.
Strictly speaking, the language^{} ${L}_{i}$ of PL${}_{i}$ under http://planetmath.org/node/12491this system is different from the language ${L}_{c}$ of PL${}_{c}$ under http://planetmath.org/node/12507this system. In ${L}_{i}$, the logical connectives consist of $\to $, $\mathrm{\neg}$, $\wedge $, $\vee $, whereas in ${L}_{c}$, only $\to $ is used. The other connectives are introduced as abbreviational devices: $\mathrm{\neg}A$ is $A\to \u27c2$, $A\vee B$ is $\mathrm{\neg}A\to B$, and $A\wedge B$ is $\mathrm{\neg}(A\to \mathrm{\neg}B)$. So it doesn’t make much sense to say that PL$$ PL${}_{c}$.

2.
One way to get around this issue is to redefine what it means for one logical system to be a subsystem of another. For example, one can define a mapping $\tau :{L}_{i}\to {L}_{c}$ such that

–
takes propositional variables to propositional variables

–
$\tau $ preserves the formation rules of wff’s
A mapping satisfying these conditions is called a translation. Then, a system PL${}_{i}$ is a subsystem of PL${}_{c}$ if there is a translation $\tau :{L}_{i}\to {L}_{c}$ such that

–
for any wff $A$ in ${L}_{i}$, we have ${\u22a2}_{i}A$ implies ${\u22a2}_{c}\tau (A)$.
To further require that PL${}_{i}$ be a proper subsystem of PL${}_{c}$, we also need

–
there is an wff $B$ in ${L}_{i}$ such that ${\u22a2\u0338}_{i}B$ and ${\u22a2}_{c}\tau (B)$.

–

3.
Using this definition, define $\tau :{L}_{i}\to {L}_{c}$ by
$$\tau (A):=\{\begin{array}{cc}A\hfill & \text{if}A\text{is a propositional variable}\hfill \\ \tau (B)\to \tau (C)\hfill & \text{if}A\text{is}B\to C\hfill \\ \mathrm{\neg}\tau (B)\hfill & \text{if}A\text{is}\mathrm{\neg}B\hfill \\ \tau (B)\wedge \tau (C)\hfill & \text{if}A\text{is}B\wedge C\hfill \\ \tau (B)\vee \tau (C)\hfill & \text{if}A\text{is}B\vee C\text{.}\hfill \end{array}$$ where the symbols $\mathrm{\neg}$, $\wedge $, and $\vee $ in ${L}_{c}$ are used as abbreviational tools (see the first remark). Then we see that the proposition makes sense.

4.
Another way of getting around this issue is to come up with another axiom system for PL${}_{c}$ that uses $\to $, $\mathrm{\neg}$, $\wedge $, and $\vee $ as primitive logical connectives. Such an axiom system exists. In fact, add $\mathrm{\neg}\mathrm{\neg}A\to A$ to the list of axiom schemas for PL${}_{i}$, and we get an axiom system for PL${}_{c}$.

5.
Using the idea in 2 above further, it can be shown that PL${}_{c}$ is a subsystem of PL${}_{i}$ (under the right translation)! The existence of such a translation $\nu $ is known as the Glivenko’s theorem. This translation $\nu $ has the further property that for any wff $A$ in ${L}_{c}$,
$${\u22a2}_{c}A\mathit{\hspace{1em}\hspace{1em}}\text{iff}\mathit{\hspace{1em}\hspace{1em}}{\u22a2}_{i}\nu (A).$$
Title  intuitionistic propositional logic is a subsystem of classical propositional logic 

Canonical name  IntuitionisticPropositionalLogicIsASubsystemOfClassicalPropositionalLogic 
Date of creation  20130322 19:33:12 
Last modified on  20130322 19:33:12 
Owner  CWoo (3771) 
Last modified by  CWoo (3771) 
Numerical id  31 
Author  CWoo (3771) 
Entry type  Result 
Classification  msc 03B20 
Classification  msc 03F55 