nLab intuitionistic logic

Contents

Context

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Contents

Idea

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.

Beware the terminological ambiguity: Some people insist that “intuitionistic logic” refers to Brouwerian intuitionism, which includes axioms that contradict classical logic; but other people use “intuitionistic” to mean the same as what in other contexts is called “constructive”, i.e. mathematics without the principle of excluded middle or the axiom of choice but nothing added that contradicts them. Some people (particularly material set theorists) use “constructive” to mean predicative constructive and “intuitionistic” to mean impredicative constructive.

Idea

General

Intuitionistic logic is most easily described as classical logic without the principle of 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.

Constructive interpretation of connectives

The intuitionistic interpretation of the logical connectives (known as the BHK interpretation, due to Kolmogorov (1932, p. 59), Heyting (1956, §7.1.1), Troelstra (1969, §2)) is such that the resulting proposition is regarded as true only if it is possible to construct a proof of its assertion.

For instance, to assert a logical conjunction (“and”) or a universal quantification (“for all”) is taken to mean to provide a proof of all the instances.

Dually but more notably, to assert a logical disjunction (“or”) or an existential quantification (“exists”) is taken to mean to prove one of the instances, so that there is no intuitionistic existence statement without construction of an example (the “disjunction property”, see below).

This constructive interpretation of logical truth is the crux of the rejection of the principle of excluded middle, for it implies that to prove P(¬P)P \vee (\not P) (which may superficially/classically seem tautologous) one must prove PP or one must prove ¬P\not P — but neither proof may be known (e.g. if PP = Riemann hypothesis).

(Here the classical mathematician is regarded as “idealistic” in their assumption that either case must hold, even if it is impossible to tell which one.)

From Kolmogorov (1932, p. 59):

From Heyting (1956, p. 97):

From Troelstra (1969, p. 5):

From Troelstra (1977, p. 977):

From Bridges (1999), p. 96:

The analogous discussion for inference rules in intuitionistic type theory is then given spring in Girard (1989, §2) and with more emphasis in Martin-Löf (1996, Lec 3).

Properties

Double negation

The double negation translation says that a proposition PP is provable in classical logic precisely if its double negation ¬¬P\not \not P is provable in constructive logic.

Disjunction property

Unlike classical logic, intuitionistic logic has the disjunction- and existence properties (cf. above): 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.

Classicality principles

The principle of excluded middle is not provable in intuitionistic logic, and if we assume it then the logic becomes classical logic. But there are other principles that are provable classically but not intuitionistically, but which are weaker than full PEM, such as

categoryfunctorinternal logictheoryhyperdoctrinesubobject posetcoverageclassifying topos
finitely complete categorycartesian functorcartesian logicessentially algebraic theory
lextensive categorydisjunctive logic
regular categoryregular functorregular logicregular theoryregular hyperdoctrineinfimum-semilatticeregular coverageregular topos
coherent categorycoherent functorcoherent logiccoherent theorycoherent hyperdoctrinedistributive latticecoherent coveragecoherent topos
geometric categorygeometric functorgeometric logicgeometric theorygeometric hyperdoctrineframegeometric coverageGrothendieck topos
Heyting categoryHeyting functorintuitionistic first-order logicintuitionistic first-order theoryfirst-order hyperdoctrineHeyting algebra
De Morgan Heyting categoryintuitionistic first-order logic with weak excluded middleDe Morgan Heyting algebra
Boolean categoryclassical first-order logicclassical first-order theoryBoolean hyperdoctrineBoolean algebra
star-autonomous categorymultiplicative classical linear logic
symmetric monoidal closed categorymultiplicative intuitionistic linear logic
cartesian monoidal categoryfragment {&,}\{\&, \top\} of linear logic
cocartesian monoidal categoryfragment {,0}\{\oplus, 0\} of linear logic
cartesian closed categorysimply typed lambda calculus

References

Original articles on intuitionism:

Early monographs:

  • Arend Heyting, Intuitionism: An introduction, Studies in Logic and the Foundations of Mathematics, North-Holland (1956, 1971) [ISBN:978-0720422399]

  • Georg Kreisel, Section 2 of: Mathematical Logic, in T. Saaty et al. (ed.), Lectures on Modern Mathematics III, Wiley New York (1965) 95-195

Early historical account:

Recognizable statemens of the BHK interpretation of intuitionistic logic appear in

(who however speaks not of propositions but of Aufgaben, i.e. “tasks”, here in the sense of: “mathematical problems”)

(who is maybe the first to speak of the “meaning of logical connectives”)

and then in

(where it is presented as the author’s invention) and then in

(where the same is now called the “Brouwer-Heyting-Kreisel explanation”, not mentioning Kolmogorov)

and then in the context of intuitionistic type theory:

(where it is called Heyting semantics), further expanded on on:

  • Per Martin-Löf, Lecture 3 of: On the Meanings of the Logical Constants and the Justifications of the Logical Laws, Nordic Journal of Philosophical Logic, 1 1 (1996) 11-60 [pdf, pdf]

and recalled in the context of constructive analysis:

See also:

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, Fundamenta Mathematicae 31 (1938), pp. 103-134.

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

Last revised on March 6, 2023 at 05:24:51. See the history of this page for a list of all contributions to it.