Axiom schema of replacement

Axiom schema of replacement: the image ${\displaystyle F[A]}$ of the domain set ${\displaystyle A}$ under the definable class function ${\displaystyle F}$ is itself a set, ${\displaystyle B}$.

Suppose ${\displaystyle P}$ is a definable binary relation (which may be a proper class) such that for every set ${\displaystyle x}$ there is a unique set ${\displaystyle y}$ such that ${\displaystyle P(x,y)}$ holds. There is a corresponding definable function ${\displaystyle F_{P}}$, where ${\displaystyle F_{P}(x)=y}$ if and only if ${\displaystyle P(x,y)}$. Consider the (possibly proper) class ${\displaystyle B}$ defined such that for every set ${\displaystyle y}$, ${\displaystyle y\in B}$ if and only if there is an ${\displaystyle x\in A}$ with ${\displaystyle F_{P}(x)=y}$. ${\displaystyle B}$ is called the image of ${\displaystyle A}$ under ${\displaystyle F_{P}}$, and denoted ${\displaystyle F_{P}[A]}$ or (using set-builder notation) ${\displaystyle \{F_{P}(x):x\in A\}}$.

The axiom schema of replacement states that if ${\displaystyle F}$ is a definable class function, as above, and ${\displaystyle A}$ is any set, then the image ${\displaystyle F[A]}$ is also a set. This can be seen as a principle of smallness: the axiom states that if ${\displaystyle A}$ is small enough to be a set, then ${\displaystyle F[A]}$ is also small enough to be a set. It is implied by the stronger axiom of limitation of size.

Because it is impossible to quantify over definable functions in first-order logic, one instance of the schema is included for each formula ${\displaystyle \phi }$ in the language of set theory with free variables among ${\displaystyle w_{1},\dotsc ,w_{n},A,x,y}$; but ${\displaystyle B}$ is not free in ${\displaystyle \phi }$. In the formal language of set theory, the axiom schema is:

${\displaystyle {\begin{aligned}\forall w_{1},\ldots ,w_{n}\,\forall A\,([\forall x\in A&\,\exists !y\,\phi (x,y,w_{1},\ldots ,w_{n},A)]\ \Longrightarrow \ \exists B\,\forall y\,[y\in B\Leftrightarrow \exists x\in A\,\phi (x,y,w_{1},\ldots ,w_{n},A)])\end{aligned}}}$

For the meaning of ${\displaystyle \exists$ !} , see uniqueness quantification.

For clarity, in the case of no variables ${\displaystyle w_{i}}$, this simplifies to:

${\displaystyle {\begin{aligned}\forall A\,([\forall x\in A&\,\exists !y\,\phi (x,y,A)]\ \Longrightarrow \ \exists B\,\forall y\,[y\in B\Leftrightarrow \exists x\in A\,\phi (x,y,A)])\end{aligned}}}$

So whenever ${\displaystyle \phi }$ specifies a unique ${\displaystyle x}$-to-${\displaystyle y}$ correspondence, akin to a function ${\displaystyle F}$ on ${\displaystyle A}$, then all ${\displaystyle y}$ reached this way can be collected into a set ${\displaystyle B}$, akin to ${\displaystyle F[A]}$.

The axiom schema of replacement is not necessary for the proofs of most theorems of ordinary mathematics. Indeed, Zermelo set theory (Z) already can interpret second-order arithmetic and much of type theory in finite types, which in turn are sufficient to formalize the bulk of mathematics. Although the axiom schema of replacement is a standard axiom in set theory today, it is often omitted from systems of type theory and foundation systems in topos theory.

At any rate, the axiom schema drastically increases the strength of ZF, both in terms of the theorems it can prove - for example the sets shown to exist - and also in terms of its proof-theoretic consistency strength, compared to Z. Some important examples follow:

