The Reverse Mathematics of writing a set as a union?

Question

To be more precise, a countable collection of sets $(S_n)_{n \in \mathbb{N}}$ is encoded as the row of some given set $S$, i.e. $S_n = S^{[n]}$. Futhermore, for any function from $\mathbb{N} \rightarrow 2$, let $\bigcup_f S$ denote the union of the $S_n$ where $f(n) = 1$.

The question is what is the strength of the following statement (over $\text{RCA}_0$) : For all $X$, if for all $m \in X$, there exists a $n$ such that $m \in S_n$ and $S_n \subset X$, then there exist a $f : \mathbb{N} \rightarrow 2$ such that $X = \bigcup_f S$.

Clearly $\text{ACA}_0$ can prove this. However, I can not reverse this, over $\text{RCA}_0$. If it helps, this property feels very much like a special collection principle. That is for any $\Pi_1^0$ formula $\varphi(m,n)$ in free variable $m$ and $n$ : $(\forall m)(\exists n)\varphi(m,n) \Rightarrow (\exists X)(\forall m)(\exists n)(n\in X \wedge \varphi(m,n) \wedge (\forall n)(n \in X \Rightarrow (\exists m)\varphi(m,n))$. So this asserts that the solution for every $m$ exists in $X$ and all the elements of $x$ are solutions for some $m$. With this and using the $\Pi_1^0$ formula asserts $S_n$ is a subset, I can prove the union property above. However, I am not sure if I can go the other way. I am not certain of the strength of this collection principle either.

Could someone tell me if the union property or the collection principle is equivalent to any well known systems over $\text{RCA}_0$ or how they relate to well-known systems. Thanks for any help.

Answer 1

Let $Y$ be a member of the Turing degree $[Y\hspace{.04 in}]$. $\; $ Define $canhalt : \omega \times \omega \to \{\text{false},\text{true}\}$ by

$canhalt(s,t) \iff$
there exists an $s$-state $Y$-oracle machine that runs exactly $t$ steps if started on a blank tape


Define $pair : \omega \times \omega \to \omega$ to be the Cantor pairing function. $\; \; pair$ has a graph and is a bijection.
There are only finitely many $m$-state $Y$-oracle machines, and these are easily enumerated,
so define $\langle S_0,S_1,S_2,S_3,...\rangle$ by

$((2\cdot n)\in S_{pair(s,t)}) \iff n=s$
and
$(((2\cdot n)+1)\in S_{pair(s,t)}) \iff (t\lt n$ and $canhalt(s,n))$


and note that for all $s$, $\{t : canhalt(s,t)\}$ is finite.
Define $bb_Y : \omega \to \omega$ by $bb_Y(s) = \operatorname{max}(\{t : canhalt(s,t)\})$. $\; $ ($bb_Y$ does not necessarily have a graph)
Define $E = \{n : n\, \text{ is even} \}$. $\; $ By construction, for all members $n$ of $E$, $\; n\in S_{pair(m,bb_Y(m))} \subseteq E \;$.
Assuming the Union Principle, let $I$ be a subset of $\omega$ such that $\; \; \; \displaystyle\bigcup_{i\in I} \; S_i \; \; = \; \; X \; \; \; $.

By the construction of $\langle S_0,S_1,S_2,S_3,...\rangle$ and $I$, for all $s$ there exists $t$ such that $pair(s,t)\in I$,
and for all $s$ and $t$ if $pair(s,t)\in I$ then $bb_Y(s) \leq t$.
Let $\langle mach_0,mach_1,mach_2,mach_3,...\rangle$ be a reasonable enumeration of the $Y$-oracle machines. $\; $ Define $states : \omega \to \omega$ by $\; states(m) =$ the number of states in $mach_m \;$.
Since the enumeration is reasonable, $states$ has a graph.
For all $m$ and $t$, if $pair(states(m),t)\in I$ then

$mach_m$ halts within $t$ steps if started on a blank tape
$\implies$
$mach_m$ halts if started on a blank tape
$\implies$
$mach_m$ runs exactly a member of $\{t : canhalt(states(m),t)\}$ steps if started on a blank tape
$\implies$
$mach_m$ halts within $bb_Y(states(m))$ steps if started on a blank tape
$\implies$
$mach_m$ halts within $t$ steps if started on a blank tape


Now, since the enumeration is reasonable, define $H = \{m : mach_m\; \text{halts within}\; t\; \text{steps when started on a blank tape, where}\; pair(states(m),t)\in I \}$. By the above, $[Y\hspace{.04 in}]' = [Y\hspace{.02 in}'] = [H\hspace{.02 in}]$ exists. $\; $ This works for all Turing degrees, so (RCA0 + Union Principle) proves all of ACA0. $\; $ Clearly ACA0 proves the Union principle, and ACA0 is stronger than RCA0.



