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!
Best Answer
The following theorem is due to Neumer and is provable in $\sf ZF$:
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.