Say two players ($A$ and $B$) are playing a game of length $\omega$ on $\omega_1$ in which they play a countable ordinal turn by turn (starting with $A$) and form a sequence of countable ordinals, $(a_0,b_0,a_1,b_1, \ldots)$ (they can see each other’s moves) of length $\omega$. Player $B$ wins if the set of the (values of the) obtained sequence is an ordinal, $A$ wins otherwise. Can player $B$ have a winning strategy in ZF + “$\omega_1$ is regular”(by which I mean, “Can ZF + ”$\omega_1$ is regular” prove that there is a winning strategy for $B$?”)?
Obvious strategy is to play every ordinal under every ordinal played by the opponent, which requires choice of some form, and I am not seeing how to do this using only the fact that $\omega_1$ is regular.
Note that converse is trivially true so if the answer is “yes”, then we have an equivalence. Thank you.
From Noah's comment, we see that if there is a sequence $\langle e_\alpha : \alpha < \omega_1 \rangle$, where each $e_\alpha \colon \omega \to \alpha$ is a surjection, then Player B has a winning strategy.
On the other hand this is easily seen to be necessary for a winning strategy as well. Namely if $\sigma$ is a winning strategy for B and $\alpha < \omega_1$ is given, we play a game according to $\sigma$ where A constantly plays $\alpha$. As $\sigma$ is winning, the plays of $B$ enumerate some ordinal greater or equal than $\alpha$ in type $\omega$.
Thus we have an equivalence.
I claim that "$\omega_1$ is regular" is in general not sufficient. The most basic example is the so called Solovay model. Namely, in this model DC (dependent choice) holds, so $\omega_1$ is regular. But there is no injection from $\omega_1$ into the reals. A sequence $\langle e_\alpha : \alpha < \omega_1 \rangle$ as above on the other hand does give an injection from $\omega_1$ by associating each $e_\alpha$ to a well-order on $\omega$ of type $\alpha$ (which is a subset of $\omega\times\omega$, and thus a real).
The Solovay model uses an inaccessible cardinal in $L$ and in fact this is necessary here. If $\omega_1$ is regular, then it is also regular in $L$. If it was a successor, say $\kappa^+$, then, since choice holds in $L$, we have a sequence of surjections $f_\alpha \colon \kappa \to \alpha$ for every $\alpha < \kappa^+$. Since $\kappa < \omega_1$ in $V$, we have a surjection $f \colon \omega \to \kappa$ in $V$. But now we can combine these functions to get our $e_\alpha$'s.