Skolem proved the need for the axiom schema of Replacement by, in essence, showing that $V\_{ω+ω}$ is a model of Zermelo's set theory Z (the smallest "natural" model) and, hence, that the existence of the set $\{ω, ℘(ω), ℘(℘(ω)), ...\}$ is independent of Z (where ω is understood to be the usual von Neumann ordinal). Now, Skolem's independence proof depends on the fact that $ω$ is already of infinite rank and, hence, that the above set will be unbounded in $V\_{ω+ω}$. But now let ZU be Z + Urelements and an axiom asserting that the urelements form a set A, and consider the set $A^\ast = \{A, ℘(A), ℘(℘(A)), ...\}$. The members of $A^\ast$ are all of finite rank, so Skolem's proof doesn't seem to apply here — $A^\ast$ will exist in $V'\_{\omega+1}$, where $V'\_{\omega+\omega}$ is the cumulative hierarchy up to $\omega+\omega$ starting with $A$ (which I assume is the smallest natural model of ZU with $V'\_0 = A$). Nonetheless, it seems to me (= Not A Set Theorist) that proving *in general* that $A^\*$ exists should require Replacement as well. But I don't see how to show this. If A is assumed to be finite, we can show that $A^\ast$ exists without Replacement by coding all the hereditarily finite sets in $V'\_\omega$ as finite ordinals and relying on the fact that inductively defined functions from ω into ω are all legit in ZU (in particular the function $n \mapsto V'\_n$). Such a coding is obviously out of the question if A is infinite. I reckon the proof, if there is a proof, that the existence of $A^\ast$ is independent of ZU would involve constructing an inner model of ZU in which $A^\ast$, or whatever is playing its role, is missing from the $\omega+1^\text{th}$ level, but figuring out how to do that is a bit beyond my abilities. Any help appreciated.



Independence of a certain set w.r.t. Z set theory with urelements
If you start with the elements in $V\_{\omega+1}$ and a nonempty set $A$ of urelements, and then simply close under pairing, unions and power sets, you get a model of Zermelo + urelements, but where $A^\*$ doesn't exist, even when $A$ is finite, since it doesn't appear after any finitely many applications of pairing, unions and power set (despite your remarks about coding). So you don't avoid the problem by considering urelements. You still need replacement to prove $A^\*$ exists, even when $A$ is finite.


