Zermelo–Fraenkel axioms and Replacement
Distinguish bounded comprehension from functional collection and track the axioms that make a mathematical construction a set.
On this page
The question for today
What you’ll understand
- Separate set quantifiers from definable-class notation in ZF.
- Explain the different roles of Separation, Power Set, and Replacement.
- Verify a Cartesian-product construction without unrestricted comprehension.
Set theory provides a language in which the objects of ordinary mathematics can be represented, but it does not license every collection described in that language as a set. Zermelo–Fraenkel theory controls set formation through specific axioms and axiom schemes. Following one construction carefully reveals what those axioms contribute. The important distinction is between selecting elements from an existing set and collecting outputs whose existence has been proved individually.
The language quantifies over sets
The first-order language has equality and the binary membership relation. Expressions such as a subset relation, an ordered pair, or the class of all ordinals abbreviate formulas rather than add new kinds of quantified objects. A definable class is a collection specified by a formula, possibly with set parameters. Calling it a class does not assert that one set contains exactly its members. This convention lets us discuss the universe while keeping every quantifier of ZF a quantifier over sets.
Extensionality identifies sets with the same members. Empty Set, Pairing, Union, and Power Set provide elementary constructions; Infinity supplies an inductive set; Foundation rules out membership cycles and supports the well-founded picture. Separation and Replacement are schemes, with one axiom for each appropriate formula. Choice is an additional axiom: ZFC means ZF together with Choice. Listing these principles is not a proof that they are jointly consistent, and a model of them need not have actual membership as its interpreted relation.
Separation starts with a containing set
Given a set A and a formula, Separation produces the subset of A whose elements satisfy that formula. The containing set prevents Russell's contradiction. If a universal set U existed, Separation would form the elements x of U for which x is not a member of itself, producing the familiar contradiction. Thus unrestricted comprehension is not an alternative notation for Separation. Power Set has a different job: it supplies a set containing every subset of one given set, rather than selecting individual elements of that set.
Replacement begins with a formula that assigns exactly one output set to each input in a set A. It asserts that all those outputs form a set, even when no containing set was supplied beforehand. The uniqueness premise must be proved on A, with all parameters fixed. A multivalued relation does not meet this premise merely because each input has some witness. Collection principles can address witnesses, but their connection with Replacement is a theorem requiring the surrounding axioms, not permission to discard functionality.
Audit the bounding set in a construction
For a Cartesian product, code an ordered pair by the Kuratowski set consisting of the singleton of its first coordinate and the unordered pair of its coordinates. Pairing makes this code a set. If the coordinates lie in A and B, both pieces are subsets of A union B. Consequently every ordered-pair code belongs to the double power set of A union B. Separation inside that double power set now constructs the product. This proof uses an explicit bound rather than invoking a universal collection of pairs.
The same discipline becomes more consequential in transfinite arguments. A rule can define an object at each earlier stage without yet proving that the earlier objects can be assembled into one set-length history. Replacement supplies that assembly when the rule is functional and the index collection is a set. Applying it to the proper class of all indices is not an instance of the scheme. Keeping that boundary visible now prevents an illegitimate set of all ordinals or a set-sized universe later. No choice of notation removes the distinction.
Work it through
Build a four-element product
Construct A×B for A={0,1} and B={2,3} using Kuratowski ordered pairs, and identify a set in which Separation can be applied.
Pairing and Union form C=A∪B={0,1,2,3}. For a∈A and b∈B, both {a} and {a,b} are subsets of C.
The ordered-pair code {{a},{a,b}} is therefore a subset of P(C), so it belongs to P(P(C)). Separate exactly the codes with first coordinate in A and second coordinate in B inside this set.
The four resulting ordered pairs are (0,2), (0,3), (1,2), and (1,3). Equality of Kuratowski codes recovers equality of both coordinates, so none of these four pairs are identified.
The product is a four-element set obtained from elementary set-forming axioms and bounded Separation; unrestricted comprehension was unnecessary.
The living notebook
Explore the model
Interactive lab · function
Inspect the outputs before collecting them
Pause and Reset, then set coefficient a = 1 and position x = 2. Predict y = 4. On paper evaluate the same rule on A={0,1,2}, obtaining image {0,1,4}. Reset and set both a = 0.5 and x = 2; predict y = 2 and paper image {0,0.5,2}. The quadratic instrument checks these finite evaluations, not the logical Replacement scheme or arbitrary set functions.
- y at chosen x
- 0.608
- Tangent slope · 2ax
- 1.35
- Signed area · ax³/3
- 0.182
This lab uses only y = ax². Playback traces the curve within the fixed integration interval from 0 to x; it does not estimate numerical error or change the chosen point. Parameter changes pause playback and recompute the model at the current elapsed time. Reset restores both parameters and returns time to zero. Playback starts paused. Adjust either parameter, then choose Play or Step.
Look forA specified rule must have well-defined outputs before a functional image can be collected.
Pause & reason
Check your understanding
Your turn
Try it yourself
Explain why {n+1:n∈ω} is a set, and why writing {x:x is a set} does not justify a universal set. Which operation gives the even natural numbers?
Take a moment to make a prediction or work it out on paper. Open a hint when you need one.
Give me a hint
Separate an image construction from a subset construction, and ask whether the proposed domain is already a set.
Compare with the solution
The successor rule assigns the unique set n∪{n} to each natural number, so Replacement on ω gives its image. In this example the image is also a subset of ω and can be obtained by Separation. The even natural numbers are selected from ω by the formula asserting n=2m for some natural m. By contrast the domain of all sets has not been given as a set. Applying Replacement or Separation to that proper class is invalid, and a purported universal set would produce Russell’s contradiction by Separation.
Keep the idea
Take it with you
- ZF uses set-forming axioms and schemes rather than unrestricted comprehension.
- Replacement collects a functional image on a set; Separation selects inside a set.
- An explicit containing set can justify a construction without invoking Choice.
Read further
Original sources and deeper explanations to follow at your own pace.
Optional progress, saved in this browser when available. Revisit any lesson at any time.
Lesson not marked complete.