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
⟨,⟩	—	Pair	Proof pairing
π₁, π₂	—	Projections	Pair access
f	—	Construction	Transformation
⊥	U+22A5	Absurdity	No proof

Metatheory. Informal semantics. Made precise via realizability, type theory. Curry-Howard: BHK = typed λ-calculus. Completeness: all "true" formulas provable in HA.

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

Limitations. Informal: "construction" undefined. Multiple formalizations. Classical math incompatible. Philosophically contentious.