Brouwer-Heyting-Kolmogorov interpretation

In mathematical logic, the Brouwer-Heyting-Kolmogorov interpretation, or BHK interpretation, of intuitionistic logic was proposed by L. E. J. Brouwer, Arend Heyting and independently by Andrey 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 Failed to parse (Missing texvc executable; please see math/README to configure.): P \wedge Q

is a pair <a,b> where a is a proof of P and b is a proof of Q.

• A proof of Failed to parse (Missing texvc executable; please see math/README to configure.): P \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 Failed to parse (Missing texvc executable; please see math/README to configure.): P \to Q

is a function f which converts a proof of P into a proof of Q.

• A proof of Failed to parse (Missing texvc executable; please see math/README to configure.): \exists x \in S : \phi(x)

is a pair <a,b> where a is an element of S, and b is a proof of φ(a).

• A proof of Failed to parse (Missing texvc executable; please see math/README to configure.): \forall x \in S : \phi(x)

is a function f which converts an element a of S into a proof of φ(a).

• The formula Failed to parse (Missing texvc executable; please see math/README to configure.): \neg P

is defined as Failed to parse (Missing texvc executable; please see math/README to configure.): P \to \bot

, so a proof of it is a function f which converts a proof of P into a proof of Failed to parse (Missing texvc executable; please see math/README to configure.): \bot .

• Failed to parse (Missing texvc executable; please see math/README to configure.): \bot

is absurdity. There ought not 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 Failed to parse (Missing texvc executable; please see math/README to configure.): P \to P , no matter what P is.

The law of non-contradiction Failed to parse (Missing texvc executable; please see math/README to configure.): \neg (P \wedge \neg P)

expands to Failed to parse (Missing texvc executable; please see math/README to configure.): (P \wedge (P \to \bot)) \to \bot

• A proof of Failed to parse (Missing texvc executable; please see math/README to configure.): (P \wedge (P \to \bot)) \to \bot

is a function f which converts a proof of Failed to parse (Missing texvc executable; please see math/README to configure.): (P \wedge (P \to \bot))
to a proof of Failed to parse (Missing texvc executable; please see math/README to configure.): \bot

.

• A proof of Failed to parse (Missing texvc executable; please see math/README to configure.): (P \wedge (P \to \bot))

is a pair of proofs <a,b>, where a is a proof of P, and b is a proof of Failed to parse (Missing texvc executable; please see math/README to configure.): P \to \bot

.

• A proof of Failed to parse (Missing texvc executable; please see math/README to configure.): P \to \bot

is a function which converts a proof of P to a proof of Failed to parse (Missing texvc executable; please see math/README to configure.): \bot

. Putting it all together, a proof of Failed to parse (Missing texvc executable; please see math/README to configure.): (P \wedge (P \to \bot)) \to \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 Failed to parse (Missing texvc executable; please see math/README to configure.): \bot
-- into a proof of Failed to parse (Missing texvc executable; please see math/README to configure.): \bot

. The function Failed to parse (Missing texvc executable; please see math/README to configure.): f(\langle a, b \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 Failed to parse (Missing texvc executable; please see math/README to configure.): P \vee (\neg P)

expands to Failed to parse (Missing texvc executable; please see math/README to configure.): P \vee (P \to \bot)

, and in general has no proof. According to the interpretation, a proof of Failed to parse (Missing texvc executable; please see math/README to configure.): P \vee (\neg P)

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 Failed to parse (Missing texvc executable; please see math/README to configure.): P \to \bot

. Thus if neither P nor Failed to parse (Missing texvc executable; please see math/README to configure.): P \to \bot

is provable then neither is Failed to parse (Missing texvc executable; please see math/README to configure.): P \vee (\neg P)

.

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 Failed to parse (Missing texvc executable; please see math/README to configure.): \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 Failed to parse (Missing texvc executable; please see math/README to configure.): \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.

References

• Troelstra, A. "History of Constructivism in the Twentieth Century". 1991. [1]
• Troelstra, A. "Constructivism and Proof Theory". 2003. [2]