BHK interpretation
Encyclopedia
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 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
is the problem of reducing Q to P; to solve it requires a method to solve problem Q given a solution to problem P.
, no matter what P is.
The law of non-contradiction
expands to 
:
Putting it all together, a proof of
is a function f which converts a pair – where a is a proof of P, and b is a function which converts a proof of P into a proof of 
– into a proof of 
.
The function
fits the bill, proving the law of non-contradiction, no matter what P is.
On the other hand, the law of excluded middle
expands to 
, and in general has no proof. According to the interpretation, a proof of 
is a pair where a is 0 and b is a proof of P, or a is 1 and b is a proof of 
. Thus if neither P nor 
is provable then neither is 
.
. The BHK interpretation instead takes "not" P to mean that P leads to absurdity, designated
, 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
in Heyting arithmetic (and the Peano axiom is rewritten 0 = Sn → 0 = S0). This use of 0 = 1 validates the principle of explosion
.
will diverge on this point.
Kleene's realizability theory identifies the functions with the computable function
s. 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.
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, the Brouwer–Heyting–Kolmogorov interpretation, or BHK interpretation, of intuitionistic logic
Intuitionistic logic
Intuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...
was proposed by L. E. J. Brouwer, Arend Heyting
Arend Heyting
Arend Heyting was a Dutch mathematician and logician. He was a student of Luitzen Egbertus Jan Brouwer at the University of Amsterdam, and did much to put intuitionistic logic on a footing where it could become part of mathematical logic...
and independently by Andrey Kolmogorov
Andrey Kolmogorov
Andrey Nikolaevich Kolmogorov was a Soviet mathematician, preeminent in the 20th century, who advanced various scientific fields, among them probability theory, topology, intuitionistic logic, turbulence, classical mechanics and computational complexity.-Early life:Kolmogorov was born at Tambov...
. It is also sometimes called the realizability interpretation, because of the connection with the realizability
Realizability
Realizability is a part of proof theory which can be used to handle information about formulas instead of about the proofs of formulas. A natural number n is said to realize a statement in the language of arithmetic of natural numbers...
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
is a pair - A proof of
is a pair - A proof of
is a function f which converts a proof of P into a proof of Q. - A proof of
is a pair - A proof of
is a function f which converts an element a of S into a proof of φ(a). - The formula
is defined as 
, so a proof of it is a function f which converts a proof of P into a proof of 
. 
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
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, no matter what P is.The law of non-contradiction
expands to :
- A proof of
is a function f which converts a proof of 
into a proof of 
. - A proof of
is a pair of proofs 
. - A proof of
is a function which converts a proof of P into a proof of 
.
Putting it all together, a proof of
is a function f which converts a pair – into a proof of .The function
fits the bill, proving the law of non-contradiction, no matter what P is.On the other hand, the law of excluded middle
Law of excluded middle
In logic, the law of excluded middle is the third of the so-called three classic laws of thought. It states that for any proposition, either that proposition is true, or its negation is....
expands to , and in general has no proof. According to the interpretation, a proof of is a pair . Thus if neither P nor is provable then neither is .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 ; see Gödel's incompleteness theoremsGödel's incompleteness theorems
Gödel's incompleteness theorems are two theorems of mathematical logic that establish inherent limitations of all but the most trivial axiomatic systems capable of doing arithmetic. The theorems, proven by Kurt Gödel in 1931, are important both in mathematical logic and in the philosophy of...
. The BHK interpretation instead takes "not" P to mean that P leads to absurdity, designated
, 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
Mathematical induction
Mathematical induction is a method of mathematical proof typically used to establish that a given statement is true of all natural numbers...
: 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
in Heyting arithmetic (and the Peano axiom is rewritten 0 = Sn → 0 = S0). This use of 0 = 1 validates the principle of explosionPrinciple of explosion
The principle of explosion, or the principle of Pseudo-Scotus, is the law of classical logic and intuitionistic and similar systems of logic, according to which any statement can be proven from a contradiction...
.
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 constructivismConstructivism (mathematics)
In the philosophy of mathematics, constructivism asserts that it is necessary to find a mathematical object to prove that it exists. When one assumes that an object does not exist and derives a contradiction from that assumption, one still has not found the object and therefore not proved its...
will diverge on this point.
Kleene's realizability theory identifies the functions with the computable function
Computable function
Computable functions are the basic objects of study in computability theory. Computable functions are the formalized analogue of the intuitive notion of algorithm. They are used to discuss computability without referring to any concrete model of computation such as Turing machines or register...
s. It deals with Heyting arithmetic
Heyting arithmetic
In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism. It is named after Arend Heyting, who first proposed it....
, 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
Lambda calculus
In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus...
as defining the notion of a function, then the BHK interpretation describes the correspondence between natural deduction and functions.