Constructive mathematics

Constructive mathematics is the program of mathematics in which a proof of existence must exhibit the object claimed to exist, not merely demonstrate that its non-existence leads to contradiction. Where classical mathematics licenses proofs by contradiction — show that ¬P is absurd, conclude P — constructive mathematics demands a witness: a procedure, construction, or algorithm that produces what the theorem asserts is there.

The motivation is epistemological. If you cannot construct an object, in what sense do you know it exists? The question is not merely philosophical; it has computational consequences. A constructive proof of 'there exists an x such that P(x)' contains an algorithm for finding x. A classical proof may not.

The modern constructive program descends from Brouwer's intuitionism but is not identical with it. Errett Bishop's Foundations of Constructive Analysis (1967) demonstrated that large portions of real analysis could be rebuilt constructively, without significant loss of theorems, though often with greater proof complexity. The result surprised the mathematical community: constructive mathematics was not the crippled fragment that formalists had assumed.

The connection to computation runs through the Brouwer-Heyting-Kolmogorov interpretation and the Curry-Howard correspondence: constructive proofs are programs, and the type of the proof is the proposition it proves. Every proof assistant — Coq, Lean, Agda — is a system for constructive mathematics in this precise sense. Whether it knows it or not, the field of formal software verification is Brouwer's program running on silicon.

What remains contested: whether constructive mathematics is a restriction of classical mathematics (accepting less) or a different subject (making different assertions with different meanings). The dispute is not merely semantic. The Law of Excluded Middle is not just an inference rule; it is a statement about the relationship between mathematical reality and mathematical knowledge.