Reverse Mathematics: The Playground of Logic

Richard A. Shore^{∗} Department of Mathematics Cornell University Ithaca NY 14853

May 6, 2010

1 Introduction

The general enterprise of calibrating the strength of classical mathematical theorems in terms of the axioms (typically of set existence) needed to prove them was begun by Harvey Friedman in [1971] (see also [1967]). His goals were both philosophical and foundational. What existence assumptions are really needed to develop classical mathematics and what other axioms and methods suffice to carry out standard constructions and proofs? In the [1971] paper, Friedman worked primarily in the set theoretic settings of subsystems (and extensions) of ZFC. As almost all of classical mathematics can be formalized in the language of second order arithmetic and its theorems proved there, he moved [1975] to the setting of second order arithmetic and subsystems of its full theory Z_{2} (i.e. arithmetic with the full comprehension axiom as described below). Of course, restricting to second order arithmetic means restricting to essentially countable structures in mathematics. By this we mean countable algebra and combinatorics and separable (or otherwise countably representable) analysis and topology. Still, this somewhat restricted area has a strong claim to embody most of what might be called classical mathematics outside of set theory. Many researchers have since contributed to this endeavor but the major systematic developer and expositor since Friedman has been Stephen Simpson.

To be more definite about the systems studied we give some brief descriptions. Here and elsewhere full details can be found in Simpson [2009] which is the basic source for both background material and extensive results.

∗This paper is essentially the author’s Gödel Lecture at the ASL Logic Colloquium ’09 in Sofia extended and supplemented by material from some of our other papers. The work was partially supported by NSF Grants DMS-0554855, DMS-0852811 and John Templeton Foundation Grant 13408.

Our language is the (two sorted) language of second order arithmetic, that is, the usual first order language of arithmetic augmented by set variables with their quantifiers and the membership relation ∈ between numbers and sets. A structure for this language is one of the form M = ⟨M, S, +, ×, <, 0, 1, ∈⟩ where M is a set (the set of the “numbers” of M) over which the first order quantifiers and variables of our language range; S ⊆ 2^{M} is the collection of subsets of the “numbers” in M over which the second order quantifiers and variables of our language range; + and × are binary functions on M; < is a binary relation on M while 0 and 1 are members of M.

In this setting, the original endeavor of reverse mathematics has proven to be a great success in classifying the theorems of countable classical mathematics from proof theoretic and epistemological viewpoints. Five subsystems of Z_{2} of strictly increasing strength emerged as the core of the subject with the vast majority of classical mathematical theorems being provable in one of them. Indeed, relative to the weakest of them (which corresponds simply to computable mathematics) almost all the theorems studied turned out to be equivalent to one of these five systems.

Here the equivalence of a theorem T to a system S means that not only is the theorem T provable in S but that, when adjoined to a weak base theory, T proves all the axioms of S as well. Thus the system S is precisely what is needed to establish T and gives a characterization of the existence assumptions needed to prove it and so its (proof theoretic) strength. It is this approach that gives the subject the name of Reverse Mathematics. In standard mathematics one proves a theorem T from axioms S. Here one then tries to reverse the process by proving the axioms of S from T (and a weak base theory).

We describe these five basic systems and set out the framework for others. They all include the standard basic axioms for +, ·, and < which say that ℕ is an ordered semiring. In addition, we always include a weak form of induction that applies only to sets (that happen to exist):

(I_{0}) (0 ∈ X ∧ ∀n (n ∈ X → n + 1 ∈ X)) → ∀n (n ∈ X).

All the systems we consider are defined by adding various types of set existence axioms (or at times induction axioms) to these axioms. The basic five, in ascending order of proof theoretic strength are as follows:

(RCA_{0}) Recursive Comprehension: This is a system just strong enough to prove the existence of the computable sets. Its axioms include the schemes of Δ_{1}^{0} comprehension and Σ_{1}^{0} induction:

(Δ_{1}^{0}-CA_{0}) ∀n (φ(n) ↔ ψ(n)) → ∃X ∀n (n ∈ X ↔ φ(n)) for all Σ_{1}^{0} formulas φ and Π_{1}^{0} formulas ψ in which X is not free.

(IΣ_{1}^{0}) (φ(0) ∧ ∀n (φ(n) → φ(n + 1))) → ∀n φ(n) for all Σ_{1}^{0} formulas φ.

RCA_{0} is the standard weak base theory for reverse mathematics and is included in all the systems we consider.

(WKL_{0}) Weak König’s Lemma: Every infinite subtree of 2^{<ω} has an infinite path.

(ACA_{0}) Arithmetic Comprehension: ∃X ∀n (n ∈ X ↔ φ(n)) for every arithmetic formula (i.e. Σ_{n}^{0} for some n) φ in which X is not free.

(ATR_{0}) Arithmetical Transfinite Recursion: If X is a set coding a well order <_{X} with domain D and Y is a code for a set of arithmetic formulas φ_{x}(z, Z) (indexed by x ∈ D) each with one free set variable and one free number variable, then there is a sequence ⟨K_{x} | x ∈ D⟩ of sets such that if y is the immediate successor of x in <_{X}, then ∀n (n ∈ K_{y} ↔ φ_{x}(n, K_{x})), and if x is a limit point in <_{X}, then K_{x} is ⨁{K_{y} | y <_{X} x}.

(Π_{1}^{1}-CA_{0}) Π_{1}^{1} Comprehension: ∃X ∀k (k ∈ X ↔ φ(k)) for every Π_{1}^{1} formula φ in which X is not free.

Although they make almost no appearance in practice (but see §6), one can now climb up the comprehension hierarchy for Π_{n}^{1} sentences (Π_{n}^{1}-CA_{0}) all the way to the end.

(Z_{2}) or (Π_{∞}^{1}-CA_{0}) Full Second Order Arithmetic: RCA_{0} plus the comprehension axioms: ∃X ∀k (k ∈ X ↔ φ(k)) for every formula φ of second order arithmetic in which X is not free.

If we strengthen the basic induction axiom I_{0} by replacing it with induction for all formulas φ of second order arithmetic we get full induction

(I) (φ(0) ∧ ∀n (φ(n) → φ(n + 1)) → ∀n (φ(n)) for every formula φ of second order arithmetic.

Each of the systems above has an analog in which I_{0} is replaced by I. It is designated by the same letter sequence as above but without the subscript 0, as for example, RCA in place of RCA_{0}. Obviously, if an ω-model M (those with M = ℕ) is a model of one of the systems above, such as Π_{1}^{1}-CA_{0}, then it is also a model of the analogous system, such as Π_{1}^{1}-CA. At times systems with an intermediate set of induction axioms such as for Σ_{n}^{i} formulas (Σ_{n}^{i}-IND_{0}) for i = 0 or 1 and n ∈ ω as well as transfinite induction axioms over all well-orderings for Π_{n}^{1} formulas, Π_{n}^{1}-TI_{0}, or Π_{∞}^{1}-TI_{0} for all formulas of Z_{2}.

The five basic systems correspond to well known philosophical approaches to, and foundational systems for, mathematics. In ascending order they are essentially similar to Bishop’s constructivism; Hilbert’s finitistic reductionism; the Predicativism of Weyl and Feferman; the Predicative Reductionism of Friedman and Simpson and Impredicativity as developed by Feferman and others. (For references and further discussion see Simpson [2009, I.12].) These systems also correspond to classical principles in recursion theory: the existence of recursive sets and closure under Turing reducibility and join; the Jockusch-Soare [1972] low basis theorem; closure under the Turing jump; closure under hyperarithmetic reducibility (roughly); closure under the hyperjump. Indeed for ω-models M, the basic proof theoretic systems (other than ATR_{0} which is a bit more complicated) are equivalent to these recursion theoretic principles. (For notation, background and basic information about recursion theory, we refer to Rogers [1967], Odifreddi [1989], [1999] and Soare [1987].)

We pursue three themes in the rest of this paper. First, we present an alternative viewpoint from which one can pursue the goals of reverse mathematics. Instead of being proof theoretic, it is recursion theoretic and based on a computational approach to the analysis of the complexity of mathematical theorems and constructions. In addition to having some expository advantages, this approach provides immediate generalizations to uncountable structures and so a setting in which one can hope to pursue the goals of reverse mathematics for intrinsically uncountable structures, constructions and theorems.

Next, we consider both techniques and theorems of various branches of logic that provide either tools or fodder for reverse mathematical analysis. While almost all of the mathematical theorems analyzed in the first years of the subject and the bulk of them even to this date, turned out to be equivalent to one of the five basic systems, we now have a fair number of theorems that are not equivalent to any of them. These outliers fall at times below WKL_{0}, above Π_{1}^{1}-CA_{0} or between some of the other systems. There are also now instances of incomparability (in the sense of reverse mathematics) among classical theorems. As our third theme, we present and explore some examples of each of these phenomena along with our discussions of the roles of the branches of mathematical logic within reverse mathematics. Our choices of examples and results in each of these themes are admittedly colored by my own views, prejudices and research (and that of my students and coauthors). They come primarily from logic and combinatorics. Still, we hope they convey and sufficiently exemplify our concerns.

2 A Computational Point of View

Traditionally, reverse mathematics is presented as in §1 in terms of formal logical systems and proofs in those systems. As logicians, this seems quite natural and so a perfect way of measuring the strength or difficulty of mathematical theorems. We suspect that most mathematicians do not approach the issue (if they do so at all) from such a viewpoint. While they may concern themselves with (or attempt to avoid) the axiom of choice or transfinite recursion, they certainly do not think about (nor care), for example, how much induction is used in any particular proof. We want to present another view of the subject that eschews formal logic, syntax and proof systems in favor of computability. It is actually already in widespread use in practice, if not theory, but we think is worth making explicit for expository reasons in the countable setting and as a way of generalizing the subject to the uncountable.

As an illustration, we begin with a personal story about how I began to work in the area. Many years ago, I was visiting at Ben Gurion University. At the department tea, one of my logician colleagues came over with another mathematician and said, let me introduce you to someone who can answer your questions. This was a bit frightening as an introduction but I said hello and met Ron Aharoni, a combinatorist from the Technion, who also happened to be visiting in Be’er Sheva that day. Aharoni told me that, after many years of hard work, he had answered an old problem of Erdös by showing that an important theorem of classical combinatorics about finite graphs could be generalized to graphs of all cardinalities. While very pleased to have proven the theorem, Ron was disturbed (or perhaps also pleased) that he had to use various set theoretic techniques beyond those typical of classical combinatorics. In particular, he said that usually when a combinatorists generalizes a result about finite graphs to infinite ones, the proof proceeds fairly simply by a compactness argument. In this case, he had to use the axiom of choice, transfinite recursion and more. So he was concerned, not that the problem was hard in the sense of combinatorially intricate and complex (after all that was his bread and butter), but that its solution required construction procedures that seemed outside the usual bounds of the subject. His question was if there was a way to prove that no argument by compactness would suffice and that the methods he used were actually necessary.

My reply was that there was a subject (called reverse mathematics) that dealt with such questions and we should talk about his theorem. I asked that he explain the theorem and why he thought it was complicated. The classical result was the König Duality Theorem (or min-max theorem). It asserts (in a common formulation) that in any bipartite graph the minimal size of a cover is the maximal size of a matching. (A graph G = ⟨V, E⟩ is bipartite if its vertex set V can be divided into two disjoint sets A and B such that every edge e ∈ E connects a vertex in A with one in B. A matching in G is a set F ⊆ E of disjoint edges (no vertex in common). A subset C of the vertices V is a cover of G if it contains a vertex from every edge.) To make proper sense of this in the infinite setting (where simply having the same cardinality turns out not to be particularly informative), one notes that the proof for finite graphs supplies an explicit demonstration of the equality of cardinalities. The correct formulation of the theorem is that there is always a particular matching F in G and a set C consisting of one vertex from each edge in F such that C is a cover of G. As C is a cover, the matching F is clearly maximal. We call such F and C a König matching and cover. Of course, F also has the same size as C. It was the existence of a König matching and cover that Aharoni had proven for bipartite graphs of all cardinalities. We denote this version of the König duality theorem by KDT.

In answer to my question as to why he thought the problem was complicated, Aharoni began by saying that there was (in the finite case) no greedy algorithm. This means that there is no algorithm that goes through the graph and, as it finds each edge, decides whether to put it into the required matching and, if so, which vertex goes into the desired cover. He then drew some pictures to explain why there is no such algorithm. We quickly realized the same diagonalization type proof would show that there is a recursive graph with no recursive König cover. The next step was to code in the halting problem K in the sense of constructing a (recursive) graph such that any König cover for it would compute K. This was not too difficult and seemed quite normal to Aharoni. What stopped him in his tracks was my assertion that we had now proven that applications of the compactness theorem would not suffice to prove KDT. This required considerably more explanation (which we provide below). We then went on to show that the sets computable from König covers of recursive graphs were closed under complementation, projection and effective unions. I then asserted that we had proven that transfinite recursion was necessary to prove KDT. Once again, much more explanation was needed (and again provided below). In a more classical style we also proved that the axiom of choice was implied by KDT for all bipartite graphs.

[As an aside to complete this story in the setting of reverse mathematics, we note first that at the time all known proofs of KDT used some lemma that exploited Zorn’s Lemma to produce König covers with a certain maximality principle. Working with Menachem Magidor (Aharoni, Magidor and Shore [1992]), we also showed that for countable graphs, not only that one could carry out these proofs in Π_{1}^{1}-CA_{0} but that each of the lemmas and the stronger form of KDT itself actually implied Π_{1}^{1}-CA_{0}. Simpson [1994] later showed that KDT is provable in ATR_{0} by exploiting metamathematical arguments. These methods allowed him to work inside substructures of arbitrary models of ATR_{0} that satisfied enough choice principles to make arguments similar to the ones using Zorn’s lemma work in the submodels. On the other hand, they were sufficiently absolute to carry the result (for the classical version of KDT) back to the original model. Thus his metamathematical constructions produced more effective König covers than those of the known strictly mathematical proofs.]

Another version of mathematicians attempting to come to grips with reverse mathematical issues in this context can be seen in Lovasz and Plummer [1986] a basic book on matching theory. They describe (p. 4) KDT “along with the equivalent versions...” as “probably the single most important result to date in all of matching theory.” Later (p. 6), after presenting a number of related results about matchings (or marriages) in bipartite graphs, they remark that “the theorem of Frobenius is a special case of that of P. Hall, which in turn may be viewed as a special case of König’s Theorem. On the other hand, it is not difficult to derive König’s Theorem from that of Frobenius. For this reason the Marriage Theorem is often said to be a self-refining result.” (Some, perhaps logicians, might ask if, instead of self-refining, this is not a kind of circular argument.) Nonetheless, they go on (p. 12) to say “One feels, however, that König’s theorem is the deeper result. Why? These are extremely important questions. The fact that we are now able to answer them in a mathematically precise way has altered the whole of combinatorics.” Lovasz and Plummer then go on to give a long explanation of P vs. NP and explain how this can be used to distinguish among the consequences of various “equivalent” versions of the marriage theorem in such a way as to make clear why the König version is the “good” one.

Our point here is that the computational and construction oriented arguments were natural for Aharoni who was interested in infinite and even uncountable structures. For him they exhibited the complexity of solving his problem of finding König matchings and covers. For Lovasz and Plummer they were also a welcome method to distinguish among various versions of what seemed (in some quasiformal but not intuitive sense) to be the same theorem and find the better or stronger one. We now want to present a formal version of a computational approach to reverse mathematics that characterizes construction principles such as compactness (König’s Lemma) and transfinite recursions and allows one to determine which of them are required to prove specific mathematical theorems.

For the practicing reverse mathematician, especially the recursion theorists among them, these ideas are implicitly used all the time in the countable case and (for the proof theorist) amount to nothing more than restricting attention to ω-models. One can then replace basic systems with the recursion theoretic principles described in §1 and prove nonimplications among systems and particular mathematical theorems being analyzed by exploiting Turing degree or other computational complexity measures to distinguish among them. Typically, to reverse mathematically compare two Π_{2}^{1} statements ∀X∃Y Φ_{i}(X, Y), one builds a special purpose Turing ideal, i.e. a collection of sets closed under Turing reducibility and join) C. When C is taken to be the collection S of sets for a standard, i.e. ω-model of second order arithmetic, one has a model of one statement but not the other: for every X ∈ C there is a Y ∈ C such that Φ_{1}(X, Y) but there is an X ∈ C for which no Y ∈ C satisfies Φ_{2}(X, Y). One then concludes that ∀X∃Y Φ_{2} does not imply ∀X∃Y Φ_{1} over RCA as any Turing ideal is a model of RCA.

