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

arXiv comment23 pages; remark and question added at the end of Section 3, references updated, typos and other minor issues corrected throughout