記一則無窮組合的"應用題"

如圖， 作業題：

假設

是一個日常隨處可見的數量單位（強行應用題。。。）。 考慮如下鐵軌站點

， 其中一輛火車從

出發， 每個站

都會上來

個乘客， 並且如果車內不空， 則會有一個乘客下車， 這位下了車的乘客不會再回到火車上。 火車的終點站是

。 問： 到達終點站時火車上有多少人？

Notations：

是自然數的基數，

是第一個不可數的基數（或最小不可數良序集的序型）。

有一個特質， 那就是它的任意無界（unbounded）子集都與它一樣大。

Fact （special case of Fodor‘s Lemma）： 一個定義在序數上的函式

是regressive的， 當且僅當 對於其定義域的所有非零

， 我們都有

。 對於任意的regressive

， 我們都能找到一個無界的

， 使得

， 即

在

上為constant function。

Claim： 火車在到達

時是空車。

Proof： 定義如下函式

即， 如果在

有人下車， 那麼

就是這個人上車的站號， 要是沒人下車（也就是說車是空車）， 那麼

。 顯而易見，

是一個regressive的函式， 所以根據Fact， 我們可以找到一個無界的

， 使得

在

上是constant function。

特別的，

在

上的固定值一定為0， 因為不然的話，

意味著在

有

個乘客上了車， 與題目表述矛盾。 所以我們知道， 到站時火車上為空的站號在

中無界。

此時我們假設 火車在到達

時不為空。 那麼根據題目要求，

一定會有一個乘客下車。 這個乘客需要在某個

時上車。 然而

在

中無界， 所以我們可以找到一個

， 使得

。 即， 在

後的某個站點

， 火車將會成為空車。 所以在

上車的乘客不可能持續呆到

， 從而得到矛盾。 證畢。

後續： @反射序數 在評論裡提出了Fodor引理是否必須的建設性討論， 在此感謝。 由於評論形式不方便跟進， 我把思考結果寫在這裡。

這個題目有幾個要素：

的正則性

弱化的Fodor’s Lemma on

： 對於任意的regressive

， 我們都能找到一個無界的

， 使得

， 即

在

上為constant function。

車在 到達

時是空車。

在文章中， 我用了1和2來推論出3。 @反射序數 認為2不是必須的， 然後我們來回討論了一下他的證明。 他的證明中用到了

的正則性， 而我直覺認為2應該是必須的。 同時我也在stackexchange上問了同樣的問題。 經過一段時間思考後， 得出結論： 1，2，3在ZF中等價。 詳見：