Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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.

share|improve this question
add comment

3 Answers

up vote 8 down vote accepted

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$
$(((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
$mach_m$ halts if started on a blank tape
$mach_m$ runs exactly a member of $\{t : canhalt(states(m),t)\}$ steps if started on a blank tape
$mach_m$ halts within $bb_Y(states(m))$ steps if started on a blank tape
$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.

share|improve this answer
It isn't possible to form the function $bb_Y(s)$ in $RCA_0$. When $Y = \emptyset$ this is the Busy Beaver function, which will not be in the $\omega$-model REC of $RCA_0$ because every function in that model is computable. It is true that for each $s$ the set $B_s = \{ t : canhalt(s,t)\}$ is finite, but there is no computable sequence of canonical indices for the sequence $(B_s)$, and this is what would be needed to define the bb function. By comparison, for each $s$ the set $C_s = \{ 0 : s \text{ halts}\} \cup \{ 1 : s \text{ doesn't halt}\}$ is finite, but we can't form $f(s) = \max C_s$. –  Carl Mummert Jul 27 '11 at 20:59
I retyped this in a different way as a community wiki post to help myself understand it. –  Carl Mummert Jul 27 '11 at 22:07
OK. I sorted through the confusion. Your argument is basically correct, but you need to fix a few things to make it right. - The first step of your sequence of implications should not be there. - Your $H$ at the end is defined by a $\Sigma^0_1$-formula. You need to first use $I$ to define a function $h$ such that $(s,h(s)) \in I$. Then define $H$ to be the set {$m$ : $mach_m$ halts in $h(states(m))$ steps}. - Carl's objection to 'defining' $bb_Y$ is right. Try something like "consider the (external!) function $bb_Y$" to warn the reader that you're not claiming that $bb_Y$ actually exists. –  François G. Dorais Jul 27 '11 at 22:30
You don't need to follow my advice to the word. However, I strongly recommend that you do two things: (1) always announce what you're proving, and (2) always conclude your arguments. Once you start doing that, you will find that people will find your arguments much less confusing. –  François G. Dorais Jul 28 '11 at 1:40
The other tricky thing in this proof is showing that $\{t : canhalt(s,t)\}$ is always bounded. This seems to require actually analyzing the complexity of the canhalt relation and associated functions, because just being in definable bijection with a bounded set is not good enough to ensure boundedness. The fact that not every machine will halt is another wrinkle. –  Carl Mummert Jul 28 '11 at 2:12
show 4 more comments

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$.

share|improve this answer
@William Chan: I added a brief statement of what the bounding principle says. These sorts of principles are more well known in the study of fragments of first-order arithmetic, but it shows up occasionally in the context of reverse math. –  Carl Mummert Jul 28 '11 at 1:50
Also, in my opinion this is just a rephrasing of Ricky Demer's proof, and if you would like to accept an answer I would prefer if you did not accept this one. –  Carl Mummert Jul 28 '11 at 1:50
@Francois: thanks for rewording the last paragraph. –  Carl Mummert Jul 28 '11 at 1:52
add comment

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$.

share|improve this answer
add comment

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.