Would axiom schema of Replacement follow from well-ordered Replacement?

What I mean is that if we restrict Replacement to only well ordered sets, then can that still prove full Replacement?

Well ordered Replacement is the axiom schema stating that for every set $A$ that admits a well ordering on it, and for every definable function $f$ [not using the symbol $B$], there exists the set $B=\{f(x): x \in A \}$.

So can $\sf ZF\text{-Replacement+Well ordered Replacement} \vdash Replacement$

I think well ordered replacement is of the same consistency strength of full replacement, but can it prove it??

  • 4
    $\begingroup$ Re: your last paragraph, it is indeed of the same consistency strength. This is because using well-ordered replacement we can carry out the usual construction and analysis of $L$. $\endgroup$ Apr 27, 2021 at 22:02
  • 2
    $\begingroup$ It is enough to prove the principle of transfinite recursion for arbitrary well-orders; and I think that should be fine with WORep. $\endgroup$
    – Asaf Karagila
    Apr 28, 2021 at 8:16
  • $\begingroup$ @AsafKaragila, where can I read about that proof, that transfinite recursion for arbitrary well orders would prove replacement for all sets including non well orderable ones. $\endgroup$
    – Zuhair
    Apr 28, 2021 at 11:41
  • $\begingroup$ jdh.hamkins.org/… $\endgroup$
    – Asaf Karagila
    Apr 28, 2021 at 11:42
  • $\begingroup$ Ah! Thanks a lot. $\endgroup$
    – Zuhair
    Apr 28, 2021 at 11:51

1 Answer 1


We will show that replacement is provable in Zermelo set theory plus foundation plus well ordered replacement.

(1) Suppose $a$ is a set , $F$ is a formula, and for every $x \in a$ there is a unique $y$ such that $F(x,y)$. Suppose that if $x \in a$ and $F(x,y)$, then $y \in V_\beta$ for some ordinal $\beta$. Then there is a set $b$ such that

$y \in b \iff \exists x \in a : F(x,y)$

Proof: Define an equivalence relation W on a by (r,s)∈W iff (for all ordinals β, if Vβ exists, F(r,r') and F(s,s') then r'∈Vβ<-->s'∈Vβ). Define an ordering on the equivalence classes of W by [r]<[s] iff there

is an ordinal β such that r'∈Vβ and s'∉Vβ where F(r,r') and F(s,s'). The equivalence classes of W are well-ordered by this ordering. Let G(u,v) be the formula "there is an x∈a such that u=[x], F(x,y), β is the least ordinal such that y∈Vβ, and v=Vβ. By well ordered replacement there is a set c such that

v∈c<-->(G(u,v) for some u in the set of equivalence classes of W).LetY=Uc.
Then b={y∈Y|F(x,y) for some x∈a}

(2)For every x there is an ordinal β such that x∈Vβ.

Proof:Suppose that this is not true and that c is not in Vβ for any ordinal β. By well ordered replacement there is a set d which is the transitive closure of c. Let s={x∈dU{c}| x∉Vβ for any ordinal β}.

By foundation there is t∈s such that t intersect s is empty.Let F(x,y) be the formula "y is the least Vα with x∈Vα". By (1), there is a set b such that y∈b<-->(F(x,y) for some x∈t). Then

  t is in the power set of Ub. This contradicts our assumption about t.

Replacement follows from (1) and (2).

  • $\begingroup$ It's really hard to read this answer. Why not use $\rm\LaTeX$ for the math parts? $\endgroup$
    – Asaf Karagila
    Apr 29, 2021 at 7:46
  • $\begingroup$ I think its a good idea to link Hamkins proof (link is present in Asaf's comment on the original posting) to this answer. $\endgroup$
    – Zuhair
    Apr 29, 2021 at 10:47

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .