Building with ZFC

Separation tells us how to extract a subset from a set already in hand. It leaves a natural question: which sets can we put in hand in the first place? Zermelo–Fraenkel set theory, usually called ZF, combines several existence principles. Adding the axiom of choice gives ZFC.

In the usual formulation, the variables range over sets and membership is the sole nonlogical relation beyond equality. The list below describes families of principles, not one short formula from which every set simply appears. Separation and replacement are schemas: they provide an axiom for each formula of the specified kind.

A map of the rules

Identity and basic constructions

Extensionality says that two sets with exactly the same elements are equal. Pairing supplies $\{a,b\}$ for any sets $a$ and $b$. Union collects the members of members of a set $A$ into $\bigcup A$. Together these let us construct a singleton $\{a\}$ by pairing $a$ with itself, and then build finite combinations.

Power set supplies the set of all subsets of a given set:

$$\mathcal P(A)=\{x\mid x\subseteq A\}.$$

The existence claim is substantial. From a countably infinite set it leads to a strictly larger set, as Cantor's theorem in Article 1.1 showed. The subsets of $\mathbb N$ also provide a way to represent real numbers. This is one reason power set matters in a set-theoretic account of analysis.

Selection, images, and infinity

Separation selects elements of an existing set according to a first-order formula. Replacement says, roughly, that the image of a set under a definable function is a set. If a formula assigns exactly one $y$ to each $x$ in $A$, then

$$\{y\mid \exists x\in A\;\varphi(x,y)\}$$

exists as a set. The qualification “definable function” matters: the schema does not assert the existence of an arbitrary function with no rule specifying it.

Infinity asserts the existence of an inductive set: one containing the empty set and closed under $x\mapsto x\cup\{x\}$. Foundation says every nonempty set has a member disjoint from it. In ordinary ZF this rules out a set belonging to itself and supports the cumulative-hierarchy view in which sets have ranks. Foundation is a separate axiom; the Russell contradiction was already blocked by separation.

From rules to familiar objects

The empty set and natural numbers

Many presentations list an empty-set axiom. In the version just described, infinity guarantees that some set $I$ exists. Separation then selects from $I$ the elements satisfying $x\ne x$. None do, so the selected set is empty. Extensionality makes it unique. Thus an empty-set axiom can be redundant relative to these other assumptions.

Now define $0=\varnothing$ and the successor of a set $n$ by

$$n+1=n\cup\{n\}.$$

The first few von Neumann natural numbers are $0=\varnothing$, $1=\{0\}$, and $2=\{0,1\}$. Infinity gives an inductive set, and separation lets us isolate the least one, $\omega$. The familiar sequence is therefore encoded within set theory, though the symbols $0,1,2$ remain mathematical choices of representation rather than objects found in nature.

An ordered pair made of sets

A set $\{a,b\}$ forgets the order of $a$ and $b$. The Kuratowski encoding keeps it:

$$(a,b):=\bigl\{\{a\},\{a,b\}\bigr\}.$$

It can be built with pairing. Its defining property is $(a,b)=(c,d)$ exactly when $a=c$ and $b=d$. Relations and functions can then be represented as sets of ordered pairs. The encoding is one useful convention, not a claim that an ordered pair is essentially this particular arrangement of braces.

What choice adds

The axiom of choice says that for every indexed family of nonempty sets, there is a function choosing one member from each set. For a finite family we can choose successively. For an arbitrary infinite family, the axiom makes a general existence claim without providing an explicit algorithm for every case.

Choice was once controversial and remains worth noticing when a proof uses it. Gödel showed that, if ZF is consistent, adding choice does not introduce a contradiction. Cohen later showed that, if ZF is consistent, its negation can also be added consistently. This is a relative independence result. It is not an absolute proof that ZF itself is consistent.

One striking consequence of choice is the Banach–Tarski theorem. A solid ball in three-dimensional space can be partitioned into finitely many sets of points and rearranged by rigid motions into two balls congruent to the original. The pieces are not ordinary solid chunks with well-defined volumes; they are nonmeasurable sets. The theorem exposes how far abstract existence principles can travel from physical cutting and reassembly.

A common language, with limits

ZFC supports a remarkably wide range of ordinary mathematics. Its axioms specify ways to identify, select, combine, and enlarge sets, and familiar objects can be encoded inside that framework. It does not follow that ZFC is the only possible foundation or that these rules prove their own consistency.

The next essay steps back from the particular rules. What does it mean for a formal theory to prove a sentence? What does it mean for that sentence to hold in a model? Those questions become unavoidable once the foundation itself is an object of study.

Sources

• Zermelo, “Untersuchungen über die Grundlagen der Mengenlehre I” (1908), an ancestor of modern ZF.
• Gödel, “The Consistency of the Axiom of Choice and of the Generalized Continuum-Hypothesis” (1938).
• Cohen, “The Independence of the Continuum Hypothesis, II” (1964), which includes the independence of choice among its results.
• Banach and Tarski, “Sur la décomposition des ensembles de points en parties respectivement congruentes” (1924).