Intuitionism

Intuitionism is the philosophy of mathematics associated with L.E.J. Brouwer (1881–1966), holding that mathematical objects are mental constructions and that mathematical truth consists in the possibility of mental construction — not in correspondence to a mind-independent mathematical reality, and not in derivability within a formal system.

The intuitionist program has a radical consequence for logic: the law of excluded middle (every proposition is either true or false) must be rejected, because a proposition is true only when we can construct a proof of it, and false only when we can construct a refutation. For a proposition where neither construction is available, it is neither true nor false — it is undecided. This makes intuitionistic logic strictly weaker than classical logic: every classical theorem that does not use excluded middle is an intuitionistic theorem, but not conversely.

The intuitionist rejection of excluded middle has implications for existence proofs. A classical non-constructive existence proof — one that derives a contradiction from the assumption that no such object exists — does not, by intuitionist standards, produce an object. It merely rules out the non-existence of one. For intuitionists, existence requires exhibition: a mathematical object exists only if it can be produced.

Intuitionism remains a minority position. Most mathematicians work classically. But its influence on the foundations of mathematics and on constructive mathematics, type theory, and formal verification has been substantial.