The ZFC Axioms Overview

ZFC is the substrate on which the vast majority of contemporary mathematics is formally built: real numbers as Dedekind cuts or Cauchy sequences of rationals, functions as sets of ordered pairs (built exactly as in Example 1 above), cardinal and ordinal arithmetic, and the entire theory of the transfinite all rest on Pairing, Union, Power Set, Infinity, Separation, and Replacement. In mathematical logic and model theory, ZFC is the standard background theory in which one studies independence results (Gödel's constructible universe $L$ and Cohen's forcing method both work by building alternative models of ZF/ZFC to show the Continuum Hypothesis and Choice are independent of ZF). In computer science, the cumulative hierarchy and well-founded recursion (guaranteed by Foundation) underlie the semantics of recursive data types and the theory of well-founded induction used to prove program termination. In category theory, the need to speak of "the category of all sets" without contradiction leads directly to Grothendieck universes, themselves constructed using strengthenings of ZFC's Power Set and Replacement axioms (large cardinal axioms). Descriptive set theory, measure theory, and the foundations of probability all quietly rely on Replacement to construct the transfinite hierarchies of Borel and projective sets. And the entire question of the Axiom of Choice — whether the ninth axiom should be accepted, and what changes if it is dropped or replaced by alternatives like the Axiom of Determinacy — is a live and central topic that builds directly on the ZF framework surveyed here.

Ask the tutor: How does the Axiom of Choice interact with Zorn's Lemma and the Well-Ordering Theorem, and why are all three provably equivalent over ZF?

Think of the universe of sets as built in stages, indexed by ordinals, forming the cumulative hierarchy $V_0, V_1, V_2, \dots, V_\omega, V_{\omega+1}, \dots$ defined by

Every set that ZF proves exists lives in some $V_\alpha$, and conversely Foundation is exactly the axiom asserting that every set lives somewhere in this hierarchy — nothing is "left out" at the bottom, floating in an infinite regress of membership. Extensionality tells you sets are nothing but their extensions: no two different "bags" with the same contents. Pairing, Union, and Power Set are the three basic moves that let you climb the hierarchy: pair two known sets, take a union of a known family, or take all subsets of a known set. Infinity is the one axiom that forces the hierarchy past every finite stage, guaranteeing an actual infinite set exists rather than merely arbitrarily large finite ones. Separation and Replacement are the two definability axioms: Separation lets you carve out a subset of something you already have using a formula, while Replacement — strictly stronger — lets you replace each element of a known set by (possibly a "larger" or differently-structured) image under a definable rule, which is essential once you need sets of very large or complicated ordinals that no amount of power-setting alone would reach. The picture below shows the first few levels of the cumulative hierarchy and where Foundation forbids "sideways" or "downward-infinite" membership chains, while the second figure shows conceptually how the roles of the eight ZF axioms partition into "existence/building" versus "restriction/safety."

