38
$\begingroup$

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.

$\endgroup$
1
  • 2
    $\begingroup$ 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. $\endgroup$ May 29, 2016 at 23:15

2 Answers 2

37
$\begingroup$

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!

$\endgroup$
5
  • 1
    $\begingroup$ 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. $\endgroup$
    – none
    May 27, 2016 at 2:44
  • $\begingroup$ 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. $\endgroup$
    – none
    May 27, 2016 at 2:51
  • 6
    $\begingroup$ No, what I wrote is correct. PRA does not prove that the Ackermann function is total. $\endgroup$ May 27, 2016 at 8:51
  • $\begingroup$ PRA is quantifier free, right? How can it prove Pi_2 statements? $\endgroup$ Jun 9, 2021 at 15:28
  • $\begingroup$ @pyrulez using standard rules of inference. For example, PRA proves $\forall x \exists y (y = x^2)$ because squaring is primitive recursive. $\endgroup$ Jun 9, 2021 at 16:52
17
$\begingroup$

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

$\endgroup$
14
  • 4
    $\begingroup$ Well, nothing compares to Gödel's incompleteness theorem... $\endgroup$ May 27, 2016 at 1:31
  • 2
    $\begingroup$ @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. $\endgroup$ May 27, 2016 at 2:22
  • 3
    $\begingroup$ @ThomasKlimpel I don't understand your comment, since $WKL_0$ is a stronger system than $RCA_0$. $\endgroup$ May 27, 2016 at 15:46
  • 1
    $\begingroup$ @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. $\endgroup$ May 27, 2016 at 18:33
  • 3
    $\begingroup$ @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. $\endgroup$ May 28, 2016 at 4:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.