Intuitionistic logic

Intuitionistic logic is a system of logic developed by L.E.J. Brouwer and formalized by Arend Heyting, which rejects the law of the excluded middle (every proposition is either true or false) and the principle of double negation elimination. In intuitionistic logic, a proposition is proved true only by explicit construction or direct evidence; indirect proofs that show a proposition cannot be false are insufficient. This makes intuitionistic logic the logical backbone of constructive mathematics, where existence claims require algorithms rather than mere non-contradiction.

The intuitionistic critique was aimed squarely at David Hilbert's formalism and at the set-theoretic foundations that Georg Cantor had built. Brouwer argued that mathematical objects are mental constructions, not formal symbols, and that reasoning about infinite totalities as if they were completed entities is illegitimate. The dispute split the foundations of mathematics into camps that remain unreconciled: the intuitionists demand proof by construction, while classical mathematicians accept proof by contradiction.

Intuitionistic logic is not a weaker version of classical logic. It is a different logic, with its own semantics (Kripke models, realizability), its own proof theory, and its own computational interpretation — the Curry-Howard correspondence identifies intuitionistic proofs with typed lambda calculus programs. In this sense, intuitionistic logic is the logic of computation, while classical logic is the logic of eternal, pre-given truth.