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 which essentially asserts that the image of a set under a mapping is also a set. It is necessary for the construction of certain large sets.

Statement

---

Suppose P is any predicate in two variables such that for every set x there is a unique set y such that P(x,y). Then we can form the function F in one variable such that F(X) = Y if and only if P(X,Y).

The axiom of replacement then states that given a set A, we can find a set B whose members are precisely the values of F at the members of A. Note that there is one axiom for every such predicate P; thus, this is an axiom schema.

In the formal language of the Zermelo-Fraenkel axioms, the axiom schema reads:

$(\backslash forall\; x,\; \backslash exist!\backslash ,\; y:\; P(x,\; y))\; \backslash rightarrow\; \backslash forall\; A,\; \backslash exist\; B,\; \backslash forall\; y:\; y\; \backslash in\; B\; \backslash iff\; \backslash exist\; x\; \backslash in\; A\; :\; P(x,\; y)$

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 y, y is a member of B if and only if there is a set x which is a member of A such that P holds for x and y.

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:

$\backslash forall\; A,\; \backslash exist\; B,\; \backslash forall\; y:\; y\; \backslash in\; B\; \backslash iff\; \backslash exist\; x\; \backslash in\; A\; :\; y\; =\; F(x)$

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 y, y is a member of B if and only if there is a set x which is a member of A such that y is equal to the value of F at x.

We can use the axiom of extensionality 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(x) : x ∈ A}.

Occasionally the axiom is quoted without the uniqueness requirement:

$\backslash forall\; A\; (\backslash forall\; x\; \backslash in\; A,\; \backslash exist\; y:\; P(x,\; y))\; \backslash rightarrow\; \backslash exist\; B,\; \backslash forall\; x\; \backslash in\; A,\; \backslash exist\; y\; \backslash in\; B:\; P(x,\; y)$

That is, the predicate P is not required to be functional: to apply it to a set A, it is enough that there exist at least one element y which corresponds to each element x of A; it is not necessary that this y be unique for each x. In this case, the image set B whose existence is asserted will then contain at least one such y for each x of the original set, with no guarantee that it will contain only one.

This is also sometimes stated without any restrictions on the predicate:

$\backslash forall\; A,\; \backslash exist\; B,\; \backslash forall\; x\; \backslash in\; A\; :\; ((\backslash exist\; y\; :\; P(x,\; y))\; \backslash rightarrow\; \backslash exist\; y\; \backslash in\; B\; :\; P(x,\; y))$

That is, the predicate P is not required to map an element of the set A to anything at all. But, if for an element x of A there is at least one y corresponding to it, then the image set B will contain at least one such y.

The resulting axiom, also called the axiom of boundedness or the axiom of collection, appears stronger, but either version can be derived from the axiom of replacement. Any functional predicate is a predicate of course, so boundedness also entails replacement, and thus the two axioms are equivalent (in the presence of the other Zermelo-Fraenkel axioms).

Example applications

---

The ordinal number ω2 = ω + ω (using the modern definition due to von Neumann) is the first ordinal that cannot be constructed without replacement. The axiom of infinity asserts the existence of the infinite sequence ω = {0, 1 ,2 ,...}, and only this sequence. One would like to define ω2 to be the sequence {ω, ω + 1, ω + 2,...}, but in general classes of ordinals need not be sets (the class of all ordinals is not a set, for example). Replacement allows one to replace each finite number n in ω with the corresponding ω + n, and guarantees that the class of these is a set. Note that one can easily construct a well-ordered set that is isomorphic to ω2 without resorting to replacement: simply take the disjoint union of two copies of ω, with the second copy greater than the first, but that this is not an ordinal since it is not totally ordered by inclusion.

Clearly then, the existence of assignment of an ordinal to every well-ordered set requires replacement as well. Similarly the von Neumann cardinal assignment which assigns a cardinal number to each set requires replacement, as well as axiom of choice.

Every countable limit ordinal requires replacement for its construction analogously to ω2. Larger ordinals rely on replacement less directly. For example ω₁ the first uncountable ordinal, can be constructed as follows: the set of countable well orders exists as a subset of ℘(N×N) by separation and powerset (a relation on A is a subset of A×A, and so an element of the power set ℘(A×A). A set of relations is thus a subset of ℘(A×A)). Replace each well-ordered set with its ordinal. This is the set of countable ordinals ω₁, which can itself be shown to be uncountable. The construction uses replacement twice; once to ensure an ordinal assignment for each well ordered set and again to replace well ordered sets by their ordinals. This is a special case of the result of Hartogs number, and the general case can be proved similarly.

The axiom of choice without replacement (ZC set theory) is not strong enough to show that Borel sets are determined; for this, you need replacement.

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 like when defining operations on subsets of proper classes.

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:

$\backslash forall\; A,\; \backslash exist\; B,\; \backslash forall\; C,\; C\; \backslash in\; B\; \backslash Leftrightarrow\; (C\; \backslash in\; A\; \backslash and\; 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 that occurs 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 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. axioms of set theory

Schema di assiomi di rimpiazzamento | Aksjomat zastępowania