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.


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

  • $\begingroup$ Apologies for deleting and undeleting, my original argument had a flaw that has now been fixed... $\endgroup$ Jun 5, 2012 at 15:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.