Inmathematical logic, theBrouwer–Heyting–Kolmogorov interpretation, orBHK interpretation, is an explanation of the meaning ofproof inintuitionistic logic, proposed byL. E. J. Brouwer andArend Heyting, and independently byAndrey Kolmogorov. It is also sometimes called therealizability interpretation, because of the connection with therealizability theory ofStephen Kleene. It is the standard explanation of intuitionistic logic.^[1]

This sectionneeds additional citations forverification. Please helpimprove this article byadding citations to reliable sources in this section. Unsourced material may be challenged and removed.(December 2025) (Learn how and when to remove this message)

The interpretation states what is intended to be a proof of a givenformula. This is specified byinduction on the structure of that formula:

• A proof of${\displaystyle P\wedge Q}$ is a pair${\displaystyle ⟨a,b⟩}$ where${\displaystyle a}$ is a proof of${\displaystyle P}$ and${\displaystyle b}$ is a proof of${\displaystyle Q}$.
• A proof of${\displaystyle P\vee Q}$ is either${\displaystyle ⟨0,a⟩}$ where${\displaystyle a}$ is a proof of${\displaystyle P}$ or${\displaystyle ⟨1,b⟩}$ where${\displaystyle b}$ is a proof of${\displaystyle Q}$.
• A proof of${\displaystyle P\to Q}$ is a construction (see§ Definition of construction) that converts a (hypothetical) proof of${\displaystyle P}$ into a proof of${\displaystyle Q}$.
• A proof of${\displaystyle (\mathrm{\exists }x\in S)(Px)}$ is a pair${\displaystyle ⟨x,a⟩}$ where${\displaystyle x}$ is an element of${\displaystyle S}$ and${\displaystyle a}$ is a proof of${\displaystyle Px}$.
• A proof of${\displaystyle (\mathrm{\forall }x\in S)(Px)}$ is a construction that converts an element${\displaystyle x}$ of${\displaystyle S}$ into a proof of${\displaystyle Px}$.
• The formula${\displaystyle \mathrm{\neg }P}$ is defined as${\displaystyle P\to \mathrm{\perp }}$, so a proof of it is a construction that converts a proof of${\displaystyle P}$ into a proof of${\displaystyle \mathrm{\perp }}$.
• There is no proof of${\displaystyle \mathrm{\perp }}$, theabsurdity.

Note that it may be possible to prove${\displaystyle P\to Q}$ even though there are no proofs of${\displaystyle P}$ (or proofs of${\displaystyle Q}$);${\displaystyle P\to Q}$ is the hypothetical assertion that a proof of${\displaystyle Q}$ could be built out of a proof of${\displaystyle P}$, if one were available.

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${\displaystyle P\to Q}$ is the problem of reducing${\displaystyle Q}$ to${\displaystyle P}$; to solve it requires a method to solve problem${\displaystyle Q}$ given a solution to problem${\displaystyle P}$.

The interpretation of a primitive proposition is supposed to be known from context. In the context of arithmetic, a proof of the formula${\displaystyle x=y}$ is a computation reducing the two terms to the same numeral.

This sectionneeds additional citations forverification. Please helpimprove this article byadding citations to reliable sources in this section. Unsourced material may be challenged and removed.(December 2025) (Learn how and when to remove this message)

The BHK interpretation will depend on the view taken about what constitutes aconstruction that converts one proof to another, or that converts an element of a domain to a proof. Different versions ofconstructivism will diverge on this point.

Kleene'srealizability theory identifies constructions with thecomputable functions. It deals with Heyting arithmetic, where the domain of quantification is the natural numbers and the primitive propositions are of the formx =y. A proof ofx =y is simply the trivial algorithm ifx evaluates to the same number thaty 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 takeslambda calculus as defining the notion of a construction, then the BHK interpretation describes thecorrespondence between natural deduction and lambda functions.

This sectionneeds additional citations forverification. Please helpimprove this article byadding citations to reliable sources in this section. Unsourced material may be challenged and removed.(December 2025) (Learn how and when to remove this message)

It is not, in general, possible for alogical system to have a formal negation operator such that there is a proof of "not"${\displaystyle P}$ exactly when there isn't a proof of${\displaystyle P}$; seeGödel's incompleteness theorems. The BHK interpretation instead takes "not"${\displaystyle P}$ to mean that${\displaystyle P}$ leads to absurdity, designated${\displaystyle \mathrm{\perp }}$, so that a proof of${\displaystyle \mathrm{\neg }P}$ is a construction converting a proof of${\displaystyle P}$ into a proof of absurdity.

