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

Journal of Mathematical Logic 24 (2) (2023)
  Copy   BIBTEX


We prove that any proof of a [Formula: see text] sentence in the theory [Formula: see text] can be translated into a proof in [Formula: see text] at the cost of a polynomial increase in size. In fact, the proof in [Formula: see text] can be obtained by a polynomial-time algorithm. On the other hand, [Formula: see text] has nonelementary speedup over the weaker base theory [Formula: see text] for proofs of [Formula: see text] sentences. We also show that for [Formula: see text], proofs of [Formula: see text] sentences in [Formula: see text] can be translated into proofs in [Formula: see text] at a polynomial cost in size. Moreover, the [Formula: see text]-conservativity of [Formula: see text] over [Formula: see text] can be proved in [Formula: see text], a fragment of bounded arithmetic corresponding to polynomial-time computation. For [Formula: see text], this answers a question of Clote, Hájek and Paris.



    Upload a copy of this work     Papers currently archived: 93,031

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

The mouse set theorem just past projective.Mitch Rudominer - forthcoming - Journal of Mathematical Logic.
Specializing trees and answer to a question of Williams.Mohammad Golshani & Saharon Shelah - 2020 - Journal of Mathematical Logic 21 (1):2050023.
The equivalence of Axiom (∗)+ and Axiom (∗)++.W. Hugh Woodin - forthcoming - Journal of Mathematical Logic.


Added to PP

7 (#1,411,318)

6 months
5 (#711,375)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations