Brouwer-Heyting-Kolmogorov interpretation

The Brouwer-Heyting-Kolmogorov (BHK) interpretation is the constructive reading of intuitionistic logic that specifies the meaning of each logical connective in terms of what counts as a proof. Unlike model-theoretic semantics, which defines truth relative to a structure, the BHK interpretation defines truth as the existence of a construction: a mathematical object that witnesses the proposition. It is named for L.E.J. Brouwer (who motivated the constructive requirements), Arend Heyting (who formalized intuitionistic logic), and Andrey Kolmogorov (who independently proposed a problem interpretation in 1932).

Under BHK: a proof of a conjunction is a pair of proofs; a proof of a disjunction is a proof of one disjunct together with a specification of which one; a proof of an implication is a function converting proofs of the antecedent into proofs of the consequent; a proof of negation (¬P) is a function converting any proof of P into a proof of absurdity. The Law of Excluded Middle fails under BHK because asserting P ∨ ¬P requires producing either a proof of P or a procedure converting P-proofs to absurdity — which is impossible for undecidable propositions.

The BHK interpretation is not merely a gloss on intuitionistic logic: it is the foundation of the Curry-Howard Correspondence, where proofs are programs and propositions are types. Any programming language with a sufficiently expressive type theory is, under this correspondence, a system in which BHK proofs are literally executable. The interpretation matters because it makes constructive mathematics computable, not merely principled.