ZFC: axiomatic set theory

In 1902 Gottlob Frege was finishing the second volume of his Basic Laws of Arithmetic, a book that derived arithmetic from logic. One of his basic laws said, in modern words, that every property determines a set: for any condition $\varphi(x)$ there is a set $\{x \mid \varphi(x)\}$ of exactly the things satisfying it. A letter from Bertrand Russell showed that this law is contradictory. Take $\varphi(x)$ to be $x \notin x$ and let $R = \{x \mid x \notin x\}$. Then

The lesson on Russell's paradox explored what went wrong. This lesson is about the repair that most mathematicians use today: Zermelo–Fraenkel set theory with the axiom of Choice, or ZFC. Instead of "every property determines a set", ZFC lists a handful of precise ways of building new sets from old ones. Each of them is safe enough that no paradox has been found in more than a century of intensive use, and together they are strong enough to build essentially all of the mathematics in the other lessons of this curriculum — numbers, functions, groups, spaces, measures.

ZFC is written in the language of first-order logic, with a single non-logical symbol: the membership relation $\in$. By the end of this lesson you will know each axiom, why it is there, how pairs, functions and numbers become sets, and what it does and does not mean to say that a theorem "follows from ZFC".

A helpful picture, called the iterative conception of set, is that sets are formed in stages. At stage $0$ there is nothing to collect, so the only set we can form is the empty set. At each later stage we may form any collection of sets formed at earlier stages. Write $V_\alpha$ for the sets available before stage $\alpha$:

So $V_1 = \{\varnothing\}$, $V_2 = \{\varnothing, \{\varnothing\}\}$, and $V_3$ has four elements. The finite stages grow as towers of powers of two: $|V_{n+1}| = 2^{|V_n|}$, so $|V_4| = 16$ and $|V_5| = 65536$. After all finite stages comes the stage $V_\omega$, the set of hereditarily finite sets, and the process continues through the transfinite ordinals.

The axioms of ZFC can be read as describing what the stages make possible. Pairing and Union say that sets available by some stage can be combined; Power set says that all subsets of a set form a set; Separation says we may cut out a subset by a property; Replacement says that if we can index sets by the elements of a set, the stages they appear at are bounded; Infinity says there is a stage after all finite ones; Foundation says every set appears at some stage. The picture is a heuristic, not part of the theory — the theory is the list of axioms below — but it explains why the axioms look the way they do, and why Russell's $R$ is not a set: there is no stage at which "all sets that are not members of themselves" could be collected, because new such sets keep appearing.

The language of set theory has variables (ranging over sets), the logical symbols $\neg, \land, \lor, \to, \leftrightarrow, \forall, \exists, =$, and one binary relation symbol $\in$. Everything else is an abbreviation: $x \subseteq y$ abbreviates $\forall z\,(z \in x \to z \in y)$, and $\forall z \in x\ \psi$ abbreviates $\forall z\,(z \in x \to \psi)$.

Axioms 7 and 9 use abbreviations ($\varnothing$, $y \cup \{y\}$, "function") that are themselves defined from $\in$ using earlier axioms; each can be expanded into a formula of the bare language. Two remarks on the list:

• Schemas. Separation and Replacement are infinite lists of axioms, one per formula. First-order logic cannot quantify over "all properties", so this is how a first-order theory says "for every property". Richard Montague proved in 1961 that this is unavoidable: if ZF is consistent, no finite list of its theorems implies all of ZF.
• Separation is not comprehension. Separation only lets us form $\{z \in x \mid \varphi\}$, the members of an existing set $x$ with property $\varphi$. Frege's contradictory law formed $\{z \mid \varphi\}$ out of nothing.

The same pattern — Separation to show a set exists, Extensionality to show it is unique — gives the intersection $a \cap b = \{z \in a \mid z \in b\}$ and the difference $a \setminus b = \{z \in a \mid z \notin b\}$; the union $a \cup b = \bigcup\{a, b\}$ uses Pairing and Union.

The proof uses only Separation, and it does not need the law of excluded middle (from $P \leftrightarrow \neg P$ one derives $\neg P$, and then $P$). It turns Russell's paradox into a theorem: collections such as "all sets", "all groups" or "all topological spaces" are not sets. One can still talk about them — "$x$ is a group" is a formula — and set theorists call such definable collections classes; a class that is not a set is a proper class.

The same argument rules out cycles $x_1 \in x_2 \in \cdots \in x_n \in x_1$ of any length (apply Foundation to $\{x_1, \dots, x_n\}$), and infinite descending chains $\cdots \in x_2 \in x_1 \in x_0$ given by a function on $\omega$ (apply Foundation to its set of values). The converse — that the absence of descending chains implies Foundation — needs the axiom of dependent choice.

Ordinary mathematics talks about ordered pairs, relations, functions and numbers. In ZFC each of these must be a set. The point is not that a pair "really is" a set, but that some set-theoretic construction has exactly the properties we use.

