In recent work, Alfredo Roque Freire and I have realized that the axiom of well-ordered replacement is equivalent to the full replacement axiom, over the Zermelo set theory with foundation.

The well-ordered replacement axiom is the scheme asserting that if 𝐼 is well-ordered and every 𝑖 ∈𝐼 has unique 𝑦𝑖 satisfying a property 𝜙⁡(𝑖,𝑦𝑖), then {𝑦𝑖 ∣𝑖 ∈𝐼} is a set. In other words, the image of a well-ordered set under a first-order definable class function is a set.

Alfredo had introduced the theory Zermelo + foundation + well-ordered replacement, because he had noticed that it was this fragment of ZF that sufficed for an argument we were mounting in a joint project on bi-interpretation. At first, I had found the well-ordered replacement theory a bit awkward, because one can only apply the replacement axiom with well-orderable sets, and without the axiom of choice, it seemed that there were not enough of these to make ordinary set-theoretic arguments possible.

But now we know that in fact, the theory is equivalent to ZF.

Theorem. The axiom of well-ordered replacement is equivalent to full replacement over Zermelo set theory with foundation.

ZF=Z+foundation+well-ordered replacement

Proof. Assume Zermelo set theory with foundation and well-ordered replacement.

Well-ordered replacement is sufficient to prove that transfinite recursion along any well-order works as expected. One proves that every initial segment of the order admits a unique partial solution of the recursion up to that length, using well-ordered replacement to put them together at limits and overall.

Applying this, it follows that every set has a transitive closure, by iteratively defining ∪𝑛𝑥 and taking the union. And once one has transitive closures, it follows that the foundation axiom can be taken either as the axiom of regularity or as the ∈-induction scheme, since for any property 𝜙, if there is a set 𝑥 with ¬𝜙⁡(𝑥), then let 𝐴 be the set of elements 𝑎 in the transitive closure of {𝑥} with ¬𝜙⁡(𝑎); an ∈-minimal element of 𝐴 is a set 𝑎 with ¬𝜙⁡(𝑎), but 𝜙⁡(𝑏) for all 𝑏 ∈𝑎.

Another application of transfinite recursion shows that the 𝑉𝛼 hierarchy exists. Further, we claim that every set 𝑥 appears in the 𝑉𝛼 hierarchy. This is not immediate and requires careful proof. We shall argue by ∈-induction using foundation. Assume that every element 𝑦 ∈𝑥 appears in some 𝑉𝛼. Let 𝛼𝑦 be least with 𝑦 ∈𝑉𝛼𝑦. The problem is that if 𝑥 is not well-orderable, we cannot seem to collect these various 𝛼𝑦 into a set. Perhaps they are unbounded in the ordinals? No, they are not, by the following argument. Define an equivalence relation 𝑦 ∼𝑦′ iff 𝛼𝑦 =𝛼𝑦′. It follows that the quotient 𝑥/ ∼ is well-orderable, and thus we can apply well-ordered replacement in order to know that {𝛼𝑦 ∣𝑦 ∈𝑥} exists as a set. The union of this set is an ordinal 𝛼 with 𝑥 ⊆𝑉𝛼 and so 𝑥 ∈𝑉𝛼+1. So by ∈-induction, every set appears in some 𝑉𝛼.

The argument establishes the principle: for any set 𝑥 and any definable class function 𝐹 :𝑥 →Ord, the image 𝐹”𝑥 is a set. One proves this by defining an equivalence relation 𝑦 ∼𝑦′ ↔𝐹⁡(𝑦) =𝐹⁡(𝑦′) and observing that 𝑥/ ∼ is well-orderable.

We can now establish the collection axiom, using a similar idea. Suppose that 𝑥 is a set and every 𝑦 ∈𝑥 has a witness 𝑧 with 𝜙⁡(𝑦,𝑧). Every such 𝑧 appears in some 𝑉𝛼, and so we can map each 𝑦 ∈𝑥 to the smallest 𝛼𝑦 such that there is some 𝑧 ∈𝑉𝛼𝑦 with 𝜙⁡(𝑦,𝑧). By the observation of the previous paragraph, the set of 𝛼𝑦 exists and so there is an ordinal 𝛼 larger than all of them, and thus 𝑉𝛼 serves as a collecting set for 𝑥 and 𝜙, verifying this instance of collection.

From collection and separation, we can deduce the replacement axiom ◻

I’ve realized that this allows me to improve an argument I had made some time ago, concerning Transfinite recursion as a fundamental principle. In that argument, I had proved that ZC + foundation + transfinite recursion is equivalent to ZFC, essentially by showing that the principle of transfinite recursion implies replacement for well-ordered sets. The new realization here is that we do not need the axiom of choice in that argument, since transfinite recursion implies well-ordered replacement, which gives us full replacement by the argument above.

Corollary. The principle of transfinite recursion is equivalent to the replacement axiom over Zermelo set theory with foundation.

ZF=Z+foundation+transfinite recursion

There is no need for the axiom of choice.