Whitehead and Russell's Principia Mathematica

Page of formal logic from Principia Mathematica showing the proof leading to 1 plus 1 equals 2
The famous proposition 54.43 from Principia Mathematica (1910), a step on the way to proving that 1 plus 1 equals 2 Public domain | Source

Between 1910 and 1913 the English philosophers Alfred North Whitehead and Bertrand Russell published “Principia Mathematica” in three volumes through Cambridge University Press. It was the most ambitious attempt ever made to carry out the program Frege had begun: to show that the whole of pure mathematics could be derived from a small set of logical axioms and rules of inference, with every step written out as a formal proof that left nothing to intuition. The copy cited here is the full scan of the three-volume work held at the Internet Archive. The first edition appeared across 1910 to 1913, and the date recorded here is the year the first volume was issued.

The book is famous for its extreme rigor. Simple facts were built up from the ground with painstaking care, and the proof that one plus one equals two does not arrive until well into the first volume. To avoid the contradiction Russell had found in Frege’s system in 1902, the paradox of the set of all sets that are not members of themselves, Whitehead and Russell introduced a layered “theory of types” that forbade the self-reference that had caused the trouble. The result was a vast, carefully staged formal system in which mathematical statements became strings of symbols manipulated by fixed rules.

That very precision is what made Principia Mathematica the proving ground for the deepest questions about formal systems. By spelling out a complete formal language for arithmetic, it gave later logicians a concrete target to reason about. When Kurt Godel set out in 1931 to show the limits of formal reasoning, he framed his result in exactly these terms; the German title of his paper translates as “On Formally Undecidable Propositions of Principia Mathematica and Related Systems.” Godel proved that any consistent system at least as strong as the one in Principia Mathematica must contain true statements it can never prove.

So the work occupies a strange double place in this history. As a foundational project it did not fully succeed, since the dream of a complete and self-justifying mathematics was shown to be impossible. But as a demonstration that mathematics can be reduced to symbol manipulation under explicit rules, it was a direct ancestor of the theory of computation, supplying the formal-system notion that Godel, Church, and Turing all worked against.