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.



Strength of $\Delta_1^0$ subset of $2^\mathbb{N}$ as finite union of specific basic open sets.
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.


