4

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.

David Roberts
  • 33,851
William
  • 155
  • 5

3 Answers3

8

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.

  • 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 do not need to 'form' the function $bb_Y$ in RCA0, I just need to define it. I do not need a sequence of canonical indices for the sequence $\langle B_0,B_1,B_2,B_3,...\rangle$ to define it, as can be seen from the fact that I did define it without such a sequence. –  Jul 27 '11 at 21:14
  • Why does if $pair(s,t) \in I$ imply $bb_Y(s) \leq t$? All I see is that if $pair(s,t) \in I$, then $canhalt(s,t)$ must be false. – François G. Dorais Jul 27 '11 at 21:31
  • I just fixed the typo in the second part of the definition of $\langle S_0,S_1,S_2,S_3,...\rangle$. –  Jul 27 '11 at 21:47
  • 1
    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
  • 1
    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
  • The first step of the sequence of implications is to show the equivalence (and thus independence) for suitable $t$, which is what I need. No, it's defined by a $\Delta_1^0$-formula, since I proved that a suitable $t$ exists. I edited to say that $bb_Y$ does not necessarily have a graph. –  Jul 28 '11 at 00:47
  • 2
    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 01:40
  • 1
    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 02:12
7

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

Carl Mummert
  • 9,593
  • @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 01: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 01:50
  • @Francois: thanks for rewording the last paragraph. – Carl Mummert Jul 28 '11 at 01:52
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$.

François G. Dorais
  • 43,723