Mathematical intuitionism

Mathematical intuitionism is a philosophy of mathematics developed by L. E. J. Brouwer in the early twentieth century, holding that mathematical objects are not discovered in a pre-existing Platonic realm but are constructed by the mathematician's own mental activity. On this view, a mathematical statement is true only if there exists a mental construction that demonstrates it; it is false only if a construction demonstrating its impossibility exists. The law of excluded middle — that every proposition is either true or false — does not hold universally, because there may be propositions for which neither a proof nor a disproof has been (or can be) constructed.

This is not mere philosophical eccentricity. Intuitionism has direct technical consequences. Arend Heyting formalized intuitionistic logic, which differs from classical logic precisely in rejecting the law of excluded middle and double negation elimination. The resulting logic is the natural proof theory for constructive mathematics — mathematics in which every proof of existence must provide a method for constructing the object whose existence is claimed. The Curry-Howard correspondence reveals that intuitionistic logic corresponds exactly to the typed lambda calculus, making intuitionism not a philosophical outlier but the logical foundation of modern functional programming and type theory.

Brouwer's original formulation was deeply psychological — he spoke of the 'creative subject' and the 'primordial intuition of time' as the basis of number. This made his position vulnerable to the charge of solipsism: if mathematics is private mental construction, how is mathematical communication possible? Later intuitionists, particularly Heyting and Per Martin-Löf, replaced Brouwer's psychological vocabulary with proof-theoretic and type-theoretic machinery, transforming intuitionism from a philosophy of mind into a branch of formal logic.

The tension persists: is intuitionism a claim about what mathematics is (ontology), or a claim about what mathematics should be (methodology)? Brouwer believed the former. Most contemporary constructivists hold the latter. The difference matters. If intuitionism is ontological, then classical mathematicians are simply wrong — they are studying objects that do not exist. If it is methodological, then classical mathematics is legitimate but less informative, because it permits proofs that do not yield constructions.

The contemporary revival of intuitionism through dependent type theory and proof assistants is not a retreat into constructivist asceticism. It is the recognition that when mathematics becomes software, the distinction between 'exists' and 'can be computed' is not philosophical hair-splitting — it is the difference between a theorem and a running program.