You are here
Homeintuitionistic propositional logic is a subsystem of classical propositional logic
Primary tabs
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}\leq$ PL${}_{c}$ to mean that PL${}_{i}$ is a subsystem of PL${}_{c}$, or $<$ if it is proper.
Proposition 1.
PL${}_{i}<$ PL${}_{c}$.
Unless otherwise specified, $\vdash A$ means the wff $A$ is a theorem of PL${}_{c}$.
Before proving this, we need the following facts about PL${}_{c}$:
Proof.
Fact 4 is equivalent to $\vdash(A\to B)\to((\neg A\to B)\to B)$ by the deduction theorem twice. Use the theorem schemas $\vdash(A\to B)\leftrightarrow(\neg B\to\neg A)$ and $\vdash A\leftrightarrow\neg\neg A$ (law of double negation), and the substitution theorem twice, it is enough to show
$\vdash(\neg B\to\neg A)\to((\neg B\to A)\to\neg\neg B).$ 
By the deduction theorem three times, it is enough to show $\neg B\to\neg A,\neg B\to A,\neg B\vdash\perp$, which is provided by the deduction $\neg B\to\neg A,\neg B\to A,\neg B,\neg A,A,\perp$.
For the last fact, given deduction $\mathcal{E}_{1}$ of $A$ from $\Delta$, and deduction $\mathcal{E}_{2}$ of $A\to B$ from $\Gamma$, $\mathcal{E}_{1},\mathcal{E}_{2},B$ is a deduction of $B$ from $\Delta\cup\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 $\vdash A$ and $\vdash A\to B$, then $\vdash B$), 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\land B)$.
$A,B,A\to\neg B,\neg B,\perp$ leads to $A,B,A\to\neg B\vdash\perp$. Applying the deduction theorem three times, we get $\vdash A\to(B\to((A\to\neg B)\to\perp))$, or $\vdash A\to(B\to A\land B)$.
3. $A\land B\to A$ and $A\land B\to B$. See here.
4. $A\to A\lor B$.
$A,\neg A,\perp,\perp\to B,B$ results in $A,\neg A\vdash B$, since $\perp\to B$ is a theorem. By applying the deduction theorem twice, we get $\vdash A\to(\neg A\to B)$, or $\vdash A\to A\lor B$.
5. $B\to A\lor B$.
Clearly, $B,\neg A\vdash B$. By the deduction theorem, $B\vdash\neg A\to B$, or $B\vdash A\lor B$. By the deduction theorem again, $\vdash B\to A\lor B$.
6. $(A\to C)\to((B\to C)\to(A\lor B\to C))$.
By fact 3, $A\to C,B\to C,\neg A\to B\vdash\neg A\to C$. With fact 4: $A\to C,\neg A\to C\vdash C$, so $A\to C,B\to C,\neg A\to B\vdash C$ 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\vdash C$. Applying the deduction theorem three times, we have the result.
8. $(A\to B)\to((A\to\neg B)\to\neg A)$. This is just 7, where $C$ is $\perp$.
9. $\neg A\to(A\to B)$.
From $\neg A,A\vdash\perp$ and $\perp\vdash B$, we get $\neg A,A\vdash B$ by fact 5, and the result follows with two applications of the deduction theorem.
Since $A\lor\neg A$ is a theorem of PL${}_{c}$ and not of PL${}_{i}$ (see here), we conclude that PL${}_{i}$ is a proper subsystem of PL${}_{c}$. ∎
Remarks.
1. Strictly speaking, the language $L_{i}$ of PL${}_{i}$ under this system is different from the language $L_{c}$ of PL${}_{c}$ under this system. In $L_{i}$, the logical connectives consist of $\to$, $\neg$, $\land$, $\lor$, whereas in $L_{c}$, only $\to$ is used. The other connectives are introduced as abbreviational devices: $\neg A$ is $A\to\perp$, $A\lor B$ is $\neg A\to B$, and $A\land B$ is $\neg(A\to\neg B)$. So it doesn’t make much sense to say that PL${}_{i}<$ 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 $\vdash_{i}A$ implies $\vdash_{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 $\not\vdash_{i}B$ and $\vdash_{c}\tau(B)$.

3. Using this definition, define $\tau:L_{i}\to L_{c}$ by
$\tau(A):=\left\{\begin{array}[]{ll}A&\textrm{if $A$ is a propositional % variable}\\ \tau(B)\to\tau(C)&\textrm{if $A$ is $B\to C$}\\ \neg\tau(B)&\textrm{if $A$ is $\neg B$}\\ \tau(B)\land\tau(C)&\textrm{if $A$ is $B\land C$}\\ \tau(B)\lor\tau(C)&\textrm{if $A$ is $B\lor C$.}\end{array}\right.$ where the symbols $\neg$, $\land$, and $\lor$ 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$, $\neg$, $\land$, and $\lor$ as primitive logical connectives. Such an axiom system exists. In fact, add $\neg\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}$,
$\vdash_{c}A\qquad\mbox{iff}\qquad\vdash_{i}\nu(A).$
Mathematics Subject Classification
03B20 no label found03F55 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