MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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.

share|cite|improve this question
up vote 8 down vote accepted

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.

share|cite|improve this answer
Apologies for deleting and undeleting, my original argument had a flaw that has now been fixed... – François G. Dorais Jun 5 '12 at 15:08

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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