# 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,\ldots$, and symbols for logical connectives $\to$, $\land$, $\lor$. Well-formed formulas (wff) are defined recursively as follows:

• propositional letters are wff

• if $A,B$ are wff, so are $A\to B$, $A\land B$, $A\lor B$, and $\neg A$.

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

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

1. 1.

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

2. 2.

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

3. 3.

$A\land B\to A$.

4. 4.

$A\land B\to B$.

5. 5.

$A\to A\lor B$.

6. 6.

$B\to A\lor B$.

7. 7.

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

8. 8.

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

9. 9.

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

10. 10.

$\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 $\Sigma$ of wff’s, a deduction   of a wff $A$ from $\Sigma$ is a finite sequence  of wff’s $A_{1},\ldots,A_{n}$ such that $A_{n}$ is $A$, and $A_{i}$ is either an axiom, a wff in $\Sigma$, or is obtained by an application of modus ponens on $A_{j}$ to $A_{k}$ where $j,k. In other words, $A_{k}$ is the wff $A_{j}\to A_{i}$. We write

 $\Sigma\vdash_{i}A$

to mean that $A$ is a deduction from $\Sigma$. When $\Sigma$ is the empty set  , we say that $A$ is a theorem (of PL${}_{i}$), and simply write $\vdash_{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. 1.

$A\land B\to B\land A$.

2. 2.

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

3. 3.

$A\land\neg A\to B$

4. 4.

$A\to\neg\neg A$

5. 5.

$\neg\neg\neg A\to\neg A$

6. 6.

$(A\to B)\to(\neg B\to\neg A)$

7. 7.

$\neg A\land\neg A$

8. 8.

$\neg\neg(A\lor\neg A)$

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

###### Proof.

From the deduction,

1. 1.

$A\land B\to A$,

2. 2.

$A\land B\to B$,

3. 3.

$A\land B$,

4. 4.

$A$,

5. 5.

$B$,

6. 6.

$B\to(A\to B\land A)$,

7. 7.

$A\to B\land A$,

8. 8.

$B\land A$,

we have $A\land B\vdash_{i}B\land A$, and therefore $\vdash_{i}(A\land B)\to(B\land 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 $\vdash_{i}X$ implies $\vdash_{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. 1.

$A\lor\neg A$.

2. 2.

$\neg\neg A\to A$

3. 3.

$(\neg A\to\neg B)\to(B\to A)$

4. 4.

$((A\to B)\to A)\to A$

5. 5.

$(\neg A\to B)\to((\neg A\to\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 $\vdash_{c}X$ and $\not\vdash_{i}X$. However, this condition is not sufficient to imply the equation, even if PL${}_{i}+X$ is consistent (that is, the schema $C\land\neg C$ of wff’s are not theorems). One such schema is $\neg\neg A\lor\neg A$. A logical system PL such that PL${}_{i}\leq$ PL $\leq$ 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 $\perp$ (for falsity) instead of $\neg$. The wff’s in this language consists of all propositional letters, the symbol $\perp$, and $A\land B$, $A\lor 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. 1.

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

2. 2.

$\perp\to A$.

$\neg A$ is the abbreviation for $A\to\perp$. The only rule of inference is modus ponens. Deductions and theorems are defined in the exact same way as above. Let us write $\vdash_{i1}A$ to mean wff $A$ is a theorem in this axiom system. As mentioned, both axiom systems are equivalent     , in that $\vdash_{i1}A$ implies $\vdash_{i}A$, and $\vdash_{i}A$ implies $\vdash_{i1}A^{*}$, where $A^{*}$ is the wff obtained from $A$ by replacing every occurrence of $\perp$ by the wff $(p\land\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