Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Leszek Aleksander Kołodziejczyk, Mengzhou Sun

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 $Σ^0_1$-definable cuts. Consequences include non-elementary proof speedup of $\mathrm{RCA}_0^* + \mathrm{CRT}^2_2$ over $\mathrm{RCA}_0^*$ for $Π_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 Π^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.

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

Abstract

We show that over the weak base theory , cohesive Ramsey's theorem for pairs implies exponential closure of the definable cut , which is the intersection of all -definable cuts. Consequences include non-elementary proof speedup of over for sentences and the unprovability of in . On the other hand, we show that , where is stable Ramsey's theorem for pairs, is polynomially simulated by with respect to proofs of sentences. Nevertheless, also implies a nontrivial property of , specifically closure under functions of quasipolynomial growth rate.

Paper Structure

This paper contains 11 sections, 15 theorems, 21 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. The strength of Cohesive Ramsey's Theorem
  4. Stable Ramsey's Theorem: upper and lower bounds
  5. Polynomial simulation
  6. Forcing interpretations.
  7. Structure of the polynomial simulation argument.
  8. Interpreting the auxiliary theory.
  9. Interpreting $\mathrm{SRT}^2_2$.
  10. Reflection.
  11. Completing the argument.

Key Result

Theorem 3.1

The theory $\mathrm{RCA}_0^* + \mathrm{CRT}^2_2$ proves that $\mathrm{I}^0_1$ is closed under $\mathrm{exp}$. $\blacktriangleleft$$\blacktriangleleft$

Figures (2)

  • Figure 1: Proof of Lemma \ref{['lem:SRT_lb']}: construction of the colouring $f$, steps $1$ and $2$. In step $i$, we define the colouring for pairs of elements that belong to the same interval $I_\sigma$ of length $s^{t-i+1}$ but to distinct subintervals $I_{\sigma a}$, $I_{\sigma b}$ of length $s^{t-i}$.
  • Figure 2: Proof of Theorem \ref{['thm:upperbound']}: the construction of $A_\sigma$ for $|\sigma|\leq 2$. Note that in general, $A_{\sigma0}$ is not a convex subset of $A_\sigma$.

Theorems & Definitions (36)

  • Theorem 3.1
  • proof
  • Corollary 3.2
  • proof
  • Corollary 3.3
  • proof
  • Corollary 3.4
  • proof
  • Definition 4.1
  • Lemma 4.2
  • ...and 26 more