BHK Interpretation

Origin. Brouwer, Heyting, Kolmogorov (1920s-1930s). Proofs as constructions. Meaning-as-use for connectives. Foundation for intuitionistic logic semantics. Basis for Curry-Howard.

Models. Propositions interpreted by proof conditions. A proof of A → B transforms proofs of A to proofs of B. Constructive existence: provide witness. No truth independent of proof.

Formalism.

Conjunction: A proof of A ∧ B is a pair ⟨p, q⟩ where

p is a proof of A
q is a proof of B

Disjunction: A proof of A ∨ B is a pair ⟨i, p⟩ where

i ∈ {0, 1} indicates which disjunct
if i=0: p is a proof of A
if i=1: p is a proof of B

Implication: A proof of A → B is a construction f that transforms any proof of A into a proof of B.

Negation: ¬A ≡ A → ⊥ A proof of ¬A transforms proofs of A to absurdity.

Universal: A proof of ∀x.A(x) is a construction f that given any object a, yields a proof of A(a).

Existential: A proof of ∃x.A(x) is a pair ⟨a, p⟩ where

a is an object (witness)
p is a proof of A(a)

Absurdity: ⊥ has no proof. From ⊥, anything follows (ex falso).

Non-validity: A ∨ ¬A: requires deciding A constructively. ¬¬A → A: double negation elimination fails.

Symbols.

Symbol	Unicode	Name	Meaning
⟨ ⟩	U+27E8, U+27E9	Angle brackets / Pairing	⟨p, q⟩ proves a conjunction; ⟨a, p⟩ proves an existential
π	U+03C0	Pi / Projection	π₁ and π₂ recover the components of a pair
∧	U+2227	Conjunction	Proved by a pair of proofs
∨	U+2228	Disjunction	Proved by a tag naming a disjunct plus a proof of it
→	U+2192	Implication	Proved by a construction sending proofs to proofs
¬	U+00AC	Negation	Not primitive: ¬A abbreviates A → ⊥
⊥	U+22A5	Absurdity	The proposition stipulated to have no proof
∀	U+2200	Universal quantifier	Proved by a construction defined on every object
∃	U+2203	Existential quantifier	Proved by a witness together with a proof about it
∈	U+2208	Element of	The disjunction tag ranges over i ∈ {0, 1}
≡	U+2261	Identical to / Definition	Definitional abbreviation, as in ¬A ≡ A → ⊥
λ	U+03BB	Lambda	The Curry–Howard term-former matching →
f	—	Construction	The primitive the interpretation leaves unexplained

Metatheory. BHK stipulates what counts as a proof rather than assigning truth values, so its content is fixed only when "construction" is made precise, and each precisification is a theorem with its own reach. Kleene's number realizability (1945) reads constructions as indices of partial recursive functions and validates Heyting arithmetic — but it validates more besides, since Church's thesis CT₀ and Markov's principle are realizable and not intuitionistically provable, so realizability strengthens the interpretation rather than merely rendering it. Under Curry–Howard the clauses become typing rules: pairing for ∧, injection for ∨, abstraction for →, and dependent sums and products for ∃ and ∀, which is what Martin-Löf's type theory adopts as a definition. Kreisel's theory of constructions attempted a direct formalization and required a second clause, demanding that the construction come with a proof that it does what is claimed. The predicted properties do hold: Heyting arithmetic has the disjunction and existence properties.

Applies to. Intuitionistic foundations. Type theory semantics. Constructive mathematics. Proof assistants. Program extraction.

Limitations. The interpretation is circular where it matters most: "a construction transforming any proof of A into a proof of B" presupposes the notion of proof it purports to explain, and quantifies over the unbounded totality of proofs of A. Making that precise forces the second clause — the construction must be accompanied by a proof that it works — and the attempts by Kreisel and Goodman to formalize it did not settle the matter. No precisification is neutral: realizability validates Church's thesis and Markov's principle, Kripke semantics validates neither, and both are complete for intuitionistic logic, so BHK underdetermines its own semantics. The clauses say nothing about ⊥ beyond stipulating that it has no proof, so ex falso is imposed rather than derived — which is why minimal logic remains a coherent alternative reading of the same clauses.