English

Ramsey's theorem for pairs, collection, and proof size

Logic 2021-01-19 v2

Abstract

We prove that any proof of a Σ20\forall \Sigma^0_2 sentence in the theory WKL0+RT22\mathrm{WKL}_0 + \mathrm{RT}^2_2 can be translated into a proof in RCA0\mathrm{RCA}_0 at the cost of a polynomial increase in size. In fact, the proof in RCA0\mathrm{RCA}_0 can be found by a polynomial-time algorithm. On the other hand, RT22\mathrm{RT}^2_2 has non-elementary speedup over the weaker base theory RCA0\mathrm{RCA}^*_0 for proofs of Σ1\Sigma_1 sentences. We also show that for n0n \ge 0, proofs of Πn+2\Pi_{n+2} sentences in BΣn+1+exp\mathrm{B}\Sigma_{n+1}+\exp can be translated into proofs in IΣn+exp\mathrm{I}\Sigma_{n} + \exp at polynomial cost. Moreover, the Πn+2\Pi_{n+2}-conservativity of BΣn+1+exp\mathrm{B}\Sigma_{n+1} + \exp over IΣn+exp\mathrm{I}\Sigma_{n} + \exp can be proved in PV\mathrm{PV}, a fragment of bounded arithmetic corresponding to polynomial-time computation. For n1n \ge 1, this answers a question of Clote, H\'ajek, and Paris.

Cite

@article{arxiv.2005.06854,
  title  = {Ramsey's theorem for pairs, collection, and proof size},
  author = {Leszek Aleksander Kołodziejczyk and Tin Lok Wong and Keita Yokoyama},
  journal= {arXiv preprint arXiv:2005.06854},
  year   = {2021}
}

Comments

33 pages. Corrected definition of forcing in Section 4, with appropriate modifications to the argument. Minor editorial changes throughout the text

R2 v1 2026-06-23T15:32:31.676Z