Ramsey's theorem and lengths of proofs

Keita Yokoyama, Japan Advanced Institute of Science and Technology. Part of the Logic Seminar series.

In the recent study of reverse mathematics, it is known that Ramsey's theorem for pairs and two colors (RT^2_2) is Pi^0_3-conservative over both of RCA_0 and RCA_0*.  In this talk, we will refine these conservation results from the view point of lengths of proofs.  We will reformulate the conservation proofs with forcing indicators and show that RT^2_2 gives no speed-up for Pi^0_3-consequences over RCA_0, but it gives super-exponential speed-up over RCA_0*.