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

Abstract: We prove that any proof of a

f o r a l l S i g m a_{2}^{0}

sentence in the theory

m a t h r m {W K L}_{0} + m a t h r m {R T}_{2}^{2}

can be translated into a proof in

m a t h r m {R C A}_{0}

at the cost of a polynomial increase in size. In fact, the proof in

m a t h r m {R C A}_{0}

can be found by a polynomial-time algorithm. On the other hand,

m a t h r m {R T}_{2}^{2}

has non-elementary speedup over the weaker base theory

m a t h r m {R C A}_{0}^{*}

for proofs of

S i g m a_{1}

sentences. We also show that for

n g e 0

, proofs of

P i_{n + 2}

sentences in

m a t h r m B S i g m a_{n + 1} + e x p

can be translated into proofs in

m a t h r m I S i g m a_{n} + e x p

at polynomial cost. Moreover, the

P i_{n + 2}

-conservativity of

m a t h r m B S i g m a_{n + 1} + e x p

over

m a t h r m I S i g m a_{n} + e x p

can be proved in

m a t h r m P V

, a fragment of bounded arithmetic corresponding to polynomial-time computation. For

n g e 1

, this answers a question of Clote, H'ajek, and Paris.

This page was built for publication: Ramsey's theorem for pairs, collection, and proof size