The BHK interpretation of intuitionistic logic articulates the sense in which intuitionistic logic captures constructive reasoning. Statements that involve logical connectives are interpreted as constructions that transform proofs of simpler statements into proofs of more complicated statements. The interpretation requires a primitive notion of what it means to give a construction function that turn objects and proofs into another proof.
Generally, the BHK interpretation is invoked as a piece of metamathematical reasoning, with the actual definition of a constructive function left to the particular theory under development. This puzzled me, since there is a natural notion of construction: one given by an arbitrary Turing machine. At first, I chalked it up to a philosophical unwillingness to accept the Church-Turing thesis, but I think I’ve identified the real problem: it doesn’t work.
For the BHK interpretation to work, Turing machines that represent constructions must be total functions. Worse, to satisfy the philosophical aim of constructivism, they must be provably total in a constructive system. But a simple diagonal argument shows that there exists total functions that are not provably total in any constructive system since we would expect the valid proofs in such a system to be recursively enumerable. You can simply identify constructions with those provably total in a specific system, but philosophically the diagonal argument is constructively valid: given any recursively enumerable axiomatization of valid constructions, I can give you an explicit construction that is different from every element of that enumeration, and for any given element an explicit proof that it’s different.
The way this issue is handled in the realizability interpretation (and therefore the effective topos) is by identifying the constructions as those functions that are provably total in Heyting arithmetic, the intuitionistic analogue of Peano arithmetic.
