- Brouwer–Heyting–Kolmogorov interpretation
In
mathematical logic , the Brouwer–Heyting–Kolmogorov interpretation, or BHK interpretation, ofintuitionistic logic was proposed byL. E. J. Brouwer ,Arend Heyting and independently byAndrey Kolmogorov . It is also sometimes called the realizability interpretation, because of the connection with therealizability theory ofStephen 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 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 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 o Q is a function "f" which converts a proof of "P" into a proof of "Q".
*A proof of 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 forall x in S : phi(x) is a function "f" which converts an element "a" of "S" into a proof of "φ(a)".
*The formula eg P is defined as P o ot, so a proof of it is a function "f" which converts a proof of "P" into a proof of ot.
*ot is absurdity. There ought not be a proof of it.The interpretation of a primitive proposition is supposed to be known from context. In the context of arithmetic, a proof of the formula "s"="t" 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. To assert a formula is to claim to know a solution to the problem represented by that formula. For instance P o Q is the problem of reducing "Q" to "P"; to solve it requires a method to solve problem "Q" given a solution to problem "P".
Examples
The identity function is a proof of the formula P o P, no matter what P is.
The
law of non-contradiction eg (P wedge eg P) expands to P wedge (P o ot)) o ot:
* A proof of P wedge (P o ot)) o ot is a function "f" which converts a proof of P wedge (P o ot)) to a proof of ot.
* A proof of P wedge (P o ot)) is a pair of proofs <"a","b">, where "a" is a proof of "P", and "b" is a proof of P o ot.
* A proof of P o ot is a function which converts a proof of "P" to a proof of ot.Putting it all together, a proof of P wedge (P o ot)) o ot 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 ot – into a proof of ot.The function f(langle a, b angle) = 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 vee ( eg P) expands to P vee (P o ot), and in general has no proof. According to the interpretation, a proof of P vee ( eg 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 P o ot. Thus if neither "P" nor P o ot is provable then neither is P vee ( eg P).What is absurdity?
It is not in general 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" ; seeGödel's incompleteness theorems . The BHK interpretation instead takes "not" P" to mean that "P" leads to absurdity, designated ot, 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: S"m" = S"n" 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 ot in Heyting arithmetic (and the Peano axiom is rewritten 0=S"n" → 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 function s. It deals withHeyting 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. [http://staff.science.uva.nl/~anne/hhhist.pdf]
*Troelstra, A. "Constructivism and Proof Theory". 2003. [http://staff.science.uva.nl/~anne/eolss.pdf]
Wikimedia Foundation. 2010.