Desktop version

Home arrow Philosophy arrow Advances in Proof-Theoretic Semantics


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 “ab 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 AB, 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
Found a mistake? Please highlight the word and press Shift + Enter  

Related topics