{
  "id": "2005.06854",
  "version": "v1",
  "published": "2020-05-14T10:15:13.000Z",
  "updated": "2020-05-14T10:15:13.000Z",
  "title": "Ramsey's theorem for pairs, collection, and proof size",
  "authors": [
    "Leszek Aleksander Kołodziejczyk",
    "Tin Lok Wong",
    "Keita Yokoyama"
  ],
  "comment": "32 pages",
  "categories": [
    "math.LO"
  ],
  "abstract": "We prove that any proof of a $\\forall \\Sigma^0_2$ sentence in the theory $\\mathrm{WKL}_0 + \\mathrm{RT}^2_2$ can be translated into a proof in $\\mathrm{RCA}_0$ at the cost of a polynomial increase in size. In fact, the proof in $\\mathrm{RCA}_0$ can be found by a polynomial-time algorithm. On the other hand, $\\mathrm{RT}^2_2$ has non-elementary speedup over the weaker base theory $\\mathrm{RCA}^*_0$ for proofs of $\\Sigma_1$ sentences. We also show that for $n \\ge 0$, proofs of $\\Pi_{n+2}$ sentences in $\\mathrm{B}\\Sigma_{n+1}+\\exp$ can be translated into proofs in $\\mathrm{I}\\Sigma_{n} + \\exp$ at polynomial cost. Moreover, the $\\Pi_{n+2}$-conservativity of $\\mathrm{B}\\Sigma_{n+1} + \\exp$ over $\\mathrm{I}\\Sigma_{n} + \\exp$ can be proved in $\\mathrm{PV}$, a fragment of bounded arithmetic corresponding to polynomial-time computation. For $n \\ge 1$, this answers a question of Clote, H\\'ajek, and Paris.",
  "revisions": [
    {
      "version": "v1",
      "updated": "2020-05-14T10:15:13.000Z"
    }
  ],
  "analyses": {
    "subjects": [
      "03B30",
      "03F35",
      "03F20",
      "03F25",
      "03F30",
      "03H15",
      "05D10"
    ],
    "keywords": [
      "ramseys theorem",
      "proof size",
      "collection",
      "weaker base theory",
      "polynomial-time computation"
    ],
    "note": {
      "typesetting": "TeX",
      "pages": 32,
      "language": "en",
      "license": "arXiv",
      "status": "editable"
    }
  }
}