A standard example of absurdity is found in dealing with arithmetic. Assume that 0 = 1, and proceed bymathematical induction: 0 = 0 by the axiom of equality. Now (induction hypothesis), if 0 were equal to a certainnatural numbern, then 1 would be equal ton + 1, (Peano axiom:Sm =Sn if and only ifm =n), but since 0 = 1, therefore 0 would also be equal ton + 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 that states that 0 is "not" the successor of any natural number. This makes 0 = 1 suitable as${\displaystyle \mathrm{\perp }}$ inHeyting arithmetic (and the Peano axiom is rewritten 0 =Sn → 0 =S0). This use of 0 = 1 validates theprinciple of explosion.

The identity function is a proof of the formula${\displaystyle P\to P}$, no matter whatP is.

Thelaw of non-contradiction${\displaystyle \mathrm{\neg }(P\wedge \mathrm{\neg }P)}$ expands to${\displaystyle (P\wedge (P\to \mathrm{\perp }))\to \mathrm{\perp }}$:

• A proof of${\displaystyle (P\wedge (P\to \mathrm{\perp }))\to \mathrm{\perp }}$ is a construction that converts a proof of${\displaystyle (P\wedge (P\to \mathrm{\perp }))}$ into a proof of${\displaystyle \mathrm{\perp }}$.
• A proof of${\displaystyle (P\wedge (P\to \mathrm{\perp }))}$ is a pair of proofs${\displaystyle ⟨a,b⟩}$, where${\displaystyle a}$ is a proof ofP, and${\displaystyle b}$ is a proof of${\displaystyle P\to \mathrm{\perp }}$.
• A proof of${\displaystyle P\to \mathrm{\perp }}$ is a construction that converts a proof of${\displaystyle P}$ into a proof of${\displaystyle \mathrm{\perp }}$.

Putting it all together, a proof of${\displaystyle (P\wedge (P\to \mathrm{\perp }))\to \mathrm{\perp }}$ is a construction that converts a pair${\displaystyle ⟨a,b⟩}$ – where${\displaystyle a}$ is a proof of${\displaystyle P}$, and${\displaystyle b}$ is a construction that converts a proof of${\displaystyle P}$ into a proof of${\displaystyle \mathrm{\perp }}$ – into a proof of${\displaystyle \mathrm{\perp }}$. There is a function${\displaystyle f}$ that does this, where${\displaystyle f(⟨a,b⟩)=b(a)}$, proving the law of non-contradiction, no matter whatP is.

Indeed, the same line of thought provides a proof for themodus ponens rule${\displaystyle (P\wedge (P\to Q))\to Q}$ as well, where${\displaystyle Q}$ is any proposition.

On the other hand, thelaw of excluded middle${\displaystyle P\vee (\mathrm{\neg }P)}$ expands to${\displaystyle P\vee (P\to \mathrm{\perp })}$, and in general has no proof. According to the interpretation, a proof of${\displaystyle P\vee (\mathrm{\neg }P)}$ is a pair${\displaystyle ⟨a,b⟩}$ wherea is 0 andb is a proof of${\displaystyle P}$, ora is 1 andb is a proof of${\displaystyle P\to \mathrm{\perp }}$. Thus if neither${\displaystyle P}$ nor${\displaystyle P\to \mathrm{\perp }}$ is provable then neither is${\displaystyle P\vee (\mathrm{\neg }P)}$.

• Curry–Howard correspondence
• Logics for computability

• Troelstra, A. (1991)."History of Constructivism in the Twentieth Century"(PDF).
• Troelstra, A. (2003). "Constructivism and Proof Theory (draft)".CiteSeerX 10.1.1.10.6972.

• Van Atten, Mark (4 May 2022)."The Development of Intuitionistic Logic". InZalta, Edward N. (ed.).Stanford Encyclopedia of Philosophy.ISSN 1095-5054.OCLC 429049174.
• BHK interpretation at thenLab

• Dependently typed programming
• Functional programming
• Constructivism (philosophy of mathematics)
• Intuitionism
• Mathematical logic
• Proof theory
• Philosophy of logic
• Foundations of mathematics
• Logic in computer science
• Type theory

• Articles with short description
• Short description matches Wikidata
• Articles needing additional references from December 2025
• All articles needing additional references