This proof technique — instantiate a universally quantified biconditional at the very object it defines, then apply excluded middle — is the paradigm diagonal/self-reference argument reused throughout logic (compare the Liar paradox, Cantor's theorem on power sets, and the undecidability of the halting problem). The proof of Part 1 is a direct derivation of $\bot$ (non-circular: it uses only propositional logic and universal instantiation, no set-theoretic axiom other than the assumed unrestricted Comprehension). The Corollary's proof uses only Separation (already established as one of our axioms) and Part 1's propositional argument, so there is no circularity: we do not use the Corollary or any theorem depending on it anywhere in Part 1 or Part 2.

Example 1 — Building the ordered pair and verifying it from the axioms alone. We construct the Kuratowski ordered pair $\langle a, b\rangle := \{\{a\},\{a,b\}\}$ using only Pairing, and verify the defining property using Extensionality — with an asymmetric pair $a \ne b$ to make sure the construction isn't accidentally symmetric. Let $a$ and $b$ be arbitrary sets with $a \neq b$. By Pairing applied to $a$ and $a$, the set $\{a\} := \{a,a\}$ exists (Pairing only requires two, possibly equal, inputs, and $\forall w\,(w \in z \leftrightarrow w = a \lor w = a)$ simplifies to $w = a$). By Pairing applied to $a$ and $b$, the set $\{a,b\}$ exists. By Pairing applied to the two sets $\{a\}$ and $\{a,b\}$, the set

exists. All three applications of Pairing are legitimate since each takes two already-constructed sets as input.

Claim. For all sets $a,b,c,d$: $\langle a,b \rangle = \langle c,d\rangle$ if and only if $a=c$ and $b=d$. Proof. ($\Leftarrow$) If $a=c$ and $b=d$ then $\{a\} = \{c\}$ and $\{a,b\}=\{c,d\}$ as sets (by Extensionality, since they have identical elements), so $\{\{a\},\{a,b\}\} = \{\{c\},\{c,d\}\}$. ($\Rightarrow$) Suppose $\langle a,b\rangle = \langle c,d \rangle$, i.e. $\{\{a\},\{a,b\}\} = \{\{c\},\{c,d\}\}$. By Extensionality these two-element sets have the same elements, so $\{a\}$ equals $\{c\}$ or $\{c,d\}$. Case A: Suppose our pair is genuinely asymmetric with $a \ne b$. Since $\{a\}$ is a singleton, and $\{c,d\}$ has the property that it is a singleton iff $c=d$, we split further:

• If $\{a\} = \{c,d\}$: then since $\{a\}$ is a singleton, $c = d = a$. Then the right-hand pair is $\{\{a\},\{a,a\}\} = \{\{a\}\}$, a genuine singleton as a set (only one distinct element, $\{a\}$). But the left-hand pair $\{\{a\},\{a,b\}\}$ has two distinct elements since $a \ne b$ implies $\{a\} \ne \{a,b\}$ (as $b \in \{a,b\}$ but $b \notin \{a\}$, using $a\ne b$). A one-element set cannot equal a two-element set (their elements, compared via Extensionality, would force $\{a\} = \{a,b\}$, contradiction). So this sub-case is impossible.
• Hence $\{a\} = \{c\}$, forcing $a = c$ (two singletons are equal iff their unique elements are equal, by Extensionality). And then $\{a,b\}$ must equal $\{c,d\} = \{a,d\}$ (the other element of the right side, since $\{a\}\ne\{c,d\}$ was just ruled out — more precisely, since the two-element set on the right, $\{c,d\}$, must equal the two-element set on the left, $\{a,b\}$, because $\{a\}$ already matched $\{c\}$ and by Extensionality the sets $\{\{a\},\{a,b\}\}$, $\{\{c\},\{c,d\}\}$ having equal first components force the remaining components equal too, using that $\{a\}\ne\{a,b\}$). From $\{a,b\}=\{a,d\}$, Extensionality gives: $b \in \{a,d\}$, so $b=a$ or $b=d$; since $b\neq a$, we get $b=d$.

So $a=c$ and $b=d$, as required. $\blacksquare$ This confirms the ordered pair is correctly recoverable using only Pairing and Extensionality — no new axiom for "ordered pair" is needed; it is a definable notion, and Cartesian products $A\times B := \{\langle a,b\rangle : a\in A, b\in B\}$ are then obtained rigorously via Separation applied inside $\mathcal P(\mathcal P(A\cup B))$ (every $\langle a,b\rangle$ with $a\in A, b\in B$ is an element of $\mathcal P(\mathcal P(A \cup B))$, and Separation carves out exactly those elements of this power set that have the ordered-pair form with first coordinate in $A$ and second in $B$), invoking Power Set and Union along the way.

Example 2 — Why Replacement is strictly needed: constructing $V_\omega$ and beyond. Using Infinity, we get a set $I$ with $\varnothing \in I$ and closed under $y \mapsto y \cup \{y\}$. Define $0 := \varnothing$, $1 := 0 \cup \{0\} = \{\varnothing\}$, $2 := 1\cup\{1\} = \{\varnothing,\{\varnothing\}\}$, and generally $n+1 := n \cup \{n\}$; write $\omega$ for the set of natural numbers obtained by Separation from $I$ using the formula "$z$ is a natural number" (formalized as: $z$ belongs to every subset of $I$ containing $\varnothing$ and closed under successor — this is itself a legitimate first-order formula, since it quantifies over subsets of $I$, which is fine because Power Set gives us $\mathcal P(I)$ to quantify over, and Separation then extracts $\omega = \{z \in I : \forall S \in \mathcal P(I)(\varnothing \in S \land (\forall y\in S)(y\cup\{y\}\in S) \to z \in S)\}$). Now consider the cumulative hierarchy restricted to finite levels:

Each individual $V_n$ exists by $n$ applications of Power Set (a finite iteration, licensed one step at a time — this needs no new axiom beyond Power Set applied repeatedly, which is a legitimate meta-level induction on the natural number $n$, itself justified since $\omega$ exists by Infinity). But now ask for the single set

This requires a single set $\{V_n : n \in \omega\}$ to exist, to which we could then apply Union. But "$\{V_n : n \in \omega\}$" is exactly the image of the set $\omega$ under the function $n \mapsto V_n$ — and $n \mapsto V_n$ is a class function definable by the formula

which one checks defines a genuine function of $n$ (existence and uniqueness of such $f$ for each $n \in \omega$ is proved by ordinary finite induction on $n$, using Pairing/Power Set/Union at each successor step to build $f$ one value longer). Replacement, applied to the set $a := \omega$ and this formula $\varphi$, now directly yields

i.e. the set $x = \{V_n : n \in \omega\}$ exists as a single set. Only then can Union be applied to $x$ to produce $V_\omega = \bigcup x$. Without Replacement, Separation alone cannot produce $x = \{V_n : n\in\omega\}$, because Separation only carves subsets out of an already-existing set — and no set containing all the $V_n$'s is given in advance by Pairing, Union, or Power Set applied a bounded number of times; those axioms only ever hand you one new set per application, never "one new set for each of infinitely many previously constructed, increasingly large sets, collected together." This is precisely the sense in which Replacement is strictly stronger than Separation, and it is indispensable once one moves from finite iteration to genuinely transfinite constructions (e.g., defining $V_{\omega+\omega}$, or the sequence of alephs $\aleph_0, \aleph_1, \aleph_2, \dots$, all require Replacement in exactly this pattern).