axiom system for intuitionistic propositional logic

There are several Hilbert-style axiom systems for intuitionistic propositional logic, or PL${}_i$ for short. One such a system is by Heyting, and is presented in this entry (http://planetmath.org/IntuitionisticLogic). Here, we describe another, based on the one by Kleene. The language of the logic consists of a countably infinite set of propositional letters $p,q,r,\mathrm{\dots }$, and symbols for logical connectives $\to$, $\wedge$, $\vee$. Well-formed formulas (wff) are defined recursively as follows:

• propositional letters are wff

• if $A,B$ are wff, so are $A\to B$, $A\wedge B$, $A\vee B$, and $\mathrm{\neg }A$.

In addition, $A\leftrightarrow B$ (biconditional) is the abbreviation for $(A\to B)\wedge (B\to A)$, like PL${}_c$ (classical propositional logic),

We also use parentheses to avoid ambiguity. The axiom schemas for PL${}_i$ are

1. $A\to (B\to A)$.

2. $A\to (B\to A\wedge B)$.

3. $A\wedge B\to A$.

4. $A\wedge B\to B$.

5. $A\to A\vee B$.

6. $B\to A\vee B$.

7. $(A\to C)\to ((B\to C)\to (A\vee B\to C))$.

8. $(A\to B)\to ((A\to (B\to C))\to (A\to C))$.

9. $(A\to B)\to ((A\to \mathrm{\neg }B)\to \mathrm{\neg }A)$.

10. $\mathrm{\neg }A\to (A\to B)$.

where $A$, $B$, and $C$ are wff’s. In addition, modus ponens is the only rule of inference for PL${}_i$.

As usual, given a set $\mathrm{\Sigma }$ of wff’s, a deduction of a wff $A$ from $\mathrm{\Sigma }$ is a finite sequence of wff’s $A_1,\mathrm{\dots },A_n$ such that $A_n$ is $A$, and $A_i$ is either an axiom, a wff in $\mathrm{\Sigma }$, or is obtained by an application of modus ponens on $A_j$ to $A_k$ where . In other words, $A_k$ is the wff $A_j\to A_i$. We write

$$\mathrm{\Sigma }{⊢}_{i}A$$

to mean that $A$ is a deduction from $\mathrm{\Sigma }$. When $\mathrm{\Sigma }$ is the empty set, we say that $A$ is a theorem (of PL${}_i$), and simply write ${⊢}_{i}A$ to mean that $A$ is a theorem.

As with PL${}_c$, the deduction theorem holds for PL${}_i$. Using the deduction theorem, one can derive the well-known theorem schemas listed below:

1. $A\wedge B\to B\wedge A$.

2. $(A\to (B\to C))\to ((A\to B)\to (A\to C))$

3. $A\wedge \mathrm{\neg }A\to B$

4. $A\to \mathrm{\neg }\mathrm{\neg }A$

5. $\mathrm{\neg }\mathrm{\neg }\mathrm{\neg }A\to \mathrm{\neg }A$

6. $(A\to B)\to (\mathrm{\neg }B\to \mathrm{\neg }A)$

7. $\mathrm{\neg }A\wedge \mathrm{\neg }A$

8. $\mathrm{\neg }\mathrm{\neg }(A\vee \mathrm{\neg }A)$

For example, the first schema can be proved as follows:

Proof.

From the deduction,

1. $A\wedge B\to A$,

2. $A\wedge B\to B$,

3. $A\wedge B$,

4. $A$,

5. $B$,

6. $B\to (A\to B\wedge A)$,

7. $A\to B\wedge A$,

8. $B\wedge A$,

we have $A\wedge B{⊢}_{i}B\wedge A$, and therefore ${⊢}_i(A\wedge B)\to (B\wedge A)$ by the deduction theorem. ∎

Deductions of the other theorem schemas can be found here (http://planetmath.org/SomeTheoremSchemasOfIntuitionisticPropositionalLogic). In fact, it is not hard to see that ${⊢}_{i}X$ implies ${⊢}_{c}X$ (that $X$ is a theorem of PL${}_c$). The converse is false. The following are theorems of PL${}_c$, not PL${}_i$:

1. $A\vee \mathrm{\neg }A$.

2. $\mathrm{\neg }\mathrm{\neg }A\to A$

3. $(\mathrm{\neg }A\to \mathrm{\neg }B)\to (B\to A)$

4. $((A\to B)\to A)\to A$

5. $(\mathrm{\neg }A\to B)\to ((\mathrm{\neg }A\to \mathrm{\neg }B)\to A)$

Remark. It is interesting to note, however, if any one of the above schemas were added to the list of axioms for PL${}_i$, then the resulting system is an axiom system for PL${}_c$. In notation,

PL${}_i+X=$ PL${}_c$,

where $X$ is one of the schemas above. When this equation holds for some $X$, it is necessary that ${⊢}_{c}X$ and ${⊬}_{i}X$. However, this condition is not sufficient to imply the equation, even if PL${}_i+X$ is consistent (that is, the schema $C\wedge \mathrm{\neg }C$ of wff’s are not theorems). One such schema is $\mathrm{\neg }\mathrm{\neg }A\vee \mathrm{\neg }A$. A logical system PL such that PL${}_i\le$ PL $\le$ PL${}_c$ is called an intermediate logic. It can be shown that there are infinitely many such intermediate logics.

Remark. Yet another popular axiom system for PL${}_i$ uses the symbol $⟂$ (for falsity) instead of $\mathrm{\neg }$. The wff’s in this language consists of all propositional letters, the symbol $⟂$, and $A\wedge B$, $A\vee B$, and $A\to B$, whenever $A$ and $B$ are wff’s. The axiom schemas consist of the first seven axiom schemas in the first system above, as well as

1. $(A\to (B\to C))\to ((A\to B)\to (A\to C))$ (the second theorem schema above)

2. $⟂\to A$.

$\mathrm{\neg }A$ is the abbreviation for $A\to ⟂$. The only rule of inference is modus ponens. Deductions and theorems are defined in the exact same way as above. Let us write ${⊢}_{i1}A$ to mean wff $A$ is a theorem in this axiom system. As mentioned, both axiom systems are equivalent, in that ${⊢}_{i1}A$ implies ${⊢}_{i}A$, and ${⊢}_{i}A$ implies ${⊢}_{i1}{A}^{*}$, where $A^{*}$ is the wff obtained from $A$ by replacing every occurrence of $⟂$ by the wff $(p\wedge \mathrm{\neg }p)$, where $p$ is a propositional letter not occurring in $A$.

Title	axiom system for intuitionistic propositional logic
Canonical name	AxiomSystemForIntuitionisticPropositionalLogic
Date of creation	2013-03-22 19:30:58
Last modified on	2013-03-22 19:30:58
Owner	CWoo (3771)
Last modified by	CWoo (3771)
Numerical id	38
Author	CWoo (3771)
Entry type	Axiom
Classification	msc 03F55
Classification	msc 03B20
Classification	msc 03B55
Related topic	TruthValueSemanticsForIntuitionisticPropositionalLogic
Related topic	SomeTheoremSchemasOfIntuitionisticPropositionalLogic
Related topic	KripkeSemanticsForIntuitionisticPropositionalLogic
Related topic	DeductionTheoremForIntuitionisticPropositionalLogic
Related topic	DisjunctionProperty