Brouwer–Heyting–Kolmogorov Interpretation

The Brouwer–Heyting–Kolmogorov interpretation, usually abbreviated BHK interpretation, explains the logical operations of intuitionistic logic through the constructions required to prove statements. Rather than assigning only truth values to propositions, it describes the evidence a mathematical proof must provide: a conjunction requires proofs of both components, an existence statement requires a witness, and an implication requires a method for transforming proofs. Its central notions—construction and constructive proof—are not completely defined by the interpretation itself. (mathematik.uni-muenchen.de)

Historical background

The interpretation developed from L. E. J. Brouwer’s foundations of intuitionistic mathematics, Arend Heyting’s work on its logical formulation, and Andrey Kolmogorov’s interpretation of logic as a calculus of problems. Heyting published his formal intuitionistic calculus in 1930; Kolmogorov’s On the Interpretation of Intuitionistic Logic followed in 1932. (arxiv.org)

For Kolmogorov, the logical operations organize tasks and their solutions. Solving $A\land B$ means solving both tasks; solving $A\to B$ means giving a method that converts a solution of $A$ into a solution of $B$ . This closely parallels the proof interpretation, but the combined name should not imply complete philosophical agreement: Kolmogorov distinguished problems from propositions and did not simply adopt Brouwer’s foundational position. (arxiv.org)

The constructive clauses

Let $A$ and $B$ be propositions, and let $D$ be a domain of objects. The interpretation explains compound statements recursively, assuming that the evidence appropriate to atomic statements is already understood. Its principal clauses are as follows. (mathematik.uni-muenchen.de)

Logical form	Required constructive evidence
$A\land B$	A pair consisting of a proof of $A$ and a proof of $B$ .
$A\lor B$	A proof of one component, together with an indication of which component was proved.
$A\to B$	A construction transforming any proof of $A$ into a proof of $B$ .
$\bot$	No proof; $\bot$ represents absurdity.
$\neg A$	A proof of $A\to\bot$ , transforming a hypothetical proof of $A$ into absurdity.
$\forall x\in D\,A(x)$	A construction producing a proof of $A(d)$ for any supplied $d\in D$ .
$\exists x\in D\,A(x)$	A pair containing a witness $d\in D$ and a proof of $A(d)$ .

Conjunction therefore preserves both pieces of evidence. Disjunction preserves a choice as well as evidence: a proof of $A\lor B$ cannot merely leave unresolved which alternative has been established. Implication is understood through a constructive function on proofs, not simply through a table of truth values. These readings also explain the corresponding product, sum, and function types in computational accounts of logic. (pure.ed.ac.uk)

The universal clause requires a single method applicable to arbitrary inputs, rather than merely an assertion that each instance has some proof. The existential clause requires both an object and verification of its claimed property. For example, constructive evidence for

\forall n\in\mathbb N\,\exists m\in\mathbb N\;(m>n)

can be given by the procedure that receives a natural number $n$ , returns $m=n+1$ , and supplies the elementary proof that $n+1>n$ . This illustrates the universal and existential clauses together. (mathematik.uni-muenchen.de)

Consequences for classical principles

The law of excluded middle asserts

A\lor\neg A.

Under the BHK reading, proving an instance requires either a proof of $A$ or a constructive refutation of $A$ , with the alternative identified. The logical form alone supplies neither. Consequently, intuitionistic logic does not accept excluded middle as an unrestricted principle, unlike classical logic. This does not prevent particular instances from being proved when the required evidence is available. (pure.ed.ac.uk)

Likewise, double-negation elimination,

\neg\neg A\to A,

has no general BHK construction. Evidence for $\neg\neg A$ transforms a refutation of $A$ into absurdity; it does not automatically supply evidence for $A$ . This conclusion follows from applying the implication and negation clauses. By contrast, $A\to\neg\neg A$ has a direct construction: given a proof of $A$ , apply any proposed refutation to it. (mathematik.uni-muenchen.de)

Thus constructive reasoning does allow arguments deriving contradictions. What requires additional justification is using the impossibility of a refutation as a general substitute for constructing the asserted object or proof.

Natural deduction and proof computation

BHK evidence closely matches the rules of inference of natural deduction. Conjunction introduction builds a pair of proofs; conjunction elimination selects a component. Implication introduction turns a derivation under an assumption into a proof-transforming operation, while implication elimination—modus ponens—applies that operation to evidence for its premise. (pure.ed.ac.uk)

For example, the proof of

(A\land B)\to(B\land A)

can be represented by the operation

\langle p,q\rangle\longmapsto\langle q,p\rangle.

Here the logical argument has an explicit computational action: rearranging evidence. Proof normalization removes unnecessary introduction–elimination detours, such as constructing a pair and immediately selecting a component. Under the computational correspondence, these simplifications match program evaluation. (pure.ed.ac.uk)

Type theory and applications

The Curry–Howard correspondence makes this relationship precise for suitable logical and computational systems: propositions correspond to types, proofs to terms, and proof simplification to computation. Conjunction corresponds to a product type, disjunction to a tagged sum, and implication to a function type. Quantifiers lead to dependent types, in which the type of evidence can depend on an input or witness. (pure.ed.ac.uk)

BHK is nevertheless not identical to Curry–Howard. BHK gives a meaning explanation in terms of constructive evidence; Curry–Howard establishes correspondences between specified calculi. These ideas support type theory, proof assistants, and formal verification, where mathematical statements can serve as specifications and checked terms as evidence that those specifications are met. (pure.ed.ac.uk)

Scope and limitations

BHK is a framework for explaining meaning, not by itself a fully specified formal semantics. It leaves questions about constructions open: which operations are admissible, how their correctness is established, and how evidence for atomic propositions is determined. The treatment of implication is particularly important because it quantifies over possible proofs of its premise, rather than only proofs currently known. (mathematik.uni-muenchen.de)

Realizability interpretations give related ideas mathematical form by specifying objects that realize formulas and operations on those objects. They should not simply be identified with the informal BHK clauses. Research on formalizing the interpretation investigates how constructive operations and semantic consequence must be understood; proposed realizability, categorical, and other models embody additional choices beyond the clauses themselves. (pure.ed.ac.uk)

References

Kolmogorov's Calculus of Problems and Its Legacyarxiv.org
Propositions as Typespure.ed.ac.uk
Mathematical semantics of intuitionistic logicarxiv.org