ZF is sufficient to construct the von Neumann hierarchy, and prove that every set appears at some stage $V_\alpha$. This is the basis for Scott's trick, for instance. But how much of ZF is needed? Is bounded Zermelo/Mac Lane set theory enough, no Choice assumed? I know Foundation is necessary, and I'm not getting rid of that. I've seen something called the "rank axiom" in discussion of second-order version of original Zermelo (these notes), but I'm sure people have finely calibrated what precisely is needed.

To be honest, all I really want is an ordinal-valued rank function such that sets of rank at most $\alpha$ form a set, for all $\alpha$, and all sets have a rank. So if the von Neumann hierarchy doesn't work, I'm happy to work with something else (and for 'ordinals', I don't *need* von Neumann ordinals).

andthe von Neumann ordinals. $\endgroup$ – Asaf Karagila Jun 20 at 9:06