# Heyting's Approach to Meaning

A mathematical proposition expresses according to Heyting the intention of a construction that satisfies certain conditions. He explained the assertion of a proposition to mean that the intended construction had been realized, and a proof of a proposition to consist in the realization of the intended construction (Heyting 1930 [5, pp. 958–959], 1931 [6, p. 247], 1934 [7, p. 14]). Thus, according to this explanation, to assert a proposition is equivalent with declaring that there is proof of the proposition. The notion of proof retains in this way its usual epistemic connotation: to have a proof is exactly what one needs in order to be justified in asserting the proposition.

As an important example, Heyting explained the meaning of implication, saying that “*a* ⊃ *b* means the intention of a construction that takes any proof of *a* to a proof of *b*”.

There are several proposals for how to develop Heyting's ideas more explicitly. One early proposal due to Kreisel (1959, 1962) [10, 11] suggests quite straightforwardly that the constructions intended by implications and universal quantifications are constructive functionals of finite type satisfying the conditions stated by Heyting^{[1]}. The so-called BHK-interpretation stated by Troelstra and van Dalen (1988) [24], which is less developed ontologically, defines recursively “what forms proofs of logically compound statements take in terms of the proofs of the constituents”^{[2]}. What is here called a proof corresponds rather to what Heyting calls an intended construction, but it has become common in intuitionism to speak about proofs in this way, and I shall follow this way of speaking.

For my purpose here it is sufficient to stay roughly at the level of precision of the BHK-interpretation. I assume that we are given a set *P* of proofs of atomic sentences of a first order language and an individual domain *D*. What it is to be a *proof over P* of a closed compound sentence *A* in that language is then defined by recursive clauses like the ones below:

(1) *α* is a proof over *P* of *A* ⊃ *B*, if and only if, *α* is an effective operation such that if *β* is any proof over *P* of *A* then *α(β)* is a proof over *P* of *B*.

(2) *α* is a proof over *P* of ∀*x A(x )*, if and only if, *α* is an effective operation such that for any element *e* in the individual domain *D*, *α(e)* is a proof over *P* of the instance *A(e)*.

Instead of speaking of proofs of open sentences *A(x )* under assignments of individuals to variables, I have here assumed for convenience that each element *e* in the individual domain *D* has a canonical name, and understand by *A(e)* the closed sentence obtained by substituting in *A(x )* this canonical name of *e* for *x* . Furthermore, I assume that if *α* is as stated in clause (2), then there is another effective operation *α*∗, effectively obtained from *α*, such that for any closed term *t* , *α*∗*(t )* is a proof of *A(t )*.

To distinguish proofs defined by recursive clauses of this kind, I shall sometimes refer to them as *BHK-proofs*.

- [1] Kreisel was interested in this interpretation as a technical tool for obtaining certain non-derivability results. For a foundation of intuitionistic logic he suggested another interpretation that took a proof of an implication to consist of a pair
*(α, β)*where*α*is a construction satisfying the condition stated by Heyting and*β*is a proof of the fact that*α*satisfies this condition (Kreisel 1962 [12]) - [2] 3BHK stands here for Brouwer-Heyting-Kolmogorov, but there is also another interpretation stated by Troelstra (1977) [23] that is called the BHK-interpretation, where BHK stands for BrouwerHeyting-Kreisel. It is more akin to Kreisel's second proposal mentioned in footnote 2