Russell's paradox and why sets need axioms

In a certain village there is a barber who shaves exactly those villagers who do not shave themselves. Who shaves the barber?

If the barber shaves himself, then he is one of the people who shave themselves — and the barber shaves none of those. So he does not shave himself. But then he is one of the people who do not shave themselves — and the barber shaves all of those. So he does shave himself. Either way we are stuck.

The way out is simple: there is no such village. The description "a barber who shaves exactly those who do not shave themselves" describes nobody, just as "a square circle" describes nothing.

That would be a mere puzzle, except for what happened in 1901. Bertrand Russell noticed that the same reasoning applies to a principle about sets that mathematicians had been using freely — and that Gottlob Frege had made a cornerstone of his attempt to build all of mathematics on logic. Russell himself later used the barber, in lectures given in 1918, as a popular illustration of his discovery. This lesson tells what he found, and how mathematics recovered.

We describe sets by properties all the time: $\{n \in \N : n \text{ is even}\}$, the set of solutions of an equation, the set of points at distance $1$ from the origin. It is tempting to believe that any property defines a set — the set of all things having that property.

Sets can be elements of other sets: $\{\{1, 2\}, \{3\}\}$ has two elements, each a set. So we can ask of a set $x$ whether it is an element of itself, $x \in x$. For familiar sets the answer is no: the set of all triangles is not a triangle, and $\{1, 2\}$ is not an element of $\{1, 2\}$. But if every property defined a set, there would be a set of all sets, and it would be an element of itself.

Now consider the property "$x$ is not an element of itself". It looks harmless; most sets have it. What could go wrong with the set of all of them?

Separation looks like a cautious version of comprehension: it only carves subsets out of a set we already have. As we shall see, that caution is exactly what is needed. A collection described by a property, which may or may not be a set, is informally called a class.

At the heart of everything is a tiny fact of logic.

In truth-table terms, $p \leftrightarrow \neg p$ is false in both rows: it is a contradiction. (You can check this in the explorer below.)

That is the whole argument. Its strength is its generality: it does not matter what the objects are or what $E$ means.

• If the objects are villagers and $x \mathrel{E} y$ means "$y$ shaves $x$", Theorem 2 says no villager $r$ shaves exactly those who do not shave themselves: there is no such barber.
• If the objects are sets and $x \mathrel{E} y$ means $x \in y$, Theorem 2 says that no set $R$ has as its elements exactly the sets that are not elements of themselves.

So naive comprehension cannot be part of a consistent theory of sets: a theory that proves a contradiction proves everything, and is useless. What should replace it?

Notice what changed. Naive comprehension forced the Russell set to exist and to be one of the things it was talking about. Separation lets us build the Russell set inside $A$ — and the argument, instead of a contradiction, now proves a theorem: $R_A$ is something outside $A$.

The collection of all sets is a perfectly good class, but it is too big to be a set. Halmos summed this up in his textbook as "nothing contains everything".

This is no coincidence: Russell found his paradox by thinking about Cantor's proof that there is no largest set (see countability). If there were a set $U$ of all sets, then $\mathcal{P}(U) \subseteq U$, so $U$ would be at least as large as its own power set — contradicting Cantor's theorem. Following Cantor's diagonal set for this situation leads straight to Russell's set.

After Russell's discovery mathematicians took two main routes.

Ernst Zermelo (1908) listed explicit axioms saying which sets exist, with separation in place of comprehension. With later additions by Abraham Fraenkel and Thoralf Skolem (the replacement axiom, 1922) and the axiom of choice, these became ZFC, the standard foundation of mathematics today. Informally:

Every set that ordinary mathematics needs — $\N$, $\R$, the set of continuous functions, $\{x \in \R : x^2 < 2\}$ — is built from these, and separation is always applied inside a set we already have. The details are in ZFC.

Russell himself took a different route: the theory of types (1908), developed with Alfred North Whitehead in Principia Mathematica (1910–1913). Objects come in levels — individuals, sets of individuals, sets of sets of individuals, … — and a set may only contain objects of the level just below. Then "$x \in x$" is not false but meaningless, so the Russell set cannot even be described. Modern type theories, including the one behind the Lean proof assistant, descend in part from this idea; see type theory.

