We define $\mathsf{BWKL}$ as follows:  

Every infinite binary tree of bounded width has an infinite path.


This obviously follows from $\mathsf{WKL}$. Is this principle true in $\mathsf{RCA}\_0$? If not, what does it need?


I've found [a paper](https://www.mimuw.edu.pl/~lak/buchi_strength.pdf) that addresses a related principle by the same name and shows it follows from $\mathsf{I\Sigma}^0\_2$ ($\Sigma^0\_2$-induction)... but it appears to assume that the tree has finite width, not merely bounded. (Also, I don't think it gives any lower bound on the principle's strength.)




---


EDIT: After some off-site discussion with Prof. Kołodziejczyk (one of the authors of this paper), I'd like to correct two minor confusions on my part. The bounded-width Konig's lemma discussed by Kołodziejczyk, Michalewski, Pradic, and Skrzypczak is precisely what I was asking about (which appears in Simpson & Yokoyama's work, as mentioned in Denis Hirschfeldt's answer). This is already pointed out in the journal version of the paper, though not in the preprint I'd linked. On the other hand, it is true that the paper does not address lower bounds, so it did not already answer my question.


Also: of course the distinction I was drawing between finite & bounded does not apply in this context; since we're talking about sets IN the model, it's straightforward to see that every bounded set (with maximum less than some first-order object) is finite (in the sense of having a canonical index). My only excuse: I always get bogged down in the details of first-order concerns, so I erred on the overly-cautious side.



Bounded-width Konig's lemma in reverse math
If I understand your question correctly, this principle is indeed provable from either WKL or I$\Sigma^0\_2$, but not in RCA$\_0$, or even WWKL$\_0$. See slides 12 and 13 in [this talk](https://www.birs.ca/cmo-workshops/2016/16w5072/files/Yokoyama.pdf) by Yokoyama. Based on [this paper](https://arxiv.org/pdf/1704.00931.pdf) by Nies, Triplett, and Yokoyama, it seems that these results will appear in a paper by Simpson and Yokoyama. It is interesting that, as noted in both these links, if we bound the size of prefix-free sets rather than just that of levels, the principle becomes provable in RCA$\_0$.


