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](https://en.wikipedia.org/wiki/Left-child_right-sibling_binary_tree) 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$).



Why is weak Kőnig's lemma weaker than Kőnig's lemma?
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".


