basic constructions:
strong axioms
further
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.
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.
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).
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.
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.
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
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:
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:
and recalled in the context of constructive analysis:
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
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.