A Letter, a Paradox, and the Tower of Types That Fixed Math
A Letter That Changed Everything
In June 1902, the German logician Gottlob Frege (1848–1925) was about to publish the second volume of his grand book Grundgesetze der Arithmetik. He believed he had reduced all of mathematics to pure logic. Then a letter arrived from a young English philosopher, Bertrand Russell (1872–1970). Russell pointed out a tiny crack in Frege’s system — a crack that shattered everything.
Russell asked Frege to imagine the set of all sets that do not contain themselves. Most everyday sets are like that: the set of all chairs is not itself a chair, so it does not belong to itself. But now ask: does this new set contain itself? If it does, then by its own definition it must not contain itself. If it does not, then it must contain itself. You get a contradiction either way.
Think of a librarian making a catalog of all catalogs that do not list themselves. Should that very catalog list itself? If it does, it shouldn’t; if it doesn’t, it should. Russell had uncovered a logical loop that made Frege’s rules crumble. The paradox showed that the seemingly innocent idea of “a set of all sets” was explosive.
Frege added a hasty appendix admitting the problem. Russell, for his part, set out to build a logic where such paradoxes could never arise. His answer was a towering new vision: type theory.
Building a Tower of Types
Russell’s first fix was simple but radical: stop treating all objects as if they lived on a single flat plane. Instead, sort them into types arranged in a strict hierarchy.
At the bottom are individuals — concrete things like you, a tree, a particular apple. They are type 0.
One level up, type 1, you get sets of individuals: the set of all apples in a basket, for example.
Type 2 contains sets of sets of individuals — classes of classes.
Type 3 continues upward, and so on forever.
The crucial rule: a set of type n can only contain objects of type n-1. A set can never belong to itself, because that would require it to be of a higher type than itself — which the rules forbid. The looping question “does the set of all sets that don’t contain themselves contain itself?” cannot even be asked. The dangerous set R simply cannot be formed.
Frege had already hinted at something like this with his division between objects and concepts, but Russell made it the backbone of a whole logical system. The tower blocks self‑membership completely. Yet Russell realized there was another kind of circularity hiding in ordinary definitions — and that called for an even more intricate structure.
The Danger of Circular Definitions
Russell wasn’t just afraid of sets that contain themselves. He worried about definitions that sneakily refer to the very thing they are trying to pin down. He called such definitions impredicative.
Imagine saying: “A typical Englishman is one who possesses all the properties possessed by a majority of Englishmen.” To check whether someone is typical, you need to look at all properties — including the property of being typical itself. The definition chases its own tail.
Russell gave a simpler example. Saying “Napoleon was Corsican” is perfectly safe — it names a plain property. But saying “Napoleon had all the qualities of a great general” suddenly drags in a whole collection of qualities. The phrase “all the qualities of a great general” is impredicative: it talks about a totality that already includes whatever quality you are trying to define.
Henri Poincaré (1854–1912) pointed out the same trouble in mathematics. Suppose you define a “number” as anything that satisfies all inductive properties — but then the property “is a number” itself turns out to be one of those inductive properties. You are, again, running in a circle.
To stamp out this circularity, Russell introduced the ramified hierarchy. He didn’t just split objects into types of things (individuals, sets, sets of sets). Inside each type, he further split definitions into orders. A first‑order definition never mentions the totality of its own type. A second‑order definition can mention first‑order totals, but not itself. Third‑order can mention second‑order, and so on.
The result was a dizzying, many‑layered tower where every definition had a precise level. The upside: no vicious circles could ever appear. The downside: simple mathematics became nearly impossible, because even basic ideas like “natural number” splintered into different versions at every order.
A Desperate Shortcut: The Axiom of Reducibility
Russell and his co‑author Alfred North Whitehead wanted to rebuild all of mathematics on type theory. But in the ramified system, you couldn’t even prove that adding two natural numbers of order 2 gave a number of the same order. The whole project threatened to grind to a halt.
Their solution, published in Principia Mathematica, was the Axiom of Reducibility. It declared that for every higher‑order property, there is a completely equivalent first‑order property. In one stroke, the sprawling ramified orders collapsed back into a single level. You could work with first‑order definitions and still get the power of the higher‑order ones.
Critics immediately pounced. Leon Chwistek and Frank Ramsey (1903–1930) argued that if you accept the reducibility axiom, there was never any point in building the ramified hierarchy at all. You might as well stay with the original simple type theory — the basic tower of types without orders — and let impredicative definitions run free. Simple type theory still blocks self‑membership paradoxes, even if it allows some circular-looking definitions.
Russell never liked the axiom; he called it a defect and a pragmatic patch. Yet no one has ever found a contradiction that follows from it. Later, logicians showed that impredicative quantification — the very thing Russell feared — is enormously powerful. It allows you to define Leibniz’s notion of equality (“a equals b if a has all the properties b has”) and the least upper bound of a set of real numbers. Used carefully, impredicativity doesn’t lead to disaster; it just makes logic much, much stronger.
Types in Your Pocket: From Paradox to Programs
Russell’s tower wasn’t just a temporary fix for a logic puzzle. Over the twentieth century, type theory evolved into a practical tool. The logician Alonzo Church (1903–1995) reformulated simple type theory using the λ‑calculus, a compact language for describing functions. In Church’s version, everything has a type: individuals have type i, propositions have type o, and a function from type A to type B has type A → B.
This looks exactly like the type systems inside programming languages you might use today — Python, Java, or Haskell. When a program tries to add a number to a piece of text, the type checker stops it and says “error.” It is enforcing the very rule Russell imagined: a function of one type can’t be applied to an argument of the wrong type. Self‑application, the seed of Russell’s paradox, is ruled out automatically.
But computer scientists also learned how to bend the rules safely. Polymorphism lets you write a function that works over many types at once, like an identity function that returns whatever you give it. That involves a controlled dose of impredicativity — defining a type by quantifying over all types. The French logician Jean‑Yves Girard showed in the 1970s that if you push this too far and add a “type of all types” (a type that belongs to itself!), the system becomes inconsistent — a modern echo of Russell’s paradox. The tower still has a roof.
A New Kind of Equality: The Univalent Revolution
Today, type theory is at the center of a new foundation for mathematics. The Russian mathematician Vladimir Voevodsky (1966–2017) introduced the Univalent Foundations, inspired by the idea that a type can be seen as a space — and equalities between its elements are like paths connecting points.
In this picture, a type is a set if any two equalities between its elements are themselves identical. A type is a groupoid if those equality‑paths behave like a category of symmetries. The hierarchy of types turns into a ladder of ever more complex spaces — sets, groupoids, 2‑groupoids, and so on. Voevodsky’s Axiom of Univalence says that if two types are equivalent (they can be transformed into each other back‑and‑forth), then they are actually equal. This single rule collapses many separate axioms of older set theories into one, and it validates the common mathematical habit of treating isomorphic structures as “the same.”
The thorny issue Russell wrestled with — what can a definition legitimately talk about? — reappears in a new form. In univalent type theory, you can transport any structure along an equivalence without worrying about low‑level encoding details. You never get stuck asking whether the number 0 happens to be an element of a group’s carrier set, because the type system keeps such meaningless questions from even being formed. Russell’s old dream of a logic that enforces the right level of abstraction is alive and well, running inside proof assistants that check real mathematics today.
So next time you watch a compiler catch a type error, or puzzle over the idea that a set could contain itself, you are touching the same threads that Russell, Frege, and Poincaré pulled at more than a century ago. The tower of types isn’t a dusty museum piece — it’s the quiet architecture under a vast part of our digital and mathematical world.
Think about it
- If a library catalog lists every catalog that does not list itself, should it list itself? Can you think of a rule for catalog‑making that avoids this loop without giving up on the idea of a complete list?
- When someone defines “the smallest number that cannot be described in fewer than twenty words,” does the definition actually pick out a number? Why might such a definition feel broken even if you can’t spot an obvious contradiction?
- In a video game, a “type check” might stop you from using a health‑potion slot to hold a sword. Is that restriction similar to Russell’s type theory, or is something different going on?
