5 clarifications

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$) \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$formulas.\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$ such that 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. 4 another correction 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$) 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. 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$formulas. 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(0),\dots,e(2s)\rbrace} \lbrace{e(2s),e(1),e(3),\dots,e(2s-1)\rbrace} \subseteq \operatorname{dom}(\sigma)$,$\sigma(e(2s)) = 1$and$\sigma(e(t)) \equiv t \bmod{2}$\sigma(e(2t+1)) = 1$ for all $t \lt 2s$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$such that$\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.

Post Undeleted by François G. Dorais
3 corrected version
Post Deleted by François G. Dorais
Post Undeleted by François G. Dorais
2 corrected version
Post Deleted by François G. Dorais
1