Other approaches exist too. Von Neumann–Bernays–Gödel set theory speaks officially about classes, and calls those too big to be sets proper classes; Willard Van Orman Quine's New Foundations (1937) restricts comprehension in another way and, remarkably, does contain a universal set.

The step "$R \in R \iff R \notin R$" has the propositional form $r \leftrightarrow \neg r$. Look at its truth table:

In ZFC, sets are built in stages from the empty set. Build some below. Notice that a box is only ever put into a new box — no box can end up inside itself.

Things to try:

• Build $\{\varnothing, \{\varnothing\}\}$. For this set $A$, what is $R_A = \{x \in A : x \notin x\}$? (Since no box contains itself, $R_A$ is all of $A$ — and $A$ is not inside $A$, just as Theorem 4 says.)
• Can you build a box that contains every box on the shelf? It is always a new box, not on the shelf before — a finite shadow of Corollary 5.

The logical core is short, and constructive: the proof of $\neg(p \leftrightarrow \neg p)$ uses no law of excluded middle.

/-- **No statement is equivalent to its own negation.** If `p ↔ ¬p`, then assuming `p` gives `¬p`,
so `p` is refuted; but then `¬p` gives `p`. This proof is constructive. -/
theorem not_iff_not_self (p : Prop) : ¬ (p ↔ ¬ p) := by
  intro h
  have hnp : ¬ p := fun hp => h.mp hp hp
  exact hnp (h.mpr hnp)

/-- The same fact in core Lean: `iff_not_self`. -/
theorem not_iff_not_self_library (p : Prop) : ¬ (p ↔ ¬ p) := iff_not_self

Theorem 2 for an arbitrary relation E on an arbitrary type α, and the barber as a special case:

/-- **Russell's theorem, in pure logic.** For any relation `E` on any type, there is no `r` whose
"members" are exactly the things that are not members of themselves: taking `x = r` would give
`r E r ↔ ¬ (r E r)`. -/
theorem no_russell_relation {α : Type*} (E : α → α → Prop) :
    ¬ ∃ r, ∀ x, E x r ↔ ¬ E x x := by
  rintro ⟨r, hr⟩
  exact not_iff_not_self (E r r) (hr r)

/-- **The barber.** In no village is there a barber who shaves exactly those villagers who do not
shave themselves. This is `no_russell_relation` for the relation "`y` shaves `x`". The barber is not
a paradox: it simply proves that such a barber does not exist. -/
theorem no_barber {Person : Type*} (shaves : Person → Person → Prop) :
    ¬ ∃ b, ∀ p, shaves b p ↔ ¬ shaves p p :=
  no_russell_relation (fun x y => shaves y x)

Naive comprehension, stated as a hypothesis about a membership relation, proves False:

/-- **Naive comprehension is inconsistent.** Suppose a membership relation `mem` had the property
that every predicate `P` is the membership predicate of some "set" `s`. Applying this to
`P x := ¬ mem x x` produces a Russell set, which `no_russell_relation` forbids. -/
theorem naive_comprehension_inconsistent {α : Type*} (mem : α → α → Prop)
    (comprehension : ∀ P : α → Prop, ∃ s, ∀ x, mem x s ↔ P x) : False :=
  no_russell_relation mem (comprehension fun x => ¬ mem x x)

/-- **Separation blocks the paradox.** In Mathlib's model of ZFC, for every set `A` the Russell
set *inside `A`*, `R = {x ∈ A | x ∉ x}` (built with the separation axiom `ZFSet.sep`), is not an
element of `A`. If it were, then `R ∈ R ↔ (R ∈ A ∧ R ∉ R) ↔ R ∉ R`. Only `ZFSet.mem_sep` is used —
not the axiom of foundation. -/
theorem russell_sep_not_mem (A : ZFSet) : ZFSet.sep (fun x => x ∉ x) A ∉ A := by
  intro hA
  -- `h : R ∈ R ↔ R ∈ A ∧ R ∉ R`, where `R` is the Russell set inside `A`.
  have h := ZFSet.mem_sep (p := fun x => x ∉ x) (x := A) (y := ZFSet.sep (fun x => x ∉ x) A)
  exact not_iff_not_self _ ⟨fun hRR => (h.mp hRR).2, fun hRR => h.mpr ⟨hA, hRR⟩⟩

