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

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.