I am curious about the reverse math status of the below statement. Note that we work in second-order RM, i.e. 'closed set' is interpreted as in Simpson's excellent SOSOA.


*For any closed $E\subset [0,1]$ and $\epsilon >0$, there are $x\_0, \dots, x\_k \in E$ such that $\cup\_{i\leq k} B(x\_i, \epsilon)$ covers $E$.*


It seems that enough induction suffices to prove this theorem, but I cannot seem to formulate a nice minimal/small fragment.


Note that the above statement can be interpreted as asking for a finite sub-covering of the *uncountable* covering $\cup\_{x\in E} B(x, \epsilon)$ of $E$.



Reverse Mathematics strength of fixed radius covering theorem
The statement in provable in $\mathrm{WKL}\_0$.


Consider the following proof. Fix $k>1/\epsilon$, let $I=\{i<k:E\cap[i/k,(i+1)/k]\ne\varnothing\}$, and let $\{x\_i:i\in I\}$ be such that $x\_i\in E\cap[i/k,(i+1)/k]$. Then for any $x\in E$, we have $x\in[i/k,(i+1)/k]$ for some $i\in I$, hence $|x-x\_i|\le1/k<\epsilon$.


Now, let us formalize this. By Simpson’s definition, $E=[0,1]\smallsetminus\bigcup\_n(a\_n,b\_n)$, where $\{a\_n,b\_n:n\in\mathbb N\}$ is a sequence of rationals. By the Heine–Borel lemma, provable in $\mathrm{WKL}\_0$, we have
$$E\cap[i/k,(i+1)/k]=\varnothing\iff\exists n\:[i/k,(i+1)/k]\subseteq\bigcup\_{i<n}(a\_i,b\_i),$$
which is a $\Sigma^0\_1$ property. Thus, $I=\{i<k:E\cap[i/k,(i+1)/k]\ne\varnothing\}$ exists by bounded $\Sigma^0\_1$-comprehension, provable in $\mathrm{RCA}\_0$. Let $T$ be the set of sequences $\langle\vec x^0,\dots,\vec x^n\rangle$ such that


* $\vec x^j$ is a vector $\langle x^j\_i:i\in I\rangle$,
* $x^j\_i$ is a dyadic rational with denominator (at most) $2^j$,
* $|x^{j+1}\_i-x^j\_i|\le2^{-(j+1)}$,
* $[x^j\_i-2^{-j},x^j\_i+2^{-j}]\cap[i/k,(i+1)/k]\smallsetminus\bigcup\_{l<j}(a\_l,b\_l)\ne\varnothing$.


Then $T$ is a $3^k$-ary (or so) tree with elements of arbitrarily large height, hence it has an infinite branch by $\mathrm{WKL}\_0$. It is easy to see that such a branch determines a vector $\vec x=\langle x\_i:i\in I\rangle$ of reals such that $x\_i\in[i/k,(i+1)/k]\cap E$.


