From Vitali to Heine-Borel in reverse mathematics

Question

The Vitali and Heine-Borel covering theorems are house-hold names of analysis, and rightly well-studied in reverse mathematics. As shown in Simpson's excellent monograph [1], for countable coverings of the unit interval, the Heine-Borel theorem is equivalent to WKL (weak Koenig's lemma), while the Vitali covering theorem is equivalent to WWKL (weak weak Koenig's lemma). The theorem numbers in [1] are IV.1.2 and X.1.13.

My question is then as follows:

Is there a natural statement X such that [WWKL +X ] $\leftrightarrow$ WKL, say over RCA$_0$?

Here, $X$ should be weaker than WKL, obviously. Results in related frameworks (computability theory, Weihrauch reducibility, constructive math, ...) are also welcome.

PS: I am asking this question because in the case of uncountable coverings, such an X does exist.

[1] Stephen G. Simpson, Subsystems of second order arithmetic, 2nd ed., Perspectives in Logic, Cambridge University Press, 2009.

Answer 1

In the Weihrauch reducibility framework, my hunch is that the answer is no. Of course, "natural statement" does not lend itself to easily disprove existence, so I can't rule out changing my mind in the future.

First, we are looking at principles below $\mathrm{WKL}$ which are incomparable with $\mathrm{WWKL}$. To my knowledge, the only such principles which were studied in the literature are variants of convex choice $\mathrm{XC}_{[0,1]^n}$. All these variants are themselves below the principle $\mathrm{XC}_{[0,1]}^\diamond$, which lets us invoke choice for convex subsets of the unit interval (ie intervals) finitely many times (with subsequent queries depending on previous answers). Note that $\mathrm{XC}_{[0,1]}$ is equivalent to the intermediate value theorem.

However, $(\mathrm{XC}_{[0,1]} \sqcup \mathrm{WWKL})^\diamond <_{\mathrm{W}} \mathrm{WKL}$ (the left hand side is "make finitely many calls to both $\mathrm{XC}_{[0,1]}$ and to $\mathrm{WWKL}$). The reason for this is that on a computable input, $\mathrm{XC}_{[0,1]}$ can always return something computable, and $\mathrm{WWKL}$ can always return some ML-random. Thus, the left-hand side can always return something which is computable from a ML-random, but this doesn't hold for $\mathrm{WKL}$, as $\mathrm{PA}$-degrees are not computable from ML-randoms.

Another piece of evidence is that there is no multivalued function $g$ at all such that $\mathrm{WKL} \leq_{\mathrm{W}} \mathrm{WWKL} \circ g$. On the right, we have that every input has a positive measure of potential solutions, and $\mathrm{WKL}$ has instances where the Turing-upper cone of solutions is measure $0$.