Why is this new result such a big deal?

This popular article reports a recent result in reverse mathematics, showing that a certain theorem in Ramsey theory is provable from RCA$_0$, the base theory in SOSOA. Then there are a bunch of surprised remarks, since (according to the article) the theorem itself is infinitary. Does that just mean that it uses unbounded quantifiers, or maybe that it refers to infinite sets? Isn't that the whole point of second-order arithmetic? And aren't there tons of theorems of the same sort? I don't know much about the subject, but I thought one of the basic discoveries in RM was that lots of the familiar results of calculus and analysis can be reached from RCA$_0$.

I get that $RT^2_2$ has a Friedman-like flavour that sounds like it might need strong axioms to prove, and I get that proving its strength (that was lower than expected) was difficult, but I'm having trouble understanding why there is such excitement over this, or what far-reaching consequences it's supposed to have. I'd appreciate any enlightenment.

• There is a chance that the question could be misread. The combinatorial principle that the article describes, $\mathsf{RT}^2_2$, is not provable in $\mathsf{RCA}_0$; this has been known for some time. The new result is that $\mathsf{RT}^2_2$ is conservative over $\mathsf{RCA}_0$ for (more than) $\Pi^0_2$ sentences. – Carl Mummert May 29 '16 at 23:15

The statement in question, frequently denoted $\mathsf{RT}^2_2$ in the context of reverse mathematics, is the instance of the infinite Ramsey theorem for unordered pairs and two colors. Specifically, the theorem is that given any graph on the set of natural numbers contains an infinite clique or an infinite anticlique. This is an infinitary theorem since the graph is infinite and so is the clique or anticlique.

One of the reasons why this result is of deep interest is that it has many finitary consequences. For example, the finite Ramsey theorem follows from the infinite case by a compactness argument. The theorem has many other seemingly unrelated consequences, for example Ramsey's theorem is a key step in the proof of termination of some algorithms.

The recent results of Patey and Yokoyama show (among other things) that $\mathsf{RT}^2_2$ is $\Pi^0_2$ conservative over $\mathsf{PRA}$, i.e. that every $\Pi^0_2$ statement provable using the infinitary theorem $\mathsf{RT}^2_2$ is already provable using only primitive recursive arithmetic. This is surprising because primitive recursive arithmetic is a completely finitary theory: primitive recursive functions have a finite description and they always terminate in finite time. Thus $\mathsf{PRA}$ is considered among the "safest" theories of arithmetic. It is much weaker than Peano Arithmetic, in fact Peano Arithmetic is far from conservative over $\mathsf{PRA}$.

$\Pi^0_2$ statements include statements of the form "this algorithm terminates on every input" so we now know that all algorithms that have been shown to terminate assuming $\mathsf{RT}^2_2$ have an alternate proof of termination that only uses $\mathsf{PRA}$ and therefore that these algorithms are primitive recursive themselves!

• Thanks! The explanation of RT$^2_2$ being useful in termination proofs adds helpful context. But do you really mean to say that (PRA proves termination) means the algorithm itself is primitive recursive? For example I thought PRA proves that the (partial recursive) algorithm for the Ackermann function terminates. – none May 27 '16 at 2:44
• Btw, regarding above comment about primitive recursive algorithms: I'm not sure whether the question was a minor point of terminology, or whether the issue is actually significant. – none May 27 '16 at 2:51
• No, what I wrote is correct. PRA does not prove that the Ackermann function is total. – François G. Dorais May 27 '16 at 8:51

They show that $\DeclareMathOperator{\WKL}{WKL}\DeclareMathOperator{\RT}{RT}\DeclareMathOperator{\RCA}{RCA} \RT^2_2$ is $\Pi^0_3$-conservative over $\RCA_0$. Thus, there is no way that $\RT^2_2$ can be essential in a proof of simple first-order statements like for instance the twin prime conjecture, that have a $\Pi^0_3$ form: $$(\forall n)(\exists p>n)(p\text{ is prime and }p+2\text{ is prime.})$$ (This is $\Pi^0_2$ which is, in particular, $\Pi^0_3$.)

First-order means you quantify over numbers only, whereas $\RT^2_2$ itself involves quantifying over sets of numbers, making it second order.

For comparison, Leo Harrington (1978) showed that $\WKL_0$ (weak König's lemma) is $\Pi^1_1$-conservative, hence in particular also $\Pi^0_3$-conservative, over $\RCA_0$.

• Well, nothing compares to Gödel's incompleteness theorem... – Bjørn Kjos-Hanssen May 27 '16 at 1:31
• @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. – Henry Towsner May 27 '16 at 2:22
• @ThomasKlimpel I don't understand your comment, since $WKL_0$ is a stronger system than $RCA_0$. – Andreas Blass May 27 '16 at 15:46
• @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. – Andreas Blass May 27 '16 at 18:33
• @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. – Henry Towsner May 28 '16 at 4:27