After the paradoxes, mathematicians did not agree on what mathematics fundamentally is. Three programs gave different answers: logicism tried to reduce mathematics to logic, formalism treated mathematics as rule-governed symbolic practice, and intuitionism grounded mathematics in constructive mental acts.
Logicism
Frege wanted arithmetic to follow from logic alone. Russell and Whitehead carried the project into Principia Mathematica, replacing naive comprehension by type distinctions. Logicism made explicit how much ordinary mathematics depends on quantification, identity, and classes.
Proposition. Logicism succeeds in revealing the logical form of large parts of mathematics, but the need for type theory, reducibility principles, or set-theoretic axioms shows that arithmetic is not obtained from completely neutral logic without further commitments.
Formalism
Hilbert's formalism asked for axioms and proof rules to be written explicitly, then sought finitary proofs that these formal systems are consistent. The slogan was not that symbols are meaningless, but that reliability should be certified by a precise metamathematics.
Definition. A formal system consists of a formal language, axioms, and inference rules. A proof is a finite sequence of formulas, each an axiom or following from earlier formulas by a rule.
Intuitionism
Brouwer rejected the unrestricted use of classical existence proofs. To assert \(\exists x P(x)\) should mean that one can construct such an \(x\). The law of excluded middle is not accepted as a universal principle for infinite mathematical domains.
Constructive principle. A constructive proof of \(\exists x P(x)\) supplies a witness \(x\) and a proof of \(P(x)\). A proof by contradiction may show \(\neg\neg\exists x P(x)\) without producing such a witness.
What the debate taught
The three programs turned foundations into a study of mathematical meaning. Do proofs discover objects, manipulate symbols, or construct possibilities? Modern mathematics often uses all three temperaments: logical clarity, formal proof, and constructive content.
Legacy in modern practice
The debate survives in ordinary mathematical choices. A classical analyst may prove existence by contradiction; a constructive analyst asks for an algorithm or witness; a proof theorist studies the formal strength needed for the argument; a logician asks which axioms are doing the work. These are not merely philosophical moods but different ways of controlling information in a proof.
Proof assistants make this visible again. Lean, Coq, Agda, and related systems require definitions, inference rules, and dependencies to be explicit. In that sense, the old foundational programs return as working infrastructure for checking modern mathematics.
Logicism, formalism, and intuitionism
Frege gave logicism its first great system; Russell and Whitehead rebuilt it through type theory; Hilbert shaped formalism and proof theory; Brouwer founded intuitionism; Heyting gave intuitionistic logic a formal calculus.
Three answers to what mathematics is
Logicism, formalism, and intuitionism were not merely rival proof styles. They answered different questions exposed by the foundational crises. Frege and Russell asked whether mathematics could be reduced to logic. Hilbert asked whether classical mathematics could be secured by finitary reasoning about formal proofs. Brouwer asked whether a mathematical object exists only when it can be mentally or constructively built.
Logicism achieved a lasting analysis of number through structure. In a modern set-theoretic implementation, \[ 0=\varnothing,\qquad n+1=n\cup\{n\}, \] and arithmetic operations are defined recursively. But Russell's paradox and the complexity of Principia Mathematica showed that the word “logic” itself required a carefully delimited formal system.
The law of excluded middle becomes a fault line
Classical logic accepts \[ P\lor\neg P \] without requiring a method to decide \(P\). Intuitionistic logic does not accept this as a universal principle. To prove an existential assertion \(\exists x\,P(x)\), one should construct such an \(x\); to prove a disjunction, one should know which side holds.
Example. The classical proof that there exist irrational \(a,b\) with \(a^b\) rational considers \((\sqrt2)^{\sqrt2}\). If it is rational, take \(a=b=\sqrt2\). If it is irrational, take \[ a=(\sqrt2)^{\sqrt2},\qquad b=\sqrt2, \] so \(a^b=2\). The proof establishes existence by excluded middle without deciding which witness applies. Constructively, one seeks an explicit pair or a decision procedure.
What survived the confrontation
No single school simply won. Classical set-theoretic mathematics became the dominant common language; proof theory realized much of Hilbert's program in restricted form; constructive mathematics and type theory developed powerful computational meanings of proof. The Curry-Howard correspondence, which reads propositions as types and proofs as programs, gives a modern technical form to the intuitionist insistence that proving should construct.