We investigate the complexity of various combinatorial theorems about linear and partial orders, from the points of view of computability theory and reverse mathematics. We focus in particular on the principles ADS (Ascending or Descending Sequence), which states that every infinite linear order has either an infinite descending sequence or an infinite ascending sequence, and CAC (Chain-AntiChain), which states that every infinite partial order has either an infinite chain or an infinite antichain. It is well-known that Ramsey's Theorem for pairs (...) (RT₂²) splits into a stable version (SRT₂²) and a cohesive principle (COH). We show that the same is true of ADS and CAC, and that in their cases the stable versions are strictly weaker than the full ones (which is not known to be the case for RT₂² and SRT₂²). We also analyze the relationships between these principles and other systems and principles previously studied by reverse mathematics, such as WKL₀, DNR, and BΣ₂. We show, for instance, that WKL₀ is incomparable with all of the systems we study. We also prove computability-theoretic and conservation results for them. Among these results are a strengthening of the fact, proved by Cholak, Jockusch, and Slaman, that COH is Π₁¹-conservative over the base system RCA₀. We also prove that CAC does not imply DNR which, combined with a recent result of Hirschfeldt, Jockusch, Kjos-Hanssen, Lempp, and Slaman, shows that CAC does not imply SRT₂² (and so does not imply RT₂²). This answers a question of Cholak, Jockusch, and Slaman. Our proofs suggest that the essential distinction between ADS and CAC on the one hand and RT₂² on the other is that the colorings needed for our analysis are in some way transitive. We formalize this intuition as the notions of transitive and semitransitive colorings and show that the existence of homogeneous sets for such colorings is equivalent to ADS and CAC, respectively. We finish with several open questions. (shrink)

