Is Fodor's Lemma necessary for the $\omega_1$ train station puzzle?

Question

A common homework problem with Fodor's lemma is to imagine a train network with stations $\langle S_\alpha\mid \alpha<\omega_1+1\rangle$. The train starts at $S_0$ and stops at each station. At each station $S_\alpha$, two conditions hold: 1. if there's anyone on the train, then one passenger gets off; 2. $\omega$ many passengers get on. It is also assumed that the passengers that get off will never get on again (this is to avoid ambiguities in the behavior at limit stations). The question asks "how many passengers arrive at station $S_{\omega_1}$?".

Assuming the following very weak Fodor's lemma for $\omega_1$, we can show that the train arrives empty at $S_{\omega_1}$ (not typing the solution here because it seems like a pretty common assignment, so I wouldn't want to spoil it).

The weak Fodor's lemma for $\omega_1$ I'm referring to is this: if $f:\omega_1\to\omega_1$ is regressive, then there is an unbounded $S\subseteq\omega_1$ for which $f$ is constant (i.e., $f[S]={\gamma}$ for some $\gamma$).

My question is: over ZF, does the converse hold? More particularly, I wonder if the following implication is true (in ZF):

If the stations at which the train arrives empty is unbounded below $\omega_1$, then the weak Fodor's lemma for $\omega_1$ holds.

A couple of observations: if the stations at which the train arrives empty is unbounded below $\omega_1$, then the train arrives empty at $\omega_1$. In fact, the stations at which the train arrives empty form a club in $\omega_1$.

I guess a proof would involve some clever interpretation of $f$ and use that to build a "travel schedule". I have not been able to find one. It's also possible that the implication isn't true. Either way, help much appreciated!

Answer 1

The following theorem is due to Neumer and is provable in $\sf ZF$:

Suppose that $\operatorname{cf}(\alpha)>\omega$, if $f\colon\alpha\to\alpha$ is a regressive function, then there is some $\beta<\alpha$ and an unbounded set $A$ such that $f(a)<\beta$ for all $a\in A$.

So if $\omega_1$ is regular, and $f$ is a regressive function, there is a countable ordinal such that unboundedly many points are mapped below it. But since $\omega_1$ is regular, we can partition this unbounded set to the various fibers, and one of them will have to be unbounded. Therefore, the weak version of Fodor's lemma holds whenever $\omega_1$ is regular.

Of course, if $\omega_1$ is singular, which is of course consistent with $\sf ZF$, then the above is moot and by fixing a cofinal sequence $\alpha_n$ for $n<\omega$, we can define a regressive function $\alpha\mapsto\min\{n\mid\alpha<\alpha_n\}$, which is not constant on any unbounded set (we may need to assume that $\alpha_0=0$ and $\alpha_1=\omega$, but that's fine). Now, if $\omega_1$ is singular indeed, then we can easily arrange for the train to arrive with as many passengers we want (none, finitely many, countably many, or even $\aleph_1$ of them if you allow "countably many" rather than explicitly enumerated countable set of passengers!), and therefore the ticketmaster at $S_{\omega_1}$ are no longer safely taking a nap.

To your question, then, yes, the emptiness of the train at $S_{\omega_1}$ is equivalent to the weak Fodor's lemma.

Answer 2

After some coffee and scratch papers, I've found a solution. (I'm accepting Asaf's answer which was posted an hour before mine).

Write Fodor($X,Y,P$) for "every regressive function $f:X\to Y$ is constant on some subset of $X$ of type $P$". For example, the usual statement of Fodor's lemma is "for all regular cardinal $\kappa$ and stationary $S\subseteq \kappa$, Fodor($S,\kappa,$ stationary)". And the weak Fodor's lemma for $\omega_1$ is "Fodor($\omega_1,\omega_1$, unbounded)"

I claim that Fodor($\omega_1,\omega_1$, unbounded) implies the regularity of $\omega_1$ over ZF.

Proof: suppose that $\omega_1$ is not regular, and let $g:\omega\to\omega_1$ be cofinal in $\omega_1$. We will construct a regressive $f:\omega_1\to\omega_1$ that is not constant on any unbounded subset of $\omega_1$. $f$ is defined as follows: $$ f(\alpha)= \begin{cases} \emptyset &\text{ if } \alpha\in\omega\\ \beta &\text{ if } \beta \text{ is the largest } \eta\in ran(g) \text{ with } \eta<\alpha \end{cases} $$ $f$ is well-defined, because $g$ is cofinal and has range of ordertype $\omega$ (so that ``largest" makes sense). To see that $f$ cannot be constant on an unbounded set, suppose for contradiction that $f$ is constant on some $S$ that's unbounded in $\omega_1$. That is, $f$ maps every $s\in S$ to a fixed $\gamma$. This would imply that $\gamma=g(k)$ is the largest element in $ran(g)$ that is below every $s\in S$. But since $S$ in unbounded, there must be some $s'\in S$ such that $s'>g(k+1)>g(k)$, so $\gamma=g(k)$ cannot be largest. This completes the proof of claim.

Now I claim that Fodor($\omega_1,\omega_1$, unbounded) is necessary for concluding that the train arrives empty at $S_{\omega_1}$. To show this, I find a model of ZF in which $\omega_1$ is singular, and the train arrives nonempty at $S_{\omega_1}$.

Take a model of ZF where $\omega_1$ is a countable union of countable sets. Such models can be found e.g., in Feferman & Levy's "Independence results in set theory by Cohen's method II". Let $\omega_1=\bigcup_{n\in\omega\smallsetminus\{0\}}A_n$ witness this. We arrange the following travel plan: write $A_0$ for the set of passengers that get on at $A_0$. Let $f_0: \omega+1\to A_0$ witness that countability of $A_0$. For each station $S_n$ with finite index, let $f_0(n)$ get off, and let $A_n$ get on. When the train arrives at $S_\omega$, let $f_0(\omega)$ get off, and the train has $\omega_1$ many passengers. Let these passengers get off one by one. Then at station $S_{\omega_1}$, only those passengers in $\bigcup_{n\in\omega\smallsetminus\{0\}}A_n$ have gotten off, and the train is not empty.