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 well-formed 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}$ :

1.

$\vdash A$ and $\vdash B$ iff $\vdash A\land B$ .
2.

$\vdash A$ implies $\vdash B$ iff $\vdash A\to B$ .
3.

$A\to B,B\to C\vdash A\to C$
4.

$A\to B,\neg A\to B\vdash B$
5.

if $\Delta\vdash A$ and $\Gamma,A\vdash B$ , then $\Delta,\Gamma\vdash B$ .

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 $\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 http://planetmath.org/node/12533here.
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 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$ , $\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 re-define 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).$

Title	intuitionistic propositional logic is a subsystem of classical propositional logic
Canonical name	IntuitionisticPropositionalLogicIsASubsystemOfClassicalPropositionalLogic
Date of creation	2013-03-22 19:33:12
Last modified on	2013-03-22 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