Abstract

We show that a theory of autonomous iterated Ramseyness based on second order arithmetic (SOA) is proof-theoretically equivalent to ${\Pi^1_2}$ -comprehension. The property of Ramsey is defined as follows. Let X be a set of real numbers, i.e. a set of infinite sets of natural numbers. We call a set H of natural numbers homogeneous for X if either all infinite subsets of H are in X or all infinite subsets of H are not in X. X has the property of Ramsey if there exists a set which is homogeneous for X. The property of Ramsey is considered in reverse mathematics to compare the strength of subsystems of SOA. To characterize the system of ${\Pi^1_2}$ -comprehension in terms of Ramseyness we introduce a system of autonomous iterated Ramseyness, called R-calculus. We augment the language of SOA with additional set terms (called R-terms) ${R\vec{x}X\phi(\vec{x},X)}$ for each first order formula ${\phi(\vec{x},X)}$ (where φ may contain further R-terms). The R-calculus is a system which comprises comprehension for all first order formulas (which may contain R-terms or other set parameters) and defining axioms for the R-terms which claim that for each ${\vec{x}}$ , we can remove finitely many elements from the set ${R\vec{x}X\phi(\vec{x},X)}$ such that the remaining set is homogeneous for ${\{{X}{\phi(\vec{x},X)\}}}$ . We show that the R-calculus proves the same ${\Pi^1_1}$ -sentences as the system of ${\Pi^1_2}$ -comprehension