Strength of $\Delta_1^0$ subset of $2^\mathbb{N}$ as finite union of specific basic open sets.

Question

This question is to find the Reverse Mathematical strength of writing $\Delta_1^0$ (clopen) subset of $2^\mathbb{N}$ as a finite union $\bigcup_{\sigma \in F} [|\sigma|]$ where $F \subset 2^{<\mathbb{N}}$ is finite and $[|\sigma|] = \{f \in 2^{\mathbb{N}} : \sigma \prec f\}$.

More formally, if $\varphi(f)$ is a $\Delta_1^0$ formula in second order arithmetic, does there exists a finite set $F \subset 2^{<\mathbb{N}}$ such that for any $f \in 2^\mathbb{N}$, $\varphi(f)$ holds if and only if there exists a $\sigma \in F$ such that $\sigma \prec f$.

I am quite sure that $WKL_0$ can prove this by formalizing the usual compactness argument in Cantor space. Is this property equivalent to $WKL_0$ over $RCA_0$? Can anyone see a proof of this result from weaker systems like $WWKL_0$, $RCA_0$?

Thanks for any help you can provide. I have proved something using the clopen principle above and an idea of the strength of this result would help me pinpoint the proof theoretic strength of what I am really interested in. Thanks very much.

Answer 1

This is equivalent to $\mathsf{WKL}_0$, with little a caveat... Note that there is no such thing as a "$\Delta^0_1$ formula." Below, I will use the most permissive meaning for $\Delta^0_1$, which is the usual one in this context. If one uses a more restrictive meaning (e.g. bounded formula, provably $\Delta^0_1$ formula) then we can possibly prove the existence of such a finite set $F$ in plain $\mathsf{RCA}_0$.

I will show that the statement implies $\Sigma^0_1$-separation, which is a well known equivalent of the Weak König Lemma. (The reverse implication is a standard compactness argument as you described.) Suppose, for the sake of contradiction, that $e:\mathbb{N}\to\mathbb{N}$ is an injection such that $\lbrace e(2s) : s \in \mathbb{N}\rbrace$ and $\lbrace e(2s+1) : s \in \mathbb{N}\rbrace$ form an inseparable pair: there is no $f:\mathbb{N}\to2$ such that $f(e(s)) \equiv s \bmod{2}$ for all $s$.

Now consider the statements $$\phi_0(f) \equiv (\exists s)(f(e(2s))=1 \land (\forall t \lt 2s)(f(e(t)) \equiv t \bmod{2}))$$ and $$\phi_1(f) \equiv (\exists s)(f(e(2s+1)) = 0 \land (\forall t \lt 2s+1)(f(e(t)) \equiv t \bmod{2})).$$ These are both $\Sigma^0_1$-formulas. Clearly, these represent disjoint subsets of $2^{\mathbb{N}}$. In fact, by our inseparability assumption, these represent complementary subsets of $2^{\mathbb{N}}$. Therefore, $\phi_0(f)$ and $\phi_1(f)$ are $\Delta^0_1$.

Now suppose $F_0$ and $F_1$ are finite sets of binary sequences such that $$\phi_0(f) \leftrightarrow f \in \bigcup_{\sigma \in F_0} [\sigma], \quad \phi_1(f) \leftrightarrow f \in \bigcup_{\sigma \in F_1} [\sigma].$$ Note that by definition of $\phi_0(f)$, every $\sigma \in F_0$ must be such that for some $s$, we have $\lbrace{e(2s),e(1),e(3),\dots,e(2s-1)\rbrace} \subseteq \operatorname{dom}(\sigma)$, $\sigma(e(2s)) = 1$ and $\sigma(e(2t+1)) = 1$ for all $t \lt s$. Similarly for $F_1$. Let $m$ be the maximum length of a sequence in $F_0 \cup F_1$ and let $n$ be such that $e(t) \geq m$ for all $t \geq n$ (such an $n$ must exist since $e$ is injective). It must then be the case that for every $f:\mathbb{N}\to2$, whether $\phi_0(f)$ or $\phi_1(f)$ is already determined by looking at the restriction $f{\upharpoonright}\lbrace0,\dots,m-1\rbrace$. But this is impossible since the characteristic function of the finite set $\lbrace e(2s+1) : s \lt n\rbrace$ does not have this property, for example.