In mathematical logic, the Brouwer–Heyting–Kolmogorov interpretation, or BHK interpretation, of intuitionistic logic was proposed by L. E. J. Brouwer and 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.
It is the standard explanation of intuitionistic logic.
[1] The interpretation states what is intended to be a proof of a given formula.
This is specified by induction on the structure of that formula: The interpretation of a primitive proposition is supposed to be known from context.
In the context of arithmetic, a proof of the formula
is a computation reducing the two terms to the same numeral.
Kolmogorov followed the same lines but phrased his interpretation in terms of problems and solutions.
The identity function is a proof of the formula
is a function that converts a proof of
, proving the law of non-contradiction, no matter what P is.
Indeed, the same line of thought provides a proof for the modus ponens rule
On the other hand, the law of excluded middle
It is not, in general, possible for a logical system to have a formal negation operator such that there is a proof of "not"
; see Gödel's incompleteness theorems.
The BHK interpretation instead takes "not"
leads to absurdity, designated
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.
Furthermore, to get this result it was not necessary to invoke the Peano axiom that states that 0 is "not" the successor of any natural number.
in Heyting arithmetic (and the Peano axiom is rewritten 0 = Sn → 0 = S0).
This use of 0 = 1 validates the principle of explosion.
The BHK interpretation will depend on the view taken about what constitutes a function that converts one proof to another, or that converts an element of a domain to a proof.
Different versions of constructivism will diverge on this point.
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.
If one takes lambda calculus as defining the notion of a function, then the BHK interpretation describes the correspondence between natural deduction and functions.