/-- **There is no set of all sets.** If `U` contained every set, it would contain its own Russell
set `{x ∈ U | x ∉ x}`, contradicting `russell_sep_not_mem`. -/
theorem no_universal_set : ¬ ∃ U : ZFSet, ∀ x, x ∈ U := by
  rintro ⟨U, hU⟩
  exact russell_sep_not_mem U (hU _)

In ZFC, the axiom of foundation also implies that no set is an element of itself. Mathlib proves it — but our proofs above never used it, which is the point of the third misconception below. With foundation, the Russell set inside $A$ is just $A$.

/-- In ZFC no set is a member of itself — Mathlib's `ZFSet.mem_irrefl`, which comes from the axiom
of foundation (Mathlib proves that membership of `ZFSet`s is well-founded). The paradox is *not*
avoided this way: `russell_sep_not_mem` never used this fact. -/
theorem mem_irrefl (x : ZFSet) : x ∉ x := ZFSet.mem_irrefl x

/-- With foundation, the Russell set inside `A` is `A` itself: every element `x` of `A` satisfies
`x ∉ x`. So `russell_sep_not_mem` then says simply `A ∉ A`. -/
theorem russell_sep_eq_self (A : ZFSet) : ZFSet.sep (fun x => x ∉ x) A = A := by
  ext x
  rw [ZFSet.mem_sep]
  exact ⟨fun h => h.1, fun h => ⟨h, mem_irrefl x⟩⟩

Cantor's theorem, derived from Russell's (Theorem 6):

/-- **Cantor's theorem is Russell's argument in disguise.** For `f : α → Set α`, read `x ∈ f y` as
"`x` is a member of `y`". A surjective `f` would hit the diagonal set `{x | x ∉ f x}` at some `r`,
and that `r` would be a Russell element for this relation. -/
theorem cantor_of_russell {α : Type*} (f : α → Set α) : ¬ Function.Surjective f := by
  intro hf
  obtain ⟨r, hr⟩ := hf {x | x ∉ f x}
  apply no_russell_relation (fun x y => x ∈ f y)
  refine ⟨r, fun x => ?_⟩
  rw [hr]
  rfl

Finally, types. In Lean, a set of elements of type α has type Set α. The set of all elements of α exists — but it lives one level up, so asking whether it is a member of itself is not false but ill-typed: Lean would reject Set.univ ∈ Set.univ before any proof starts.

/-- **In type theory a "set of everything" is harmless.** For each type `α` there is a set
containing every element of `α` — `Set.univ` — but it has type `Set α`, so it is not itself an
element of `α`, and the question "is it a member of itself?" cannot be asked. -/
theorem typed_universe (α : Type*) : ∃ U : Set α, ∀ x : α, x ∈ U :=
  ⟨Set.univ, fun _ => trivial⟩

"""Russell's argument as a finite search.

Russell's paradox rests on a fact of pure logic: for any relation E on any
collection, no r has  x E r  <->  not (x E x)  for every x.  Here we test that
fact exhaustively on every relation on a set of at most 4 elements, reading
"x E y" as "x is a member of y" (or as "y shaves x"). The proof says why it
must fail: the candidate r disagrees with the Russell set at r itself.

Then we build the hereditarily finite sets V_0, ..., V_4 (sets of sets of ...
of the empty set; |V_4| = 16) and check that for every A among them the set
R_A = {x in A : x not in x} produced by the separation axiom is not an element
of A. (In fact no hereditarily finite set is a member of itself, so R_A is A.)

Runs unchanged in the browser (Pyodide) using only the standard library.
"""

from itertools import combinations, product

def relations(n):
    """All relations on {0, ..., n-1}, as frozensets of pairs (x, y) meaning
    'x E y'."""
    pairs = [(x, y) for x in range(n) for y in range(n)]
    for mask in product([False, True], repeat=len(pairs)):
        yield frozenset(p for p, keep in zip(pairs, mask) if keep)

def russell_set(rel, n):
    """{x : not (x E x)}."""
    return frozenset(x for x in range(n) if (x, x) not in rel)

def members(rel, r, n):
    """{x : x E r}."""
    return frozenset(x for x in range(n) if (x, r) in rel)

def russell_witnesses(rel, n):
    """All r whose members are exactly the Russell set (always empty)."""
    target = russell_set(rel, n)
    return [r for r in range(n) if members(rel, r, n) == target]