Ordered pairs

The only property of ordered pairs that mathematics ever uses is that $(a, b) = (c, d)$ exactly when $a = c$ and $b = d$.

Not every encoding works. With $\langle a, b \rangle = \{a, \{b\}\}$, the pairs $\langle \{d\}, b \rangle$ and $\langle \{b\}, d \rangle$ are both $\{\{b\}, \{d\}\}$, so for $b \neq d$ two different pairs collide; the computation section finds such collisions among the sets of $V_4$.

Products, relations and functions

A relation from $A$ to $B$ is a subset $R \subseteq A \times B$. A function $f : A \to B$ is a relation such that for every $a \in A$ there is exactly one $b$ with $(a, b) \in f$; we write $f(a)$ for that $b$. The set of all functions from $A$ to $B$ is $B^A = \{f \in \mathcal P(A \times B) \mid f \text{ is a function from } A \text{ to } B\}$. Domains and ranges are cut out of $\bigcup\bigcup R$ by Separation, because $a \in \{a\} \in (a, b)$. An equivalence relation on $A$ is a subset of $A \times A$ with the usual properties, and the set of its equivalence classes is a subset of $\mathcal P(A)$.

The natural numbers

Infinity provides an inductive set $I$. Define $\omega = \{n \in I \mid n \in J \text{ for every inductive set } J\}$ by Separation. Then $\omega$ is inductive and is contained in every inductive set; by Extensionality it does not depend on which $I$ we started from.

(Foundation is convenient here but not essential: by induction one proves that every $n \in \omega$ is transitive — every element of $n$ is a subset of $n$ — and that $n \notin n$, and these facts give (b) in ZF without Foundation.) So in ZFC the order of the natural numbers is membership: $m < n$ means $m \in n$. Addition and multiplication are then defined by recursion, $m + 0 = m$, $m + S(n) = S(m + n)$, using the recursion theorem on $\omega$, whose proof builds the graph of $+$ as a set by Separation from $\omega \times \omega \times \omega$.

From here the familiar number systems follow one after another: $\Z$ as equivalence classes of pairs $(m, n) \in \omega \times \omega$ (thought of as $m - n$), $\Q$ as equivalence classes of pairs of integers, $\R$ as Dedekind cuts — certain subsets of $\Q$, so $\R \subseteq \mathcal P(\Q)$ needs Power set — and $\C = \R \times \R$. A topological space is a pair $(X, \tau)$ with $\tau \subseteq \mathcal P(X)$; a group is a set with a function $G \times G \to G$. All of these objects live at stages of the hierarchy below $V_{\omega + \omega}$.

There are two very different kinds of statement here.

A theorem of ZFC is a sentence $\sigma$ with $\mathrm{ZFC} \vdash \sigma$: there is a formal derivation of $\sigma$ from finitely many axioms. "There is no universal set", "every vector space has a basis" and "every continuous function on $[0, 1]$ attains a maximum" are theorems of ZFC. Mathematicians rarely write formal derivations, but the theorems of the analysis, algebra and topology lessons could be — and, increasingly, are, in proof assistants built on related foundations.

The consistency of ZFC is the statement $\mathrm{Con}(\mathrm{ZFC})$: no derivation from the axioms ends in a contradiction, such as $\exists x\,(x \neq x)$. Because derivations are finite strings of symbols, this can be written as a sentence about natural numbers, and so as a sentence of set theory. Can ZFC prove it?

