natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
In constructive mathematics (originally: intuitionistic logic), the BHK interpretation of logical connectives (due to Kolmogorov (1932, p. 59), Troelstra (1969, §2), see the comments on attribution below) 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 there).
This constructive interpretation of logical truth is the crux of the rejection of the principle of excluded middle in intuitionism/constructive mathematics, 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.)
In short this means that a proposition is regarded a true if there is an algorithm, hence a computable function, to realize its proof whence one also speaks of the realizability interpretation.
Closely related to the point of being synonymous is the paradigm of propositions as types and proofs as programs, also known as the Curry-Howard correspondence in type theory.
Indeed, the fully formal version of the BHK interpretation may be understood as being the inference rules, specifically the term introduction rules, of intuitionistic type theory (as amplified in Girard (1989, §2) and Martin-Löf (1996, Lec 3)).
The BHK interpretation evolved from a rather informal statement in Kolmogorov (1932, p. 59), over a more pronounced but still informal statement due to Troelstra (1969, p. 5), to the modern inference rules in intuitionistic type theory due to Martin-Löf 75 (gentle exposition in Martin-Löf (1996, Lec 3)):
From Kolmogorov (1932, p. 59):
From Heyting (1956, p. 97):
From Troelstra (1969, p. 5):
From Troelstra (1977, p. 977):
From Troelstra & van Dalen (1988):
From Bridges (1999), p. 96:
The analogous discussion for inference rules in intuitionistic type theory is then given in Martin-Löf (1975), reviewed in Girard (1989, §2) and with more emphasis in Martin-Löf (1996, Lec 3).
The idea of the interpretation is clearly expressed in Kolmogorov (1932, p. 59), though rather briefly and in unusual terminology: Instead of propositions, Kolmogorov speaks of Aufgaben (Deutsch for “tasks”, but here in the sense used in math classes where it means “exercises” or “mathematical problems”) in order to amplify the constructive aspects (he expands it out to Konstruktionsaufgabe, meaning “construction task”).
While Arend Heyting may have been speaking of the idea of the “proof interpretation” of propositions since the 1930s, the first recognizable statement of what later was called the BHK interpretation is given in Heyting (1956, §7.1.1).
The statement of the interpretation close to its modern formulation (but clearly of the same conceptual content as previously expressed in Kolmogorov (1932, p. 59) and Heyting (1956, §7.1.1)) was then made explicit in Troelstra (1969, §2), where it is not attributed to anyone but presented as if the author’s invention.
Later, Troelstra (1977, §2) credits the idea to “Brouwer-Heyting-Kreisel (BHK)”, not mentioning Kolmogorov — indeed Kreisel (1965) is the only reference that Troelstra (1969, §2) makes explicit use of. (While this is the origin of the term “BHK interpretation”, the adjustment/correction of its expanded version by exchanging “Kreisel” for “Kolmogorov” seems to be due to Troelstra (1990, §2.1).)
Still later, Girard (1989, §1.2.2) presents the same idea as “Heyting’s semantics” (not mentioning anyone else, nor actually citing Heyting).
More discussion of this history is in SEP: “The Development of Intuitionistic Logic”.
Notice that Brouwer never explicitly formulated any interpretation of the kind that Troelstra (1977, §2) attributes to him, and in fact remained against all formalism his entire life. (His role in this history is to provide motivation and inspiration for Heyting and Kolmogorov.) Moreover, Escardo & Xu (2015) have shown that Brouwer’s famous intuitionistic theorem “all functions $\mathbb{N}^{\mathbb{N}} \to \mathbb{N}$ are continuous” is actually inconsistent under a literal version of this interpretation (i.e. without including propositional truncation).
Thus, perhaps it should be called the “Heyting-Kolmogorov” interpretation.
Original articles on intuitionism and, eventually, on intuitionistic logic:
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
Anne Sjerp Troelstra, Dirk van Dalen, Section 3.1 of: Constructivism in Mathematics – An introduction, Vol 1, Studies in Logic and the Foundations of Mathematics 121, North Holland (1988) [ISBN:9780444702661]
Early historical review:
Recognizable formulation of the so-called “BHK interretation” first appears 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
(where it is presented as if the author’s invention) and then recalled in
(where the same is now called the “Brouwer-Heyting-Kreisel (BHK) explanation” — not mentioning Kolmogorov).
and later recalled in the context of constructive analysis:
This lead to the formulation of intuitionistic type theory in
reviewed in
(where it is called Heyting semantics) and then in
See also:
Wikipedia, BHK interpretation
Stanford Encyclopedia of Philosophy, The Development of Intuitionistic Logic
Wouter Pieter Stekelenburg, Realizability Categories, (arXiv:1301.2134).
Martin Escardo, Chuangjie Xu, The inconsistency of a Brouwerian continuity principle with the Curry–Howard interpretation, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), Leibniz International Proceedings in Informatics (LIPIcs) 38 (2015) [doi:10.4230/LIPIcs.TLCA.2015.153, pdf]
E. G. F. Díez, Five observations concerning the intended meaning of the intuitionistic logical constants , J. Phil. Logic 29 no. 4 (2000) pp.409–424 . (preprint)
Links to many papers on realizability and related topics may be found here.
For a comment see also
Last revised on March 6, 2023 at 05:25:46. See the history of this page for a list of all contributions to it.