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$).
Best Answer
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
until the answer comes back as "no".