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

2020/05/14 by Kołodziejczyk, Leszek Aleksander, Wong, Tin Lok, Yokoyama, Keita · 2 citations
#03B30 #03F20 (Primary) #03F25 #03F30 #03F35 #03H15 #05D10 (Secondary) #FOS: Mathematics #Logic (math.LO)

paper · doi:10.48550/arxiv.2005.06854

Abstract

We prove that any proof of a ∀ Σ⁰₂ sentence in the theory WKL₀ + RT²₂ can be translated into a proof in RCA₀ at the cost of a polynomial increase in size. In fact, the proof in RCA₀ can be found by a polynomial-time algorithm. On the other hand, RT²₂ has non-elementary speedup over the weaker base theory RCA^*₀ for proofs of Σ₁ 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 polynomial cost. 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.

Cited by

• A non-speedup result for the chain-antichain principle over a weak base theory
• Π⁰₄ conservation of a Carlson-Simpson lemma for 1-variable words

Related

• The strength of Ramsey's theorem for pairs and arbitrarily many colors
• How strong is Ramsey's theorem if infinity can be weak?
• Strong reductions and combinatorial principles
• Π⁰₄ conservation of Ramsey's theorem for pairs
• Conservation of Ramsey's theorem for pairs and well-foundedness