View source for Brouwer-Heyting-Kolmogorov interpretation

The '''Brouwer-Heyting-Kolmogorov (BHK) interpretation''' is the constructive reading of [[Intuitionistic Logic|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.

[[Category:Mathematics]]
[[Category:Logic]]