Timeline for The Reverse Mathematics of writing a set as a union?
Current License: CC BY-SA 3.0
14 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 28, 2011 at 2:12 | comment | added | Carl Mummert |
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.
|
|
| Jul 28, 2011 at 1:59 | vote | accept | William | ||
| Jul 28, 2011 at 1:40 | comment | added | François G. Dorais | 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. | |
| Jul 28, 2011 at 0:47 | comment | added | user5810 | 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, 2011 at 0:39 | history | edited | user5810 | CC BY-SA 3.0 |
made proof slightly better
|
| Jul 27, 2011 at 22:30 | comment | added | François G. Dorais | 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. | |
| Jul 27, 2011 at 22:18 | history | edited | user5810 | CC BY-SA 3.0 |
fixed another typo
|
| Jul 27, 2011 at 22:07 | comment | added | Carl Mummert | I retyped this in a different way as a community wiki post to help myself understand it. | |
| Jul 27, 2011 at 21:47 | comment | added | user5810 | 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, 2011 at 21:46 | history | edited | user5810 | CC BY-SA 3.0 |
fixed typo
|
| Jul 27, 2011 at 21:31 | comment | added | François G. Dorais | 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. | |
| Jul 27, 2011 at 21:14 | comment | added | user5810 | 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, 2011 at 20:59 | comment | added | Carl Mummert |
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$.
|
|
| Jul 27, 2011 at 20:16 | history | answered | user5810 | CC BY-SA 3.0 |