Editing Axiom schema of replacement (section)

== Applications ==
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 [[John von Neumann|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 [[class (set theory)|class]]es 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&nbsp;– simply take the [[disjoint union]] of two copies of ω, with the second copy greater than the first&nbsp;– but that this is not an ordinal since it is not totally ordered by inclusion.
* Larger ordinals rely on replacement less directly. For example, ω<sub>1</sub>, the [[first uncountable ordinal]], can be constructed as follows&nbsp;– the set of countable well orders exists as a subset of <math>P({\mathbb N}\times {\mathbb N})</math> by [[axiom of separation|separation]] and [[axiom of power set|powerset]] (a [[binary relation|relation]] on ''A'' is a subset of <math>A\times A</math>, and so an element of the [[power set]] <math>P(A\times A)</math>. A set of relations is thus a subset of <math>P(A\times A)</math>). Replace each well-ordered set with its ordinal. This is the set of countable ordinals ω<sub>1</sub>, 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 <math>A^n=A^{n-1}\times A</math> and for large <math>A</math>, the set <math>\{A^n\mid n\in {\mathbb N}\}</math> 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 (mathematician)|Harvey Friedman]] showed that at least some instances of replacement are required to show that [[Borel set|Borel games]] are [[determinacy|determined]]. The proven result is [[Donald A. Martin]]'s [[Borel determinacy theorem]]. A later, more careful analysis by Martin of the result showed that it only requires replacement for functions with domain an arbitrary countable [[ordinal number|ordinal]].
* ZF with replacement proves the [[consistency]] of Z, as the set V<sub>ω·2</sub> is a [[model (logic)|model]] of Z whose existence can be proved in ZF. The [[cardinal number]] <math>\aleph_\omega</math> 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.