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

DOI Web Site
  • 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

抄録

<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>

収録刊行物

関連プロジェクト

もっと見る

キーワード

詳細情報 詳細情報について

問題の指摘

ページトップへ