Why is weak Kőnig's lemma weaker than Kőnig's lemma?

Question

Kőnig's lemma states that any finitely-branching tree with infinitely many nodes contains an infinite path. Weak Kőnig's lemma states the same thing about binary trees.

It's known that these are not equivalent over the base system $RCA_0$, but I'm struggling to see what goes wrong with the following construction:

• Take an arbitrary infinite finitely-branching tree $T$;
• Apply the Knuth transform to convert this into an equivalent binary tree $B$ on the same vertex-set;
• Use the statement of Weak Kőnig's lemma to find an infinite path $P = (x_1, x_2, x_3, \dots)$ in $B$.

Note that for each pair $(x_i, x_{i+1})$ of consecutive terms in $P$, $x_{i+1}$ is either a child or a sibling of $x_i$ when viewed as elements of $T$. We then define a subsequence which consists of only the terms $x_i$ such that $x_{i+1}$ is a child (rather than a sibling) of $x_i$. The resulting subsequence is then an infinite path in the original finitely-branching tree $T$.

Since this proof appears to be valid, my guess is that it's using something that can't be proved in $RCA_0$ (or indeed in $WKL_0$).

Answer 1

The issue is that for a finitely branching subtree $T$ of $\omega^{<\omega}$, the function $f$ mapping $\sigma$ to the greatest $n$ such that the concatenation $\sigma ^\frown n$ is in $T$ may not be computably bounded.

So $f$ may not "exist" in your model. (Even though the model knows that for each $\sigma$ such an $n$ exists.)

However $ACA_0$ is enough I believe, because you can repeatedly ask a Halting Problem oracle

"is there an $m>k$ with $\sigma ^\frown m\in T$?"

until the answer comes back as "no".

Answer 2

Interestingly, even Kőnig's lemma restricted to subtrees of $\omega^\omega$ for which every node has at most two children is equivalent to the full Kőnig's lemma, not weak Kőnig's lemma. This is because you can make such a tree $T$ for which an infinite branch gives you a halting oracle: For each $\sigma\in T$ of length $n$, put $\sigma\frown0$ in $T$, and if the $n$th program halts in $k$ steps, also put $\sigma\frown k$ in $T$, and cut off all descendents of $\sigma\frown0$ of length $n+k$ (that is, instead of following the previous rules for creating child nodes, don't create any child nodes). This is a computable tree, but the only infinite branch has a $0$ in the $n$th place iff the $n$th program does not halt. This can be relativized to any oracle, and hence gives you $ACA_0$, which as Bjorn Kjos-Hanssen noted, is enough to prove Kőnig's lemma.

And Kőnig's lemma for subtrees of $n^\omega$ is equivalent to weak Kőnig's lemma. The proof of Kőnig's lemma from weak Kőnig's lemma that you described can be carried out in $RCA_0$ in this case. Same goes if you let nodes in deeper levels have more children, just so long as there is a computable bound for the labels of the children that any given node can have.

This is all just to emphasize what Bjorn already hinted at: binary vs finitely-branching is sort of a red herring; the difference is whether or not there is a function bounding how far you have to look for child nodes.