Proving that $\alpha\approx|\alpha|$ is not constructive

Question

$\sf ZF$ tells us that for every ordinal $\alpha$ there is a bijection $f:\alpha\to|\alpha|$, more or less by the definition of $|\alpha|$, the cardinal of $\alpha$. What I would like to show is that there is no way to canonically choose this bijection. I see this used as a lemma in lots of negative constructions, but it seems to be folklore.

To be more precise, I would like to prove that

There is no term $F$ in the language of $\sf ZFC$ such that for all $\alpha$, $F(\alpha):\alpha\to|\alpha|$ is a bijection (provably in $\sf ZFC$).

There is a closely related alternative formulation in the object language (no quantifying over terms) of $\sf ZF$:

${\sf ZF}\nvdash \exists f\,\forall\alpha<\omega_1\,f(\alpha):\alpha\overset{\rm bij.}{\to}|\alpha|$.

This is a bit stronger claim since it only goes as high as $\omega_1$, but I'm quite sure that even this is too much for $\sf ZF$. (Of course it is easy for $\sf ZFC$ to prove this, which is why the $\sf ZFC$ version can only be foiled by a proper class of bijections.)

Answer 1

For a positive answer to the first part of the question, perhaps the easiest thing is to consider a generic extension $V[g]$ by the poset $\operatorname{Col}(\omega,\omega_1)$. In the generic extension there is a bijection from $(\omega_1)^V$ to $\omega$. However, no such bijection can be definable from $(\omega_1)^V$: the forcing is homogeneous, so all ordinal-definable subsets of the ground model in the generic extension are in the ground model.

For the second part of the question, let me give an alternative to Asaf's answer by mentioning that the Axiom of Determinacy implies (in $\mathsf{ZF}$) that there is no function that chooses, for each countable ordinal $\alpha$, a well-ordering of $\omega$ of order type $\alpha$. This is because such wellorderings can be coded as subsets of $\omega$ using a definable pairing function $\omega \times \omega \cong \omega$, so such a choice function would be coded by a function from $\omega_1$ to $\mathcal{P}(\omega)$, which would clearly be injective. However, $\mathsf{ZF} + \mathsf{AD}$ proves that $\omega_1$ is measurable, so no such injection $\omega_1 \to \mathcal{P}(\omega)$ can exist. (To see this, adapt the usual $\mathsf{ZFC}$ proof that measurable cardinals are strong limit.)

Answer 2

First note that if $A$ is a countable set of countable ordinals, and $F$ is a function such that for every $\alpha\in A$, $F(\alpha)$ is an injection from $\alpha$ into $\omega$, then $\bigcup A=\sup A$ is also countable.

This is because $\bigcup A$ is a countable union of uniformly enumerated countable sets.

Next, look at the Feferman-Levy model, where $\omega_1$ is singular, and observe that this means that there is no such $F$ for countable sets of ordinals, let alone all the countable ordinals.