axiom system for intuitionistic propositional logic
There are several Hilbertstyle 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 $. Wellformed 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}{\u22a2}_{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 ${\u22a2}_{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 wellknown 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{\u22a2}_{i}B\wedge A$, and therefore ${\u22a2}_{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 ${\u22a2}_{i}X$ implies ${\u22a2}_{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 ${\u22a2}_{c}X$ and ${\u22a2\u0338}_{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 $\u27c2$ (for falsity) instead of $\mathrm{\neg}$. The wff’s in this language consists of all propositional letters, the symbol $\u27c2$, 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.
$\u27c2\to A$.
$\mathrm{\neg}A$ is the abbreviation for $A\to \u27c2$. The only rule of inference is modus ponens. Deductions and theorems are defined in the exact same way as above. Let us write ${\u22a2}_{i1}A$ to mean wff $A$ is a theorem in this axiom system. As mentioned, both axiom systems are equivalent^{}, in that ${\u22a2}_{i1}A$ implies ${\u22a2}_{i}A$, and ${\u22a2}_{i}A$ implies ${\u22a2}_{i1}{A}^{*}$, where ${A}^{*}$ is the wff obtained from $A$ by replacing every occurrence of $\u27c2$ 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  20130322 19:30:58 
Last modified on  20130322 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 