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$.
Best Answer
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$.