We study the proof-theoretic strength and effective content of the infinite form of Ramsey's theorem for pairs. Let RT n k denote Ramsey's theorem for k-colorings of n-element sets, and let RT $^n_{ denote (∀ k)RT n k . 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 low 2 ) to models of arithmetic enables us to show that RCA 0 + IΣ 2 + RT 2 2 is conservative over RCA 0 + IΣ 2 for Π 1 1 statements and that $RCA_0 + I\Sigma_3 + RT^2_{ , is Π 1 1 -conservative over RCA 0 + IΣ 3 . It follows that RCA 0 + RT 2 2 does not imply BΣ 3 . In contrast, J. Hirst showed that $RCA_0 + 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 RT 2 2 over RCA 0. (shrink)

We study the proof–theoretic strength and effective content of the infinite form of Ramsey's theorem for pairs. Let RTkndenote Ramsey's theorem fork–colorings ofn–element sets, and let RT<∞ndenote (∀k)RTkn. Our main result on computability is: For anyn≥ 2 and any computable (recursive)k–coloring of then–element sets of natural numbers, there is an infinite homogeneous setXwithX″ ≤T0(n). LetIΣnandBΣndenote the Σninduction and bounding schemes, respectively. Adapting the casen= 2 of the above result (whereXis low2) to models of arithmetic enables us to show that RCA0+IΣ2+ (...) RT22is conservative over RCA0+IΣ2for Π11statements and that RCA0+IΣ3+ RT<∞2is Π11-conservative over RCA0+IΣ3. It follows that RCA0+ RT22does not implyBΣ3. In contrast, J. Hirst showed that RCA0+ RT<∞2does implyBΣ3, and we include a proof of a slightly strengthened version of this result. It follows that RT<∞2is strictly stronger than RT22overRCA0. (shrink)

The larger project broached here is to look at the generally sentence “if X is well-ordered then f is well-ordered”, where f is a standard proof-theoretic function from ordinals to ordinals. It has turned out that a statement of this form is often equivalent to the existence of countable coded ω-models for a particular theory Tf whose consistency can be proved by means of a cut elimination theorem in infinitary logic which crucially involves the function f. To illustrate this theme, (...) we prove in this paper that the statement “if X is well-ordered then εX is well-ordered” is equivalent to . This was first proved by Marcone and Montalban [Alberto Marcone, Antonio Montalbán, The epsilon function for computability theorists, draft, 2007] using recursion-theoretic and combinatorial methods. The proof given here is principally proof-theoretic, the main techniques being Schütte’s method of proof search [Kurt Schütte, Proof Theory, Springer-Verlag, Berlin, Heidelberg, 1977] and cut elimination for a fragment of. (shrink)

This research is motivated by the program of reverse mathematics and non-standard arguments in second-order arithmetic. Within a weak subsystem of second-order arithmetic ACA0, we investigate some aspects of non-standard analysis related to sequential compactness. Then, using arguments of non-standard analysis, we show the equivalence of the Riemann mapping theorem and ACA0 over WKL0. (© 2007 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim).

We locate winning strategies for various ${\mathrm{\Sigma }}_{3}^{0}$ -games in the L-hierarchy in order to prove the following: Theorem 1. KP+Σ₂-Comprehension $\vdash \exists \alpha L_{\alpha}\ models"\Sigma _{2}-{\bf KP}+\Sigma _{3}^{0}-\text{Determinacy}."$ Alternatively: ${\mathrm{\Pi }}_{3}^{1}\text{\hspace{0.17em}}-{\mathrm{C}\mathrm{A}}_{0}\phantom{\rule{0ex}{0ex}}$ "there is a β-model of ${\mathrm{\Delta }}_{3}^{1}-{\mathrm{C}\mathrm{A}}_{0}\text{\hspace{0.17em}}\text{\hspace{0.17em}}+\text{\hspace{0.17 em}}{\mathrm{\Sigma }}_{3}^{0}$ -Determinacy." The implication is not reversible. (The antecedent here may be replaced with ${\mathrm{\Pi }}_{3}^{1}\text{\hspace{0.17em}}\text{\hspace{0.17em}}\left({\mathrm{\Pi }}_{3}^{1}\right)-{\mathrm{C}\mathrm{A}}_{0}:\text{\hspace{0.17em}}{\mathrm{\Pi }}_{3}^{1}$ instances of Comprehension with only ${\mathrm{\Pi }}_{3}^{1}$ -lightface definable parameters—or even weaker theories.) Theorem 2. KP +Δ₂-Comprehension +Σ₂-Replacement + ${\mathrm{\Sigma }}_{3}^{0}\phantom{\rule{0ex}{0ex}}$ -Determinacy. (Here AQI (...) is the assertion that every arithmetical quasi-inductive definition converges.) Alternatively: $\Delta _{3}^{1}{\rm CA}_{0}+{\rm AQI}\nvdash \Sigma _{3}^{0}$ -Determinacy. Hence the theories: ${\mathrm{\Pi }}_{3}^{1}-{\mathrm{C}\mathrm{A}}_{0},\text{\hspace{0.17em}}{\mathrm{\Delta }}_{3}^{1}-{\mathrm{C}\mathrm{A}}_{0}+\text{\hspace{0.17em}}{\mathrm{\Sigma }}_{3}^{0}-\mathrm{D}\mathrm{e}\mathrm{t}\phantom{\rule{0ex}{0ex}}$ -Det, ${\mathrm{\Delta }}_{3}^{1}-{\mathrm{C}\mathrm{A}}_{0}+\mathrm{A}\mathrm{Q}\mathrm{I}$ , and ${\mathrm{\Delta }}_{3}^{1}-{\mathrm{C}\mathrm{A}}_{0}\phantom{\rule{0ex}{0ex}}$ are in strictly descending order of strength. (shrink)

In [10], we have shown that the statement that all ∑ 1 1 partitions are Ramsey is deducible over ATR 0 from the axiom of ∑ 1 1 monotone inductive definition,but the reversal needs П 1 1 - CA 0 rather than ATR 0 . By contrast, we show in this paper that the statement that all ∑ 0 2 games are determinate is also deducible over ATR 0 from the axiom of ∑ 1 1 monotone inductive definition, but the (...) reversal is provable even in ACA 0 . These results illuminate the substantial differences among lightface theorems which can not be observed in boldface. (shrink)

Let CKDT be the assertion that for every countably infinite bipartite graph G, there exist a vertex covering C of G and a matching M in G such that C consists of exactly one vertex from each edge in M. (This is a theorem of Podewski and Steffens [12].) Let ATR0 be the subsystem of second-order arithmetic with arithmetical transfinite recursion and restricted induction. Let RCA0 be the subsystem of second-order arithmetic with recursive comprehension and restricted induction. We show that (...) CKDT is provable in ART0. Combining this with a result of Aharoni, Magidor, and Shore [2], we see that CKDT is logically equivalent to the axioms of ATR0, the equivalence being provable in RCA0. (shrink)

We show that there are Π5 formulas in the language of the Turing degrees, [Formula: see text], with ≤, ∨ and ∧, that define the relations x″ ≤ y″, x″ = y″ and so {x ∈ L2 = x ≥ y|x″ = y″} in any jump ideal containing 0. There are also Σ6&Π6 and Π8 formulas that define the relations w = x″ and w = x', respectively, in any such ideal [Formula: see text]. In the language with just ≤ (...) the quantifier complexity of each of these definitions increases by one. For a lower bound on definability, we show that no Π2 or Σ2 formula in the language with just ≤ defines L2 or L2. Our arguments and constructions are purely degree theoretic without any appeals to absoluteness considerations, set theoretic methods or coding of models of arithmetic. As a corollary, we see that every automorphism of [Formula: see text] is fixed on every degree above 0″ and every relation on [Formula: see text] which is invariant under the double jump or under join with 0″ is definable over [Formula: see text] if and only if it is definable in second order arithmetic with set quantification ranging over sets whose degrees are in [Formula: see text]. (shrink)

In this paper we study the determinacy strength of infinite games in the Cantor space and compare them with their counterparts in the Baire space. We show the following theorems:1. RCA0 ⊢ equation image-Det* ↔ equation image-Det* ↔ WKL0.2. RCA0 ⊢ 2-Det* ↔ ACA0.3. RCA0 ⊢ equation image-Det* ↔ equation image-Det* ↔ equation image-Det ↔ equation image-Det ↔ ATR0.4. For 1 < k < ω, RCA0 ⊢ k-Det* ↔ k –1-Det.5. RCA0 ⊢ equation image-Det* ↔ equation image-Det.Here, Det* stands for (...) the determinacy of infinite games in the Cantor space, and k is the collection of formulas built from equation image formulas by applying the difference operator k – 1 times. (shrink)

Jullien's indecomposability theorem (INDEC) states that if a scattered countable linear order is indecomposable, then it is either indecomposable to the left, or indecomposable to the right. The theorem was shown by Montalbán to be a theorem of hyperarithmetic analysis, and then, in the base system RCA₀ plus ${\mathrm{\Sigma }}_{1}^{1}\text{\hspace{0.17em}}$ induction, it was shown by Neeman to have strength strictly between weak ${\mathrm{\Sigma }}_{1}^{1}$ choice and ${\mathrm{\Delta }}_{1}^{1}$ comprehension. We prove in this paper that ${\mathrm{\Sigma }}_{1}^{1}$ induction is needed for (...) the reversal of INDEC, that is for the proof that INDEC implies weak ${\mathrm{\Sigma }}_{1}^{1}$ choice. This is in contrast with the typical situation in reverse mathematics, where reversals can usually be refined to use only ${\mathrm{\Sigma }}_{1}^{0}$ induction. (shrink)

We initiate the reverse mathematics of general topology. We show that a certain metrization theorem is equivalent to Π2 1 comprehension. An MF space is defined to be a topological space of the form MF(P) with the topology generated by $\lbrace N_p \mid p \in P \rbrace$ . Here P is a poset, MF(P) is the set of maximal filters on P, and $N_p = \lbrace F \in MF(P) \mid p \in F \rbrace$ . If the poset P is countable, (...) the space MF(P) is said to be countably based. The class of countably based MF spaces can be defined and discussed within the subsystem ACA0 of second order arithmetic. One can prove within ACA0 that every complete separable metric space is homeomorphic to a countably based MF space which is regular. We show that the converse statement, "every countably based MF space which is regular is homeomorphic to a complete separable metric space," is equivalent to Π2 1-CA0. The equivalence is proved in the weaker system Π1 1-CA0. This is the first example of a theorem of core mathematics which is provable in second order arithmetic and implies Π2 1 comprehension. (shrink)

We initiate the reverse mathematics of general topology. We show that a certain metrization theorem is equivalent to Π12 comprehension. An MF space is defined to be a topological space of the form MF with the topology generated by {Np ∣ p ϵ P}. Here P is a poset, MF is the set of maximal filters on P, and Np = {F ϵ MF ∣ p ϵ F }. If the poset P is countable, the space MF is said to (...) be countably based. The class of countably based MF spaces can be defined and discussed within the subsystem ACA0 of second order arithmetic. One can prove within ACA0 that every complete separable metric space is homeomorphic to a countably based MF space which is regular. We show that the converse statement, “every countably based MF space which is regular is homeomorphic to a complete separable metric space,” is equivalent to. The equivalence is proved in the weaker system. This is the first example of a theorem of core mathematics which is provable in second order arithmetic and implies Π12 comprehension. (shrink)

A statement of hyperarithmetic analysis is a sentence of second order arithmetic S such that for every Y⊆ω, the minimum ω-model containing Y of RCA0 + S is HYP, the ω-model consisting of the sets hyperarithmetic in Y. We provide an example of a mathematical theorem which is a statement of hyperarithmetic analysis. This statement, that we call INDEC, is due to Jullien [13]. To the author's knowledge, no other already published, purely mathematical statement has been found with this property (...) until now. We also prove that, over RCA0, INDEC is implied by [Formula: see text] and implies ACA0, but of course, neither ACA0, nor ACA 0+ imply it. We introduce five other statements of hyperarithmetic analysis and study the relations among them. Four of them are related to finitely-terminating games. The fifth one, related to iterations of the Turing jump, is strictly weaker than all the other statements that we study in this paper, as we prove using Steel's method of forcing with tagged trees. (shrink)

We show that each of $\Delta _{3}^{1}-{\rm CA}_{0}+\Sigma _{3}^{1}-{\rm IND}$ and $\Pi _{2}^{1}-{\rm CA}_{0}+\Pi _{3}^{1}-{\rm TI}$ proves $\Delta _{3}^{0}-{\rm Det}$ and that neither $\Sigma _{3}^{1}-{\rm IND}$ nor $\Pi _{3}^{1}-{\rm TI}$ can be dropped. We also show that neither $\Delta _{3}^{1}-{\rm CA}_{0}+\Sigma _{\infty}^{1}-{\rm IND}$ nor $\Pi _{2}^{1}-{\rm CA}_{0}+\Pi _{\infty}^{1}-{\rm TI}$ proves $\Sigma _{3}^{0}-{\rm Det}$. Moreover, we prove that none of $\Delta _{2}^{1}-{\rm CA}_{0}$, $\Sigma _{3}^{1}-{\rm IND}$ and $\Pi _{2}^{1}-{\rm TI}$ is provable in $\Delta _{1}^{1}-{\rm Det}_{0}={\rm ACA}_{0}+\Delta _{1}^{1}-{\rm Det}$.

We show that each of Δ13-CA0 + Σ13-IND and Π12-CA0 + Π13-TI proves Δ03-Det and that neither Σ31-IND nor Π13-TI can be dropped. We also show that neither Δ13-CA0 + Σ1∞-IND nor Π12-CA0 + Π1∞-TI proves Σ03-Det. Moreover, we prove that none of Δ21-CA0, Σ31-IND and Π21-TI is provable in Δ11-Det0 = ACA0 + Δ11-Det.

We study the computability-theoretic complexity and proof-theoretic strength of the following statements: (1) "If X is a well-ordering, then so is ε X ", and (2) "If X is a well-ordering, then so is φ(α, X)", where α is a fixed computable ordinal and φ represents the two-placed Veblen function. For the former statement, we show that ω iterations of the Turing jump are necessary in the proof and that the statement is equivalent to ${\mathrm{A}\mathrm{C}\mathrm{A}}_{0}^{+}$ over RCA₀. To prove the (...) latter statement we need to use ω α iterations of the Turing jump, and we show that the statement is equivalent to ${\mathrm{\Pi }}_{{\mathrm{\omega }}^{\mathrm{\alpha }}}^{0}{-\mathrm{C}\mathrm{A}}_{0}$ . Our proofs are purely computability-theoretic. We also give a new proof of a result of Friedman: the statement "if x is a well-ordering, then so is φ(x, 0)" is equivalent to ATR₀ over RCA₀. (shrink)

We prove that the maximal order type of the wqo of linear orders of finite Hausdorff rank under embeddability is φ2, the first fixed point of the ε-function. We then show that Fraïssé’s conjecture restricted to linear orders of finite Hausdorff rank is provable in +“φ2 is well-ordered” and, over , implies +“φ2 is well-ordered”.

We show that each of the five basic theories of second order arithmetic that play a central role in reverse mathematics has a natural counterpart in the language of nonstandard arithmetic. In the earlier paper [3] we introduced saturation principles in nonstandard arithmetic which are equivalent in strength to strong choice axioms in second order arithmetic. This paper studies principles which are equivalent in strength to weaker theories in second order arithmetic.

First order reasoning about hyperintegers can prove things about sets of integers. In the author’s paper Nonstandard Arithmetic and Reverse Mathematics, Bulletin of Symbolic Logic 12 100–125, it was shown that each of the “big five” theories in reverse mathematics, including the base theory, has a natural nonstandard counterpart. But the counterpart of has a defect: it does not imply the Standard Part Principle that a set exists if and only if it is coded by a hyperinteger. In this paper (...) we find another nonstandard counterpart, *RCA0′, that does imply the Standard Part Principle. (shrink)

Jullien's indecomposability theorem states that if a scattered countable linear order is indecomposable, then it is either indecomposable to the left, or indecomposable to the right. The theorem was shown by Montalbán to be a theorem of hyperarithmetic analysis. We identify the strength of the theorem relative to standard reverse mathematics markers. We show that it lies strictly between weak [Formula: see text] choice and [Formula: see text] comprehension.

We study the effective and proof-theoretic content of the polarized Ramsey’s theorem, a variant of Ramsey’s theorem obtained by relaxing the definition of homogeneous set. Our investigation yields a new characterization of Ramsey’s theorem in all exponents, and produces several combinatorial principles which, modulo bounding for ${\Sigma^0_2}$ formulas, lie (possibly not strictly) between Ramsey’s theorem for pairs and the stable Ramsey’s theorem for pairs.

We construct the set of the title, answering a question of Cholak, Jockusch, and Slaman [1], and discuss its connections with the study of the proof-theoretic strength and effective content of versions of Ramsey's Theorem. In particular, our result implies that every ω-model of RCA 0 + SRT 2 2 must contain a nonlow set.

We construct the set of the title, answering a question of Cholak, Jockusch, and Slaman [1], and discuss its connections with the study of the proof-theoretic strength and effective content of versions of Ramsey's Theorem. In particular, our result implies that every $\omega$-model of RCA$_0$+ SRT$^2_2$ must contain a nonlow set.