You are here
Homeaxiom system for intuitionistic propositional logic
Primary tabs
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. 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$. Wellformed 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. $A\to(B\to A)$.
2. $A\to(B\to A\land B)$.
3. $A\land B\to A$.
4. $A\land B\to B$.
5. $A\to A\lor B$.
6. $B\to A\lor B$.
7. $(A\to C)\to((B\to C)\to(A\lor B\to C))$.
8. $(A\to B)\to((A\to(B\to C))\to(A\to C))$.
9. $(A\to B)\to((A\to\neg B)\to\neg A)$.
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<i$. 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 wellknown theorem schemas listed below:
1. $A\land B\to B\land A$.
2. $(A\to(B\to C))\to((A\to B)\to(A\to C))$
3. $A\land\neg A\to B$
4. $A\to\neg\neg A$
5. $\neg\neg\neg A\to\neg A$
6. $(A\to B)\to(\neg B\to\neg A)$
7. $\neg A\land\neg A$
8. $\neg\neg(A\lor\neg A)$
For example, the first schema can be proved as follows:
Proof.
From the deduction,
1. $A\land B\to A$,
2. $A\land B\to B$,
3. $A\land B$,
4. $A$,
5. $B$,
6. $B\to(A\to B\land A)$,
7. $A\to B\land A$,
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. 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. $A\lor\neg A$.
2. $\neg\neg A\to A$
3. $(\neg A\to\neg B)\to(B\to A)$
4. $((A\to B)\to A)\to A$
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. $(A\to(B\to C))\to((A\to B)\to(A\to C))$ (the second theorem schema above)
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$.
Mathematics Subject Classification
03F55 no label found03B20 no label found03B55 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