intuitionistic logic



Intuitionistic logic was introduced by Arend Heyting as a logic for Brouwer's intuitionistic mathematics. It applies more generally to constructive mathematics and so may also be called constructive logic.


Intuitionistic logic is most easily described as classical logic without the principle of the excluded middle (A¬A\vdash A \vee \neg{A}) or the double-negation rule (¬¬AA\neg\neg{A} \vdash A). It may also be defined by starting with Gentzen's sequent calculus for classical logic (with ¬\neg but not \bot) and restricting to sequents ΓΔ\Gamma \vdash \Delta where Δ\Delta may contain at most one formula, or by starting with sequent calculus with \bot and restricting to such sequents where Δ\Delta must contain exactly one formula.


Unlike classical logic, intuitionistic logic has the disjunction? and existence? properties: any proof of AB\vdash A \vee B must contain a proof of either A\vdash A or B\vdash B, and similarly any proof of x.F(x)\vdash \exists x.\,F(x) must construct a term tt and a proof of F(t)\vdash F(t). These properties are what justify our calling intuitionistic logic ‘constructive’.

On the other hand, (classical) Peano arithmetic is conservative over (intuitionistic) Heyting arithmetic? when restricted to Π 1 0\Pi^0_1 formulas; that is, formulas of the form x:N.y:N.F(x,y)\forall x\colon N.\, \exists y\colon N.\, F(x,y). Roughly speaking, classical logic can be just as ‘constructive’ as intuitionistic logic as far as proving the totality of functions \mathbb{N} \to \mathbb{N} is concerned.


The observation that the poset of open subsets of a topological space (the internal logic of the sheaf topos) serves as a model for intuitionistic logic is apparently originally due to

  • Alfred Tarski, Der Aussagenkalkül und die Topologie, FundamentaMathemeticae 31 (1938), pp. 103–134.

A textbook account in the context of programming languages is in section 30 of

Revised on December 4, 2012 21:57:02 by Urs Schreiber (