Axiom schema of replacement

In axiomatic set theory and the branches of logic, mathematics, and computer science that use it, the axiom schema of replacement is a schema of axioms in Zermelo-Fraenkel set theory.

Suppose P is any predicate in two variables that doesn't use the symbol B. Then in the formal language of the Zermelo-Fraenkel axioms, the axiom schema reads:

(∀ X, ∃! Y, P(X,Y)) → ∀ A, ∃ B, ∀ C, C ∈ B ↔ (∃ D, D ∈ A ∧ P(D,C));

or in words:

If, given any set X, there is a unique[?] set Y such that P holds for X and Y, then, given any set A, there is a set B such that, given any set C, C is a member of B if and only if there is a set D such that D is a member of A and P holds for D and C.

Note that there is one axiom for every such predicate P; thus, this is an axiom schema[?].

To understand this axiom, first note that the clause in the first set of parentheses above is exactly what one needs to construct a functional predicate F in one variable such that F(X) = Y if and only if P(X,Y). Indeed, if one formalises the language of predicate logic to allow the use of derived functional predicates in axiom schemas, then the axiom schema may be rewritten as:

∀ A, ∃ B, ∀ C, C ∈ B ↔ (∃ D, D ∈ A ∧ C = F(D))

for each derived functional predicate F in one variable; or in words:

Given any set A, there is a set B such that, given any set C, C is a member of B if and only if there is a set D such that D is a member of A and C is equal to the value of F at D.

Next, note that the clause in parentheses in the reformulation above (equivalent to the second clause in parentheses in the original statement) simply states that C is the value of F at some member D of A. Thus, what the axiom schema is really saying is that, given a set A, we can find a set B whose members are precisely the values of F at the members of A.

We can use the axiom of extension to show that this set B is unique. We call the set B the image of A under F, and denote it F(A) or (using a form of set-builder notation) {F(D) : D in A}. Thus the essence of the axiom schema is:

The image of a set under a mapping is a set.

History and philosophy

Most of the applications to which replacement might naïvely be put in fact do not require it. For example, suppose that f is a function from a set S to a set T. Then we may construct a functional predicate F such that F(x) = f(x) whenever x is a member of S, letting F(x) be anything we like otherwise (it won't matter for this application). Then given a subset A of S, applying the axiom schema of replacement to F constructs the image f(A) of the subset A under the function f; it is just F(A). However, replacement is in fact not needed here, because f(A) is a subset of T, so we could instead construct this image using the axiom schema of specification as the set {y in T : for some x in A, y = f(x)}. In general, specification will suffice when the values of F at the members of A all belong to some previously constructed set T; replacement is needed only when such a T isn't already available.

According to some philosophies, it's preferable to apply specification to a set like T in the example above, since specification is logically weaker than replacement (as explained in the next section). Indeed, replacement is arguably unnecessary in ordinary mathematics, needed only for certain features of axiomatic set theory. For example, you need replacement to construct the von Neumann ordinals from ω2 onwards, and the von Neumann ordinals are necessary for certain set-theoretic results. However, you don't need replacement to construct these ordinal numbers in other ways that are sufficient for applications to the theory of well-ordered sets. Some mathematicians working on the foundations of mathematics, particularly those that focus on type theory as opposed to set theory, find this axiom unnecessary for any purpose and therefore do not include it (nor a type-theoretic analogue) in their foundations. Replacement is difficult to express at all in foundations built upon topos theory, so it's usually left out there as well. Nevertheless, replacement is not controversial in the sense that some people find its consequences to be necessarily false (a sense in which the axiom of choice, for example, is controversial); it's just that they find it unnecessary.

The axiom schema of replacement wasn't part of Ernst Zermelo's 1908 axiomatisation of set theory (Z); its introduction by Adolf Fraenkel[?] in 1922 is what makes modern set theory Zermelo-Fraenkel set theory (ZF). The axiom was independently discovered by Thoralf Skolem[?] later in the same year, and it is in fact Skolem's final version of the axiom list that we use today -- but he usually gets no credit since each individual axiom was developed earlier by either Zermelo or Fraenkel. Including replacement makes a big difference from the proof-theoretic point of view; adding this schema to Zermelo's axioms makes for a much stronger system logically, allowing one to prove more statements. In particular, in ZF one can prove the consistency of Z by constructing the von Neumann universe[?] V_ω2 as a model. (Of course, Gödel's second incompleteness theorem shows that neither of these theories can prove its own consistency, if it is consistent.)

Relation to the axiom schema of specification

The axiom schema of specification can almost be derived from the axiom schema of replacement.

First, recall this axiom schema:

∀ A, ∃ B, ∀ C, C ∈ B ↔ (C ∈ A ∧ P(C)),

for any predicate P in one variable that doesn't use the symbol B. Given such a predicate P, define the mapping F by F(D) = D if P(D) is true and F(D) = E if P(D) is false, where E is any member of A such that P(E) is true. Then the set B guaranteed by the axiom of replacement is precisely the set B required for the axiom of specification. The only problem is if no such E exists. But in this case, the set B required for the axiom of specification is the empty set, so the axiom schema follows in general using also the axiom of empty set.

For this reason, the axiom schema of specification is often left out of modern lists of the Zermelo-Fraenkel axioms. However, specification is still important for historical considerations, and for comparison with alternative axiomatisations of set theory. For example, the argument above used the law of the excluded middle, so specification can't be left out of an intuitionistic set theory. And any formulation of set theory that excludes replacement as unnecessary certainly will want to keep specification.