The strength of Ramsey Theorem for coloring relatively large sets

TL;DR

This paper characterizes the computational and proof-theoretic strength of a Ramsey-type theorem for exactly large sets, showing its equivalence to arithmetical truth and extending understanding of Ramsey theorem complexities.

Contribution

It provides a complete characterization of the theorem's strength in computability and proof theory, linking it to the ω Turing jump and truth predicates.

Findings

The theorem is equivalent to closure under the ω Turing jump.

Analogous results hold for a related Regressive Ramsey principle.

The characterization extends to a proof-theoretic understanding involving truth predicates.

Abstract

We characterize the computational content and the proof-theoretic strength of a Ramsey-type theorem for bi-colorings of so-called {\em exactly large} sets. An {\it exactly large} set is a set $X\subset\Nat$ such that $\card(X)=\min(X)+1$. The theorem we analyze is as follows. For every infinite subset $M$ of $\Nat$, for every coloring $C$ of the exactly large subsets of $M$ in two colors, there exists and infinite subset $L$ of $M$ such that $C$ is constant on all exactly large subsets of $L$. This theorem is essentially due to Pudl\`ak and R\"odl and independently to Farmaki. We prove that --- over Computable Mathematics --- this theorem is equivalent to closure under the $\omega$ Turing jump (i.e., under arithmetical truth). Natural combinatorial theorems at this level of complexity are rare. Our results give a complete characterization of the theorem from the point of view of Computable Mathematics and of the Proof Theory of Arithmetic. This nicely extends the current knowledge about the strength of Ramsey Theorem. We also show that analogous results hold for a related principle based on the Regressive Ramsey Theorem. In addition we give a further characterization in terms of truth predicates over Peano Arithmetic. We conjecture that analogous results hold for larger ordinals.