Proving the existence of $\beth_\omega$ in ZF

Question

I just wanted to confirm that the proof of the existence of Beth_omega, using Replacement, and defining a function from N into Beth_1, Beth_2..., does not assume Choice somehow. That is, the existence of Beth_omega is provable in ZF, right? Thanks, in advance.

Answer 1

The real question is what is $\beth_\omega$ when you don't assume choice.

Assuming $\sf ZF$ the axiom of choice is equivalent to "The power set of an ordinal can be well-ordered". So if $\beth$ numbers are assumed to be $\aleph$ numbers, the axiom of choice already holds, and your question is moot.

However, we can define cardinals in a broader way, which does not necessitate them being well-ordered. This means that we are now free to define the $\beth$ numbers as iterated powers from $\omega$ (or $V_\omega$, which is provably countable). This indeed means that $\beth_\alpha$ is the cardinality of $V_{\omega+\alpha}$, so $\beth_\omega$ is simply the cardinality of $V_{\omega+\omega}$. And indeed Replacement proves that $V_{\omega+\omega}$ is a set, so $\beth_\omega$ exists, in this case.