nLab intuitionistic logic

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 ($\vdash A \vee \neg{A}$) or the double-negation rule ($\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 \vee (\not P)$ (which may superficially/classically seem tautologous) one must prove $P$ or one must prove $\not P$ — but neither proof may be known (e.g. if $P$ = 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 $P$ is provable in classical logic precisely if its double negation $\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 $\vdash A \vee B$ must contain a proof of either $\vdash A$ or $\vdash B$, and similarly any proof of $\vdash \exists x.\,F(x)$ must construct a term $t$ and a proof of $\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 $\Pi^0_1$ formulas; that is, formulas of the form $\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

• various omniscience principles such as LPO and LLPO
• the double-negation shift
• de Morgan's law, i.e. weak excluded middle
• the world's simplest axiom of choice?

Related concepts

• BHK interpretation

category	functor	internal logic	theory	hyperdoctrine	subobject poset	coverage	classifying topos
finitely complete category	cartesian functor	cartesian logic	essentially algebraic theory
lextensive category		disjunctive logic
regular category	regular functor	regular logic	regular theory	regular hyperdoctrine	infimum-semilattice	regular coverage	regular topos
coherent category	coherent functor	coherent logic	coherent theory	coherent hyperdoctrine	distributive lattice	coherent coverage	coherent topos
geometric category	geometric functor	geometric logic	geometric theory	geometric hyperdoctrine	frame	geometric coverage	Grothendieck topos
Heyting category	Heyting functor	intuitionistic first-order logic	intuitionistic first-order theory	first-order hyperdoctrine	Heyting algebra
De Morgan Heyting category		intuitionistic first-order logic with weak excluded middle			De Morgan Heyting algebra
Boolean category		classical first-order logic	classical first-order theory	Boolean hyperdoctrine	Boolean algebra
star-autonomous category		multiplicative classical linear logic
symmetric monoidal closed category		multiplicative intuitionistic linear logic
cartesian monoidal category		fragment $\{\&, \top\}$ of linear logic
cocartesian monoidal category		fragment $\{\oplus, 0\}$ of linear logic
cartesian closed category		simply typed lambda calculus

References

Original articles on intuitionism:

• Arend Heyting, Die formalen Regeln der intuitionistischen Logik. I, II, III. Sitzungsberichte der Preußischen Akademie der Wissenschaften, Physikalisch-Mathematische Klasse (1930) 42-56, 57-71, 158-169

  abridged reprint in:

  Karel Berka, Lothar Kreiser (eds.), Logik-Texte, De Gruyter (1986) 188-192 [doi:10.1515/9783112645826]

• Arend Heyting, Die intuitionistische Grundlegung der Mathematik, Erkenntnis 2 (1931) 106-115 [jsotr:20011630, pdf]

• Andrey Kolmogorov, Zur Deutung der intuitionistischen Logik, Math. Z. 35 (1932) 58-65 [doi:10.1007/BF01186549]

• Hans Freudenthal, Zur intuitionistischen Deutung logischer Formeln, Comp. Math. 4 (1937) 112-116 [numdam:CM_1937__4__112_0]

• Arend Heyting, Bemerkungen zu dem Aufsatz von Herrn Freudenthal “Zur intuitionistischen Deutung logischer Formeln”, Comp. Math. 4 (1937) 117-118 [doi:CM_1937__4__117_0]

• L. E. J. Brouwer, Points and Spaces, Canadian Journal of Mathematics 6 (1954) 1-17 [doi:10.4153/CJM-1954-001-9]

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:

• Anne Sjerp Troelstra, On the Early History of Intuitionistic Logic, in Mathematical Logic, Springer, (1990) [doi:10.1007/978-1-4613-0609-2_1]

Recognizable statemens of the BHK interpretation of intuitionistic logic appear in

• Kolmogorov (1932, p. 59)

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

• Heyting (1956, §7.1.1)

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

and then in

• Anne Sjerp Troelstra, §2 of: Principles of Intuitionism, Lecture Notes in Mathematics 95 Springer Heidelberg (1969) [doi:10.1007/BFb0080643]

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

• Anne Sjerp Troelstra, §2 of: Aspects of Constructive Mathematics, Studies in Logic and the Foundations of Mathematics 90 973-1052 (1977) [doi:10.1016/S0049-237X(08)71127-3]

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

and then in the context of intuitionistic type theory:

• Jean-Yves Girard (translated and with appendiced by Paul Taylor and Yves Lafont), §1.2.2 of: Proofs and Types, Cambridge University Press (1989) [ISBN:978-0-521-37181-0, webpage, pdf]

(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:

• Douglas Bridges, p. 96 of: Constructive mathematics: a foundation for computable analysis, Theoretical Computer Science 219 1–2 (1999) 95-109 [doi:10.1016/S0304-3975(98)00285-0]

See also:

• Wikipedia, Intuitionistic logic

• Stanford Encyclopedia, The Development of Intuitionistic Logic

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

• Robert Harper, Practical Foundations for Programming Languages