In this paper, we propose a weak regularity principle which is similar to both weak König's lemma and Ramsey's theorem. We begin by studying the computational strength of this principle in the context of reverse mathematics. We then analyze different ways of generalizing this principle.

In this paper we study with proof-theoretic methods the function(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 functional provably recursive from are primitive recursive. This also provides a uniform method to extract bounds from proofs that use these principles. As a consequence we obtain a new proof of the fact that is -conservative over PRA.

Recent work of the first author showed that 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 we obtain the upper bounded that the type 2 functional provable recursive relative to 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 . Moreover, this yields a new proof of the fact that is -conservative over .

The results are obtained in two steps: in the first step a term including Skolem functions for the above principles is extracted from a given proof. This is done using Gödel's functional interpretation. After this the term is normalized, such that only specific instances of the Skolem functions are used. In the second step this term is interpreted using -comprehension. The comprehension is then eliminated in favor of induction using either elimination of monotone Skolem functions (for COH) or Howard's ordinal analysis of bar recursion (for ).

We prove that by showing that for any set C not of PA-degree and any set A, there exists an infinite subset G of A or such that G ⊕ C is also not of PA-degree.

We study the proof–theoretic strength and effective content of the infinite form of Ramsey's theorem for pairs. Let RTkn denote Ramsey's theorem for k–colorings of n–element sets, and let RT<∞n denote (∀k)RTkn. Our main result on computability is: For any n ≥ 2 and any computable (recursive) k–coloring of the n–element sets of natural numbers, there is an infinite homogeneous set X with X″ ≤T 0(n). Let IΣn and BΣn denote the Σn induction and bounding schemes, respectively. Adapting the case n = 2 of the above result (where X is low2) to models of arithmetic enables us to show that RCA0 + IΣ2 + RT22 is conservative over RCA0 + IΣ2 for Π11 statements and that RCA0 + IΣ3 + RT<∞2 is Π11-conservative over RCA0 + IΣ3. It follows that RCA0 + RT22 does not imply BΣ3. In contrast, J. Hirst showed that RCA0 + RT<∞2 does imply BΣ3, and we include a proof of a slightly strengthened version of this result. It follows that RT<∞2 is strictly stronger than RT22 over RCA0.

Ramsey's Theorem states that if P is a partition of [ω]k into finitely many partition classes, then there exists an infinite set of natural numbers which is homogeneous for P. We consider the degrees of unsolvability and arithmetical definability properties of infinite homogeneous sets for recursive partitions. We give Jockusch's proof of Seetapun's recent theorem that for all recursive partitions of [ω]2 into finitely many pieces, there exists an infinite homogeneous set A such that ∅′ ≰TA. Two technical extensions of this result are given, establishing arithmetical bounds for such a set A. Applications to reverse mathematics and introreducible sets are discussed.

Solovay has shown that if F: [ω]ω → 2 is a clopen partition with recursive code, then there is an infinite homogeneous hyperarithmetic set for the partition (a basis result). Simpson has shown that for every 0α, where α is a recursive ordinal, there is a clopen partition F: [ω]ω → 2 such that every infinite homogeneous set is Turing above 0α (an anti-basis result). Here we refine these results, by associating the “order type” of a clopen set with the Turing complexity of the infinite homogeneous sets. We also consider the Nash-Williams barrier theorem and its relation to the clopen Ramsey theorem.