In the special, but typical, case of Π_{2}^{1} sentences, our proposal captures this approach, formalizes and makes explicit the intuition that “being harder to prove” means “harder to compute”. (See Shore [2011].)

Definition 2.1. If C is a closed class of sets, i.e. closed under Turing reducibility and join, we say that C computably satisfies Ψ (a sentence of second order arithmetic) if Ψ is true in the standard model of arithmetic whose second order part consists of the sets in C. We say that Ψ computably entails Φ, Ψ ⊨_{c} Φ, If every closed C satisfying Ψ also satisfies Φ. We say that Ψ and Φ are computably equivalent, Ψ ≡_{c} Φ, if each computably entails the other.

One can now express the computable equivalence of some Ψ with, e.g. ACA, ATR or Π_{1}^{1}-CA in this way as these systems are characterized in the terms of Definition 2.1 by closure under the recursion theoretic operations of the Turing jump, hyperarithmetic in and the hyperjump respectively. (One needs to be careful in the case of ATR. We are not assuming that our models are β-models for which being a well ordering is absolute. Thus one must understand ATR as applying to iterations of arithmetic operations along any linear ordering in which there is no descending chain in the model.) One can also describe entailment or equivalence over one of these systems by either adding them on to the sentences Ψ and Φ or by requiring that the classes C be closed under the appropriate operators and reductions. For KDT, for example, coding in the halting problem (i.e. the Turing jump) shows that it computably entails ACA. Now as WKL is simply another form of the compactness theorem for Cantor space (2^{ω}) we can see that compactness does not computably entail KDT. The Jockusch-Soare low basis theorem [1972] says that any infinite recursive binary branching tree T has an infinite path P which is low, i.e. P′ ≡_{T} 0′. Iterating this theorem and dovetailing produces a closed class C consisting entirely of low sets such that C ⊨_{c}WKL but, of course, even 0′ ∉ C and so WKL does not computably entail ACA or KDT. The other constructions described above show that KDT does computably entail ATR and that its strong form computably entails Π_{1}^{1}-CA.

More interestingly, one can directly express, in terms of computable entailment, the relationships between two mathematical statements or construction principles without going through or even mentioning any formal proof systems. As for the five basic systems themselves, they can be characterized based on construction principles seen in mathematics (in addition to the recursion theoretic ones above). RCA just corresponds to computable mathematics in the sense of algorithmic solutions to problems. WKL is already given as a type of construction principle. ACA is equivalent to König’s Lemma for arbitrary finitely branching trees. ATR is equivalent to transfinite recursion (indeed, its formal version above directly says one can iterate any (arithmetic) operation over any (computable) well-ordering) and Π_{1}^{1}-CA is equivalent to a kind of uniformization or choice principle for well founded sets.

We should note that, as the class of models considered in computable entailment (ωmodels only) is smaller than that in the usual approach to reverse mathematics, proofs of the failure of computable entailment are stronger than the failure of (logical) implication over RCA_{0} (or even RCA). On the other hand, computable entailment is weaker than implication over RCA_{0}.

Turning now to uncountable structures, one can simply interpret computability as some version of generalized computability (on uncountable domains). One then immediately has a notion of computable entailment for uncountable settings. For example, if one is interested in algebraic or combinatorial structures where the usual mathematical setting assumes that an uncountable structure is given with its cardinality, i.e. the underlying set for the structure (vector space, field, graph, etc.) may as well be taken to be a cardinal κ, then a plausible notion of computation is given by α-recursion theory. In this setting, one carries out basic computations (including an infinitary sup operation) for κ many steps. (Note that every infinite cardinal is admissible.)

