The cohesive and stable Ramsey theorems and proof size over a weak base theory

TL;DR

This paper explores the logical strength and proof size implications of cohesive and stable Ramsey theorems over a weak base theory, revealing their impact on definable cuts and proof complexity.

Contribution

It establishes new connections between Ramsey theorems and proof-theoretic properties in weak arithmetic systems, including unprovability and proof speedup results.

Findings

CRT^2_2 implies exponential closure of I^0_1 in RCA_0^*

SRT^2_2 is polynomially simulated by RCA_0^* for Pi_3 sentences

CRT^2_2 is unprovable in RCA_0^* + CAC

Abstract

We show that over the weak base theory $\mathrm{RCA}_0^*$, cohesive Ramsey's theorem for pairs $\mathrm{CRT}^2_2$ implies exponential closure of the definable cut $\mathrm{I}^0_1$, which is the intersection of all $\Sigma^0_1$-definable cuts. Consequences include non-elementary proof speedup of $\mathrm{RCA}_0^* + \mathrm{CRT}^2_2$ over $\mathrm{RCA}_0^*$ for $\Pi_1$ sentences and the unprovability of $\mathrm{CRT}^2_2$ in $\mathrm{RCA}_0^* + \mathrm{CAC}$. On the other hand, we show that $\mathrm{RCA}_0^* + \mathrm{SRT}^2_2$, where $\mathrm{SRT}^2_2$ is stable Ramsey's theorem for pairs, is polynomially simulated by $\mathrm{RCA}_0^*$ with respect to proofs of $\forall \Pi^0_3$ sentences. Nevertheless, $\mathrm{SRT}^2_2$ also implies a nontrivial property of $\mathrm{I}^0_1$, specifically closure under functions of quasipolynomial growth rate.