The proof is beyond this lesson (see Gödel's incompleteness theorems); it applies to every consistent, effectively axiomatised theory that contains a modest amount of arithmetic. So the consistency of ZFC is not something ZFC can establish about itself. It is assumed — on the evidence of more than a century of intensive use without contradiction and of the intuitive picture of the hierarchy — not proved.

What can be proved are relative consistency results, theorems of the form "if $T$ is consistent, then so is $T'$":

• Kurt Gödel (1938) showed that if ZF is consistent, so is ZFC together with the generalised continuum hypothesis, by building inside any model of ZF the constructible universe $L$.
• Paul Cohen (1963) invented forcing and showed that if ZF is consistent, so are ZF + $\neg$AC and ZFC + $\neg$CH. See the axiom of choice and forcing.

Lean is not built on ZFC. Its foundation is a dependent type theory (see type theory), in which every object has a type and "$2 \in 3$" is not even a well-formed question about natural numbers. Nevertheless Mathlib constructs a model of ZFC inside Lean. A pre-set is a well-founded tree — a type $\alpha$ together with a family of pre-sets indexed by $\alpha$ — and ZFSet is the type of pre-sets up to extensional equivalence. Mathlib then proves, about ZFSet, statements corresponding to each axiom. We restate them in the form a set theorist writes them:

/-- **Extensionality.** Two sets with the same elements are equal.
This applies Mathlib's `ZFSet.ext`. -/
theorem extensionality (x y : ZFSet.{u}) (h : ∀ z, z ∈ x ↔ z ∈ y) : x = y :=
  ZFSet.ext h

/-- **Pairing.** For any `a` and `b` there is a set `{a, b}` whose elements are exactly `a` and
`b`. This applies Mathlib's `ZFSet.mem_pair`. -/
theorem pairing (a b : ZFSet.{u}) : ∃ p : ZFSet.{u}, ∀ z, z ∈ p ↔ z = a ∨ z = b :=
  ⟨{a, b}, fun _ => ZFSet.mem_pair⟩

/-- **Union.** For every set `x` there is a set `⋃ x` whose elements are the elements of the
elements of `x`. This applies Mathlib's `ZFSet.mem_sUnion`. -/
theorem union (x : ZFSet.{u}) : ∃ v : ZFSet.{u}, ∀ z, z ∈ v ↔ ∃ y ∈ x, z ∈ y :=
  ⟨ZFSet.sUnion x, fun _ => ZFSet.mem_sUnion⟩

/-- **Power set.** For every set `x` there is a set `𝒫 x` whose elements are exactly the subsets
of `x`. This applies Mathlib's `ZFSet.mem_powerset`. -/
theorem power_set (x : ZFSet.{u}) : ∃ p : ZFSet.{u}, ∀ z, z ∈ p ↔ z ⊆ x :=
  ⟨ZFSet.powerset x, fun _ => ZFSet.mem_powerset⟩

/-- **Separation.** For every set `x` and every property `φ` there is a set
`{z ∈ x | φ z}`. In first-order ZFC this is a *schema*, one axiom for each formula `φ`; in Lean
it is a single statement quantifying over all predicates. This applies `ZFSet.mem_sep`. -/
theorem separation (φ : ZFSet.{u} → Prop) (x : ZFSet.{u}) :
    ∃ s : ZFSet.{u}, ∀ z, z ∈ s ↔ z ∈ x ∧ φ z :=
  ⟨ZFSet.sep φ x, fun _ => ZFSet.mem_sep⟩

/-- **Replacement.** The image of a set under any operation `F` is a set:
`{F w | w ∈ x}`. Like Separation, this is a schema in first-order ZFC. This applies Mathlib's
`ZFSet.range` and `ZFSet.mem_range` (a set indexed by the elements of `x` is a set). -/
theorem replacement (F : ZFSet.{u} → ZFSet.{u}) (x : ZFSet.{u}) :
    ∃ r : ZFSet.{u}, ∀ z, z ∈ r ↔ ∃ w ∈ x, F w = z := by
  refine ⟨ZFSet.range (fun w : x => F w), fun z => ?_⟩
  rw [ZFSet.mem_range]
  constructor
  · rintro ⟨⟨w, hw⟩, rfl⟩
    exact ⟨w, hw, rfl⟩
  · rintro ⟨w, hw, rfl⟩
    exact ⟨⟨w, hw⟩, rfl⟩

/-- **Infinity.** There is a set containing `∅` and closed under `y ↦ y ∪ {y}`; Mathlib's `ω`
(`ZFSet.omega`) is one. This applies `ZFSet.omega_zero` and `ZFSet.omega_succ`. -/
theorem infinity :
    ∅ ∈ ZFSet.omega.{u} ∧ ∀ y ∈ ZFSet.omega.{u}, insert y y ∈ ZFSet.omega.{u} :=
  ⟨ZFSet.omega_zero, fun _ hy => ZFSet.omega_succ hy⟩

/-- **Foundation (Regularity).** Every non-empty set `x` has an element `y` that shares no
element with `x`: an `∈`-minimal element. This applies Mathlib's `ZFSet.regularity`. -/
theorem foundation (x : ZFSet.{u}) (h : x ≠ ∅) : ∃ y ∈ x, x ∩ y = ∅ :=
  ZFSet.regularity x h

/-- **Choice**, in its set-theoretic form: if `x` is a set of non-empty sets, there is a
function — itself a set of ordered pairs — from `x` to `⋃ x`. Mathlib's `ZFSet.choice x`
(built from Lean's own choice principle) is one, and it picks `f(y) ∈ y` (`ZFSet.choice_cmem`).
This applies `ZFSet.choice_isFunc`. -/
theorem choice (x : ZFSet.{u}) (h : ∅ ∉ x) : ∃ f : ZFSet.{u}, ZFSet.IsFunc x (ZFSet.sUnion x) f :=
  ⟨ZFSet.choice x, ZFSet.choice_isFunc x h⟩

Notice how the schemas become single statements: Lean's higher-order logic quantifies over all predicates φ : ZFSet → Prop, including ones no first-order formula defines. That makes ZFSet satisfy every instance of the first-order schemas and more.

From these facts, used exactly as axioms, we prove the theorems of this lesson. Russell's argument, using Separation only:

/-- **There is no set of all sets.** If `U` contained every set, Separation would give
`R = {x ∈ U | x ∉ x}`, and then `R ∈ R ↔ R ∉ R`: Russell's paradox. Only Separation is used
(Foundation would give a different, shorter proof). -/
theorem no_universal_set : ¬ ∃ U : ZFSet.{u}, ∀ x, x ∈ U := by
  rintro ⟨U, hU⟩
  -- Separation: the members of `U` that are not members of themselves.
  obtain ⟨R, hR⟩ := separation (fun x => x ∉ x) U
  have key : R ∈ R ↔ R ∉ R :=
    (hR R).trans ⟨fun h => h.2, fun h => ⟨hU R, h⟩⟩
  -- A statement equivalent to its own negation is contradictory (no excluded middle needed).
  have hnot : R ∉ R := fun h => key.mp h h
  exact hnot (key.mpr hnot)

Kuratowski pairs, with the two-step proof from the lesson:

/-- The **Kuratowski ordered pair** `(a, b) = {{a}, {a, b}}`. It is the same set as Mathlib's
`ZFSet.pair a b`. -/
def kpair (a b : ZFSet.{u}) : ZFSet.{u} :=
  {{a}, {a, b}}

/-- **The characteristic property of ordered pairs**, proved as in the lesson.
If `{{a}, {a, b}} = {{c}, {c, d}}` then:
1. `{a}` is `{c}` or `{c, d}`; either way `c ∈ {a}`, so `a = c`.
2. If `b = a`, the left side is `{{a}}`, so `{c, d} = {a}` and `d = a = b`.
3. If `b ≠ a`, then `{a, b}` is not a singleton, so `{a, b} = {c, d} = {a, d}` and `b = d`. -/
theorem kpair_inj {a b c d : ZFSet.{u}} (h : kpair a b = kpair c d) : a = c ∧ b = d := by
  -- Membership in the two pairs, by Extensionality and Pairing.
  have mem : ∀ z : ZFSet.{u}, (z = {a} ∨ z = {a, b}) ↔ (z = {c} ∨ z = {c, d}) := by
    intro z
    rw [← ZFSet.mem_pair, ← ZFSet.mem_pair]
    exact Iff.of_eq (congrArg (z ∈ ·) h)
  -- Step 1: `a = c`.
  have hac : a = c := by
    rcases (mem {a}).mp (Or.inl rfl) with h1 | h1
    · exact ZFSet.singleton_inj.mp h1
    · have hc : c ∈ ({a} : ZFSet.{u}) := by rw [h1]; exact ZFSet.mem_pair.mpr (Or.inl rfl)
      exact (ZFSet.mem_singleton.mp hc).symm
  refine ⟨hac, ?_⟩
  rw [← hac] at mem
  -- Step 2: `b = d`, splitting on whether `b = a`.
  by_cases hba : b = a
  · -- Then `{c, d} = {a, d}` is `{a}` or `{a, b} = {a}`; either way `d ∈ {a, b}`.
    rcases (mem {a, d}).mpr (Or.inr rfl) with h2 | h2
    · have hd : d ∈ ({a} : ZFSet.{u}) := by rw [← h2]; exact ZFSet.mem_pair.mpr (Or.inr rfl)
      rw [hba, ZFSet.mem_singleton.mp hd]
    · have hd : d ∈ ({a, b} : ZFSet.{u}) := by rw [← h2]; exact ZFSet.mem_pair.mpr (Or.inr rfl)
      rcases ZFSet.mem_pair.mp hd with h3 | h3
      · rw [hba, h3]
      · exact h3.symm
  · -- `{a, b}` is `{a}` (impossible, as `b ≠ a`) or `{a, d}`.
    rcases (mem {a, b}).mp (Or.inr rfl) with h2 | h2
    · have hb : b ∈ ({a} : ZFSet.{u}) := by rw [← h2]; exact ZFSet.mem_pair.mpr (Or.inr rfl)
      exact absurd (ZFSet.mem_singleton.mp hb) hba
    · have hb : b ∈ ({a, d} : ZFSet.{u}) := by rw [← h2]; exact ZFSet.mem_pair.mpr (Or.inr rfl)
      rcases ZFSet.mem_pair.mp hb with h3 | h3
      · exact absurd h3 hba
      · exact h3

/-- Kuratowski pairs are equal **exactly** when their components are: the converse direction of
`kpair_inj` is immediate. -/
theorem kpair_eq_iff {a b c d : ZFSet.{u}} : kpair a b = kpair c d ↔ a = c ∧ b = d := by
  constructor
  · exact kpair_inj
  · rintro ⟨rfl, rfl⟩
    rfl

Mathlib's own ZFSet.pair is the same set, and Mathlib proves the same property:

/-- The same fact for Mathlib's `ZFSet.pair` (which is `{{a}, {a, b}}` too), by `ZFSet.pair_inj`. -/
theorem pair_inj_library {a b c d : ZFSet.{u}} : ZFSet.pair a b = ZFSet.pair c d ↔ a = c ∧ b = d :=
  ZFSet.pair_inj

The consequences of Foundation:

/-- **No set is a member of itself.** If `x ∈ x`, apply Foundation to `{x}`: its only element
`x` must be disjoint from `{x}`, but `x ∈ {x} ∩ x`. (Mathlib: `ZFSet.mem_irrefl`.) -/
theorem not_mem_self (x : ZFSet.{u}) : x ∉ x := by
  intro hx
  have hne : ({x} : ZFSet.{u}) ≠ ∅ := fun h =>
    ZFSet.notMem_empty x (h ▸ ZFSet.mem_singleton.mpr rfl)
  obtain ⟨y, hy, hdisj⟩ := foundation {x} hne
  rw [ZFSet.mem_singleton.mp hy] at hdisj
  have hin : x ∈ ({x} : ZFSet.{u}) ∩ x := ZFSet.mem_inter.mpr ⟨ZFSet.mem_singleton.mpr rfl, hx⟩
  rw [hdisj] at hin
  exact ZFSet.notMem_empty x hin

/-- **There are no 2-cycles `x ∈ y ∈ x`.** Apply Foundation to `{x, y}`. If its `∈`-minimal
element is `x`, then `y ∈ {x, y} ∩ x`; if it is `y`, then `x ∈ {x, y} ∩ y`. Either way the
intersection is not empty. -/
theorem no_two_cycle (x y : ZFSet.{u}) : ¬ (x ∈ y ∧ y ∈ x) := by
  rintro ⟨hxy, hyx⟩
  have hx : x ∈ ({x, y} : ZFSet.{u}) := ZFSet.mem_pair.mpr (Or.inl rfl)
  have hy : y ∈ ({x, y} : ZFSet.{u}) := ZFSet.mem_pair.mpr (Or.inr rfl)
  have hne : ({x, y} : ZFSet.{u}) ≠ ∅ := fun h => ZFSet.notMem_empty x (h ▸ hx)
  obtain ⟨z, hz, hdisj⟩ := foundation {x, y} hne
  rcases ZFSet.mem_pair.mp hz with rfl | rfl
  · have hin : y ∈ ({z, y} : ZFSet.{u}) ∩ z := ZFSet.mem_inter.mpr ⟨hy, hyx⟩
    rw [hdisj] at hin
    exact ZFSet.notMem_empty y hin
  · have hin : x ∈ ({x, z} : ZFSet.{u}) ∩ z := ZFSet.mem_inter.mpr ⟨hx, hxy⟩
    rw [hdisj] at hin
    exact ZFSet.notMem_empty x hin

And the von Neumann natural numbers: the successor, its injectivity, and the facts that $n = \{0, \dots, n - 1\}$, that the numerals lie in $\omega$, and that their order is membership:

/-- The von Neumann **successor** `x ∪ {x}`, written `insert x x` in Mathlib. -/
def succ (x : ZFSet.{u}) : ZFSet.{u} :=
  insert x x

/-- `y ∈ x ∪ {x}` exactly when `y = x` or `y ∈ x`. This applies `ZFSet.mem_insert_iff`. -/
theorem mem_succ {x y : ZFSet.{u}} : y ∈ succ x ↔ y = x ∨ y ∈ x :=
  ZFSet.mem_insert_iff

/-- **The successor operation is injective.** If `x ∪ {x} = y ∪ {y}`, then `x ∈ y ∪ {y}`, so
`x = y` or `x ∈ y`; symmetrically `y = x` or `y ∈ x`. If `x ≠ y` we would have `x ∈ y ∈ x`,
which Foundation forbids (`no_two_cycle`). -/
theorem succ_injective : Function.Injective succ := by
  intro x y h
  have hx : x ∈ succ y := by rw [← h]; exact mem_succ.mpr (Or.inl rfl)
  have hy : y ∈ succ x := by rw [h]; exact mem_succ.mpr (Or.inl rfl)
  rcases mem_succ.mp hx with hxy | hxy
  · exact hxy
  · rcases mem_succ.mp hy with hyx | hyx
    · exact hyx.symm
    · exact absurd ⟨hxy, hyx⟩ (no_two_cycle x y)

/-- The **von Neumann natural numbers**: `0 = ∅` and `n + 1 = n ∪ {n}`. So
`1 = {∅}`, `2 = {∅, {∅}}`, `3 = {∅, {∅}, {∅, {∅}}}`, … -/
def ofNat : ℕ → ZFSet.{u}
  | 0 => ∅
  | n + 1 => succ (ofNat n)

/-- Every von Neumann natural number lies in `ω`: by induction, using the two halves of the
Axiom of Infinity (`infinity`). -/
theorem ofNat_mem_omega (n : ℕ) : ofNat n ∈ ZFSet.omega := by
  induction n with
  | zero => exact infinity.1
  | succ n ih => exact infinity.2 _ ih

/-- **`n = {0, 1, …, n - 1}`**: the elements of the set `ofNat n` are exactly the sets `ofNat m`
with `m < n`. By induction on `n`, since `n + 1 = n ∪ {n}`. -/
theorem mem_ofNat {n : ℕ} {y : ZFSet.{u}} : y ∈ ofNat n ↔ ∃ m < n, y = ofNat m := by
  induction n with
  | zero =>
    constructor
    · intro h; exact absurd h (ZFSet.notMem_empty y)
    · rintro ⟨m, hm, -⟩; exact absurd hm (Nat.not_lt_zero m)
  | succ n ih =>
    show y ∈ succ (ofNat n) ↔ _
    rw [mem_succ, ih]
    constructor
    · rintro (h | ⟨m, hm, h⟩)
      · exact ⟨n, Nat.lt_succ_self n, h⟩
      · exact ⟨m, Nat.lt_succ_of_lt hm, h⟩
    · rintro ⟨m, hm, h⟩
      rcases Nat.lt_succ_iff_lt_or_eq.mp hm with hlt | heq
      · exact Or.inr ⟨m, hlt, h⟩
      · exact Or.inl (heq ▸ h)

/-- **The order of the natural numbers is membership:** `m ∈ n` (as sets) if and only if
`m < n`. The forward direction uses `mem_ofNat` and the injectivity below is a consequence. -/
theorem ofNat_mem_iff {m n : ℕ} : ofNat m ∈ ofNat n ↔ m < n := by
  constructor
  · intro h
    obtain ⟨k, hk, hmk⟩ := mem_ofNat.mp h
    -- `ofNat m = ofNat k` with `k < n`; if `m ≠ k` one of them is a member of the other.
    rcases Nat.lt_trichotomy m k with hlt | rfl | hgt
    · have hmem : ofNat m ∈ ofNat k := mem_ofNat.mpr ⟨m, hlt, rfl⟩
      rw [hmk] at hmem
      exact absurd hmem (not_mem_self _)
    · exact hk
    · have hmem : ofNat k ∈ ofNat m := mem_ofNat.mpr ⟨k, hgt, rfl⟩
      rw [← hmk] at hmem
      exact absurd hmem (not_mem_self _)
  · intro h
    exact mem_ofNat.mpr ⟨m, h, rfl⟩

/-- **Different numbers are different sets.** If `m < n` then `ofNat m ∈ ofNat n`; were the two
sets equal, we would have a set that is a member of itself. -/
theorem ofNat_injective : Function.Injective ofNat := by
  intro m n h
  rcases Nat.lt_trichotomy m n with hlt | heq | hgt
  · have hmem := ofNat_mem_iff.mpr hlt
    rw [h] at hmem
    exact absurd hmem (not_mem_self _)
  · exact heq
  · have hmem := ofNat_mem_iff.mpr hgt
    rw [h] at hmem
    exact absurd hmem (not_mem_self _)

Cartesian products, carved out of $\mathcal P(\mathcal P(x \cup y))$ by Separation:

/-- **Cartesian products are sets.** `x × y`, the set of pairs `(a, b)` with `a ∈ x`, `b ∈ y`, is
carved by Separation out of `𝒫(𝒫(x ∪ y))`, since `{{a}, {a, b}} ⊆ 𝒫(x ∪ y)`. This applies
Mathlib's `ZFSet.mem_prod`. -/
theorem mem_prod {x y z : ZFSet.{u}} : z ∈ ZFSet.prod x y ↔ ∃ a ∈ x, ∃ b ∈ y, z = ZFSet.pair a b :=
  ZFSet.mem_prod

What is and is not formalised. We formalise the axioms as facts about one particular model, ZFSet, and derive consequences from them. We do not formalise ZFC as a first-order theory — its formulas, derivations and arbitrary models — and nothing here bears on the consistency of ZFC. The relationship goes the other way: because Lean's logic has a hierarchy of type universes, it is strong enough to build a model of ZFC (ZFSet.{0} lives in Type 1). Mario Carneiro's analysis of Lean's type theory (2019) relates its consistency strength to that of ZFC with additional inaccessible cardinals — consistent with the corollary above, since a theory that proves "ZFC has a model" must be stronger than ZFC.

Python's immutable frozenset behaves like a pure set: two frozensets are equal exactly when they have the same elements, which is Extensionality, and frozensets can contain frozensets. So the finite stages of the hierarchy can be built literally.

"""Hereditarily finite sets: the finite levels of the ZFC universe, built.

Python's frozensets behave like pure sets: two frozensets are equal exactly
when they have the same elements (Extensionality), and a frozenset can contain
frozensets. Starting from the empty set we build the finite stages V_0, V_1,
..., V_4 of the cumulative hierarchy (V_{n+1} is the power set of V_n), the
von Neumann numerals 0 = {}, n + 1 = n U {n}, and Kuratowski pairs
{{a}, {a, b}}. We then check, exhaustively on V_4, that Kuratowski pairs never
collide while the naive encoding {a, {b}} does; that every non-empty set has an
element-minimal member (Foundation); and that Ackermann's coding
code(x) = sum of 2^code(y) over y in x is a bijection V_4 -> {0, ..., 15}
turning membership into binary digits. Evidence: exact and exhaustive, but only
for the finite sets examined.
"""

from itertools import combinations, product

EMPTY = frozenset()

def powerset(s):
    """All subsets of the finite set ``s``, as a frozenset of frozensets."""
    items = sorted(s, key=ackermann)
    subsets = []
    for r in range(len(items) + 1):
        subsets.extend(frozenset(c) for c in combinations(items, r))
    return frozenset(subsets)

def hierarchy(n):
    """Return [V_0, V_1, ..., V_n] with V_0 = {} and V_{k+1} = P(V_k)."""
    if n < 0:
        raise ValueError("n must be non-negative")
    stages = [EMPTY]
    for _ in range(n):
        stages.append(powerset(stages[-1]))
    return stages

def succ(x):
    """The von Neumann successor x U {x}."""
    return x | frozenset([x])

def numeral(n):
    """The von Neumann numeral for the natural number n."""
    if n < 0:
        raise ValueError("n must be non-negative")
    x = EMPTY
    for _ in range(n):
        x = succ(x)
    return x

def kpair(a, b):
    """Kuratowski's ordered pair {{a}, {a, b}}."""
    return frozenset([frozenset([a]), frozenset([a, b])])

def naive_pair(a, b):
    """A flawed encoding of ordered pairs: {a, {b}}."""
    return frozenset([a, frozenset([b])])

def collisions(universe, pair):
    """Pairs of distinct ordered pairs from ``universe`` with equal codes."""
    seen, bad = {}, []
    for a, b in product(sorted(universe, key=ackermann), repeat=2):
        code = pair(a, b)
        if code in seen and seen[code] != (a, b):
            bad.append((seen[code], (a, b)))
        seen.setdefault(code, (a, b))
    return bad

def has_minimal_element(x):
    """Foundation for one set: some y in x shares no element with x."""
    return any(not (y & x) for y in x)

def ackermann(x):
    """Ackermann's code: the sum of 2^code(y) over the elements y of x."""
    return sum(2 ** ackermann(y) for y in x)

def decode(n):
    """Inverse of ``ackermann``: the set whose elements have codes = bits of n."""
    if n < 0:
        raise ValueError("n must be non-negative")
    return frozenset(decode(i) for i in range(n.bit_length()) if n >> i & 1)

def show(x):
    """Write a hereditarily finite set with braces, {} for the empty set."""
    inner = ", ".join(show(y) for y in sorted(x, key=ackermann))
    return "{" + inner + "}"

def main():
    stages = hierarchy(4)
    sizes = ", ".join(f"|V_{k}| = {len(v)}" for k, v in enumerate(stages))
    print("1. The cumulative hierarchy, V_(n+1) = P(V_n):")
    print("   " + sizes)
    print("   |V_5| = 2^16 = 65536; |V_6| = 2^65536 has 19729 digits (not built)")
    print("2. von Neumann numerals, n + 1 = n U {n}:")
    for n in range(4):
        print(f"   {n} = {show(numeral(n))}")
    print("   Ackermann codes of 0..4:", [ackermann(numeral(n)) for n in range(5)])
    v4 = stages[4]
    good, bad = collisions(v4, kpair), collisions(v4, naive_pair)
    print("3. Ordered pairs of elements of V_4 (256 pairs):")
    print(f"   Kuratowski {{{{a}}, {{a, b}}}}: {len(good)} collisions")
    print(f"   naive {{a, {{b}}}}:          {len(bad)} collisions, for example")
    (a, b), (c, d) = bad[0]
    print(f"   a = {show(a)}, b = {show(b)}  and  c = {show(c)}, d = {show(d)}")
    print(f"   both give {show(naive_pair(a, b))}")
    nonempty = [x for x in v4 if x]
    found = sum(has_minimal_element(x) for x in nonempty)
    print(f"4. Foundation: {found} of {len(nonempty)} non-empty sets in V_4 have")
    print("   an element-minimal member (one disjoint from the set itself)")
    codes = sorted(ackermann(x) for x in v4)
    agree = all((x in y) == bool(ackermann(y) >> ackermann(x) & 1)
                for x in v4 for y in v4)
    print(f"5. Ackermann coding maps V_4 onto 0..15: {codes == list(range(16))};")
    print(f"   x in y  <=>  bit code(x) of code(y) is 1, for all 256 pairs: {agree}")
    print()
    print("Epistemic status: every check is exact and exhaustive, but only for")
    print("the sixteen sets of V_4. That Kuratowski pairs work for all sets is a")
    print("theorem proved in the lesson; Foundation for arbitrary sets is an axiom,")
    print("which no computation can confirm. That V_omega, the union of all V_n,")
    print("satisfies every ZFC axiom except Infinity is a theorem, not checked here.")

if __name__ == "__main__":
    main()

Three things to notice. The naive encoding $\{a, \{b\}\}$ fails already among the sixteen sets of $V_4$, while Kuratowski's encoding passes the exhaustive test. Every non-empty set examined has an $\in$-minimal element, as Foundation demands. And Ackermann's coding (1937), $\mathrm{code}(x) = \sum_{y \in x} 2^{\mathrm{code}(y)}$, is a bijection from $V_\omega$ to $\N$ under which "$x \in y$" becomes "the $\mathrm{code}(x)$-th binary digit of $\mathrm{code}(y)$ is $1$". So the hereditarily finite sets are, in disguise, just the natural numbers with an arithmetic relation. This is the first step towards a classical fact, made precise by Richard Kaye and Tin Lok Wong (2007): ZF with the axiom of Infinity replaced by its negation is bi-interpretable with Peano arithmetic.

This is exact, exhaustive evidence about finitely many sets. It proves nothing about infinite sets, and it cannot test an axiom such as Foundation for all sets: Foundation is an assumption, not a fact that computation can confirm.

Sets made only of sets can be pictured as boxes nested inside boxes; a set is determined by which boxes it contains, not by how they are arranged.

Try to build $V_3$: its four elements are $\varnothing$, $\{\varnothing\}$, $\{\{\varnothing\}\}$ and $\{\varnothing, \{\varnothing\}\}$. Then build the numerals $0, 1, 2, 3$ by repeatedly forming $x \cup \{x\}$, and check that each numeral contains all the earlier ones. Can you find two different-looking ways of writing the same set? (Extensionality says they are the same box.)

The trail below starts from boxes inside boxes and reaches the axioms of ZFC; it is written for young learners but makes a good warm-up.

• Georg Cantor created set theory between 1874 and 1897, starting from questions about trigonometric series and the sizes of infinite sets. He worked with sets informally, though he was aware that some collections (such as "all ordinals") could not consistently be treated as sets.
• Gottlob Frege's Grundgesetze der Arithmetik (1893, 1903) contained the unrestricted comprehension law. Bertrand Russell found the contradiction in 1901 and wrote to Frege in 1902; Ernst Zermelo had noticed essentially the same contradiction slightly earlier without publishing it.
• Zermelo published the first axiom system for set theory in 1908, partly to defend his 1904 proof that every set can be well-ordered, which used the axiom of choice. His axioms were Extensionality, elementary sets (empty set, singletons, pairs), Separation, Power set, Union, Choice and Infinity.
• In 1922 Abraham Fraenkel and Thoralf Skolem independently proposed the Replacement axiom, and Skolem suggested making Zermelo's "definite properties" precise as first-order formulas. Dmitry Mirimanoff (1917) studied well-founded sets, and John von Neumann introduced his ordinals (1923) and the axiom of foundation (1925). Zermelo's 1930 paper described the cumulative hierarchy and its connection with inaccessible cardinals.
• Ordered pairs as sets: Norbert Wiener (1914) gave the first definition, $\{\{\{a\}, \varnothing\}, \{\{b\}\}\}$; Felix Hausdorff (1914) another; Kazimierz Kuratowski's simpler $\{\{a\}, \{a, b\}\}$ (1921) became standard. Wilhelm Ackermann's coding of hereditarily finite sets by natural numbers dates from 1937.
• Kurt Gödel (1931, incompleteness; 1938, the constructible universe) and Paul Cohen (1963, forcing; Fields Medal 1966) established the limits of what ZFC decides. F. William Lawvere proposed ETCS in 1964, and Saharon Shelah in Jerusalem settled Whitehead's problem in 1974.
• Set theory grew in many places: the Polish school around the journal Fundamenta Mathematicae (founded in Warsaw in 1920; Wacław Sierpiński was one of its first editors) made set-theoretic topology a field of its own, and today set theory is an international research area, with active groups across Europe, the Americas, Israel, Japan, China and elsewhere.

• Herbert B. Enderton, Elements of Set Theory (1977) — a careful first course: axioms, encodings, natural numbers, the reals, ordinals.
• Paul R. Halmos, Naive Set Theory (1960) — a short, classic informal introduction to the axioms.
• Kenneth Kunen, Set Theory: An Introduction to Independence Proofs (1980), and Set Theory (2011) — the standard graduate texts, through Gödel's $L$ and forcing.
• Thomas Jech, Set Theory (third millennium edition, 2003) — the comprehensive reference.
• Jean van Heijenoort (ed.), From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931 (1967) — translations of Russell's letter to Frege and the founding papers of Zermelo, Fraenkel, Skolem and von Neumann.
• George Boolos, "The iterative conception of set", Journal of Philosophy (1971).
• Paul Benacerraf, "What numbers could not be", Philosophical Review (1965).
• F. William Lawvere, "An elementary theory of the category of sets", Proceedings of the National Academy of Sciences (1964); and Tom Leinster, "Rethinking set theory", American Mathematical Monthly (2014), a friendly account of ETCS.