The Reverse Mathematics of writing a set as a union? 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. 
 A: 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.
A: 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$. 
A: 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$.
