Home Philosophy Advances in Proof-Theoretic Semantics
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. The so-called BHK-interpretation stated by Troelstra and van Dalen (1988) , which is less developed ontologically, defines recursively “what forms proofs of logically compound statements take in terms of the proofs of the constituents”. 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.