# A strong form of the Axiom Schema of Replacement

Let us consider the following stronger version of the Axiom Schema of Replacement (let us call it the Axiom Schema of Replacement for Definable Relations):

Let $$\varphi$$ be any formula in the language of ZF whose free variables are among the symbols $$x,y,A,w_1,\dots,w_n$$.

Then: $$\forall w_1\dots\forall w_n \forall A \;[(\forall x\;(x\in A\to\exists y\; \varphi))\to\exists B\;\forall x(x\in A\to \exists y\; (y\in B\wedge \varphi))]$$.

It can be shown that this Axiom Schema of Replacement for Definable Relations holds in ZF but for its proof one should apply the Axiom of Foundation (and the von Neumann cumulative hierarchy).

Question. Does the Axiom Schema of Replacement for Definable Relations follow from the axioms ZF with removed Axiom of Foundation?

• This is collection, rather than replacement. Also, you seem to missing the quantifier $\forall A$. Apr 3 at 21:57
• @JoelDavidHamkins Indeed, I forgot this $\forall A$, now added. Thank you. Why collection? This stronger version of relpacement can also be seen as a weaker form of choice: in the definable family of nonempty classes we can choose a family of nonempty subsets. Apr 3 at 22:04
• As Hamkins replied, your strong form of Replacement already has the name "Axiom of Collection." I vaguely recall we may construct a class permutation model of $\mathsf{ZFC}$ without Foundation if we start from $\mathsf{ZFC}$ with a proper class of urelements and make the class of urelements "amorphous" in the sense that every subclass of the class of urelements is either a set or a complement of a set, then Collection would fail over there. Apr 4 at 1:48
• I believe Bokai Yao's doctoral thesis might be the right place to find an answer to your question. Apr 4 at 1:51
• Apr 4 at 12:35

Your axiom is known as the axiom of collection.

There are a variety of contexts where it is known that replacement does not imply collection over what may seem reasonable theories.

For example, in set theory without the power set axiom, one cannot prove collection from replacement and the other standard axioms (first observed by Andrzej Zarach). Indeed, the theory axiomatized with replacement and not collection suffers from many issues, and it is now recognized that the correct axiomation of ZFC- uses collection and not just replacement. For example, in the replacement version of the theory, one cannot prove that $$\omega_1$$ is regular, even though one has AC, and one cannot prove the Los theorem for ultrapowers or that $$\Sigma_n$$ assertions are closed under bounded quantifiers. See the paper:

Similar issues arise in urelement set theory. It turns out to be surprisingly complicated to specify exactly what "set theory with urelements" should be. My student Bokai Yao has separated a hierarchy of many different theories, depending on whether one has replacement or collection and several other issues. Yao's dissertation is available at:

One of the classic models of set theory with urelements is constructed like this. Take a model $$V$$ of ZFC and interpret a model $$V(A)$$ of ZFCU with infinitely many urelements. Inside $$V(A)$$ take the model $$U$$ consisting of all sets whose transitive closure has at most finitely many urelements. One can prove that $$U$$ satisfies all the most basic urelement set theory axioms, including replacement, but not collection. Collection fails because for every finite $$n$$ there is a set with $$n$$ urelements, but one cannot collect on this in $$U$$. Replacement holds essentially because it is too hard for there to be unique witnesses of a property, as any two urelements are automorphic. One can use this fact to show that any instance of replacement is trivialized into the same finite-atom subuniverse. See Yao's dissertation for further discussion of this model, which has been known since the 1960s.

Finally, one can turn this model $$U$$ into a model $$\bar U$$ of your desired theory, simply by turning each of the urelement atoms into a Quine atom, that is, a set that is equal to its own singleton. This allows one to recover extensionality in $$\bar U$$, at the cost of foundation. But we still have replacement just as in $$U$$. So this is a model of the replacement version of ZFC-foundation, but without collection.

• Thank you for the answer. Very interesting. Is there any historical information about the Axiom Schema of Collection or just the Axiom of Collection mentioned in Yao's dissertation on page 93? When has it appeared for the first time and who did invent this axiom? Apr 4 at 4:23
• I am unsure of the history, but my understanding is that the collection scheme was considered from the earliest days of set theory. Collection+separation is typically mentioned as an alternative to replacement in ZF, and the second-order version you mention plays a similar role in GBC and KM. See also en.wikipedia.org/wiki/Axiom_schema_of_replacement#Collection. Apr 4 at 13:25