Timeline for Why is this new result such a big deal?
Current License: CC BY-SA 3.0
16 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 7, 2016 at 3:18 | comment | added | Eric Astor | @AndreasBlass To clarify: that's exactly the situation here. Since $\mathsf{RT}^2_2$ does not imply $\mathsf{WKL}_0$ over $\mathsf{RCA}_0$, showing $\mathsf{RT}^2_2$ to be $\Pi^0_3$-conservative over $\mathsf{WKL}_0$, which is already known to be $\Pi^1_1$-conservative over $\mathsf{RCA}_0$, is the stronger result in this instance. | |
| May 28, 2016 at 20:09 | comment | added | Andreas Blass | The only way I can see "stronger than" in such a situation is if the issue isn't really "conservative" but "extension",i.e., if $T_3$ doesn't actually include $T_2$ (but does include $T_1$). | |
| May 28, 2016 at 20:08 | comment | added | Andreas Blass | @HenryTowsner I agree with your comment in the case that you already have conservativity between the two "lower" theories, but in general, if $T_1\subseteq T_2\subseteq T_3$ and $T_3$ is $\Gamma$-conservative over the weaker $T_1$, then $T_3$ is automatically $\Gamma$-conservative over $T_2$. And even if you already have that $T_2$ is $\Gamma$-conservative over $T_1$, then saying that $T_3$ is $\Gamma$-conservative over $T_2$ is equivalent to (not stronger than) saying it's $\Gamma$-conservative over $T_1$. (continued in next comment) | |
| May 28, 2016 at 4:27 | comment | added | Henry Towsner | @AndreasBlass In general being conservative over a stronger theory is unrelated to being conservative over a weaker one (the strong theory might be able to absorb more consequences, but the strong theory together with the extension might combine to give new consequences that neither alone had). But since WKL0 is already conservative over RCA0, conservation over WKL0 is stronger: assume conservation over WKL0; if RCA0+RT22 proves a Pi03 sentence A then a fortiori so does WKL0+RT22, so by assumption WKL0 proves A, so by conservation RCA0 proves A. | |
| May 27, 2016 at 18:33 | comment | added | Andreas Blass | @ThomasKlimpel What I didn't understand in your earlier comment was the claim that being conservative over $WKL_0$ is "stronger and more useful then merely being conservative over $RCA_0$." Being conservative over a stronger theory (like $WKL_0$) is a weaker property, not a stronger one. | |
| May 27, 2016 at 17:22 | comment | added | Thomas Klimpel | @AndreasBlass Yes, $WKL_0$ is stronger than $RCA_0$, but it is $\Pi_1^1$ conservative over $RCA_0$ nevertheless. The paper shows that $RT_2^2$ is $\tilde{\Pi}_3^0$ conservative over $WKL_0$, and being $\Pi_3^0$ conservative over $RCA_0$ follow as a corollary. But I don't want to claim that I read or even understood that paper. The question whether $RT_2^2$ is also conservative over $WKL_0$ immediately poped up in my mind, and it was the reason why I checked what was actually proved in the paper. | |
| May 27, 2016 at 15:46 | comment | added | Andreas Blass | @ThomasKlimpel I don't understand your comment, since $WKL_0$ is a stronger system than $RCA_0$. | |
| May 27, 2016 at 9:30 | comment | added | Thomas Klimpel | They even show that $RT_2^2$ is $\Pi_3^0$ conservative over $WKL_0$. This is stronger and more useful than merely being conservative over $RCA_0$, because it essentially establishes $WKL_0$+$RT_2^2$ as another base theory among the big five, which now takes the 3rd lowest place in the linear order of those base systems. | |
| May 27, 2016 at 5:01 | comment | added | Bjørn Kjos-Hanssen | @none yes, it does mean that. We can probably think of a theorem that is not $\Pi^0_3$ but maybe that's another MO Question? | |
| May 27, 2016 at 4:34 | comment | added | none | One further question: Does RT$_2^2$ being $\Pi^0_3$-conservative over RCA$_0$ mean that there might be, say, a $\Pi^0_5$ sentence that RCA$_0$+RT$_2^2$ can prove but RCA$_0$ by itself can't? I tried to count the quantifiers in the Hilbert-Waring theorem and I think it's $\Pi^0_3$ but maybe there's something else like that which goes higher. | |
| May 27, 2016 at 2:47 | comment | added | none | Unfortunately I don't seem to be able to mark an answer as "accepted" without signing up for an account here, which I'd rather not do. But Bjørn and François' answers and Henry Towsner's comment are all very clarifying and I think I understand the matter now. Overall I think the Quanta article didn't convey the point very well, but MO came through. Thanks again everyone! | |
| May 27, 2016 at 2:22 | comment | added | Henry Towsner | @none: Yes, such conservation results are fairly uncommon, especially for principles that are well-studied and useful (indeed, this is one of the most significant, because, as François points out, RT$^2_2$ is actually used to prove termination statements where the conservation is useful). I think the only other known examples at all are WKL, COH (cohesive sets), BCT (a version of the Baire category theorem), and a weird family of artificial examples which shows that it isn't possible to determine exactly what the list of conservative principles is. | |
| May 27, 2016 at 1:31 | comment | added | Bjørn Kjos-Hanssen | Well, nothing compares to Gödel's incompleteness theorem... | |
| May 27, 2016 at 1:05 | comment | added | none | Thanks! I understand why it's an interesting and impressive result (and your explanation helped fill in the picture), but it still seems purely technical, as opposed to something like the incompleteness theorem that made people re-examine the concept of truth. The Quanta article made it sound like this RT$_2^2$ result told us something new about potential vs completed infinity, and old philosophical conundrum. So I'm wondering what that something (if any) is. And is there really such a scarcity of these conservativity results? | |
| May 27, 2016 at 0:34 | history | edited | Bjørn Kjos-Hanssen | CC BY-SA 3.0 |
deleted 46 characters in body
|
| May 27, 2016 at 0:04 | history | answered | Bjørn Kjos-Hanssen | CC BY-SA 3.0 |