• Using the modern definition due to von Neumann, proving the existence of any limit ordinal greater than ω requires the replacement axiom. The ordinal number ω·2 = ω + ω is the first such ordinal. The axiom of infinity asserts the existence of an infinite set ω = {0, 1, 2, ...}. One may hope to define ω·2 as the union of the sequence {ω, ω + 1, ω + 2,...}. However, arbitrary such classes of ordinals need not be sets - for example, the class of all ordinals is not a set. Replacement now allows one to replace each finite number n in ω with the corresponding ω + n, and thus guarantees that this class is a set. As a clarification, 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.
• 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 ${\displaystyle P({\mathbb {N} }\times {\mathbb {N} })}$ by separation and powerset (a relation on A is a subset of ${\displaystyle A\times A}$, and so an element of the power set ${\displaystyle P(A\times A)}$. A set of relations is thus a subset of ${\displaystyle P(A\times 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.
• In light of the above, the existence of an 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.
• For sets of tuples recursively defined as ${\displaystyle A^{n}=A^{n-1}\times A}$ and for large ${\displaystyle A}$, the set ${\displaystyle \{A^{n}\mid n\in {\mathbb {N} }\}}$ has too high of a rank for its existence to be provable from set theory with just the axiom of power set, choice and without replacement.
• Similarly, Harvey Friedman showed that replacement is required to show that Borel games are determined. The proven result is Donald A. Martin's Borel determinacy theorem.
• ZF with replacement proves the consistency of Z, as the set V_ω·2 is a model of Z whose existence can be proved in ZF. The cardinal number ${\displaystyle \aleph _{\omega }}$ is the first one which can be shown to exist in ZF but not in Z. For clarification, note that Gödel's second incompleteness theorem shows that each of these theories contains a sentence, "expressing" the theory's own consistency, that is unprovable in that theory, if that theory is consistent - this result is often loosely expressed as the claim that neither of these theories can prove its own consistency, if it is consistent.

The axiom schema of replacement was not part of Ernst Zermelo's 1908 axiomatisation of set theory (Z). Some informal approximation to it existed in Cantor's unpublished works, and it appeared again informally in Mirimanoff (1917).[4]

Abraham Fraenkel, between 1939 and 1949

Thoralf Skolem, in the 1930s

Its publication by Abraham Fraenkel in 1922 is what makes modern set theory Zermelo-Fraenkel set theory (ZFC). The axiom was independently discovered and announced by Thoralf Skolem later in the same year (and published in 1923). Zermelo himself incorporated Fraenkel's axiom in his revised system he published in 1930, which also included as a new axiom von Neumann's axiom of foundation.[5] Although it is Skolem's first order version of the axiom list that we use today,[6] he usually gets no credit since each individual axiom was developed earlier by either Zermelo or Fraenkel. The phrase “Zermelo-Fraenkel set theory” was first used in print by von Neumann in 1928.[7]

Zermelo and Fraenkel had corresponded heavily in 1921; the axiom of replacement was a major topic of this exchange.[6] Fraenkel initiated correspondence with Zermelo sometime in March 1921. However, his letters before the one dated 6 May 1921 are lost. Zermelo first admitted to a gap in his system in a reply to Fraenkel dated 9 May 1921. On 10 July 1921, Fraenkel completed and submitted for publication a paper (published in 1922) that described his axiom as allowing arbitrary replacements: "If M is a set and each element of M is replaced by [a set or an urelement] then M turns into a set again" (parenthetical completion and translation by Ebbinghaus). Fraenkel's 1922 publication thanked Zermelo for helpful arguments. Prior to this publication, Fraenkel publicly announced his new axiom at a meeting of the German Mathematical Society held in Jena on 22 September 1921. Zermelo was present at this meeting; in the discussion following Fraenkel's talk he accepted the axiom of replacement in general terms, but expressed reservations regarding its extent.[6]

Thoralf Skolem made public his discovery of the gap in Zermelo's system (the same gap that Fraenkel had found) in a talk he gave on 6 July 1922 at the 5th Congress of Scandinavian Mathematicians, which was held in Helsinki; the proceedings of this congress were published in 1923. Skolem presented a resolution in terms of first-order definable replacements: "Let U be a definite proposition that holds for certain pairs (a, b) in the domain B; assume further, that for every a there exists at most one b such that U is true. Then, as a ranges over the elements of a set M_a, b ranges over all elements of a set M_b." In the same year, Fraenkel wrote a review of Skolem's paper, in which Fraenkel simply stated that Skolem's considerations correspond to his own.[6]

Zermelo himself never accepted Skolem's formulation of the axiom schema of replacement.[6] At one point he called Skolem's approach “set theory of the impoverished”. Zermelo envisaged a system that would allow for large cardinals.[8] He also objected strongly to the philosophical implications of countable models of set theory, which followed from Skolem's first-order axiomatization.[7] According to the biography of Zermelo by Heinz-Dieter Ebbinghaus, Zermelo's disapproval of Skolem's approach marked the end of Zermelo's influence on the developments of set theory and logic.[6]

• Ebbinghaus, Heinz-Dieter (2007), Ernst Zermelo: An Approach to His Life and Work, Springer Science & Business Media, ISBN 978-3-540-49553-6.
• Halmos, Paul R. (1974) [1960], Naive Set Theory, Springer-Verlag, ISBN 0-387-90092-6.
• Jech, Thomas (2003), Set Theory: The Third Millennium Edition, Revised and Expanded, Springer, ISBN 3-540-44085-2.
• Kunen, Kenneth (1980), Set Theory: An Introduction to Independence Proofs, Elsevier, ISBN 0-444-86839-9.