In some recent work, I need a strengthening of König's Lemma to "trees" of arbitrary ordinal heights. Trees, in this context, are really just well-founded partially ordered sets. See, for instance, page 114 in Jech's Set Theory. One must be careful when modifying the "finite branching" hypothesis of König's Lemma in this situation, due to the existence of Aronszajn trees. The generalization is as follows:
Theorem: If $(S,<)$ is a well-founded partial order, such that for each ordinal $\beta$ the set of points of height $\beta$, denoted $S(\beta),$ is finite, then there is a branch in $S$ with the same height as $S.$
Here is my short proof of this result.
Proof: Let $\alpha$ be the height of $S.$ We recursively define the branch we want as follows. If $\{s_{i}\}_{i<\delta}$ is defined to height $\delta,$ then we choose $s_{\delta}$ to be any one of the finitely many elements $t\in S(\delta)$ that majorizes these previous points, and which has the additional property that for any ordinal $j$, $$(\ast)\,\, \text{ if }\delta<j<\alpha,\text{ then there exists some } s\in S(j) \text{ such that } t<s,$$ if such an element $t$ exists. Otherwise we end the recursion.
Let $\beta$ be the height of the branch we just defined. Suppose, by way of contradiction, that $\beta<\alpha.$ Then, from the fact that the height of $S$ is $\alpha,$ at least one of the finitely many elements $t\in S(\beta)$ satisfies $(\ast)$ with $\delta=\beta.$ Let $t_0$ be any one of them. Since our recursion ended at $\beta$, we know that $t_0$ does not majorize our branch. Let $\beta_0$ be the smallest index such that $s_{\beta_0}\not< t_0.$
Among the finitely many elements $t\in S(\beta)$ which do majorize $s_{\beta_0},$ there is at least one which satisfies $(\ast),$ since $s_{\beta_0}$ itself satisfies $(\ast).$ Let $t_1$ be any such element. Let $\beta_1$ be the smallest index such that $t_1$ doesn't majorize $s_{\beta_1}.$ Clearly $\beta_1>\beta_0.$
Repeating this process, we get an infinite list of elements $t_0,t_1,\ldots\in S(\beta),$ which are distinct since the corresponding $\beta_0,\beta_1,\ldots$ are distinct. This contradicts the finiteness of $S(\beta).$$\boxed{}$
My main question is whether or not there is a good reference for this result in the literature. While searching the internet, I found a different proof for it at this blog. The idea there is to pass to a slightly simpler structure.
Along those lines, if we replace $S$ with the set of points $S^{\ast}$ which satisfy $(\ast)$, then $(S^{\ast},<)$ is a wpo (that is, a well-founded partially ordered set with no infinite antichains) that has the same height as $S$. So it also suffices to prove this theorem for wpo's.
