# nLab BHK interpretation

Contents

### Context

#### Constructivism, Realizability, Computability

intuitionistic mathematics

# Contents

## Idea

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)).

## Historical versions

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

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.

## References

Original articles on intuitionism and, eventually, on intuitionistic logic:

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:

*

Kolmogorov (1932, p. 59)

(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

• Per Martin-Löf, An intuitionistic theory of types: predicative part, in: H. E. Rose, J. C. Shepherdson (eds.), Logic Colloquium ‘73, Proceedings of the Logic Colloquium, Studies in Logic and the Foundations of Mathematics 80, Elsevier (1975) 73-118 [doi:10.1016/S0049-237X(08)71945-1, CiteSeer]

reviewed in

(where it is called Heyting semantics) and then in

• 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]

• 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.