A strong form of the Axiom Schema of Replacement

Question

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?

Answer 1

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:

• Gitman, Victoria; Hamkins, Joel David; Johnstone, Thomas A., What is the theory ZFC without power set?, Math. Log. Q. 62, No. 4-5, 391-406 (2016). ZBL1375.03059.

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:

• Bokai Yao, Set theory with urelements, arxiv:2303.14274.

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.