In mathematical logic, the BHK interpretation of intuitionistic predicate logic was proposed by L. E. J. Brouwer, Arend Heyting and independently by Kolmogorov. It is also sometimes called the realizability interpretation, because of the connection with the realizability theory of Stephen Kleene.
The interpretation
A formula is interpreted by induction on the structure of that formula:
- A proof of is a pair <a,b> where a is a proof of P and b is a proof of Q.
- A proof of is a pair <a,b> where a is 0 and b is a proof of P, or a is 1 and b is a proof of Q.
- A proof of is a function f which converts a proof of P into a proof of Q.
- The formula is defined as
- A proof of is a pair <a,b> where a is an element of S, and b is a proof of φ(a).
- A proof of is a function f which converts an element a of S into a proof of φ(a).
The interpretation of a primitive proposition is supposed to be known from context. The interpretation of is taken to be that a proof of is a proof of all primitive propositions (as appropriate for that context), which usually means that there is no proof of at all.
What is a function
The BHK interpretation will depend on the view taken about what constitutes a function which converts one proof to another, or which converts an element of a domain to a proof. Different versions of constructivism will diverge on this point.
Kleene's realizability theory identifies the functions with the recursive functions. It deals with Heyting arithmetic, where the domain of quantification is the natural numbers and the primitive propositions are of the form x=y. A proof of x=y is simply the trivial algorithm if x evaluates to the same number that y does (which is always decidable for natural numbers), otherwise there is no proof. These are then built up by induction into more complex algorithms.
Examples
The identity function is a proof of the formula .
The law of non-contradiction expands to which is then proven by the function .
