Ramsey's theorem for pairs, collection, and proof size
Abstract
We prove that any proof of a sentence in the theory can be translated into a proof in at the cost of a polynomial increase in size. In fact, the proof in can be found by a polynomial-time algorithm. On the other hand, has non-elementary speedup over the weaker base theory for proofs of sentences. We also show that for , proofs of sentences in can be translated into proofs in at polynomial cost. Moreover, the -conservativity of over can be proved in , a fragment of bounded arithmetic corresponding to polynomial-time computation. For , 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