Intuitionistic Logic

The proof theories of propositional calculus and first-order logic are often referred to as classical logic.

Intuitionistic propositional logic can be described as classical propositional calculus in which the axiom schema

(1)

is replaced by

(2)

Similarly, intuitionistic predicate logic is intuitionistic propositional logic combined with classical first-order predicate calculus.

Intuitionistic logic is a part of classical logic, that is, all formulas provable in intuitionistic logic are also provable in classical logic. Although, even some basic theorems of classical logic do not hold in intuitionistic logic. Of course, the law of the excluded middle

(3)

does not hold in intuitionistic propositional logic.

Here are some examples of propositional formulas that are not provable in intuitionistic propositional logic:

(4)

(5)

Here are some examples of first-order formulas that are not provable in intuitionistic predicate logic:

(6)

(7)

Truth tables for propositional connectives define the interpretation of classical propositional calculus over the domain of two elements: true and false. This interpretation is a model of classical propositional calculus, that is, tautologies and only tautologies are formal theorems. In contrast, intuitionistic propositional calculus does not have a finite model but it has countable models.

Proofs by contradiction are not permissible in intuitionistic logic. All intuitionistic proofs are constructive, which is justified by the following properties. Intuitionistic propositional logic has the disjunction property: If is provable in intuitionistic propositional calculus, then either or is provable in intuitionistic propositional calculus. Intuitionistic predicate logic has the existence property: If is a formula without free variables, and it is provable in intuitionistic predicate logic, then there is term without free variables such that is provable in intuitionistic predicate logic.

The deduction theorem holds in intuitionistic propositional and predicate logics. The following theorem by Glivenko captures the essence of relation between intuitionistic and classical logics: If is provable in classical propositional calculus, then is provable in intuitionistic propositional calculus. Note that this theorem cannot be extended onto intuitionistic predicate logic.