Ramsey’s theorem for pairs, collection, and proof size
-
- Leszek Aleksander Kołodziejczyk
- Institute of Mathematics, University of Warsaw, Banacha 2, Warszawa 02-097, Poland
-
- Tin Lok Wong
- Department of Mathematics, National University of Singapore, 10 Lower Kent Ridge Road, Singapore 119076, Singapore
-
- Keita Yokoyama
- Mathematical Institute, Tohoku University, Aoba, Sendai 980-8578, Japan
Abstract
<jats:p> 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. </jats:p>
Journal
-
- Journal of Mathematical Logic
-
Journal of Mathematical Logic 24 (02), 2023-05-31
World Scientific Pub Co Pte Ltd
- Tweet
Details 詳細情報について
-
- CRID
- 1360580232387221632
-
- ISSN
- 17936691
- 02190613
-
- Data Source
-
- Crossref
- KAKEN