Constructivism in mathematics holds that to prove a mathematical object exists, you must actually construct it โ a proof by contradiction that merely shows non-existence is impossible is not sufficient. Constructivism rejects the law of excluded middle ("every statement is either true or false") as an unjustifiable blanket assumption, and requires that mathematical truths have explicit computational witnesses. Though a minority position among practising mathematicians, constructivism has had enormous influence on computer science, programming language design, and the modern theory of proof assistants.
Here is a non-constructive existence proof: "There exist two irrational numbers a and b such that aแต is rational." Proof: consider โ2^โ2. Either this is rational (done โ take a=b=โ2), or it is irrational, in which case (โ2^โ2)^โ2 = โ2ยฒ = 2 is rational (done โ take a=โ2^โ2, b=โ2). In either case we've found our pair. But notice: we don't actually know which case applies. We've proved existence without ever producing a specific example.
Constructive mathematics has a direct computational interpretation โ via the Curry-Howard correspondence (see the Type Theory entry), a constructive proof of "there exists an x satisfying P(x)" is literally a program that produces such an x. This connection between constructive proofs and programs is the theoretical foundation of verified software and proof assistants โ systems where "type-checking a program" is the same as "verifying a mathematical proof," and every proof automatically produces a computable witness.
The philosophical root of mathematical constructivism is L.E.J. Brouwer's intuitionism (c. 1907โ1920s). Brouwer held that mathematics is a free activity of the human mind โ mathematical objects are mental constructions, and mathematical truth means the existence of a mental construction demonstrating it. Brouwer concluded that the law of excluded middle (every mathematical statement is true or false) is not universally valid, because some statements may be mathematically undecidable โ neither a construction for the statement nor a construction for its negation may exist. Brouwer was willing to develop a substantial body of mathematics (including a theory of the continuum based on "choice sequences") on this basis, accepting that many classical theorems would simply be unavailable.
Rejecting the law of excluded middle (LEM) means rejecting proofs of the form "either P or ยฌP, and in both cases..." โ including most proofs by contradiction. Many classical theorems cannot be proved constructively: the intermediate value theorem (if f is continuous, f(0)<0, f(1)>0, there exists c with f(c)=0) is classically trivial but constructively fails for computable functions; the least upper bound principle for the reals requires LEM; most existence proofs in analysis, topology, and algebra use non-constructive methods. Constructive mathematics is significantly weaker than classical mathematics โ you can prove less.
Errett Bishop's 1967 book Foundations of Constructive Analysis showed that a substantial and useful body of analysis โ including the theory of measure, integration, Banach spaces, and much of functional analysis โ can be developed constructively, without LEM and without the axiom of choice, while remaining directly interpretable in classical mathematics (every Bishop-constructive theorem is also classically true). Bishop's work demonstrated that constructivism is not just a philosophical position but a viable mathematical programme โ though it requires substantially more work to prove results that classically follow immediately from LEM.
Intuitionistic logic is the formal logic corresponding to constructive mathematics. It removes the law of excluded middle (P โจ ยฌP) and double negation elimination (ยฌยฌP โ P) from classical propositional logic, while retaining all other classical rules. Intuitionistic logic is strictly weaker than classical logic โ every classically provable sequent is also intuitionistically provable in exactly those cases where a constructive proof exists. Crucially, intuitionistic logic is sound and complete with respect to Kripke semantics (truth in all "possible worlds" in a partially ordered set of states of knowledge) โ giving it a clean mathematical model that is quite different from classical Boolean semantics.
Realizability (introduced by Stephen Kleene in 1945) provides a formal semantics that makes the computational content of constructive proofs precise. A statement P is "realizable" if there exists a computable function (a natural number coding a Turing machine) that, given any realizer for the hypothesis of P, produces a realizer for the conclusion. This gives a rigorous interpretation of "constructive proof" in terms of computable functions, and connects intuitionistic logic to recursion theory and type theory. Modified realizability (Kreisel) and more modern variants underlie the operational semantics of functional programming languages.
The most sophisticated modern setting for constructive mathematics is topos theory (Lawvere, Tierney, 1960sโ1970s), which generalises set theory by replacing "the category of sets" with an arbitrary "topos" โ a category with certain categorical properties. Different toposes model different "mathematics": the ordinary topos of sets models classical mathematics; the effective topos models realizability and constructive mathematics; sheaf toposes model intuitionistic mathematics in a geometric context. Topos theory reveals that classical and constructive mathematics are not isolated alternatives but points in a rich landscape of possible mathematical universes, each with its own internal logic, and connects constructivism to algebraic geometry and homotopy type theory in deep and currently very active ways.