U.: Term extraction and Ramsey’s theorem for pairs

Abstract. In this paper we study with proof-theoretic methods the func-tion(al)s provably recursive relative to Ramsey’s theorem for pairs and the cohesive principle (COH). Our main result on COH is that the type 2 functionals provably recursive from RCA0 + COH + Π01-CP are primitive recursive. This also provides a uni-form method to extract bounds from proofs that use these principles. As a consequence we obtain a new proof of the fact that WKL0 + Π01-CP + COH is Π02-conservative over PRA. Recent work of the first author showed that Π01-CP + COH is equivalent to a weak variant of the Bolzano-Weierstraß principle. This makes it possible to use our results to analyze not only combinatorial but also analytical proofs. For Ramsey’s theorem for pairs and two colors (RT22) we obtain the upper bounded that the type 2 functionals provable recursive relative to RCA0 + Σ02-IA+RT 2 2 are in T1. This is the fragment of Gödel’s system T containing only type 1 recursion — roughly speaking it consists of functions of Ackermann type. With this we also obtain a uniform method for the extraction of T1-bounds from proofs that use RT22. Moreover, this yields a new proof of the fact tha