The theorem in question, frequently denoted $\mathsf{RT}^2_2$, 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!

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!

The theorem in question, frequently denoted $\mathsf{RT}^2_2$, 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}$!

The theorem in question, frequently denoted $\mathsf{RT}^2_2$, 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!