def search(n):
    """(number of relations on n elements, number with a Russell witness)."""
    count = found = 0
    for rel in relations(n):
        count += 1
        found += bool(russell_witnesses(rel, n))
    return count, found

def hereditarily_finite(levels):
    """V_0 = {} and V_(k+1) = all subsets of V_k, as frozensets of frozensets.
    Returns the list [V_0, ..., V_levels]."""
    v = [frozenset()]
    for _ in range(levels):
        prev = sorted(v[-1], key=id_of)
        subsets = [frozenset(c) for k in range(len(prev) + 1)
                   for c in combinations(prev, k)]
        v.append(frozenset(subsets))
    return v

def id_of(s):
    """A canonical string for a hereditarily finite set, e.g. {{}, {{}}}."""
    return "{" + ", ".join(sorted(id_of(x) for x in s)) + "}"

def separated_russell(a):
    """R_A = {x in A : x not in x}, formed by separation inside A."""
    return frozenset(x for x in a if x not in x)

def main():
    print("n  relations on n elements  with a 'Russell element' r")
    total = 0
    for n in range(1, 5):
        count, found = search(n)
        total += count
        print(f"{n}  {count:23d}  {found:28d}")
    print(f"Checked {total} relations: no r ever has x E r <-> not x E x.")
    print()
    v = hereditarily_finite(4)
    print("Hereditarily finite sets: |V_k| for k = 0..4:",
          ", ".join(str(len(level)) for level in v))
    sets = v[4]
    self_members = sum(1 for a in sets if a in a)
    r_not_in = sum(1 for a in sets if separated_russell(a) not in a)
    equal = sum(1 for a in sets if separated_russell(a) == a)
    print(f"Sets A in V_4 with A in A: {self_members}")
    print(f"Sets A in V_4 with R_A not in A: {r_not_in} of {len(sets)}")
    print(f"... and R_A = A (nothing in A contains itself): {equal} of {len(sets)}")
    print("Example: A = " + id_of(max(sets, key=len)))
    print()
    print("Epistemic status: an exhaustive check of finitely many relations and")
    print("sets. It cannot reach infinite collections; the one-line proof in")
    print("the lesson covers every relation on every collection, finite or not.")

if __name__ == "__main__":
    main()

No relation has a Russell element, exactly as Theorem 2 predicts — but notice how much weaker this evidence is than the proof. The search covers sixty-six thousand relations; the four-line proof covers every relation on every collection, finite or infinite, including the membership relation of all sets.

• Self-reference is old. The liar paradox ("what I am saying now is false") is attributed to Eubulides of Miletus in the 4th century BCE. In China, the Later Mohist canons (around 300 BCE) observed that the claim "all saying is contradictory" contradicts itself. These are cousins of Russell's paradox, not the same argument.
• Warning signs. Cesare Burali-Forti (1897) found a contradiction in the idea of the set of all ordinal numbers, and Georg Cantor, in letters to Richard Dedekind (1899), distinguished "consistent multiplicities" (sets) from "inconsistent" ones, such as the totality of everything.
• Frege and Russell. Gottlob Frege's Basic Laws of Arithmetic (volume 1, 1893) derived arithmetic from logic using a principle (his Basic Law V) that implies naive comprehension. Bertrand Russell discovered the contradiction in 1901 while studying Cantor's proof that there is no largest cardinal, and wrote to Frege on 16 June 1902, as volume 2 was going to press. Frege replied within days that it had shaken the basis on which he intended to build arithmetic, and added an appendix about it to volume 2 (1903). Ernst Zermelo had found the same contradiction independently, around 1900, but did not publish it.
• Repairs. Russell's theory of types (1908) and Principia Mathematica with Alfred North Whitehead (1910–1913); Zermelo's axioms (1908); replacement, added by Abraham Fraenkel and Thoralf Skolem (1922); John von Neumann's treatment of classes (1925). Together these shaped the foundations used today.

• Paul R. Halmos, Naive Set Theory (1960), section 2, "The axiom of specification", including "nothing contains everything".
• Herbert B. Enderton, Elements of Set Theory (1977), chapter 1 and the axioms of chapter 2.
• Jean van Heijenoort (editor), From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931 (1967), which contains Russell's letter to Frege and Frege's reply.
• Apostolos Doxiadis and Christos H. Papadimitriou, Logicomix (2009), a graphic novel about Russell's search for foundations.