Why is this new result such a big deal?

Question

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.

Answer 1

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!

Answer 2

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