Editing Axiom schema of replacement (section)

== Relation to other axiom schemas ==
=== Simplifications ===
Some simplifications may be made to the axiom schema of replacement to obtain different equivalent versions. [[Azriel Lévy]] showed that a version of replacement with parameters removed, i.e. the following schema, is equivalent to the original form. In particular the equivalence holds in the presence of the axioms of extensionality, pairing, union and powerset.<ref>A. Kanamori, "[https://math.bu.edu/people/aki/20.pdf In Praise of Replacement]", pp.74--75. Bulletin of Symbolic Logic vol. 18, no. 1 (2012). Accessed 22 August 2023.</ref>

: <math>\forall A \, ( [ \forall x \, \exists ! y \, \phi(x, y, A) ]\ \Longrightarrow\ \exists B \, \forall y \, [y \in B \Leftrightarrow \exists x \in A \, \phi(x, y, A) ] )</math>

=== Collection ===
[[File:Codomain2 A B.SVG|thumb|Axiom schema of collection: the image <math>f[A]</math> of the domain set <math>A</math> under the definable class function <math>f</math> falls inside a set <math>B</math>.]]
The '''axiom schema of collection''' is closely related to and frequently confused with the axiom schema of replacement. 
Over the remainder of the ZF axioms, it is equivalent to the axiom schema of replacement. The axiom of collection is stronger than replacement in the absence of the [[power set axiom]]<ref>{{cite arXiv|eprint=1110.2430 |last1=Gitman |first1=Victoria |author2=Joel David Hamkins |last3=Johnstone |first3=Thomas A. |title=What is the theory ZFC without power set? |date=2011 |class=math.LO }}</ref> or its [[constructive set theory|constructive counterpart of ZF]] and is used in the framework of IZF, which lacks the [[law of excluded middle]], instead of Replacement which is weaker.<ref>{{cite journal | last1 = Friedman | first1 = Harvey M | last2 = Ščedrov | first2 = Andrej | title = The lack of definable witnesses and provably recursive functions in intuitionistic set theories | journal = Advances in Mathematics | volume = 57 | issue = 1 | pages = 1–13 | year = 1985 | issn = 0001-8708 | doi = 10.1016/0001-8708(85)90103-3
 | url = https://www.sciencedirect.com/science/article/pii/0001870885901033 }}</ref>

While replacement can be read to say that the image of a function is a set, collection speaks about images of relations and then merely says that some [[superset|superclass]] of the relation's image is a set. 
In other words, the resulting set <math>B</math> has no minimality requirement, i.e. this variant also lacks the uniqueness requirement on <math>\phi</math>. 
That is, the relation defined by <math>\phi</math> is not required to be a function—some <math>x\in A</math> may correspond to many <math>y</math>'s in <math>B</math>. In this case, the image set <math>B</math> whose existence is asserted must contain at least one such <math>y</math> for each <math>x</math> in the original set, with no guarantee that it will contain only one.

Suppose that the free variables of <math>\phi</math> are among <math>w_1,\dotsc,w_n,x,y</math>; but neither <math>A</math> nor <math>B</math> is free in <math>\phi</math>. Then the axiom schema is:
:<math>
\forall w_1,\ldots,w_n \,[(\forall x\, \exists\, y \phi(x, y, w_1, \ldots, w_n)) \Rightarrow \forall A\, \exists B\, \forall x \in A\, \exists y \in B\, \phi(x, y, w_1, \ldots, w_n)]
</math>

The axiom schema is sometimes stated without prior restrictions (apart from <math>B</math> not occurring free in <math>\phi</math>) on the predicate, <math>\phi</math>:
:<math>
\forall w_1,\ldots,w_n \, \forall A\, \exists B\,\forall x \in A\, [ \exists y \phi(x, y, w_1, \ldots, w_n) \Rightarrow \exists y \in B\,\phi(x, y, w_1, \ldots, w_n)]
</math>

In this case, there may be elements <math>x</math> in <math>A</math> that are not associated to any other sets by <math>\phi</math>. However, the axiom schema as stated requires that, if an element <math>x</math> of <math>A</math> is associated with at least one set <math>y</math>, then the image set <math>B</math> will contain at least one such <math>y</math>. The resulting axiom schema is also called the '''axiom schema of boundedness'''.

=== Separation ===
The [[axiom schema of separation]], the other axiom schema in ZFC, is implied by the axiom schema of replacement and the [[axiom of empty set]]. Recall that the axiom schema of separation includes
:<math>\forall A\, \exists B\, \forall C\, (C \in B \Leftrightarrow [C \in A \land \theta(C)])</math>
for each formula <math>\theta</math> in the language of set theory in which <math>B</math> is not free, i.e. <math>\theta</math> that does not mention <math>B</math>. 

The proof is as follows: Either <math>A</math> contains some element <math>a</math> validating <math>\theta(a)</math>, or it does not. In the latter case, taking the empty set for <math>B</math> fulfills the relevant instance of the axiom schema of separation and one is done. Otherwise, choose such a fixed <math>a</math> in <math>A</math> that validates <math>\theta(a)</math>. Now define <math>\phi(x, y):=(\theta(x)\land y=x)\lor(\neg\theta(x)\land y=a)</math> for use with replacement. Using function notation for this predicate <math>\phi</math>, it acts as the identity <math>F_a(x)=x</math> wherever <math>\theta(x)</math> is true and as the constant function <math>F_a(x)=a</math> wherever <math>\theta(x)</math> is false. By case analysis, the possible values <math>y</math> are unique for any <math>x</math>, meaning <math>F_a</math> indeed constitutes a class function. In turn, the image <math>B := \{F_a(x) : x\in A\}</math> of <math>A</math> under <math>F_a</math>, i.e. the class <math>A\cap\{x : \theta(x)\}</math>, is granted to be a set by the axiom of replacement. This <math>B</math> precisely validates the axiom of separation.

This result shows that it is possible to axiomatize ZFC with a single infinite axiom schema. Because at least one such infinite schema is required (ZFC is not finitely axiomatizable), this shows that the axiom schema of replacement can stand as the only infinite axiom schema in ZFC if desired. Because the axiom schema of separation is not independent, it is sometimes omitted from contemporary statements of the Zermelo-Fraenkel axioms.

Separation is still important, however, for use in fragments of ZFC, because of historical considerations, and for comparison with alternative axiomatizations of set theory. A formulation of set theory that does not include the axiom of replacement will likely include some form of the axiom of separation, to ensure that its models contain a sufficiently rich collection of sets. In the study of models of set theory, it is sometimes useful to consider models of ZFC without replacement, such as the models <math>V_\delta</math> in von Neumann's hierarchy.

The proof given above assumes the [[law of excluded middle]] for the proposition that <math>A</math> is [[Inhabited set|inhabited]] by a set validating <math>\theta</math>, and for any <math>\theta(x)</math> when stipulating that the relation <math>\phi</math> is functional. The axiom of separation is explicitly included in [[Constructive_set_theory#Separation|constructive set theory]], or a [[Axiom schema of predicative separation|bounded variant thereof]].

===Reflection===
{{main article|Reflection principle}}

Lévy's [[Reflection_principle#In_ZFC|reflection principle for ZFC]] is equivalent to the axiom of replacement, assuming the axiom of infinity. Lévy's principle is as follows:<ref>A. Kanamori, "[https://math.bu.edu/people/aki/20.pdf In Praise of Replacement]", p.73. Bulletin of Symbolic Logic vol. 18, no. 1 (2012). Accessed 22 August 2023.</ref>

: For any <math>x_1,\ldots,x_n</math> and any first-order formula <math>\phi(x_1,\ldots,x_n)</math>, there exists an <math>\alpha</math> such that <math>\phi(x_1,\ldots,x_n)\iff\phi^{V_\alpha}(x_1,\ldots,x_n)</math>.

This is a schema that consists of countably many statements, one for each formula <math>\phi</math>. Here, <math>\phi^M</math> means <math>\phi</math> with all quantifiers bounded to <math>M</math>, i.e. <math>\phi</math> but with every instance of <math>\exists x</math> and <math>\forall x</math> replaced with <math>\exists(x\in V_\alpha)</math> and <math>\forall(x\in V_\alpha)</math> respectively.