Intuitionistic logic

Summary

Intuitionistic logic is the logic of constructive reasoning, in which a statement counts as true only when it has a proof. It is classical logic without the law of excluded middle $\varphi \lor \neg\varphi$ and without double negation elimination $\neg\neg\varphi \to \varphi$. Its semantics include Heyting algebras, Kripke models and the Brouwer–Heyting–Kolmogorov interpretation. Through the Curry–Howard correspondence, its proofs correspond to typed programs.