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

We prove that any proof of a ?S-2(0) sentence in the theory WKL0 +RT22 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, RT22 has nonelementary speedup over the weaker base theory RCA(0)(*) for proofs of S-1 sentences. We also show that for n > 0, proofs of ?n+2 sentences in BSn+1+exp can be translated into proofs in ISn + exp at a polynomial cost in size. Moreover, the ?(n+2)-conservativity of BSn+1 + exp over ISn + 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'ajek and Paris.