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. 



The Reverse Mathematics of writing a set as a union?
Let $Y$ be a member of the [Turing degree](http://en.wikipedia.org/wiki/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](http://en.wikipedia.org/wiki/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](http://en.wikipedia.org/wiki/Pairing_function). $\; \; pair$ has a graph and is a bijection.
  

There are only finitely many $m$-state $Y$-[oracle machines](http://en.wikipedia.org/wiki/Oracle_machine), 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](http://en.wikipedia.org/wiki/Oracle_machine). $\; $ 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](http://en.wikipedia.org/wiki/Turing_degree), 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.


