Reverse Mathematics strength of fixed radius covering theorem

Question

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

Answer 1

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

Answer 2

Let me strengthen Emil's excellent answer to a finer reverse mathematical result.

Recall that $\mathsf{RCA}_0^\star=\mathsf{EA}+\mathsf{I}\Delta^0_1+\Delta^0_1\textsf{-CA}$ and $\mathsf{WKL}_0^\star=\mathsf{RCA}_0^\star+\mathsf{WKL}$. Over $\mathsf{WKL}_0^{\star}$ the principle is equivalent to $\Sigma^0_1$-induction and over $\mathsf{RCA}_0^{\star}$ the principle is equivalent to $\forall X\Sigma^0_1$-induction. Since over $\mathsf{WKL}_0^{\star}$ every $\forall X\Sigma^0_1$-predicate could be transformed to an equivalent $\Sigma^0_1$-predicate, I'll simply prove that over $\mathsf{RCA}_0^{\star}$ the principle is equivalent to $\forall X\Sigma^0_1$-induction.

First let me prove the principle using $\forall X\Sigma^0_1$-induction. We fix $\varepsilon>0$ and a closed set $E\subseteq [0,1]$. Let $N=\lceil\frac{2}{\varepsilon}\rceil$. Clearly it will be enough to construct the finite set $A=\{0\le i<N \mid [\frac{i}{N},\frac{i+1}{N}]\cap E\ne \emptyset\}$ and a sequence $\langle x_i\in [\frac{i}{N},\frac{i+1}{N}]\cap E \mid i\in A\rangle$. Observe that the property of a real $x$ to lie in $[\frac{i}{N},\frac{i+1}{N}]\cap E$ is $\Pi^0_1$. By a standard argument $\forall X\Sigma^0_1$-induction is pairwise equivalent to the principles of $\exists X\Pi^0_1$-induction, bounded $\forall X\Sigma^0_1$-comprehension, and bounded $\exists X\Pi^0_1$-comprehension. By bounded $\exists X\Pi^0_1$-comprehension we construct $A$. By $\exists X\Pi^0_1$-induction on $k\le N$ we show that there is a sequence $\langle x_i\in [\frac{i}{N},\frac{i+1}{N}]\cap E \mid i\in A\text{ and }i<k\rangle$, which in the case of $k=N$ gives us the desired sequence.

In the other direction assuming your principle let me prove $\forall X\Sigma^0_1$-induction. In fact I'll verify bounded $\forall X\Sigma^0_1$-comprehension. Without loss of generality we fix a natural number $N$ and $\forall X\Sigma^0_1$ predicate of the form $\forall X \exists n \varphi(x,X\upharpoonright n)$, where $\varphi$ is $\Delta^0_0$, we claim that there is the set $A=\{i<N\mid \forall X\exists n\varphi(x,X\upharpoonright n)\}$.

Let $C\subseteq [0,1]$ be the ternary Cantor's set. And for $s\in \{0,1\}^{<\omega}$ let $I(s)$ be the respective closed interval $$I(s)=[\sum\limits_{i<\mathrm{lh}(s), s(i)=1}\frac{2}{3^{i+1}},\sum\limits_{i<\mathrm{lh}(s), s(i)=1}\frac{2}{3^{i+1}}+\frac{1}{3^{\mathrm{lh}(s)}}]$$ (that is $C=\bigcup\limits_{X\in\{0,1\}^\omega}\bigcap\limits_{i<\omega}I(X\upharpoonright i)$ ). Also for $s\in \{0,1\}^{<\omega}$ let $J(s)$ be
$$J(s)=(\sum\limits_{i<\mathrm{lh}(s), s(i)=1}\frac{2}{3^{i+1}}-\frac{1}{3^{\mathrm{lh}(s)}},\sum\limits_{i<\mathrm{lh}(s), s(i)=1}\frac{2}{3^{i+1}}+\frac{2}{3^{\mathrm{lh}(s)}}).$$ Naturally if $s\subseteq q$, then $J(s)\supseteq I(q)$ and if $s\bot q$, then $J(s)\cap I(q)=\emptyset$.

Let $\varepsilon=\frac{2}{3N}$ and $$E=\bigcup\limits_{i<N}\Big(\big(C\setminus\bigcup\limits_{s\in \{0,1\}^{<\omega},\varphi(i,s)}J(s)\big)\frac{1}{3N}+\frac{i}{N}\Big)$$ Clearly, $E\setminus\bigcup\limits_{i<N} [\frac{i}{N},\frac{i}{N}+\frac{1}{3N}]=\emptyset$ and for each $i$ we have $$E\cap [\frac{i}{N},\frac{i}{N}+\frac{1}{3N}]=\emptyset \iff \forall X \exists n \varphi(i,X\upharpoonright n).$$ We find the sequence $x_1,\ldots,x_k$ according to your principle for this $E$ and $\varepsilon$. Observe that each $x_j$ should lie on some $[\frac{i}{N},\frac{i}{N}+\frac{1}{3N}]$ and $i\in A$ iff for no $1\le j\le k$ we have $x_j\in[\frac{i}{N},\frac{i}{N}+\frac{1}{3N}]$. Thus we could construct the set $A$ by $\Delta^0_1$-comprehension.