For settings such as analysis where the basic underlying set is the reals ℝ or the complex numbers ℂ, it seems less natural to assume that one has a well-ordering of the structure and one wants a different model of computation. Natural possibilities include Kleene recursion in higher types, E-recursion (of Normann and Moschovakis) and Blum-Shub-Smale computability. (See for example Sacks [1990] or Chong [1984] for α-recursion theory; Sacks [1990], Moldestad [1977] or Fenstad [1980[ for the various versions of recursion in higher types or E-recursion and Blum et al. [1988] for the Blum-Shub-Smale model.)

The general program that we are suggesting consists of the following:

Problem 2.2. Develop a computability theoretic type of reverse mathematical analyses of mathematical theorems on uncountable structures using whichever generalized notion of computability seems appropriate to the subject being analyzed.

Some surprises lie in store along this road. For example, WKL is no longer a plausible basic system. For uncountable cardinals it is equivalent to the large cardinal notion of weak compactness. There is, however, another new tree property for κ that is computably equivalent to compactness for propositional or predicate logic for languages of size κ as well as the existence of prime ideals for every ring of size κ. See Shore [2011] for more details and examples.

Another “application” for our approach to reverse mathematics in the uncountable is that it provides a testing ground for notions of computation in the uncountable. For the countable setting, the widely accepted “correct” notion of computation is that of Turing and it rightfully serves as the basic ingredient of our models and approach for countable mathematics. In the uncountable setting there are many competing notions (including those mentioned above) and no consensus or even many credible claims as to one being the “right” one. We suggest that if a theory of computability for uncountable domains provides a satisfying analysis of mathematical theorems and constructions in the reverse mathematical sense based on the approach of Definition 2.1, then it has a strong claim to being a good notion of computation in the uncountable. It may well be that there is no single “right” one but that certain ones may be better than others for different branches of mathematics. These are certainly reasonable questions for the foundations of mathematics.

We now turn to the various branches of mathematical logic to see what tools they provide and what grist (theorems) for the mill of reverse mathematics. In particular, following our personal inclinations, we focus on theorems chosen from logic and combinatorics that are not equivalent to any of the four basic systems. (We exclude RCA_{0} as we continue to view it as our base theory.) Some will be below WKL_{0}, some incomparable with it, some between two of the four systems and, finally, some beyond them all.

3 Proof theory

Now, in some sense, classical reverse mathematics is simply a part of proof theory. After all, it deals with formal proof systems and the theorems that can be proved in them. (Of course, some might say that this is all of mathematics.) Nonetheless, in the hands of some (or even most) of its practitioners (myself included), it often looks like various other branches of mathematical logic. Nonetheless, there are a number of classically proof theoretic notions and methods that play a central role in its development. We briefly describe a couple of them.

The first is the notion of conservativity. We say that a theory T is conservative over one S (typically contained in T) if any theorem φ of T (in the language of S) is (already) a theorem of S. If the theorems under consideration are restricted to some (usually syntactic) class Γ then we say that T is Γ conservative over S.

Perhaps the first use of conservation results in reverse mathematics that come to mind is the obvious one of providing a wholesale method of showing that various reversals that one might be hoping for are, in fact, not possible. If S and T are two successive theories from among the five basic ones and φ is provable in T but not in S, one hopes to get a reversal by showing that S + φ ⊢ T. If, however, one shows (as is common) that S + φ is Π_{1}^{1} conservative over S then no such reversal is possible. The point here is that each of the basic theories proves the consistency of its predecessor. Thus if S + φ ⊢ T then it would also prove the consistency of S, a Π_{2}^{0} sentence, that is not provable in S by Gödel’s second incompleteness theorem. So, by the conservation result, there is no reversal, S + φ ⊬ T. Various examples, albeit not proven by proof theoretic methods, are given in the following sections. References to ones derived proof theoretically can be found in Simpson [2009].

This approach extends to a philosophical “application” central to the foundational concerns of reverse mathematics. If S and T represent philosophical approaches to (or schools of) what is acceptable mathematics then proving that T is Γ conservative over S shows that the theorems of T lying in Γ are actually acceptable to the school represented by S. As an example, we cite the fact that WKL_{0} is Π_{1}^{1} conservative over RCA_{0} and Π_{2}^{0} conservative over an even weaker theory of primitive recursive arithmetic. This means that any sentence of arithmetic that can be proven using any of the many methods of analysis or algebra that are derivable in WKL_{0} are already effectively (computably, constructively) true. Moreover, if they are Π_{2}^{0} sentences such as ones asserting the totality of some implicitly given function, ∀x∃yψ(x, y) where ψ is Σ_{1}^{0} then the function is, in fact, primitive recursive and so acceptable in the finitistic systems following Hilbert. More on this example and others can be found in Simpson [2009].

In the other (mathematical) direction of proving theorems, conservation results are also frequently very useful. If one proves that S + φ is Γ conservative over S and one wants to prove a theorem ψ ∈ Γ in S then one is allowed to use φ in the proof even though it is not itself provable in S. As an example, we cite the fact that Σ_{k+3}^{1}-AC_{0} is Π_{4}^{1} conservative over Π_{k+2}^{1}-CA_{0} (although not provable in it). This allows one to use these choice principles to prove theorems in such systems even though they are not themselves provable in the systems being used. One example is Theorem 6.1 below from Montalbán and Shore [2011] where a strong choice principle not provable in Π_{m+2}^{1}-CA_{0} but conservative over it for sentences of the desired form (by Simpson [2009, VII.6.20]) is used to prove a determinacy theorem in Π_{m+2}^{1}-CA_{0}.

Perhaps the archetypical method of classical proof theory is ordinal analysis. Here one wants to determine the (minimal) ordinal γ (and some effective presentation of it) such that an induction of length γ suffices to prove the consistency of a given system T. From the viewpoint of reverse mathematics, such results are also limiting. The most famous examples are Friedman’s early results (see Simpson [1985] or Schwichtenberg and Wainer [2011]) that various versions of Kruskal’s theorem and then later of the Graph Minor theorem (Friedman, Robertson and Seymour [1987]) are not provable in strong systems including ATR_{0} and Π_{1}^{1}-CA_{0}. Basically one proves that the combinatorial theorems in question establish the well foundedness of systems of ordinal notations larger than the ordinal needed to prove the consistency of the system in question. So again by Gödel’s second incompleteness theorem, they cannot be proven in it. More recently Marcone and Montalbán are using ordinal notation systems to analyze the strength of weak versions of Fraisse’s conjecture [2009] and [2011] with a more proof theoretic approach in Afshari and Rathjen [2009]. Rathjen and Weiermann [2011] have analyzed maximal well orderings of various types to better understand the strength of several Kruskal-like theorems.

Proof theoretic methods also contribute to more constructive approaches to many theorems in other settings as in the newly revived area of proof mining (see for example Kohlenbach [2008]). They also have appeared (for higher type systems) as another method for extending reverse mathematics to the uncountable, especially in the study of analysis (Kohlenbach [2005]). More could be said but the natural direction of proof theory is to study consistency strength rather than strength as measured in terms of provability as in reverse mathematics. It is a finer measure but one that goes in a direction opposite to the one we are expositing (and espousing) here of restricting attention to ω-models and computability.

4 Recursion theory and intermediate systems

Clearly the most common application of recursion theory in reverse mathematics is to the separation of systems and theorems. As mentioned in §2.1, given two Π_{2}^{1} theorems ∀X∃Y Φ and ∀X∃Y Ψ one builds a Turing ideal C in which the first but not the second is true. Thus Φ does not computably entail Ψ and so does not imply Ψ over RCA. If one wants the nonimplication to hold over ACA or Π_{1}^{1}-CA one makes C closed under the Turing or hyperjump, respectively. One builds these ideals by first producing a construction that, given any X adds a solution to Φ, i.e. a Y such that Φ(X, Y) holds, but such that there is no solution for Ψ recursive (or arithmetic if working, say, over ACA) in Y. One then iterates this construction dovetailing over all instances of Φ produced along the way (i.e. sets X recursive in the finite joins of Y ’s so produced) to construct a Turing ideal satisfying Φ but not Ψ.

The basic constructions in this process are often (recursion theoretic) forcing arguments. They also at times use priority arguments and many other standard recursion theoretic techniques. Cone avoiding has an obvious role to play. If, for example, one can add on solutions for Φ always avoiding the cone above 0′ (i.e. no set computing 0′ is introduced) then one proves that Φ does not imply ACA_{0}. More delicate examples often involve guaranteeing that the solution Y to Φ constructed is low or low_{2} (i.e. Y′ ≡_{T} 0′ or Y′′ ≡_{T} 0′′). One example already mentioned is the Jockush-Soare low basis theorem which constructs a low solution to any recursive instance of WKL_{0} and so proves that WKL_{0} does not computably entail (nor then imply) ACA_{0} (over RCA_{0}). This construction can be combined with cone avoiding and other properties to provide many examples of nonimplications.

To be more specific, we give some of the combinatorial theorems that appear in these sorts of applications and the relations among them. (Some model theoretic ones are in §5.) They provide several examples of construction principles or axiomatic systems that are not captured by any of the five basic systems of reverse mathematics. The extent to which these systems are outside the scope of the five basic ones and even provide examples of incomparable principles in the sense of reverse mathematics is illustrated in Diagram 1 below. Note that Ramsey’s Theorem for pairs, RT_{2}^{2}, is strictly weaker than ACA_{0}. Single arrows are implications; double arrows are strict implications and negated arrows represent known nonimplications (all over RCA_{0}). The nonimplications are essentially all proved by recursion theoretic techniques showing the failure of computable entailment. (See Hirschfeldt and Shore [2007, §3] for attributions and references for the implications and nonimplications.) The picture alone conveys the essence of our claims but for completeness we provide the formal definitions of the systems as well.

(RT_{2}^{2}) Ramsey’s Theorem for pairs: Every 2-coloring of [ℕ]^{2} (the unordered pairs of natural numbers) has a homogeneous set, i.e. for every f : [ℕ]^{2} → {0, 1} there is an infinite H such that |f“[H]^{k}| = 1.

(SRT_{2}^{2}) Stable Ramsey’s Theorem for pairs: Every stable coloring of [ℕ]^{2} (i.e. (∀x)(∃y)(∀z > y)[f(x, y) = f(x, z)]) has a homogeneous set.

(COH) Cohesive Principle: For every sequence of sets R = ⟨R_{i} | i ∈ ℕ⟩ there is an R-cohesive set S (i.e. (∀i)(∃s)[(∀j > s)(j ∈ S → j ∈ R_{i}) ∨ (∀j > s)(j ∈ S → j ∉ R_{i})]).

(CAC) Chain-AntiChain: Every infinite partial order (P, ≤_{P}) has an infinite subset S that is either a chain, i.e. (∀x, y ∈ S)(x ≤_{P} y ∨ y ≤_{P} x), or an antichain, i.e. (∀x, y ∈ S)(x ≠ y → (x ≰_{P} y ∧ y ≰_{P} x)).

(ADS) Ascending or Descending Sequence: Every infinite linear order (L, ≤_{L}) has an infinite subset S that is either an ascending sequence, i.e. (∀s < t)(s, t ∈ S → s <_{L} t), and so of order type ω, or a descending sequence, i.e. (∀s < t)(s, t ∈ S → t <_{L} s), and so of order type ω^{∗}.

(SADS) Stable ADS: Every linear order of type ω + ω^{∗} has a subset of order type ω or ω^{∗}.

(CADS) Cohesive ADS: Every linear order has a subset S of order type ω, ω^{∗}, or ω + ω^{∗}.

(SCAC) Stable CAC: Every infinite stable partial order has an infinite chain or antichain. A partial order P is stable if either

(∀i ∈ P)(∃s)[(∀j > s)(j ∈ P → i <_{P} j) ∨ (∀j > s)(j ∈ P → i |_{P} j)]

or

(∀i ∈ P)(∃s)[(∀j > s)(j ∈ P → i >_{P} j) ∨ (∀j > s)(j ∈ P → i |_{P} j)].

(CCAC) Cohesive CAC: Every partial order has a stable suborder.

(DNR) Diagonally Nonrecursive Principle: For every set A there is a function f that is diagonally nonrecursive relative to A, i.e. ∀n¬(f(n) = Φ_{n}^{A}(n)).

[figure: RT_{2}^{2}; _{SRT2 2}; DNR; CAC; |; _{WKL_{0}}; |; COH; SCAC; |; ADS; COH; COH + WKL_{0}; |; SADS; CADS; _{RCA_{0}}]

Diagram 1

Recursion theoretic techniques have also been used to reduce the reverse mathematical strength of the systems needed to prove various theorems. Of course, there are examples for recursion theoretic results. The most dramatic is for the definability of the Turing jump. The original proof of Shore and Slaman [1999] used metamathematical arguments of Slaman and Woodin (see Slaman [1991] or [2008]) that included set theoretic forcing to collapse the continuum to a countable set as well as absoluteness arguments. A new proof (Shore [2007]) eliminates all of these arguments in favor of purely recursion theoretic ones and provides a proof of the definability of the Turing jump in the Turing degrees with ≤_{T} that can be carried out in ACA_{0} + (0^{ω} exists) (more than ACA_{0} but less than ACA_{0}^{+} which is equivalent to closure under the arithmetic jump). This is a major reduction in proof theoretic strength. It is an important open question as to whether the definability can be proved in ACA_{0} (and so, as would be hoped, the definition would work inside every Turing jump ideal, not just those containing 0^{ω}).

Perhaps more surprisingly, the technique now called Shore blocking that was originally developed in my thesis (Shore [1972]) for α-recursion theory has been used with priority arguments to eliminate extra induction assumptions and prove theorems of combinatorics and model theory in RCA_{0} as well as some reversals. (See §5, [Hirschfeldt, Shore and Slaman [2009] and Hirschfeldt, Lange and Shore [2012].)

5 Model theory and weak systems

From the beginning model theoretic techniques (especially those devoted to models of arithmetic) played (and continue to play) an important role in distinguishing between different systems particularly weak ones and those involving low levels of induction as in the basic results of Kirby and Paris [1978] (see also Hajek and Pudlak [1998, IV]. Perhaps more surprisingly they (along with both recursion and set theoretic methods) play a role in the proof theoretic endeavor of establishing conservation results. (See, for example, Simpson [2009, IX.4] for uses of (recursive) saturation in the study of strong choice principles.)

More recently, the methods and approaches of nonstandard analysis have been used to attack the basic problem of reverse mathematics of describing systems that capture the strength of ordinary mathematical theorems. We point to Keisler [2006], [2011] and Yokoyama [2007], [2009] as examples.

A particularly striking recent example of the study of the structure of nonstandard models of arithmetic leading to the solution of reverse mathematical problems that seem to be of a purely combinatorial nature is Chong, Lempp and Yang [2010]. They build on a series of papers investigating cuts in models of arithmetic and their recursion theoretic properties (by Chong, Slaman, Yang and others). In particular, they apply recursion theoretic restrictions on such cuts that are based on the notions of tameness introduced by Lerman [1972] in α-recursion. These notions enable them to solve several open problems from Cholak, Jockusch and Slaman [2001], Hirschfeldt and Shore [2007] and Dzhafarov and Hirst [2009] about the reverse mathematical relationships among various purely combinatorial principles related to Ramsey theory and its weak variants.

Following the “grist for the mill” theme, we note that classical (Robinson style) model theory has recently (Hirschfeldt, Shore and Slaman [2009] and Hirschfeldt, Lange and Shore [2012]) provided an unexpectedly rich source of construction type principles that are very weak from the viewpoint of reverse mathematics. Even ones lying below all the combinatorial principles mentioned in §4.

Before stating the principles we recall the definitions of some basic model theoretic notions.

Definition 5.1. A partial type of a (countable, deductively closed, complete and consistent) theory T is a set of formulas in a fixed number of free variables that is consistent with T. A type is a complete type, i.e. a maximal partial type. A partial type Γ is realized in a model A of T if there is an ā such that A ⊨ ϕ(ā) for every ϕ ∈ Γ. Otherwise, Γ is omitted in A.

A formula φ(x_{1}, …, x_{n}) of T is an atom of T if for each formula ψ(x_{1}, …, x_{n}) we have T ⊢ φ → ψ or T ⊢ φ → ¬ψ but not both. A partial type Γ is principal if there is a formula φ consistent with T such that T ⊢ φ → ψ for all ψ ∈ Γ. Thus a complete type is principal if and only if it contains an atom of T.

The theory T is atomic if, for every formula ψ(x_{1}, …, x_{n}) consistent with T, there is an atom φ(x_{1}, …, x_{n}) of T such that T ⊢ φ → ψ. A model A of T is atomic if every n-tuple from A satisfies an atom of T, that is, every type realized in A is principal.

Now for our model theoretic principles:

(AMT): Every complete atomic theory has an atomic model.

(OPT): If S is a set of partial types of T, there is a model of T that omits all nonprincipal partial types in S.

(AST): If T is an atomic theory whose types are subenumerable, i.e. there is a set S such that (∀Γ a type of T)(∃i)({ϕ | ⟨i, ϕ⟩ ∈ S} implies the same formulas over T as Γ), then T has an atomic model.

(HMT): If X is a set of types over T satisfying some necessary closure conditions then there is a homogeneous model of T realizing exactly the types in X. [A model M of T is homogeneous, if for all ā and b̄ from M satisfying the same type and all c̄ ⊂ M, there exists an M-tuple d̄ such that (ā, c̄) satisfies the same type as (b̄, d̄). The closure conditions on an X containing T are as follows: (1) X is closed under permuting variables and subtypes. (2) If p(x̄) ∈ X and ϕ(x̄, ȳ) are consistent, ∃q ∈ X(p ∪ {ϕ} ⊆ q). (3) If p(x̄), q_{0}(ȳ_{0}), … q_{n}(ȳ_{n}) ∈ X and x̄ includes the variables shared between any q_{i} ≠ q_{j}, then ∃q ∈ X(q ⊇ p, q_{0}, …, q_{n})).]

The first (and strongest) of these principles, AMT, is a standard result of classical model theory. Surprisingly, it is strictly weaker (in the sense of reverse mathematics) than even SADS, itself a minimal principle among the combinatorial ones considered in §4. Now every atomic model is homogeneous but not the reverse. Indeed classically it seems in various ways much easier to construct homogenous models than atomic ones. Nonetheless, the construction principles (as formalized above) are computationally and reverse mathematically equivalent, i.e. AMT and HMT are equivalent over RCA_{0}. The other two principles turn out to be reverse mathematically equivalent to two standard recursion theoretic constructions. OPT is equivalent (over RCA_{0}) to the existence (for each set X) of a function f (computing X) which is not dominated by any recursive (in X) function. The last, AST, is equivalent (over RCA_{0}) to what might naturally be regarded as the weakest possible principle (above RCA_{0}): the existence (for each X) of a set not recursive (in X). We find it quite surprising but very pleasing that a simple model theoretic principle making no mention of any notions of computability turns out to have the same computational and proof theoretic strength as the existence of a nonrecursive set. These results are also quite interesting from the methodological point of view. The techniques used to establish this last equivalence (over RCA_{0}) as well as that of AMT and HMT (Hirschfeldt, Lange and Shore [2012]) include both Shore blocking and priority arguments.

We close this section with a Diagram illustrating the relations among the model theoretic principles discussed in this section with the combinatorial ones from the last section. (Augmented by one new combinatorial one that is of independent interest in analyzing the relations among weak versions of induction: (Π_{1}^{0}G) For any uniformly Π_{1}^{0} collection of sets D_{i} each of which is dense in 2^{<ℕ} there is a G such that ∀i∃s(G ↾ s ∈ D_{i}).)

[figure: COH; SADS; Π_{1}^{0}G; |; |; |; _{WKL_{0}}; |; AMT; OPT; AST; _{RCA_{0}}]

Diagram 2

6 Set theory and strong systems

The set theoretic technique most widely used in reverse mathematics is certainly forcing in its recursion theoretic setting of forcing in arithmetic. The nature of forcing, after all, is to add a set with tightly controlled properties while preserving the base theory. Thus, given a particular mathematical construction problem as expressed by a Π_{2}^{1} sentence Φ(X, Y), one looks for a notion of forcing that adds a solution Y for a given input X and preserves RCA_{0}. Iteration (and dovetailing) produces a model for the given sentence. As in set theory, one produces independence results by adding in a solution to Φ that does not add a solution to some other problem Ψ. Typically, one works over a standard (ω-) model of arithmetic and proves that Φ does not computably entail Ψ. Perhaps more surprisingly, one can often use forcing over nonstandard models to derive nonimplication results over RCA_{0}. Taken to its natural conclusion, such methods are even used to produce conservation theorems. Essentially every forcing argument that works over arbitrary models of a system T proves a Π_{1}^{1} conservation result over T since it does not change the natural numbers. Thus arithmetic formulas (even with set parameters) are absolute to the generic extension. In some cases, one can analyze the notion of forcing to show that no solutions are added to any problem (Π_{2}^{1} formula) of some specified syntactic form to prove stronger conservation results and wholesale nonimplications from the given problem Φ to a class of other problems. For example, Hirschfeldt and Shore [2007] introduce the notion of conservativity for Φ of the form ∀A(θ(A) → ∃Bψ(A, B) , θ arithmetic and ψ ∈ Σ_{3}^{0} which are called r-Π_{2}^{1} for restricted Π_{2}^{1}. Cohen, Mathias and Sacks forcing are all r-Π_{2}^{1} conservative over RCA_{0} and so none of AMT (or a fortiori, OPT or AST) (Hirschfeldt, Shore and Slaman [2007]), COH, CADS (Hirschfeldt and Shore [2007]) or the existence of minimal covers (or even all of them together) imply any of RT_{2}^{2}, SRT_{2}^{2}, WKL_{0}, DNR, CAC, ADS or SADS (over RCA_{0}). This, for example, shows that CADS and SADS (which together imply ADS) are incomparable over RCA_{0} and so each is strictly weaker than ADS.

A very recent, quite remarkable application of techniques from set theory appear in Neeman [2011], [2012]. Montalbán [2006] showed that a purely mathematical theorem of Jullien [1969] (see Rosenstein [1982], Lemma 10.3) about indecomposable linear orderings was a theorem of hyperarithmetic analysis, i.e. true in the standard models whose sets are precisely the hyperarithmetic ones in some X, but implies closure under “hyperarithmetic in” for ω-models. Indeed, he also showed that it was a consequence of Δ_{1}^{1}-CA_{0}. This was the first “natural” mathematical theorem with these properties. Neeman [2011] shows that this theorem implies, but is not implied by, a weak version of Σ_{1}^{1} choice and also does not imply Δ_{1}^{1}-CA. All of these results assume Σ_{1}^{1}-IND_{0}. The techniques here include forcing (with Steel’s tagged trees [1977], [1978]) and inner models of the generic extensions similar to those used by Steel and others. Quite surprisingly, Neeman [2012] shows that Σ_{1}^{1}-IND_{0} is necessary for the reversal from the theorem to the choice principle. As far as we know, this is the first proof of the necessity of a strong induction axiom for a reversal. Indeed, Neeman builds a (necessarily) nonstandard model of RCA_{0} + Δ_{1}^{1}-IND_{0} + the theorem of Jullien in which the relevant weak version of Σ_{1}^{1} choice fails. He here uses not only Steel’s forcing but an elementary embedding of the standard model produced into a nonstandard extension to define the desired model witnessing the nonimplication.

Not surprisingly, in the “grist for the mill” direction set theory supplies a fertile ground for the higher ends of our basic systems. The analysis of (countable) ordinal arithmetic is naturally situated at the level of ATR_{0} where most of the usual theorems can be proved. In the reverse direction, the comparability of well orderings (and even apparently weaker principles) imply ATR_{0} (over RCA_{0}) (See Simpson [2009, V.6 and the notes there for examples and references.) Some theorems require Π_{1}^{1}-CA_{0} and versions of the Cantor-Bendixson analysis, the perfect set theorem and other basic facts about descriptive set theory are equivalent to it (See Simpson [2009, VI]. At these levels one can also translate second order arithmetic into a set theoretic language that allows one to mimic the construction of Gödel’s L and use the machinery of L (such as Jensen’s fine structure analysis of Σ_{n} and Δ_{n} projecta) to analyze and apply theorems and principles such as the Shoenfield absoluteness theorem and strong versions of choice going beyond Π_{1}^{1}-CA_{0} (Simpson [2009, VII]).

Up until quite recently almost no mathematical theorems expressible in second order arithmetic were know to require much more than Π_{1}^{1}-CA_{0}. A combinatorial result or two such as the graph minor theorem (Friedman, Robertson and Seymour [1987] were long known to be beyond it and Laver’s theorem (Fraïssé’s conjecture) has long been a candidate for not being provable in ATR_{0} or perhaps even Π_{1}^{1}-CA_{0}. (See Shore [1993] for a proof that it implies ATR_{0} and Marcone and Montalbán [2009] for the beginnings of a program to show it goes beyond ATR_{0} and perhaps eventually Π_{1}^{1}-CA.) Still these sorts of results are generally known to be provable in Π_{2}^{1}-CA_{0}. Remarkably, Mumert and Simpson [2005] have found some theorems of topology equivalent to Π_{2}^{1}-CA_{0} but that has been about the limit of our examples.

To reach the heights of second order arithmetic, Z_{2}, we return to the roots of reverse mathematics: the Axiom of Determinacy and Friedman [1971]. In his first foray into the area that grew into reverse mathematics, Friedman [1971] famously proved that Borel determinacy is not provable in either ZC (ZFC without the replacement axiom) or ZFC^{−} (ZFC without the power set axiom). (We say that a set A ⊆ 2^{ω} is determined if there is a function f : 2^{<ω} → 2 (called a strategy) such that either every g ∈ 2^{ω} such that ∀n(g(2n) = f(g ↾ 2n)) is in A (player I wins the game) or no g ∈ 2^{ω} such that ∀n(g(2n + 1) = f(g ↾ 2n + 1)) is in A (player II wins the game). For a class of sets Γ, Γ determinacy says that every A ∈ Γ is determined.)

Indeed, Friedman showed that one needs ℵ_{1} many iterations of the power set to prove Borel determinacy. Martin [1975], then showed that it is provable in ZFC and provided a level by level analysis of the Borel hierarchy and the number of iterations of the power set needed to establish determinacy at those levels. Moving from set theory to second order arithmetic and so reverse mathematics, Friedman [1971] also showed that Σ_{5}^{0} determinacy is not provable in full second order arithmetic. Martin [1974a], [n.d., Ch. 1] improved this to Σ_{4}^{0} determinacy. He also presented [1974], [n.d., Ch. 1] a proof of Δ_{4}^{0} determinacy that he said could be carried out in Z_{2}. This seemed to fully determine the boundary of determinacy that is provable in second order arithmetic and to leave only the first few levels of the Borel hierarchy to be analyzed from the viewpoint of reverse mathematics.

The first very early result (essentially Steel [1976] see also Simpson [2009 V.8]) was that Σ_{1}^{0} determinacy is equivalent (over RCA_{0}) to ATR_{0}. Tanaka [1990] then showed that Π_{1}^{1}-CA_{0} is equivalent to Σ_{1}^{0} ∧ Π_{1}^{0} determinacy. Moving on to Σ_{2}^{0} determinacy, Tanaka [1991] showed that it is equivalent to an unusual system based on closure under monotonic Σ_{1}^{1} definitions. At the level of Δ_{3}^{0} determinacy, MedSalem and Tanaka [2007] showed that each of Π_{2}^{1}-CA_{0} + Π_{3}^{1}-TI_{0} and Δ_{3}^{1}-CA_{0} + Σ_{3}^{1}-IND_{0} prove Δ_{3}^{0} determinacy but Δ_{3}^{1}-CA_{0} alone does not. They improve these results in [2008] by showing that Δ_{3}^{0} determinacy is equivalent (over Π_{3}^{1}-TI_{0}) to another system based on transfinite combinations of Σ_{1}^{1} inductive definitions. Finally, Welch [2009] has shown that Π_{3}^{1}-CA_{0} proves not only Π_{3}^{0} determinacy but even that there is a β-model of Δ_{3}^{1}-CA_{0} + Π_{3}^{0} determinacy. In the other direction, he has also shown that, even augmented by an axiom about the convergence of arithmetical quasi-inductive definitions, Δ_{3}^{1}-CA_{0} does not prove Π_{3}^{0} determinacy. The next level of determinacy is then Δ_{4}^{0}.

Upon examining Martin’s proof of Δ_{4}^{0} determinacy as sketched in [1974] and then later as fully written out in [n.d., Ch. 1] with Montalbán, it seemed to us that one cannot actually carry out his proof in Z_{2}. Essentially, the problem is that the proof proceeds by a complicated induction argument over an ordering whose definition seems to require the full satisfaction relation for second order arithmetic This realization opened up anew the question of determining the boundary line for determinacy provable in second order arithmetic.

In Montalbán and Shore [2011], we answer that question by analyzing the strength of determinacy for the finite levels of the difference hierarchy on Π_{3}^{0} sets, the m-Π_{3}^{0} sets. (These are the sets of the form A_{0} − A_{1} ∪ A_{2} − A_{3} ∪ A_{4} − … A_{m} for A_{i} ∈ Π_{3}^{0}, a natural hierarchy for the finite Boolean combinations of Π_{3}^{0} sets.) In the positive direction, we produce a variant of Martin’s proof specialized and simplified to the finite levels of the difference hierarchy on Π_{3}^{0} along with the analysis needed to determine the amount of comprehension used in the proof for each level of the hierarchy.

Theorem 6.1. For each m ≥ 1, Π_{m+2}^{1}-CA_{0} ⊢ m-Π_{3}^{0} determinacy.

In the other direction, we prove that this upper bound is sharp in terms of the standard subsystems of second order arithmetic thus climbing up the comprehension hierarchy to full Z_{2} with mathematical theorems provable precisely at each level.

Theorem 6.2. For every m ≥ 1, Δ_{m+2}^{1}-CA does not prove m-Π_{3}^{0} determinacy.

As any proof in Z_{2} uses only finitely many instances of comprehension axioms, determinacy for the union of all of these classes lies beyond the scope of full second order arithmetic and gives us the precise boundary for its strength.

Corollary 6.3. Determinacy for the class of all finite Boolean combinations of Π_{3}^{0} classes of reals (ω-Π_{3}^{0} determinacy) cannot be proved in second order arithmetic. As these classes are all (well) inside Δ_{4}^{0}, Z_{2} does not prove Δ_{4}^{0} determinacy.

Note that by Theorem 6.1, any model of second order arithmetic in which the natural numbers are the standard ones (i.e. ℕ) does satisfy ω-Π_{3}^{0} determinacy and so the counterexample for its failure to be a theorem of Z_{2} must be nonstandard. In contrast, the counterexamples from Friedman [1971] and Martin [1974a], [n.d., Ch. 1] are all even β-models, so not only with its numbers standard but all its “ordinals” (well orderings) are true ordinals (well orderings) as well.

If one wants to return to the set theoretic setting, we can reformulate this limitative result by noting the following conservation result (Montalbán and Shore [2011]).

Proposition 6.4. ZFC^{−}, even with a definable well ordering of the universe assumed as well, is a Π_{4}^{1} conservative extension of Z_{2}.

Corollary 6.5. Determinacy for the class of all finite Boolean combinations of Π_{3}^{0} classes (ω-Π_{3}^{0} determinacy) and so, a fortiori, Δ_{4}^{0} determinacy cannot be proved in ZFC^{−}.

The techniques used to prove Theorem 6.2 include some elementary fine structure and admissibility theory to show that the first Σ_{m} admissible ordinal α, while a model of Δ_{m+2}^{1}-CA (even a β-model), is not a model of m − Π_{n}^{0} determinacy.

In fact, the counterexamples that establish Theorem 6.2 are all given by effective versions of the m-Π_{3}^{0} sets where the initial Π_{3}^{0} sets are effectively defined, i.e. without set parameters. This gives rise to a Gödel like phenomena for second order arithmetic with natural mathematical Σ_{2}^{1} statements saying that specific games have strategies and containing no references to provability.

Theorem 6.6. There is a Σ_{2}^{1} formula φ(x) with one free number variable x, such that, for each n ∈ ω, Z_{2} ⊢ φ(\underline{n}) but Z_{2} ⊬ ∀nφ(n).

Of course, on their face, Theorems 6.1 and 6.2 along with Corollary 6.3 produce a sequence of Π_{3}^{1} formulas ψ(n) that have the same proof theoretic properties as those in Theorem 6.6 while eliminating the references to syntax and recursion theory present in the φ of Theorem 6.6. They simply state the purely mathematical propositions that all n-Π_{3}^{0} games are determined. (Here we are thinking of the Π_{3}^{0} sets as being the F_{σδ} ones, i.e. countable intersections of countable unions of closed subsets of 2^{ω}.)

The natural question now is what about reversals, i.e. what can these determinacy results prove? The answer is nothing more than the Π_{1}^{1}-CA_{0} already derivable from Σ_{1}^{0} ∧Π_{1}^{0} determinacy. MedSalem and Tanaka [2007] have shown (using coded models and an appeal to Gödel’s second incompleteness theorem) that even full Borel determinacy does not imply Δ_{2}^{1}-CA_{0}. We (Montalbán and Shore [2011]) provide a different route finding β-model counterexamples in L or L(X) that apply to a wide class of sentences.

Theorem 6.7. If T is a true Σ_{4}^{1} sentence (e.g. a theorem of ZFC) then T + Π_{1}^{1}- CA + Π_{∞}^{1}-TI ⊬ Δ_{2}^{1}-CA_{0}.

Corollary 6.8. Borel determinacy + Π_{1}^{1}-CA + Π_{∞}^{1}-TI ⊬ Δ_{2}^{1}-CA_{0}.

We can say even more. Not only are there no reversals over RCA_{0} but even assuming Δ_{n+2}^{1}-CA does not help.

Theorem 6.9. If T is a true Σ_{4}^{1} formula then, for n ≥ 2, Δ_{n}^{1}-CA +T + Π_{∞}^{1}-TI ⊬ Π_{n}^{1}-CA_{0}.

Corollary 6.10. For n ≥ 0, Δ_{n+2}^{1}-CA + n-Π_{3}^{0} determinacy + Π_{∞}^{1}-TI ⊬ Π_{n+2}^{1}-CA_{0}.

Thus Δ_{n+2}^{1}-CA_{0} + n-Π_{3}^{0} determinacy is strictly between Δ_{n+2}^{1}-CA_{0} and Π_{n+2}^{1}-CA_{0}. Again the results follow from more general ones for Π_{n}^{1}-CA_{0} that are proved by working in L(X).

6.1 Conclusions

We have tried to paint a picture of reverse mathematics as intimately involved with all the classical fields of mathematical logic. Of course, by the nature of its subject matter, it also deals with most areas of classical mathematics. As a playground then, its playing fields are large, there are many kinds of games to play and a wide variety of equipment. I urge you to come on in and join the fun.

References

[1] Aharoni, R., Magidor, M. and Shore, R. A. [1992], On the strength of König’s duality theorem for infinite bipartite graphs, Journal of Combinatorial Theory (B) 54, 257-290.

[2] Afshari, B. and Rathjen, M. [2009], Reverse Mathematics and Well-Ordering Principles: A Pilot Study, Annals of Pure and Applied Logic 160, 231-237.

[3] Blum, L., Cucker, F., Shub, M. and Smale, S. [1998], Complexity and Real Computation, Springer-Verlag, New York.

[4] Chong, C. T. [1984], Techniques of Admissible Recursion Theory, Lecture Notes in Mathematics 1106, Springer-Verlag, Berlin.

[5] Chong, C. T., Lempp, S. and Yang, Y. [2010], On the role of the Collection Principle for Σ_{2}^{0}-formulas in second-order reverse mathematics, Proceedings of the American Mathematical Society 13, 1093-1100.

[6] Cholak, P. A., Jockusch, Jr., C. G. and Slaman, T. A. [2001], On the strength of Ramsey’s Theorem for pairs, Journal of Symbolic Logic 66, 1–55.

[7] Downey, R., Hirschfeldt, D. R., Lempp, S. and Solomon, R. [2001], A Δ_{2}^{0} set with no infinite low subset in either it or its complement. Journal of Symbolic Logic 66, 1371–1381.

[8] Dzhafarov, D. and Hirst, J. [2009], The polarized Ramsey theorem, Archive for Mathematical Logic 48, 141-157.

[9] Fenstad, Jens Erik [1980], General Recursion Theory: An Axiomatic Approach, Perspectives in Mathematical Logic, Springer-Verlag, Berlin-New York.

[10] Friedman, H. [1967], Subsystems of Set Theory and Analysis, Ph.D. Thesis, M.I.T.

[11] Friedman, H. [1971], Higher set theory and mathematical practice, Annals of Mathematical Logic 2, 325-357.

[12] Friedman, H. [1975], Some systems of second order arithmetic and their use, in Proceedings of the International Congress of Mathematicians, Vancouver 1974, v. 1, Canadian Mathematical Congress, 235-242.

[13] Friedman, H., Robertson, N. and Seymour, P. [1987], The metamathematics of the graph minor theorem, in Logic and Combinatorics, S. Simpson ed., Contemporary Mathematics, American Mathematical Society, Providence.

[14] Hajek, P. and Pudlak, P. [1998], Metamathematics of First Order Arithmetic, 2nd printing, Perspectives in Mathematical Logic, Springer-Verlag, Berlin,

[15] Hirschfeldt, D. R., Lange, K. and Shore, R. A. [2012], The Homogeneous Model Theorem, in preparation.

[16] Hirschfeldt, D. R. and Shore, R. A. [2007], Combinatorial principles weaker than Ramsey’s theorem for pairs. Journal of Symbolic Logic 72, 171–206.

[17] Hirschfeldt, D. R., Shore, R. A. and Slaman, T. A. [2009], The atomic model theorem, Transactions of the American Mathematical Society 361, 5805-5837.

[18] Jockusch, Jr., C. G. and Soare, R. I. [1972], Π_{1}^{0} classes and degrees of theories. Transactions of the American Mathematical Society 173, 33–56.

[19] Jullien, P. [1960], Contribution à l’Étude des Types d’Ordre Dispersés, Ph.D. Thesis, Marseille.

[20] Keisler, H. J. [2006], Nonstandard Arithmetic and Reverse Mathematics, Bulletin of Symbolic Logic 12, 100-125.

[21] Keisler, H. J. [2011], Nonstandard Arithmetic and Recursive Comprehension, Annals of Pure and Applied Logic, to appear.

[22] Kirby, L. and Paris, J. [1978], Σ_{n} collection schemes in arithmetic, in Logic Colloquium ’77, A. Macintyre, L. Pacholski and J. Paris eds., Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 199-209.

[23] Kohlenbach, U. [2005], Higher order reverse mathematics in Reverse mathematics 2001, S. Simpson ed., 281–295, Lecture Notes in Logic 21, Association for Symbolic Logic and A. K. Peters, Wellesley MA.

[24] Kohlenbach, U. [2008], Applied Proof Theory: Proof Interpretations and their Use in Mathematics, Springer Monographs in Mathematics, Springer, Berlin.

[25] Lerman, M. [1972], On suborderings of the α-recursively enumerable α-degrees, Annals of Mathematical Logic 4, 369-392.

[26] Lovasz, L. and Plummer, M. D. [1986], Matching Theory, Annals of Discrete Mathematics 29, North-Holland, Amsterdam.

[27] Marcone, A. and Montalbán, A. [2009], On Fraïssé’s conjecture for linear orders of finite Hausdorff rank, Annals of Pure and Applied Logic 160, 355-367.

[28] Marcone, A. and Montalbán, A. [2011], The Veblen functions for computability theorists, to appear.

[29] Martin, D. A. [1974], Analysis ⊢ Δ_{4}^{0}-determinacy, circulated handwritten notes dated April 24, 1974.

[30] Martin, D. A. [1974a], Σ_{4}^{0}-determinacy, circulated handwritten notes dated March 20, 1974.

[31] Martin, D. A. [1975], Borel Determinacy, Annals of Mathematics 102, 363-371.

[32] Martin, D. A. [n.d.] Determinacy, circulated drafts, about 578 pp.

[33] MedSalem, M. O. and Tanaka, K. [2007], Δ_{3}^{0}-determinacy, comprehension and induction, Journal of Symbolic Logic 72, 452-462.

[34] MedSalem, M. O. and Tanaka, K. [2008], Weak determinacy and iterations of inductive definitions, in Computational Prospects of Infinity, Part II: Presented Talks, Chong, C., Feng, Q., Slaman, T. A., Woodin, W. H. and Yang, Y. eds., Lecture Note Series, Institute for Mathematical Sciences, National University of Singapore, World Scientific, Singapore, 333-353.

[35] Moldestad, J. [1977], Computations in Higher Types, Lecture Notes in Mathematics 574, Springer-Verlag, Berlin.

[36] Montalbán, A. [2006], Indecomposable linear orderings and hyperarithmetic analysis, Journal of Mathematical Logic 6, 89-120.

[37] Montalbán, A. and Shore, R. A. [2011], The limits of determinacy in second order arithmetic, to appear.

[38] Mummert, C. and Simpson, S. G. [2005], Reverse Mathematics and Π_{2}^{1} comprehension, Bulletin of Symbolic Logic 11, 526–533.

[39] Neeman, I. [2011], The strength of Jullien’s indecomposability theorem, to appear.

[40] Neeman, I. [2012], Necessary uses of Σ_{1}^{1} induction in a reversal, to appear.

[41] Nemoto, T., MedSalem, M. O. and Tanaka, K. [2007], Infinite games in the Cantor space and subsystems of second order arithmetic, Mathematical Logic Quarterly 53, 226-236.

[42] Odifreddi, P. [1989], [1999]. Classical Recursion Theory I, II, North-Holland, Elsevier, Amsterdam.

[43] Rathjen, M. and Weiermann, A. [2011], Reverse mathematics and well-ordering principles, to appear.

[44] Rogers, H. Jr. [1967], Theory of Recursive Functions and Effective Computability, McGraw-Hill, New York.

[45] Rosenstein, J. [1982], Linear Orderings, Academic Press, New York-London.

[46] Sacks, G. E. [1990], Higher recursion theory, Perspectives in Mathematical Logic, Springer-Verlag, Berlin.

[47] Schwichtenberg, H. and Wainer, S. [2011], Proofs and Computations, Perspectives in Logic, Association for Symbolic Logic and Cambridge University Press, New York, to appear.

[48] Shore, R. A. [1972], Priority Arguments in α-Recursion Theory, Ph.D. Thesis, M.I.T.

[49] Shore, R. A. [1993], On the strength of Fraïssé’s conjecture, in Logical Methods, J. N. C. Crossley, J. Remmel, R. A. Shore and M. Sweedler, eds., Birkhäuser, Boston, 782-813.

[50] Shore, R. A. [2007], Direct and local definitions of the Turing jump, Journal of Mathematical Logic 7, 229-262.

[51] Shore, R. A. [2011], Reverse mathematics, countable and uncountable: a computational approach, to appear.

[52] Shore, R. A. and Slaman, T. A. [1999], Defining the Turing jump, Mathematical Research Letters 6 (1999), 711-722.

[53] Slaman, T. A. [1991], Degree structures, in Proceedings of the International Congress of Mathematicians, Kyoto 1990, Springer-Verlag, Tokyo, 303-316.

[54] Slaman, T. A. [2008], Global properties of the Turing degrees and the Turing jump, in Computational Prospects of Infinity. Part I: Tutorials, C. T. Chong, Q, Feng, T. A. Slaman, W. H. Woodin, and Y. Yang, eds., Lecture Notes Series 14, Institute for Mathematical Sciences, National University of Singapore, World Scientific, 83-101.

[55] Simpson, S. G. [1985], Nonprovability of certain combinatorial properties of finite trees, in Harvey Friedman’s Research on the Foundations of Mathematics, L. A. Harrington, M. D. Morley, A. Scedrov and S. G. Simpson eds., Studies in Logic and the Foundations of Mathematics 117, North-Holland, Amsterdam, 87-118.

[56] Simpson, S. G. [1994], On the strength of König’s duality theorem for countable bipartite graphs, Journal of Symbolic Logic 59, 113–123.

[57] Simpson, S. G. [2009], Subsystems of Second Order Arithmetic 2^{nd} ed., Perspectives in Logic, Association for Symbolic Logic and Cambridge University Press, New York.

[58] Soare, R. I. [1987], Recursively Enumerable Sets and Degrees, Springer-Verlag, Berlin.

[59] Steel, J. [1976], Determinateness and Subsystems of Analysis, Ph.D. Thesis, University of California, Berkeley.

[60] Steel, J. [1978], Forcing with tagged trees, Annals of Mathematical Logic 15, 55-74.

[61] Tanaka, K. [1990], Weak axioms of determinacy and subsystems of analysis I: Δ_{2}^{0} games), Zeitschrift für mathematische Logik und Grundlagen der Mathmatik 36, 481-491.

[62] Tanaka, K. [1991], Weak axioms of determinacy and subsystems of analysis II (Σ_{2}^{0} games), Annals of Pure and Applied Logic 52, 181-193.

[63] Welch, P. [2009], Weak systems of determinacy and arithmetical quasi-inductive definitions, preprint.

[64] Yokoyama, K. [2007], Non-standard analysis in ACA_{0} and Riemann mapping theorem, Mathematical Logic Quarterly 53, 132-146.

[65] Yokoyama, K. [2009], Standard and non-standard analysis in second order arithmetic, D.S. thesis, Tohoku University available as Tohoku Mathematical Publications 34, 2009.