We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
Ramsey's theorem for pairs, collection, and proof size.
- Authors
Kołodziejczyk, Leszek Aleksander; Wong, Tin Lok; Yokoyama, Keita
- Abstract
We prove that any proof of a ∀ Σ 2 0 sentence in the theory WKL 0 + RT 2 2 can be translated into a proof in RCA 0 at the cost of a polynomial increase in size. In fact, the proof in RCA 0 can be obtained by a polynomial-time algorithm. On the other hand, RT 2 2 has nonelementary speedup over the weaker base theory RCA 0 * for proofs of Σ 1 sentences. We also show that for n ≥ 0 , proofs of Π n + 2 sentences in B Σ n + 1 + exp can be translated into proofs in I Σ n + exp at a polynomial cost in size. Moreover, the Π n + 2 -conservativity of B Σ n + 1 + exp over I Σ n + exp can be proved in PV , a fragment of bounded arithmetic corresponding to polynomial-time computation. For n ≥ 1 , this answers a question of Clote, Hájek and Paris.
- Subjects
PARIS (France); POLYNOMIAL time algorithms; BOUNDED arithmetics; RAMSEY theory; REVERSE mathematics; PROOF theory; RAMSEY numbers; COLLECTIONS
- Publication
Journal of Mathematical Logic, 2024, Vol 24, Issue 2, p1
- ISSN
0219-0613
- Publication type
Article
- DOI
10.1142/S0219061323500071