MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).

4 made proof slightly better

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 an a reasonable enumeration of the $Y$-oracle machines such that with . $\;$ Define $states : \omega \to \omega$ defined by $\; states(m) =$ the number of states in $mach_m \;$, ;$. Since the enumeration is reasonable,$states$is computablehas 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$\impliesmach_m$halts if started on a blank tape$\impliesmach_m$runs exactly a member of $\{t : canhalt(states(m),t)\}$ steps if started on a blank tape$\impliesmach_m$halts within$bb_Y(states(m))$steps if started on a blank tape$\impliesmach_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. 3 fixed another typo 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. 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 not 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)\})$.$\; $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 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 an enumeration of the$Y$-oracle machines such that with$states : \omega \to \omega$defined by$\; states(m) =$the number of states in$mach_m \;$,$states$is computable. 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$\impliesmach_m$halts if started on a blank tape$\impliesmach_m$runs exactly a member of $\{t : canhalt(states(m),t)\}$ steps if started on a blank tape$\impliesmach_m$halts within$bb_Y(states(m))$steps if started on a blank tape$\impliesmach_m$halts within$t$steps if started on a blank tape Now, 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'] 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. 2 fixed typo Let$Y$be a member of the Turing degree$[Y]$. [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.
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,t))$ canhalt(s,n))$and not 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)\})$.$\; $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 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 an enumeration of the$Y$-oracle machines such that with$states : \omega \to \omega$defined by$\; states(m) =$the number of states in$mach_m \;$,$states$is computable. 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$\impliesmach_m$halts if started on a blank tape$\impliesmach_m$runs exactly a member of $\{t : canhalt(states(m),t)\}$ steps if started on a blank tape$\impliesmach_m$halts within$bb_Y(states(m))$steps if started on a blank tape$\impliesmach_m$halts within$t$steps if started on a blank tape Now, 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]' [Y\hspace{.04 in}]' = [Y'] = [H]$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 Union Principle is equivalent to ACA0 over RCA0.

1