In mathematical logic, the BHK interpretation of intuitionistic 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

---

The interpretation states exactly what is intended to be a proof of a given formula. This is specified by induction on the structure of that formula:

• A proof of $P\; \backslash wedge\; Q$ is a pair <a,b> where a is a proof of P and b is a proof of Q.
• A proof of $P\; \backslash vee\; Q$ 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 $P\; \backslash to\; Q$ is a function f which converts a proof of P into a proof of Q.
• A proof of $\backslash exists\; x\; \backslash in\; S\; :\; \backslash phi(x)$ is a pair <a,b> where a is an element of S, and b is a proof of φ(a).
• A proof of $\backslash forall\; x\; \backslash in\; S\; :\; \backslash phi(x)$ is a function f which converts an element a of S into a proof of φ(a).
• The formula $\backslash neg\; P$ is defined as $P\; \backslash to\; \backslash bot$, so a proof of it is a function f which converts a proof of P into a proof of $\backslash bot$.
• $\backslash bot$ is absurdity. There ought not to be a proof of it.

The interpretation of a primitive proposition is supposed to be known from context.

Examples

---

The identity function is a proof of the formula $P\; \backslash to\; P$, no matter what P is.

The law of non-contradiction $\backslash neg\; (P\; \backslash wedge\; \backslash neg\; P)$ expands to $(P\; \backslash wedge\; (P\; \backslash to\; \backslash bot))\; \backslash to\; \backslash bot$:

• A proof of $(P\; \backslash wedge\; (P\; \backslash to\; \backslash bot))\; \backslash to\; \backslash bot$ is a function f which converts a proof of $(P\; \backslash wedge\; (P\; \backslash to\; \backslash bot))$ to a proof of $\backslash bot$.
• A proof of $(P\; \backslash wedge\; (P\; \backslash to\; \backslash bot))$ is a pair of proofs <a,b>, where a is a proof of P, and b is a proof of $P\; \backslash to\; \backslash bot$.
• A proof of $P\; \backslash to\; \backslash bot$ is a function which converts a proof of P to a proof of $\backslash bot$.

Putting it all together, a proof of $(P\; \backslash wedge\; (P\; \backslash to\; \backslash bot))\; \backslash to\; \backslash bot$ is a function f which converts a pair <a,b> -- where a is a proof of P, and b is a function which converts a proof of P to a proof of $\backslash bot$ -- into a proof of $\backslash bot$. The function $f(\backslash langle\; a,\; b\; \backslash rangle)\; =\; b(a)$ fits the bill, proving the law of non-contradiction, no matter what P is.

On the other hand, the law of excluded middle $P\; \backslash vee\; (\backslash neg\; P)$ expands to $P\; \backslash vee\; (P\; \backslash to\; \backslash bot)$, and in general has no proof.

What is absurdity?

---

It is not possible for a logical system to have a formal negation operator such that there is a proof of "not" P exactly when there isn't a proof of P (in general -- see Gödel's incompleteness theorems). The BHK interpretation instead takes "not" P to mean that P leads to absurdity, designated $\backslash bot$, so that a proof of ¬P is a function converting a proof of P into a proof of absurdity.

A standard example of absurdity is found in dealing with arithmetic. Assume that 0=1, and proceed by mathematical induction: 0=0 by the axiom of equality. Now (induction hypothesis), if 0 were equal to a certain natural number n, then 1 would be equal to n+1, (Peano axiom: Sm = Sn if and only if m = n), but since 0=1, therefore 0 would also be equal to n+1. By induction, 0 is equal to all numbers, and therefore any two natural numbers become equal.

Therefore, there is a way to go from a proof of 0=1 to a proof of any basic arithmetic equality, and thus to a proof of any complex arithmetic proposition. Furthermore, to get this result it was not necessary to invoke the Peano axiom which states that 0 is "not" the successor of any natural number. This makes 0=1 suitable as $\backslash bot$ in Heyting arithmetic (and the Peano axiom is rewritten 0=Sn → 0=S0). This use of 0=1 validates the principle of explosion.

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 computable 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.

Mathematical logic | Functional programming | Mathematical constructivism