Principia Mathematica: hundreds of pages to reach 1 + 1 = 2

Few books are as famous and as rarely read as Principia Mathematica. Alfred North Whitehead and Bertrand Russell published it in three volumes between 1910 and 1913. It has close to two thousand pages of dense symbolic logic, and it tries to show that all of mathematics can be derived from a handful of logical principles.

It is best known for a joke: the proof that $1 + 1 = 2$ only appears after hundreds of pages. That joke hides one of the most important intellectual projects of the twentieth century. Its failures shaped mathematics and computer science as much as its successes did.

“The above proposition is occasionally useful.” Whitehead & Russell, remark after proving 1 + 1 = 2 (✱110.643)

The dream: mathematics is logic

Around 1900, mathematics was in a strange position. Calculus had finally been made rigorous by Cauchy, Weierstrass and Dedekind, who reduced it to statements about real numbers. The real numbers had been built from the rationals, and the rationals from the natural numbers. Everything rested on arithmetic.

So what does arithmetic rest on? The German logician Gottlob Frege gave a bold answer: logic. If numbers, addition and induction could all be defined in purely logical terms, then mathematics would need no special intuitions. It would be logic, all the way down. This programme is called logicism.

Frege spent decades building the system. Then, in 1902, a letter arrived from a young Bertrand Russell.

The paradox that broke the foundations

Frege’s system allowed any property to define a set: the set of all $x$ such that $\varphi(x)$. That sounds harmless. Russell asked what happens with a very particular property.

Now ask: is $R$ a member of itself?

A system that proves a contradiction proves everything: from $P \land \lnot P$ any statement follows. Frege’s foundations had collapsed. He added a hurried appendix to the second volume of his Grundgesetze (1903), acknowledging that the basis of his work had been shaken.

The everyday version is the barber who shaves exactly those who do not shave themselves. Does he shave himself? The barber is easy to dismiss: such a barber simply doesn’t exist. With sets, it was not so easy, because the naive rule “every property defines a set” was exactly what logicism needed.

Russell’s fix: a hierarchy of types

Principia is, in large part, Russell’s repair job. Its diagnosis is the vicious-circle principle: no collection may contain members that can only be defined in terms of the collection itself. $R$ is defined by quantifying over all sets, including $R$, and that is what goes wrong.

The cure is the theory of types. Every object lives at a level:

Under this rule $x \in x$ is not false. It is meaningless, just as "hello".length().length() doesn’t compile in Java. Russell’s set cannot even be written down.

Principia actually uses a more complicated ramified hierarchy, which also stratifies propositions by how they quantify. To recover ordinary mathematics inside it, the authors needed the axiom of reducibility, a principle that many critics considered an ad-hoc patch rather than a truth of logic. Similarly, the axiom of infinity and the multiplicative axiom (the axiom of choice) are carried as explicit hypotheses rather than asserted as logic.

If you’ve written generics, you’ve used the descendants of this idea. Type systems in programming languages exist for the same reason: some expressions must be ruled out before evaluation, because evaluating them makes no sense.

Building logic from almost nothing

Principia starts with two primitive connectives, negation $\sim p$ and disjunction $p \lor q$, and defines implication from them:

$$p \supset q \;\overset{\text{def}}{=}\; \sim p \lor q. \qquad (\ast 1.01)$$

On top of the rule of modus ponens (from $p$ and $p \supset q$, infer $q$) it lays down five primitive propositions:

Number	Name	Proposition
✱1.2	Taut	$p \lor p \;\supset\; p$
✱1.3	Add	$q \;\supset\; p \lor q$
✱1.4	Perm	$p \lor q \;\supset\; q \lor p$
✱1.5	Assoc	$p \lor (q \lor r) \;\supset\; q \lor (p \lor r)$
✱1.6	Sum	$(q \supset r) \;\supset\; (p \lor q \supset p \lor r)$

Everything in propositional logic follows from these. In 1926 Paul Bernays showed that ✱1.5 is redundant: it can be derived from the other four. Even the giants left a spare axiom lying around.

What is a number?

Here is the most beautiful idea in the book, inherited from Frege. We recognise that two collections have the same size without counting: a pair of shoes and a pair of gloves can be matched one-to-one.

A number, in this view, isn’t a symbol or a mental object. It is a property shared by all collections of that size, turned into an object. That is also why the theory of types matters: “the class of all pairs” is exactly the kind of enormous totality that leads to paradox if you aren’t careful.

The famous proposition

With all that machinery, the authors can finally state a fact about one and one. In ✱54.43 of Volume I they prove this, in their own notation:

⊢ :. α, β ∈ 1 . ⊃ : α ∩ β = Λ . ≡ . α ∪ β ∈ 2

The dots replace brackets (a convention borrowed from Peano), $\supset$ is implication, $\Lambda$ is the empty class and $\vdash$ marks an asserted theorem. The authors add that from this, “when arithmetical addition has been defined”, it will follow that $1 + 1 = 2$. Addition of cardinals only arrives in Volume II, where ✱110.643 finally completes the proof, along with the dry remark quoted at the top of this article.

The modern way: Peano arithmetic

Today we rarely derive numbers from logic. Instead, we describe them directly with a few axioms, following Giuseppe Peano (1889):

We write $1 = S(0)$ and $2 = S(S(0))$, and define addition by recursion on the second argument:

$$\begin{aligned} a + 0 &= a, \\ a + S(b) &= S(a + b). \end{aligned}$$

Now the proof that took Principia hundreds of pages fits in one line:

That’s not cheating. It’s a different trade-off: Peano assumes the numbers and their basic behaviour, while Principia tried to derive them from logic alone. The length was the price of that ambition.

A modern proof assistant checks it by pure computation. In Lean 4:

example : 1 + 1 = 2 := rfl

Lean is built on a type theory, a direct descendant of the hierarchy Russell invented to escape his paradox.

The ending nobody expected

In 1931 the young Kurt Gödel published a paper whose title names the book directly: On Formally Undecidable Propositions of Principia Mathematica and Related Systems I.

The dream of a single system in which every mathematical truth could be derived was over. It wasn’t just Principia’s particular axioms. No such system can be complete. Five years later, Alan Turing showed in the same spirit that no algorithm can decide, for every program, whether it halts.

A short timeline

1. 1879 Frege's Begriffsschrift introduces modern quantified logic.
2. 1889 Peano publishes his axioms for arithmetic.
3. 1901 Russell discovers his paradox and writes to Frege in 1902.
4. 1908 Russell publishes the ramified theory of types.
5. 1910–13 Principia Mathematica, Volumes I–III.
6. 1925–27 Second edition, with a new introduction by Russell.
7. 1931 Gödel's incompleteness theorems.
8. 1936 Church and Turing: the Entscheidungsproblem has no solution.
9. 1940 Church's simply typed λ-calculus, the ancestor of modern type systems.

Why it still matters

Principia failed at what it set out to do, and yet:

• It made formal proof a real, mechanical object. That’s the idea behind every proof assistant, from Coq/Rocq to Lean.
• It gave us type theory, which now runs through programming languages, compilers and verified software.
• It forced the questions that Gödel, Church and Turing answered. Those answers became the theory of computation and, eventually, the computer.

Every time a compiler rejects an ill-typed expression, it applies the lesson of Russell’s paradox: some things should not even be sayable.