An interpretation of intuitionistic logic that provides a semantics for intuitionistic logic by means of constructive proofs.

1. 1 A proof of a conjunction $\phi \wedge \psi$ is a pair $〈\sigma ,\tau 〉$ where $\sigma$ is a proof of $\phi$ and $\tau$ is a proof of $\psi$

2. 2 A proof of a disjunction $\phi \vee \psi$ is a pair $〈n,\sigma 〉$ where either $n=0$ and $\sigma$ is a proof of $\phi$ or $n=1$ and $\sigma$ is a proof of $\psi$

3. 3 A proof of a conditional $\phi \to \psi$ is a construction $f$ such that given a proof $\sigma$ of $\phi$, $f$ returns a proof $f\left(\sigma \right)$ of $\psi$

4. 4 A proof of an existential formula $\exists x\phi \left(x\right)$ is a pair $〈c,\sigma 〉$, where $c$ is a term and $\sigma$ is a proof of $\phi \left(c\right)$

5. 5 A proof of a universal formula $\forall x\phi \left(x\right)$ is a construction $f$ such that given any term $c$, $f$ returns a proof $f\left(c\right)$ of $\phi \left(c\right)$

6. 6 A proof of a negation $\neg \phi$ (i.e., $\phi \to \perp$) is a construction $f$ that converts any putative proof $\sigma$ of $\phi$ into a proof $f\left(\sigma \right)$ of absurdity

On this account, the validity of intuitionistic properties such as the disjunction property, i.e., that for any theorem $\phi \vee \psi$, either $\phi$ is a theorem or $\psi$ is a theorem, become clear. The BHK interpretation stems from the combined work of mathematicians L. E. J. Brouwer (1881–1966), Arend Heyting (1898–1980), and Andrey Kolmogorov (1903–1987).