Therefore the Union Principle is equivalent to ACA0 over RCA0.

Answer 2

Due to my own confusion, I had a hard time reading Ricky Demer's proof, but I think it is correct. I couldn't fit this remark in a comment so this is a community wiki post where I will try to rephrase the proof in a way that I can grasp more quickly. Maybe it will help others as well.

We work in $RCA_0$. To establish $ACA_0$ it is sufficient to prove that the range of each injective function exists. Let $f\colon \mathbb{N} \to \mathbb{N}$ be injective.

For each $i$ define $$ S_{(i,j)} = \{2i\} \cup \{ 2k+1 : j < k \land f(k) < i\} $$ The sequence $\{ S_{(i,j)} : i,j \in \mathbb{N}\}$ is uniformly definable with a bounded-quantifier formula relative to $f$ so it can be formed in $RCA_0$.

Because $f$ is injective, for each $i$ the set $\{ k : f(k) < i\}$ is bounded, and so for each $i$ there is a $j$ such that $S_{(i,j)} = \{2i\}$. To prove that the set is bounded seems to require an argument using bounded $\Sigma^0_1$ comprehension to form the set of elements less than $i$ in the range, then using quantifier-free bounding to show the range of this is bounded. (Is there an easier way?) In general, the "bounding principle" for a class of formulas $\Gamma$ says that the image of a bounded set of numbers under a $\Gamma$-definable function is bounded.

Let $E$ be the set of even numbers. By the Union Principle, there is a set $I$ such that $E = \bigcup_{(i,j) \in I} S_{(i,j)}$. Note that if $(i,j) \in I$ then $S_{(i,j)} = \{2i\}$. Also note that for every $i$ there is at least one $j$ such that $(i,j) \in I$. Given $i$, let $h(i)$ be the first $j$ such that $(i,j) \in I$. Since $$(\exists k)(f(k) = \ell) \iff (\exists k < h(\ell+1))(f(k) = \ell)$$ we can define the range of $f$ using only bounded quantifiers. Thus we can form the range of $f$ in $RCA_0$.

Answer 3

I only have a partial answer so far...

The Union Principle implies $\Sigma^0_1$-Separation (which is equivalent to the Weak König Lemma).

Let $h_0, h_1:\mathbb{N}\to\mathbb{N}$ be two functions with disjoint ranges. Define $$S_{2n+i} = \{ m : m = n \lor (\exists k \leq m)(h_i(k) = n)\}.$$ Note that either $S_{2n} = \{n\}$ or $S_{2n+1} = \{n\}$ (possibly both) so every set $X$ satisfies the precondition for the Union Principle.

Let $f_0,f_1:\mathbb{N}\to2$ be such that $\bigcup_{f_0} S_n$ is the set of even numbers and $\bigcup_{f_1} S_n$ is the set of odd numbers.

Note that if $f_0(4n) = 1$ then $2n$ is not in the range of $h_0$ and if $f_0(4n+1) = 1$ then $2n$ is not in the range of $h_1$. Since we must have either $f_0(4n) = 1$ or $f_0(4n+1) = 1$, the set $$X_0 = \{2n : f_0(4n) = 1\}$$ is such that all the even values of $h_1$ are in $X_0$ and none of the even values of $h_0$ are in $X_0$.

Similarly, if $f_1(4n+2) = 1$ then $2n+1$ is not in the range of $h_0$ and if $f_1(4n+3) = 1$ then $2n+1$ is not in the range of $h_1$. Since we must have either $f_1(4n+2) = 1$ or $f_1(4n+3) = 1$, the set $$X_1 = \{2n+1 : f_1(4n+2) = 1\}$$ is such that all the odd values of $h_1$ are in $X_1$ and none of the odd values of $h_0$ are in $X_1$.

It follows that $X_0 \cup X_1$ separates the ranges of $h_0$ and $h_1$.