Brouwer–Heyting–Kolmogorov interpretation

The Brouwer–Heyting–Kolmogorov (BHK) interpretation is a key principle in intuitionistic logic and type theory that provides a constructive interpretation of mathematical statements. It is named after mathematicians L.E.J. Brouwer, Arend Heyting, and Andrey Kolmogorov. Unlike classical logic, which allows for non-constructive proofs (such as proof by contradiction), intuitionistic logic emphasizes the need for constructive evidence of existence.