$|\alpha\times\alpha|=|\alpha|$ for infinite ordinal $\alpha$, definably

Question

I am trying to prove Proposition 1.7 of http://math.bu.edu/people/aki/7.pdf:

Proposition 1.7 (Halbeisen–Shelah). If $\aleph_0\le|X|$, then $|{\cal P}(X)|\not\le|{\rm Seq}(X)|$.

In words, this says that if $X$ is a Dedekind-infinite set, then the powerset of $X$ does not inject into the set ${\rm Seq}(X)$ of finite sequences on $X$. The proof is described in the link, and I follow most of it well enough. But it requires that we "canonically associate to [the well-ordering] $R$ of $Y$ a bijection $H:Y\to {\rm Seq}(Y)$", and I don't see how this is done.

I do have a proof that $|Y|=|{\rm Seq}(Y)|$, and by tracing the proof, in principle I should get an explicit bijection. The proof $|{\rm Seq}(Y)|\le|Y|$ produces an explicit injection by iterating an injection $f:Y\times Y\to Y$, so it is sufficient to prove the following:

There is a definable term $F$ in ZF such that if $\alpha$ is an infinite ordinal, then $F(\alpha)$ is an injection from $\alpha\times\alpha$ to $\alpha$.

My current (nonconstructive) proof of $|\alpha\times\alpha|=|\alpha|$ goes roughly as follows:

Define $\langle\alpha_1,\alpha_2\rangle\prec\langle\beta_1,\beta_2\rangle$ when $\max(\alpha_1,\alpha_2)<\max(\beta_1,\beta_2)$, or $\max(\alpha_1,\alpha_2)=\max(\beta_1,\beta_2)$ and $\alpha_1<\beta_1$, or $\alpha_1=\beta_1$ and $\alpha_2<\beta_2$. (In other words, lexicographic order on $\max(\alpha_1,\alpha_2);\alpha_1;\alpha_2$.) Then this is a well-order of $\sf On\times On$ with the property that for any infinite cardinal $\kappa$ and $\alpha<\kappa$, its restriction to $\alpha\times\alpha$ has order type $<\kappa$. Thus the unique order isomorphism corresponding to this well-order is a canonical bijection from $\kappa\times\kappa\to\kappa$ on cardinals, and any other $\alpha$ can be put in bijection with some cardinal $\kappa$, yielding a (non-canonical) bijection $\alpha\times\alpha\to\alpha$.

Answer 1

I'm recording my solution here for posterity. The key step is indeed the usage of Cantor normal form, but there are quite a few extra details that were not obvious to me at the start. First, some facts about ordinals, whose proofs are relatively straightforward and so ommitted:

If $\alpha<\omega^\gamma\le\beta$, then $\alpha+\beta=\beta$.

If $\alpha<\omega^\gamma$, then $\alpha\cdot\omega^\gamma=\omega^\gamma$.

The ordinal sum $\alpha+\beta$ is equinumerous to the disjoint union $\alpha\sqcup\beta$ (written $\alpha+\beta\approx\alpha\sqcup\beta$).

The ordinal product $\alpha\cdot\beta$ is equinumerous to the cartesian product $\alpha\times\beta$.

The ordinal exponential $\alpha^\beta$ is equinumerous to the set of functions $f:\beta\to\alpha$ such that $f(\gamma)=0$ for all but finitely many $\gamma<\beta$.

The last statement is equivalent to the Cantor normal form theorem. All of the bijections here are explicitly definable. This also implies that if $\alpha\approx\beta$, $\gamma\approx\delta$, then $\alpha+\gamma\approx\beta+\delta$, $\alpha\cdot\gamma\approx\beta\cdot\delta$, $\alpha^\gamma\approx\beta^\delta$, and additionally $\alpha+\beta\approx\beta+\alpha$ and $\alpha\cdot\beta\approx\beta\cdot\alpha$ follow from properties of the disjoint union and cartesian product mapping to equivalent statements for ordinals.

Now, using these bijections inductively on the Cantor normal form of $\alpha=\sum_{i=0}^n\omega^{\alpha_i}k_i$ (where the sequence is summed in descending order of $\alpha_i$'s), we have that $$\alpha=\sum_{i=0}^n\omega^{\alpha_i}k_i\approx\sum_{i=n}^0\omega^{\alpha_i}k_i=\omega^{\alpha_0}k_0\approx k_0\omega^{\alpha_0}=\omega^{\alpha_0},$$ where in the second equality we have reversed the order of summation and in the fourth we reverse the product using the bijections above. Thus we establish:

Lemma: there is a definable term $F$ such that for all infinite ordinals $\alpha$, $F(\alpha)$ is a bijection from $\alpha$ to $\omega^\gamma$ for some $\gamma$.

Then, since $\omega^2\approx\omega\times\omega\approx\omega$ by the original proof (which is constructive for cardinals), we have $$\alpha\approx\omega^\gamma\approx(\omega^2)^\gamma=\omega^{2\cdot\gamma}\approx\omega^{\gamma\cdot2}=\omega^\gamma\cdot\omega^\gamma\approx\omega^\gamma\times\omega^\gamma\approx\alpha\times\alpha,$$

and all the bijections here are explicitly definable.

Answer 2

Looking at the original Halbeisen-Shelah paper, they point out this in Corollary 3.

This is a corollary of the fact every ordinal has a Cantor normal form. We use that fact to produce an injection from $\operatorname{Seq}(\alpha)$ into $\alpha$, then use the Cantor-Bernstein theorem (which, given two injections gives a well-defined and relatively canonical bijection).