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. The interpretation 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: A proof of is a pair where is a proof of and is a proof of . A proof of is either where is a proof of or where is a proof of . A proof of is a function that converts a proof of into a proof of . A proof of is a pair where is an element of and is a proof of . A proof of is a function that converts an element of into a proof of . The formula is defined as , so a proof of it is a function that converts a proof of into a proof of . There is no proof of , the absurdity or bottom type (nontermination in some programming languages). 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. 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 to ; to solve it requires a method to solve problem given a solution to problem . 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 that converts a proof of into a proof of . A proof of is a pair of proofs <a, b>, where is a proof of P, and is a proof of . A proof of is a function that converts a proof of P into a proof of . Putting it all together, a proof of is a function that converts a pair <a, b> – where is a proof of P, and is a function