THE LIMITS OF DETERMINACY IN SECOND ORDER ARITHMETIC

ANTONIO MONTALBÁN AND RICHARD A. SHORE

Abstract. We establish the precise bounds for the amount of determinacy provable in second order arithmetic. We show that for every natural number n, second order arithmetic can prove that determinacy holds for Boolean combinations of n many Π_{3}^{0} classes, but it cannot prove that all finite Boolean combinations of Π_{3}^{0} classes are determined. More specifically, we prove that Π_{n+2}^{1}-CA _{0} ⊢ n-Π_{3}^{0}-DET, but that Δ_{n+2}^{1}-CA ⊬ n-Π_{3}^{0}-DET, where n-Π_{3}^{0} is the nth level in the difference hierarchy of Π_{3}^{0} classes.

We also show some conservativity results that imply that reversals for the theorems above are not possible. We prove that for every true Σ_{4}^{1} sentence T (as for instance n-Π_{3}^{0}-DET ) and every n ≥ 2, Δ_{n}^{1}-CA_{0} + T + Π_{∞}^{1}-TI ⊬ Π_{n}^{1}-CA_{0} and Π_{n−1}^{1}-CA_{0} + T + Π_{∞}^{1}-TI ⊬ Δ_{n}^{1}-CA_{0}.

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]. In that paper he worked primarily in the set theoretic settings of subsystems (and extensions) of ZFC. Actually, almost all of classical mathematics can be formalized in the language of second order arithmetic. This language consists of that of ordinary (first order) arithmetic and membership only for numbers in sets of numbers. It also has variables for, and quantification over, numbers and subsets of the natural numbers ℕ. (In terms of representing classical mathematics in this setting, we are restricting our attention to the countable case for algebraic and combinatorial results and, analogously, the separable situation for analytic or topological ones.) Moreover, the standard theorems of classical (countable) mathematics can be established in systems requiring only the basic axioms for arithmetic and set existence axioms just for subsets of ℕ. Realizing this, Friedman [1975] moved to the setting of second order arithmetic and subsystems of its full theory Z_{2} which assumes some basic axioms of arithmetic and the existence of each subset of ℕ defined by a formula of second order arithmetic. (See §2.3 for the precise definitions of our language, structures, axiom systems and their models.) Many researchers have since contributed to this endeavor but the major systematic developer and expositor since Friedman has been Stephen Simpson and the basic source for both background material and extensive results is his book [2009].

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. (Formal definitions of the subsystems of second order arithmetic used in this paper are in §2.3.)

Date: Submitted Jan 22nd, 2010.

Compiled: January 26, 2010.

Montalbán was partially supported by NSF grant DMS-0901169, and by the AMS centennial fellowship.

Shore was partially supported by NSF Grants DMS-0554855 and DMS-0852811, Grant 13408 from the John Templeton Foundation and as a visitor by the University of Chicago.

Indeed, relative to the weakest of them (RCA_{0}, 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 RCA_{0} + 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 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 (over a weak base theory) by proving the axioms of S from T (and RCA_{0}). In fact, for those theorems that are not true effectively (essentially the same as provable in RCA_{0}), the vast majority turn out to be equivalent in the sense of reverse mathematics to one of the two weakest of these systems (WKL_{0} or ACA_{0}). Only a handful are equivalent to one of the two stronger systems (ATR_{0} or Π_{1}^{1}-CA_{0}) and just a couple lie beyond them. (See Simpson [2009] for examples.) There is one now known (Mummert and Simpson [2005]) to be at the next level (Π_{2}^{1}-CA_{0}) and (as far as we know) none that are not known to be provable a bit beyond this level but still at one less than Π_{3}^{1}-CA_{0}.

In this paper we supply a natural hierarchy of theorems that require, respectively, each of the natural levels of set existence assumptions going from the previous known systems all the way up to full second order arithmetic. These theorems come from the realm in which the subject began, axioms of determinacy. The subject here is that of two person games with complete information. Our games (at least in this section) are played by two players I and II. They alternate playing natural numbers with I playing first to produce a play of the game which is a sequence x ∈ ω^{ω}. A game G_{A} is specified by a subset A of ω^{ω}. We say that I wins a play x of the game G_{A} specified by A if x ∈ A. Otherwise II wins that play. A strategy for I (II) is a function σ from strings p of even (odd) length into ω. We say that the game G_{A} is determined if there is a winning strategy for I or II in this game. (More details and terminology can be found in §2.1 where we switch from Baire space, ω^{ω}, to Cantor space, 2^{ω} to better match the standard setting for reverse mathematics and for other technical reasons. Basic references are Moschovakis [2009] and Kechris [1995].)

Now, in its full form, the Axiom of Determinacy says that all games G_{A} are determined. It has many surprising implications (e.g. all sets of reals are Lebesgue measurable) that contradict the Axiom of Choice. So instead, one considers restricted classes of games: If Γ is a class of sets A (of reals), then we say that Γ is determined if G_{A} is determined for every A ∈ Γ. We denote the assertion that Γ is determined by Γ determinacy or Γ-DET. One is then interested in determinacy for “simple” or easily definable classes Γ. One hopes that, for such Γ, determinacy will be provable (in some system of set theory including the axiom of choice) and that many of the consequences of the full axiom will then follow for sets in Γ. This has, indeed, turned out to be the case and a remarkably rich and extensive theory with applications in measure theory, descriptive set theory, harmonic analysis, ergodic theory, dynamical systems and other areas has been developed. (In addition to the basic texts mentioned above, one might refer, for example, to Kechris and Becker [1996], Kechris and Louveau [1987], Kechris and Miller [2004] and Foreman [2000] for sample applications.) A crowning achievement of this theory has been the calibration of the higher levels of determinacy for Γ in the projective hierarchy of sets of reals that begins with the analytic sets and progresses by complementation and projection. Here work of Martin, Steel and Woodin (Martin and Steel [1989], Woodin [1988]) has precisely characterized the large cardinal assumptions needed to prove each level of determinacy in the projective hierarchy (and beyond).

We are here concerned with lower levels of determinacy. Friedman’s first foray [1971] into the area that grew into reverse mathematics dealt with these issues. He famously proved that Borel determinacy is not provable in ZFC without the power set axiom. Indeed, he showed that one needed ℵ_{1} many iterations of the power set to prove it. Martin [1975], then showed that Borel determinacy is provable in ZFC and provided a level by level analysis of 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 the realm of what is now called reverse mathematics, Friedman [1971] also showed that Σ_{5}^{0} determinacy (i.e. for G_{δσδσ} sets or see §2.2) is not provable in full second order arithmetic. Martin [1974a], [n.d., Ch. I] improved this to Σ_{4}^{0} determinacy (i.e. F_{σδσ} sets). He also presented [1974] [n.d., Ch. 1] a proof of Δ_{4}^{0} determinacy (sets that are both F_{σδσ} and G_{δσδ}) 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 left 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} (open) 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} (intersections of open and closed sets) determinacy. Moving on to Σ_{2}^{0} (F_{σ}) determinacy, Tanaka [1991] showed that it was equivalent to an unusual system based on closure under monotonic Σ_{1}^{1} definitions. At the level of Δ_{3}^{0} (sets in both F_{σδ} and G_{δσ}) determinacy, MedSalem and Tanaka [2007] showed that each of Π_{2}^{1}-CA_{0} + Π_{3}^{1}-TI_{0} (an axiom system of transfinite induction) and Δ_{3}^{1}-CA_{0} + Σ_{3}^{1}-IND_{0} (induction for Σ_{3}^{1} formulas) prove Δ_{3}^{0}-DET but Δ_{3}^{1}-CA_{0} alone does not. They improve these results in [2008] by showing that Δ_{3}^{0}-DET 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} (F_{δσ}) determinacy but even that there is a β-model (Definition 2.9) of Δ_{3}^{1}-CA_{0} + Π_{3}^{0}- DET. 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}-DET. 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], 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. We answer that question in this paper by analyzing the strength of determinacy for the finite levels of the difference hierarchy on Π_{3}^{0} (F_{σδ}) sets, the m-Π_{3}^{0} sets. (As defined in §2.2, these give a natural hierarchy for the finite Boolean combinations of Π_{3}^{0} sets.)

In the positive direction (§4), we carefully present 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. (It is a classical theorem of Kuratowski [1958] that extending the hierarchy into the transfinite to level ℵ_{1} gives all the Δ_{4}^{0} sets. Martin’s proof proceeds by an induction encompassing all these levels.) This establishes an upper bound for the provability of the m-Π_{3}^{0} sets in Z_{2}.

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

In the other direction, we prove that this upper bound is sharp in terms of the standard subsystems of second order arithmetic.

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

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

Note that by Theorem 1.1, any model of second order arithmetic in which the natural numbers are the standard ones (i.e. ℕ) does satisfy ω-Π_{3}^{0}-DET and so the counterexample for its failure to be a theorem of Z_{2} must be nonstandard. Of course, it can be constructed by a compactness argument or, equivalently, as an ultraproduct of the L_{α_{n}} defined below. 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.

We can reformulate this limitative result in the setting of set theory by noting the following conservation result.

Proposition 1.4. ZFC^{−} (ZFC with collection but without the power set axiom) and even with a definable well ordering of the universe assumed as well, is a Π_{4}^{1} conservative extension of Z_{2}.

Proof: (Sketch) This fact should be “well known” and certainly follows from the extensive analysis of the relations between models of (subsystems of) second order arithmetic and those of the form L(X) in Simpson [2009, VII]. Basically, given a model M of Z_{2} and an X a set in M, one defines an interpretation L^{M}(X) (defined over the well orderings of M) of L(X) in M and checks that it is a model of ZFC^{−}. This is detailed work but fairly straight forward for Z_{2}. Much of the work in Simpson [2009 VII.7] (whose ideas are described there as “probably well known but we have been unable to find bibliographic references for them”) is devoted to showing that the facts required for the interpretation to satisfy the basic axioms of set theory can be derived in ATR_{0} and the Shoenfield absoluteness theorem (VII.4.14) in Π_{1}^{1}-CA_{0}. As a guide we note that the basic translations and interpretations between second order arithmetic and a simple set theory are in VII.3. The relations with L and L(X) and their basic properties are in VII.4. The material needed to verify the comprehension axioms is in VII.5 with Theorem VII.5.9(10) and the proof of its Corollary VII.5.11 being the closest to what is needed here. The material for replacement is in VII.6 with Lemma VII.6.15 and Theorem VII.6.16 being the closest to what is needed here. Finally, as L^{M}(X) is a model of V = L(X), L^{M}(X) satisfies even global choice, i.e. there is a definable well ordering of the universe. Thus L^{M}(X) is a model of ZFC^{−} (and global definable choice).

Now if T = ∀X∃Y ∀Z∃W φ is Π_{4}^{1} and false in some M ⊨ Z_{2}, we take X to be the counterexample and consider L^{M}(X) and any Y ∈ L^{M}(X). By assumption, M ⊨ ∃Z∀W ¬φ(X, Y) and so by Shoenfield absoluteness, L^{M}(X) ⊨ ∃Z∀W ¬φ(X, Y). Thus T fails in L^{M}(X) for the desired contradiction. □

It is worth pointing our that Π_{4}^{1} is as far as conservation results can go for ZFC^{−} over Z_{2}. As Simpson [2009, VII.6.3] points out, Feferman and Levy have produced a model of Z_{2} in which a Σ_{3}^{1}-AC axiom fails. Now each Σ_{3}^{1}-AC axiom is clearly a Σ_{5}^{1} sentence and a theorem of ZFC^{−}. Now if T = ∀X∃Y ∀Z∃W φ is Π_{4}^{1} and false in some M ⊨ Z_{2}, we take X to be the counterexample and consider L^{M}(X) and any Y ∈ L^{M}(X). By assumption, M ⊨ ∃Z∀W ¬φ(X, Y) and so by Shoenfield absoluteness, L^{M}(X) ⊨ ∃Z∀W ¬φ(X, Y). Thus T fails in L^{M}(X) which is a model of ZFC^{−}.

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

In fact, our counterexamples that establish Theorem 1.2 (the games with no strategy in L_{α_{n}} as described below) are all given by effective versions of the m-Π_{3}^{0} sets where the initial Π_{3}^{0} sets are effectively defined, i.e. given by recursive unions and intersections starting with closed sets that are “lightfaced”, i.e. defined by Π_{1}^{0} formulas of first order arithmetic without real (second order) parameters. (See the remarks in the last paragraph of §2.2. We use notations such as Π_{1}^{0} and Π_{3}^{0} to denote these “lightfaced’ versions of the Borel classes.) 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 1.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 1.1 and 1.2 along with Corollary 1.3 produce a sequence of Π_{3}^{1} formulas ψ(n) that have the same proof theoretic properties while eliminating the references to syntax and recursion theory present in the φ of Theorem 1.6. They simply state the purely mathematical propositions that all n-Π_{3}^{0} games are determined.

The plan for the first few sections of this paper is as follows. We provide basic definitions and notations about games and determinacy, hierarchies of sets and formulas and subsystems of second order arithmetic in §2. Basic facts about Gödel’s constructible universe L not found in the standard texts are given in §3. The proof of Theorem 1.1 is in §4.

To prove Theorem 1.2, we will work in set theory or more specifically in fragments of ZFC + V=L instead of directly in second order arithmetic. We can do this as Simpson [2009, VII] shows how one can move back and forth between systems of second order arithmetic and subsystems of ZFC + V=L(X), once one has ATR_{0} (or at times Π_{1}^{1}-CA_{0}) as a base theory. (Note also that, as mentioned above, these systems are equivalent to even weaker forms of determinacy than any we consider and so are provable even in Π_{3}^{0}-DET.)

Let α_{n} denote the first n-admissible ordinal, and ℝ the set of subsets of ω. (See §3 for the basic definitions.) By Lemma 3.2 and Simpson [2009, VII.5.3], ℝ∩L_{α_{n}} is a β-model of Δ_{n+1}^{1}- CA for n ≥ 2. Let T h_{α_{n}} denote the true theory of L_{α_{n}}. We think of T h_{α_{n}} as a subset of ω, or as the characteristic function (in 2^{ω}) for the set of indices of sentences of set theory (without parameters) true in L_{α_{n}}. As every element of L_{α_{n}} is definable in L_{α_{n}} without parameters (Lemma 3.6), the Gödel-Tarski undefinability of truth (a simple diagonal argument at this point) says that T h_{α_{n}} ∉ L_{α_{n}}. Our plan is to show that, for n ≥ 2, (n-1)-Π_{3}^{0}-DET does not hold in L_{α_{n}} by showing that, if it did, T h_{α_{n}} would be a member of L_{α_{n}}.

As the L_{α_{n}} are β-models, Theorem 1.2 can be immediately improved in various ways by including in the base theory any axioms true in all β-models, as for example:

Theorem 1.7. For every n ≥ 1, Σ_{n+2}^{1}-DC + Π_{∞}^{1}-TI does not prove n-Π_{3}^{0}-DET.

Proof: Every β-model is obviously a model of Π_{∞}^{1}-TI and, as L_{α_{n+1}} ⊨ Δ_{n+1}^{1}-CA, it also satisfies Σ_{n+2}^{1}-DC (which is stronger than Δ_{n+1}^{1}-CA) by Simpson [2009, VII.6.18]. □

The key result needed to prove Theorem 1.2 is the following.

Lemma 1.8. For every n ≥ 2, there is a game G that is (n-1)-Π_{3}^{0}, such that, if we interpret the play of each player as the characteristic function of a set of sentences in the language of set theory, then

(1) If I plays T h_{α_{n}}, he wins.

(2) If I does not play T h_{α_{n}} but II does, then II wins.

We prove this Lemma in §5 but we now show how it implies our main result, Theorem 1.2. Proof of Theorem 1.2: As we mentioned above, ℝ ∩ L_{α_{n}} is a β-model of Δ_{n+1}^{1}-CA and so it suffices to show that L_{α_{n}} ⊭ (n-1)-Π_{3}^{0}-DET. Let G be as in the Lemma; and suppose it is determined in L_{α_{n}}. Player II cannot have a winning strategy for G in L_{α_{n}} because if II has a winning strategy σ in L_{α_{n}}, σ would also be a winning strategy in V as ℝ ∩ L_{α_{n}} is a β-model (and σ being a winning stratgey for G is a Π_{1}^{1} property). But, I has a winning strategy for G in V by clause (1) of the Lemma. So, I must have a winning strategy σ for G in L_{α_{n}}. Again, as ℝ ∩ L_{α_{n}} is a β-model, σ is truly a winning strategy for I (in V). We claim that if II plays so as to simply copy I’s moves, then σ has to play T h_{α_{n}}. If not, then at some first point I plays a bit that is different from T h_{α_{n}}. At this point II could stop copying I and just continue playing T h_{α_{n}} and he would win (by clause (2) of the Lemma). Thus σ would not be a truly winning strategy for I (in V). We conclude that σ computes T h_{α_{n}} as the sequence of I’s plays against II’s copying his moves and so T h_{α_{n}} ∈ L_{α_{n}} for the desired contradiction. □

In the spirit of reverse mathematics one should now ask for reversals showing that m-Π_{3}^{0}-DET implies Π_{m+2}^{1}-CA_{0} or something along these lines. Nothing like this is, however, possible. MedSalem and Tanaka [2007] have shown that even full Borel (Δ_{1}^{1}) determinacy does not imply even Δ_{2}^{1}-CA_{0}. (Indeed they also show that it does not imply either induction for Σ_{3}^{1} formulas or Π_{2}^{1}-TI_{0}.) Their proofs proceed via constructing countably coded β-models and appealing to the second Gödel incompleteness theorem.

In §6, we provide a very different approach that applies to any true (or even consistent with ZFC) Σ_{4}^{1} sentence T and shows that no such sentence can imply Δ_{2}^{1}-CA_{0} even for βmodels. The counterexamples are all initial segments of L(X) (for X a witness to the Σ_{4}^{1} sentence). We also show that for any such T and n ≥ 2, Δ_{n}^{1}-CA_{0} + T + Π_{∞}^{1}-TI ⊬ Π_{n}^{1}-CA_{0} and Π_{n}^{1}-CA_{0} + T + Π_{∞}^{1}-TI ⊬ Δ_{n+1}^{1}-CA_{0} (even for β-models). These results are also suitably generalized to Σ_{m}^{1} theorems of ZFC in an optimal way. As Borel and m-Π_{3}^{0} determinacy are Π_{3}^{1} theorems of ZFC, these general conservation results apply and we have the following results:

Borel-DET + Π_{∞}^{1}-TI ⊬ Δ_{2}^{1}-CA_{0}.

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

Thus, by Theorem 1.1, for n ≥ 0, n-Π_{3}^{0}-DET is a consequence of Π_{n+2}^{1}-CA_{0} incomparable (in terms of provability) with Δ_{k+2}^{1}-CA_{0} for all k ≤ n while Δ_{n+2}^{1}-CA_{0} + n-Π_{3}^{0}-DET is a system strictly between Δ_{n+2}^{1}-CA_{0} and Π_{n+2}^{1}-CA_{0} given by a mathematically natural proposition.

2. Definitions and Notations

2.1. Games and Determinacy. From now on, our basic playing field is not Baire space but Cantor space, 2^{ω}, the set of infinite (length ω) binary sequences (reals), x which we identify with the set X ⊆ ℕ with its characteristic function x. Our games are played by two players I and II. They alternate playing 0 or 1 with I playing first to produce a play of the game which is a real x. A game G_{A} is specified by a subset A of 2^{ω}. We say that I wins a play x of the game G_{A} specified by A if x ∈ A. Otherwise II wins that play. A strategy for I (II) is a function σ from binary strings p of even (odd) length into {0, 1}. The intuition here is that at any finite string of even (odd) length, a position in the game at which it is I’s (II’s) turn to play, the strategy σ instructs I (II) to play σ(p). We say that a position q (play x) is consistent with σ if, for every p ⊂ q (x) of even (odd) length, σˆ σ(p) ⊆ q (x). (We use ˆ for concatenation of strings and confuse a number i with the string ⟨i⟩.) The stratgey σ is a winning strategy for I (II) in the game G_{A} if every play consistent with σ is in A (Ā). (We use Ā for 2^{ω}\A, the complement of A in Cantor space.)

We say that the game G_{A} is determined if there is a winning strategy for I or II in this game. If Γ is a class of sets A (of reals), then we say that Γ is determined if G_{A} is determined for every A ∈ Γ. We denote the assertion that Γ is determined by Γdeterminacy or Γ-DET.

Note that easy codings translate between games on Baire space to ones on Cantor space. Given an A ⊆ ω^{ω} we code it by Â ⊆ 2^{ω} with elements precisely the ones of the form f̂ = 0^{f(0)}10^{f(1)}10^{f(2)} … 10^{f(n)}1 … where we use 0^{k} to denote the sequence consisting of k many 0’s. A stratgey for G_{A} can be gotten effectively from one for Ã = {x ∈ 2^{ω}|[∃n∀m > n(x(2m + 1) = 0] or [∀n∃m > n(x(2m) = 1) & for the f such that x = f̂, f ∈ A]}. In the other direction, given an A ⊆ 2^{ω} a strategy for G_{A} can be found effectively from one for GǍ where Ǎ = {f ∈ ω^{ω}|∃n(f(2n + 1) ∉ {0, 1} or f ∈ A}. Thus if Γ is rich enough to be closed under these operations, it makes no difference whether we play in Baire space or Cantor space. It is clear that once Γ is at least at the level of Π_{3}^{0} (F_{σδ}) (or even Δ_{3}^{0}) Γ determinacy in one space is equivalent to it in the other, and in this paper we consider only classes from Π_{3}^{0} and above. For the record, we note that there are significant differences at levels below Δ_{3}^{0}. In contrast to the standard low level results for Baire space mentioned in §1, Nemoto, MedSalem and Tanaka [2007] show that in Cantor space Δ_{1}^{0}-DET is equivalent (over RCA_{0}) to each of Σ_{1}^{0}-DET and WKL_{0}. ACA_{0} is equivalent to (Σ_{2}^{0} ∧Π_{2}^{0})-DET. Δ_{2}^{0}-DET is equivalent to each of Σ_{2}^{0}-DET and ATR_{0} while, as indicated above, Δ_{3}^{0}-DET is equivalent to the same level of determinacy in Baire space.

As usual, we let Γ̆ = {Ā|A ∈ Γ}. Idiosyncratically, and only for the purposes of the next Lemma, we let A^{∗} = {0ˆ x|x ∈ A} ∪ {1ˆ x|x ∈ A} and Γ^{∗} = {A^{∗}|A ∈ Γ}.

Lemma 2.1. (RCA_{0}) If Γ^{∗} ⊆ Γ and Γ is determined then so is Γ̆. Proof: A winning stratgey σ for I (II) in G_{A^{∗}} is easily converted into one τ for II (I) in GĀ: τ(p) = σ(τ(p) = σ(∅)ˆ p) (σ(0ˆ p)). □

This is as much as we need about determinacy for our proof of its failure for various Γ in specified models of Δ_{n+2}^{1}-CA_{0} in §5. To show that determinacy holds for these Γ in Π_{n+2}^{1}-CA_{0} in §4, we need to generalize these notions a bit.

We now allow games to be played on arbitrary binary trees T. The idea here is that we replace 2^{ω} by [T], the set of paths through T, {x|∀n(x ↾ n ∈ T)}. (So the basic notion takes T to be 2^{<ω}, the tree of all finite binary sequences.) A (binary) tree is a set of finite binary sequences closed under initial segments and with no dead ends, i.e. ∀p ∈ T (pˆ 0 ∈ T or pˆ 1 ∈ T). If T is a tree and p ∈ T then T_{p} is the subtree of all q ∈ T comparable with p, T_{p} = {q ∈ T |q ⊆ p or p ⊆ q}. (A subtree of a tree T is a subset T which is also a tree.) A play (real) x is one in the game on T if x ∈ [T]. A game G(A, T) is now specified by an A ⊆ [T]. The other notions defined above are generalized accordingly with the positions restricted to T and the plays to [T]. A quasistrategy for I ( II) in G(A, T) is a subtree S of T such that if p ∈ S is of odd (even) length then the immediate successors in S are precisely the same as the ones in T. Thus a strategy for I (II) can be viewed as a quasistrategy in which each p ∈ S of even (odd) length has precisely one immediate successor in S. A position p or play x in G(A, T) being consistent with S now just means that p ∈ S or x ∈ [S]. We say that S is a winning quasistrategy for I ( II) if every x consistent with S is in A (Ā). If I (II) does not have a winning strategy in G(A, T) then we define II’s (I’s) nonlosing quasistrategy W in this game to be the set of all p ∈ T such that I (II) has no winning strategy in G(A, T_{p}). If this set exists (e.g. we have enough comprehension as when A is arithmetic and we have at least Π_{2}^{1}-CA_{0}), it is easily seen to be a quasistrategy for II (I) by induction on the length of p ∈ W.

2.2. Classes and Hierarchies. We have to deal with several classes and hierarchies of both formulas and sets that have standard but at times conflicting (or overlapping) designations. We try to use as single unambiguous system through out the paper while choosing notations whose meaning in specific contexts should be evident to readers familiar with work in the appropriate areas.

We begin with formulas. Here we have formulas of both second order arithmetic and set theory. We use Σ_{n}^{0}, Π_{n}^{0}, Σ_{n}^{1} and Π_{n}^{1} in the usual way for the formulas of second order arithmetic with the understanding (typical in reverse mathematics) that the second order quantifiers range over subsets of ℕ (or equivalently reals) and the formulas may include free set variables (i.e. ones over reals) at no cost to the quantifier complexity. For formulas of set theory, we use the notations Σ_{n} and Π_{n} in the usual way with the understanding that at the bottom level we allow bounded quantifiers in the Σ_{0} = Π_{0} formulas and may also include free variables.

We will be concerned with sets of reals and not sets of numbers and so define the relevant classes (of sets) only that setting. From the set theoretic point of view we have the usual topologically based Borel hierarchy beginning with the open or closed sets and then progressing by alternating applications of countable intersections and unions. Recursion theoretically, the open (closed) sets are those defined by Σ_{1}^{0} (Π_{1}^{0}) formulas where the free set variables other than the one representing the reals in the set being defined are replaced by specific real parameters. (It is worth noting that the closed sets are precisely those of the form [T] for some tree T.) One then moves up the Borel hierarchy as usual. We are only concerned with the first few levels and, in particular, the Π_{3}^{0} sets are those A of the form ∩A_{k} where the A_{k} ∈ Σ_{2}^{0}, i.e. they are of the form A_{k} = ∪A_{k,j} where the A_{k,j} are Π_{1}^{0}, i.e. closed, sets. They are also the classes of sets of reals defined by formulas at the indicated level of the arithmetic hierarchy with real parameters.

The sets that we will be analyzing from the viewpoint of their determinacy are the finite Boolean combinations of Π_{3}^{0} sets. These are typically laid out in the difference hierarchy of the m-Π_{3}^{0} sets.

Definition 2.2. A set A (of reals) is m-Π_{3}^{0} if there are Π_{3}^{0} sets A_{0}, A_{1}, …, A_{m−1}, A_{m} = ∅ such that

x ∈ A ⇔ the least i such that x ∉ A_{i} is odd.

We say that the sequence ⟨A_{i}|i ≤ m⟩ represents A (as an m-Π_{3}^{0} set).

Remark 2.3. Without loss of generality, we may assume that the A_{i} in Definition 2.2 are nested downward, i.e. A_{i} ⊇ A_{i+1} by simply replacing A_{i} by ∩_{j≤i}A_{j}. We assume that any given representation (as an m-Π_{3}^{0} set) is of this form.

This hierarchy is called the difference hierarchy since the sets at level m are generated by taking unions of differences of Π_{3}^{0} sets. More specifically, they are Boolean combinations of Π_{3}^{0} sets of the form (A_{0}\A_{1}) ∪ (A_{2}\A_{3}) … ∪ (A_{m−2}\A_{m−1}) if m is even and (A_{0}\A_{1}) ∪ (A_{2}\A_{3}) …∪(A_{m−3}\A_{m−2})∪A_{m−1} if m is odd. (We write A\B for A∩B̄.) Of course, when m is even, A_{m} = ∅ and so A_{m−1} = A_{m−1}\A_{m} and we can view it as being of the first form as well. The converse holds as well, i.e. every set A of the form (A_{0}\A_{1})∪(A_{2}\A_{3}) …∪(A_{m−2}\A_{m−1}) is m-Π_{3}^{0} for m even and each of the form (A_{0}\A_{1}) ∪ (A_{2}\A_{3}) … ∪ A_{m−1} is m-Π_{3}^{0} for m odd. One can see this as analogous to the difference hierarchy on r.e. sets.

It is easy to see that all finite Boolean combinations of Π_{3}^{0} sets are m-Π_{3}^{0}. The sets that are a union of differences of Π_{3}^{0} sets are clearly closed under union and include the Π_{3}^{0} sets. On the other hand, if A is represented by ⟨A_{i}|i ≤ m⟩, then Ā is represented by ⟨2^{ω}, A_{i}|i ≤ m⟩. Thus ∪_{m}m-Π_{3}^{0} contains the Π_{3}^{0} sets and is closed under union and complementation.

An advantage of Definition 2.2 as a hierarchy on the finite Boolean combinations of Π_{3}^{0} sets is that it can immediately be extended into the transfinite simply by allowing sequences A_{i} for i < α with the understanding that limit ordinals are even. It is a classical theorem of Kuratowski [1958] that as α ranges over the countable ordinals these sets are precisely the Δ_{4}^{0} ones, i.e. those that are both Σ_{4}^{0} and Π_{4}^{0}. (See MedSalem and Tanaka [2007] for a proof in ACA_{0}.)

In §4, we prove, in Π_{m+2}^{1}-CA_{0}, that all m-Π_{3}^{0} sets are determined for each m ∈ ℕ. Our negative results in §5, however, use a different, dual representation of the finite Boolean combinations of Π_{3}^{0} sets.

Definition 2.4. A set A ⊆ 2^{ω} is Π_{3,n}^{0} if there exist Π_{3}^{0} sets A_{0}, ..., A_{n} such that A_{n} = 2^{ω} and

x ∈ A ⟺ the least i such that x ∈ A_{i} is even.

We say that the sequence ⟨A_{i}|i ≤ m⟩ represents A (as a Π_{3,n}^{0} set).

Remark 2.5. Note that without loss of generally we may assume that the A_{i} in Definition 2.4 are nested upward, i.e. A_{i} ⊆ A_{i+1} by simply replacing A_{i} by ∪_{j≥i}A_{j}. We assume that any given representation (as a Π_{3,n}^{0} set) is of this form.

This formulation does not extend into the transfinite to capture the Δ_{4}^{0} sets as did that of the m-Π_{3}^{0} sets. Indeed, it is easy to see that at level ω one gets all the Σ_{4}^{0} sets represented by sequences ⟨A_{i}|i < ω⟩ of Π_{3}^{0} sets. (The issue here is that the Π_{3}^{0} sets are closed under countable intersections and so {x|∀i < β(x ∈ A_{i})} is still Π_{3}^{0} while they are not closed under countable (as opposed to finite) unions and so {x|∃i < β(x ∈ A_{i})} is only Σ_{4}^{0}. Thus Definition 2.4 is suited to a difference hierarchy built on the Σ_{3}^{0} rather than the Π_{3}^{0} sets. Nonetheless, at the finite levels of the two hierarchies are closely enough related to allow us to use both in our calculations of the limits of determinacy provable in fragments of second order arithmetic.

Lemma 2.6. (RCA_{0}) Π_{3,2n+1}^{0} = (2n + 1)-Π_{3}^{0} and Π̆_{3,2n}^{0} = (2n)-Π_{3}^{0}.

Proof: Consider any sequence A_{0} ⊆ A_{1} ⊆ ⋯ ⊆ A_{m−1} of Π_{3}^{0} sets. Let A be the Π_{3,m}^{0} set represented by ⟨A_{0}, …, A_{m−1}, 2^{ω}⟩. Let B be the m-Π_{3}^{0} set represented by ⟨A_{m−1}, …, A_{1}, ∅⟩. We claim that A = B when m is odd and A = B̄ when m is even. This would prove the lemma as A or B could be any m-Π_{3}^{0} or Π_{3,m}^{0} set.

Consider x ∈ 2^{ω}. Let i_{x} be the least i such that x ∈ A_{i}. So, x ∈ A if and only if i_{x} is even. Let j_{x} be the least j such that x ∉ A_{m−1−j}. So, x ∈ B if and only if j_{x} is odd. Since i_{x} − 1 is the greatest i such that x ∉ A_{i}, we have that m − 1 − j_{x} = i_{x} − 1. It then follows that i_{x} and j_{x} have the same parity if m is even and different parities if m is odd. Hence x ∈ A ⟺ x ∉ B if m is even and x ∈ A ⟺ x ∈ B if m is odd. □

Corollary 2.7. For each m ≥ 1, RCA_{0} ⊢ m-Π_{3}^{0}-DET↔ Π_{3,m}^{0}-DET.

Proof: It is immediate that (Π_{1}^{0})^{∗} ⊆ Π_{1}^{0} and so the same property clearly holds for Π_{3}^{0} as it is generated from Π_{1}^{0} by unions and intersections which preserves the desired closure property. The required closure property then holds for m-Π_{3}^{0}, Π_{3,m}^{0}, m-Π̆_{3}^{0} and Π̆_{3,m}^{0} (simply replace each A_{i} in the representation by A_{i}^{∗}). Thus the corollary holds by Lemmas 2.6 and 2.1. □

We also point out that the classes we have considered all have “light faced” versions, i.e. ones defined by the same classes of formulas but without any reals as parameters. In terms of our definitions, the light faced (or recursive) closed sets are those of the form [T] for T a recursive tree. The class of these sets is denoted by Π_{1}^{0}. The light faced class Π_{3}^{0} is defined from Π_{1}^{0} as in the boldface version except that now the closed sets A_{k,j} required to define A ∈ Π_{3}^{0} must be uniformly recursive, i.e. there is a set of uniformly recursive trees T_{k,j} (i. e. the relation p ∈ T_{k,j} is a recursive one of the triple ⟨p, k, j⟩) such that A_{k,j} = [T_{k,j}]. The light faced m-Π_{3}^{0} and Π_{3,n}^{0} sets are then defined from the Π_{3}^{0} sets exactly as in the bold faced versions in Definitions 2.2 and 2.4, respectively. Of course, each of these light faced classes are contained in the corresponding bold face class. Our negative results about the failure of determinacy in various subsystems of second order arithmetic as exhibited in the particular models of §5 all provide light face counterexamples.

2.3. Systems of Reverse Mathematics. We first briefly review the five standard systems of reverse mathematics. For the analysis of even the lowest levels of determinacy one begins near the top of this list and moves well beyond. Details, general background, and results, as well as many examples of reversals, can be found in Simpson [2009], the standard text on reverse mathematics. Each of the systems is given in 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 “numbers” of M) over which the first order quantifiers and variables of our language range; S ⊆ 2^{M} is the collection of subsets of “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.

Each subsystem of second order arithmetic that we consider contains the standard basic axioms for +, ·, and < (which say that ℕ is an ordered semiring). In addition, they all include a 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). We call the system consisting of I_{0} and the basic axioms of ordered semirings P_{0}. All five

standard systems are defined by adding various types of set existence axioms to P_{0}.

(RCA_{0}) Recursive Comprehension Axioms: This is a system just strong enough to prove the existence of the computable sets. In addition to P_{0} 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 φ.

The next system says that every infinite binary tree has an infinite path.

(WKL_{0}) Weak König’s Lemma: This system consists of RCA_{0} plus the statement that every infinite subtree of 2^{<ω} has an infinite path.

We next move up to arithmetic comprehension.

(ACA_{0}) Arithmetic Comprehension Axioms: This system consists of RCA_{0} plus the axioms ∃X ∀n (n ∈ X ↔ φ(n)) for every arithmetic formula (i.e. Σ_{n}^{0} for some n) φ in which X is not free.

The next system says that arithmetic comprehension can be iterated along any countable well order. As noted in §1, it is equivalent to Σ_{1}^{0}-determinacy in Baire space (Steel [1976]).

(ATR_{0}) Arithmetical Transfinite Recursion: This system consists of RCA_{0} plus the following axiom. 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}.

The systems that we actually need climb up to full second order arithmetic, Z_{2}, (i.e. comprehension for all formulas). They are characterized by the syntactic level of the second order formulas for which they include comprehension axioms.

(Π_{n}^{1}-CA_{0}) These systems consists of RCA_{0} plus the Π_{n}^{1} comprehension axioms: ∃X ∀k (k ∈ X ↔ φ(k)) for every Π_{n}^{1} formula φ in which X is not free.

The first of these, Π_{1}^{1}-CA_{0}, is the last of the five standard systems. As noted in §1, it is equivalent to (Σ_{1}^{0} ∧ Π_{1}^{0})-determinacy in Baire space (Tanaka [1990]). If one assumes Π_{n}^{1}-CA_{0} for every n then one has full second order arithmetic.

(Π_{∞}^{1}-CA_{0}) or (Z_{2}) This system consists of Π_{n}^{1}-CA_{0} for every n.

We also need the intermediate Δ_{n}^{1} classes and corresponding axioms.

(Δ_{n}^{1}-CA_{0}) Δ_{n}^{1} Comprehension Axioms: ∀k (ψ(k) ↔ ¬φ(k)) → ∃X ∀k (k ∈ X ↔ φ(k)) for every Σ_{n}^{1} formulas φ and ψ in which X is not free.

The other set existence axioms that play a role in our analysis are various versions of the axiom of choice in the setting of second order arithmetic.

(Σ_{n}^{1}-AC_{0}) This system consists of ACA_{0} plus the Σ_{n}^{1} choice axioms ∀n∃Y φ(n, Y) → ∃Z∀nφ(n, (Z)_{n}) for every Σ_{n}^{1} formula φ and where (Z)_{n} = {i| ⟨i, n⟩ ∈ Z}.

(Σ_{n}^{1}-DC_{0}) This system consists of ACA_{0} plus the Σ_{n}^{1} dependent choice axioms ∀n∀X∃Y φ(n, X, Y) → ∃Zφ(n, (Z)^{n}, (Z)_{n}) for every Σ_{n}^{1} formula φ and where (Z)^{n} = {⟨i, m⟩ | ⟨i, m⟩ ∈ Z & m < n}

(Strong Σ_{n}^{1}-DC_{0}) This system consists of ACA_{0} plus the strong Σ_{n}^{1} dependent choice axioms ∃Z∀n∀Y (φ(n, (Z)^{n}, Y) → φ(n, (Z)^{n}, (Z)_{n}) for every Σ_{n}^{1} formula φ.

See Simpson [2009, VII.6] for the relations among these choice principles and various comprehension axioms.

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}.

Definition 2.8. If M is a structure for second order arithmetic and its first order part M is ℕ then M is an ω-model.

Obviously if an ω-model M is a model of one of the systems above, such as Π_{n}^{1}-CA_{0}, then it is also a model of the analogous system, such as Π_{n}^{1}-CA.

Restricted versions of the full induction axioms are designated as follows:

(Σ_{n}^{1}-IND) (φ(0) ∧ ∀n (φ(n) → φ(n + 1)) → ∀n (φ(n)) for every Σ_{n}^{1} formula φ of second order arithmetic.

Definition 2.9. An ω-model M is a β-model if, for every Σ_{1}^{1} sentence φ with parameters in M, φ ⇔ M ⊨ φ.

In particular, if M is a β-model then any well ordering in M, i.e. a linear ordering in S with no infinite descending chain in S, is actually a well ordering (where S is the second order part of M). There are also some induction axioms and systems (even stronger than Σ_{n}^{1}-IND_{0}) for transfinite procedures that serve as proof theoretical approximations to being a β-model.

(Π_{∞}^{1}-TI_{0}) This system consists of ACA_{0} plus all the transfinite induction axioms ∀X(X is a well-ordering & ∀j(∀i(i <_{X} j → ψ(i)) → ψ(j)) → ∀jψ(j), where by “X is a well-ordering” we mean that the relation <_{X}= {⟨i.j⟩ | ⟨i, j⟩ ∈ X} given by the pairs of numbers in X is a well ordering, i.e. has no infinite descending chains, and ψ is any formula of second order arithmetic in which X is not free.

Obviously, every β-model satisfies Π_{∞}^{1}-TI_{0}. The systems (Π_{n}^{1}-TI_{0}) are defined analogously with ψ restricted to Π_{n}^{1} formulas.

3. Facts about L

We assume a familiarity with the basic facts about L and Σ_{1} admissible sets of the form L_{α} as can be found, for example, in Devlin [1984, I-II] or Barwise [1975, I-II]. Generalizing from 1 to n we say that an L_{α} is Σ_{n} admissible if it satisfies Σ_{n} bounding: For any δ < α and any Π_{n−1}/L_{α} formula φ(x, y), if L_{α} ⊨ ∀γ < δ∃yφ(γ, y), then there is a λ < α such that L_{α} ⊨ ∀γ < δ∃y ∈ L_{λ}φ(γ, y). This property is equivalent (for initial segments of L) to the requirements that the set satisfy (in addition to the standard (KP) axioms of admissibility) Δ_{n−1} collection and Σ_{n−1} separation (also called comprehension). It is also equivalent to there not being a function f with domain some δ < α which is Σ_{n} (or equivalently Π_{n−1}) over L_{α} whose range is unbounded in α or L_{α}. One more equivalent is that for any Σ_{n}/L_{α} function f, f ↾ γ ∈ L_{α} for every γ < α. Thus we have the usual bounded quantifier manipulation rules: for φ ∈ Π_{n−1}, ∀x ∈ t∃yφ is equivalent to a Σ_{n} formula. We also say that α is n-admissible if L_{α} is Σ_{n} admissible.

We need a few facts about Σ_{n} Skolem functions and projections which are deep and difficult theorems of Jensen’s fine structure theory in general (as in Devlin [1984, VI]) but become quite simple via standard arguments when enough admissibility is assumed. We also need a couple of special facts about the ordinals less than β_{0}, the first ordinal which is Σ_{n} admissible for all n. All of these ought to be at least known folklore but seem to be missing from the couple of standard texts we consulted.

Proposition 3.1. If α is Σ_{k} admissible then L_{α} has a parameterless Σ_{k+1} Skolem function.

Proof: For a Σ_{k+1} formula ∃xφ(x, ȳ) with Gödel number n we let f(n, ȳ) = x ⇔ φ(x, ȳ) ∧ (∀x′ <_{L} x)(¬φ(x, ȳ)). The first conjunct is Π_{k} while the second one is equivalent to a Σ_{k} formula by Σ_{k} admissibility. □

Lemma 3.2. If L_{α} is Σ_{n} admissible then it satisfies Δ_{n} comprehension, i.e. for any u ∈ L_{α} and Σ_{n} formulas φ(z) and ψ(z) such that L_{α} ⊨ ∀z(φ(z) ↔ ¬ψ(z)), {z ∈ u|φ(z)} ∈ L_{α}.

Proof: For n = 1 this is a standard fact. We now proceed by induction on n ≥ 2. Consider any Σ_{n−2} formulas φ(x, y, z) and ψ(x, y, z) such that L_{α} ⊨ ∀z(∃x∀yφ(x, y, z) ↔ ¬∃x∀yψ(x, y, z)) and any u ∈ L_{α}. We must show that {z ∈ u|L_{α} ⊨ ∃x∀yφ(x, y, z)} ∈ L_{α}. Define in L_{α} a function on every z ∈ u by f(z) = x ⇔ [∀yφ(x, y, z) ∧ (∀x′ <_{L} x)∃y′¬φ(x′, y′, z)] ∨ [∀yψ(x, y, z) ∧ (∀x′ <_{L} x)∃y′¬ψ(x′, y′, z)]. By Σ_{n} admissibility, the formula defining f is equivalent to one that is Δ_{n} and so its range is bounded, say by L_{γ}. We then have that {z ∈ u|L_{α} ⊨ ∃x∀yφ(x, y, z)} = {z ∈ u|L_{α} ⊨ ∃x ∈ L_{γ}∀yφ(x, y, z)} = {z ∈ u|L_{α} ⊨ ∀x ∈ L_{γ}∃y¬ψ(x, y, z)}. Again by Σ_{n} admissibility these last two definitions are equivalent to ones that are Π_{n−1} and Σ_{n−1}, respectively and so by Δ_{n−1} comprehension which we have by induction, they belong to L_{α} as required. □

Lemma 3.3. If α is (k + 1)-admissible, then there are unboundedly many γ < α such that L_{γ} ≼_{k} L_{α}. (We write M ≼_{k} N to denote the assertion that M is a Σ_{k} elementary submodel of N, i.e. for any Σ_{k} formula φ with parameters in M, M ⊨ φ ⇔ N ⊨ φ.)

Proof: Consider any δ < α. We want to show there is a γ between δ and α such that L_{γ} ≼_{k} L_{α}. Let h be a (parameterless) Σ_{k}-Skolem function for L_{α}. Let H_{1} be the Σ_{k}-Skolem hull of L_{δ} in L_{α}. Since α is (k + 1)-admissible, H_{1} is bounded in L_{α}; let δ_{1} < α be the least ordinal such that H_{1} ⊆ L_{δ_{1}}. We now iterate this process. Let H_{l} be the Σ_{k}-Skolem hull of L_{δ_{l−1}} in L_{α}, and let δ_{l} be the least ordinal such that H_{l} ⊆ L_{δ_{l}}. As for δ_{1}, one can show that all the δ_{l} are < α. Let γ = sup_{l∈ω} δ_{l}. First, let us show that L_{γ} ≼_{k} L_{α}. Suppose that i < k and that we know that L_{γ} ≼_{i} L_{α}; we claim that L_{γ} ≼_{i+1} L_{α}. Let φ be a Π_{i} formula with parameters in L_{δ_{l}} for some l such that L_{α} ⊨ ∃xφ(x). Then, there exists an x ∈ H_{l+1} such that L_{α} ⊨ φ(x), and since L_{γ} ≼_{i} L_{α} we have that L_{γ} ⊨ φ(x). This proves our claim, and hence L_{γ} ≼_{k} L_{α}.

Next, we need to show that γ < α. The reason is that the function l ↦ δ_{l}: ω → L_{α} is Σ_{k+1}:

δ_{l} = μβ(∃β_{0}, …, β_{l} ≤ β(β_{0} = δ ∧ β_{l} = β ∧ ⋀_{i<l} ∀x ∈ L_{β_{i}}(h(x) ∈ L_{β_{i+1}}))).

Since α is (k+1)-admissible and h is Σ_{k}, the formula in parenthesis is Σ_{k}. Finding the least such β is Δ_{k+1}. Therefore, again by (k + 1)-admissibility, this function has to be bounded below α, and hence γ = sup_{l∈ω} δ_{l} < α. □

Lemma 3.4. If L_{γ} ≼_{k} L_{β} and β is Σ_{k−1} admissible then γ is Σ_{k} admissible.

Proof: We proceed by induction on k ≥ 1. Consider k and L_{γ} ≼_{k} L_{β} with β Σ_{k−1} admissible. (By convention, Σ_{0} admissibility is just transitivity and so every L_{β} is Σ_{0} admissible.) If the Lemma fails, there is a Π_{k−1}/L_{γ} function f with domain some δ < γ and range unbounded in L_{γ}. Suppose, for η < δ, f(η) = y ⇔ ψ(η, y) where ψ is Π_{k−1}/L_{γ}.For each η < δ and y = f(η), L_{β} ⊨ ψ(η, y) since L_{γ} ≼_{k} L_{β}. Thus L_{β} ⊨ ∃x∀η < δ∃y <_{L} x(ψ(η, y)). By the usual rules for manipulating bounded quantifiers, there is a Π_{k−1} formula θ(x) which is equivalent to ∀η < δ∃y <_{L} x(ψ(η, y)) in any Σ_{k−1} admissible L_{ζ} for ζ ≥ γ. As L_{β} is Σ_{k−1} admissible by assumption, L_{β} ⊨ ∃xθ(x). As L_{γ} ≼_{k} L_{β}, L_{γ} ⊨ ∃xθ(x, η, y). Finally, as L_{γ} is Σ_{k−1} admissible by induction, L_{γ} ⊨ ∃x∀η < δ∃y <_{L} x(ψ(η, y)) for the desired contradiction.

□

Lemma 3.5. For γ < β_{0}, L_{γ} is countable in L_{γ+1}.

Proof: For γ = ω, the conclusion is immediate. We now proceed by induction on γ. For a successor ordinal γ + 1, the conclusion follows simply from the countability of the formulas paired with the (inductively given) countability of the parameter space L_{γ}. If γ is a limit ordinal less than β_{0}, it is not Σ_{n} admissible for some n, i.e. there is a Σ_{n}/L_{γ} map f from some δ < γ with range unbounded in γ. We now define a counting of L_{γ} by combining the countings of δ and L_{f(ζ)} for each ζ < δ (which are uniformly definable as they are each in L_{f(ζ)+1} by induction). □

Lemma 3.6. Every member of L_{α_{n}} is Σ_{n+1} definable over L_{α_{n}} without parameters.

Proof: By Lemma 3.1 we may take f to be a parameterless Σ_{n+1} Skolem function for L_{α_{n}}. Let H be the Skolem hull of the empty set under f. As L_{α_{n}} is not (n + 1)-admissible (by Lemmas 3.3 and 3.4), H is unbounded in L_{α_{n}}. On the other hand, By Lemma 3.5, H is transitive. (Say δ ∈ H and so a counting of δ also belongs to H but then so does the value of this counting on every k ∈ ω.) Thus H = L_{α_{n}} and so every element of L_{α_{n}} is Σ_{n+1} definable (as the value of f on some k ∈ ω) over L_{α_{n}} without parameters. □

4. Proving m-Π_{3}^{0} determinacy in Π_{m+2}^{1}-CA_{0}

This section is devoted to proving Theorem 1.1: For each m ≥ 1, Π_{m+2}^{1}-CA_{0} ⊢ m-Π_{3}^{0}- DET. Our proof is a variant of Martin’s proof [1974], [n.d., Ch. 1] of Δ_{4}^{0}-DET specialized and simplified to the finite levels of the difference hierarchy on Π_{3}^{0}. Our proof of the main Lemma (Lemma 4.9) is perhaps somewhat different from his. In addition, we supply the analysis needed to see precisely how much comprehension is needed at every level.

We fix m ∈ ω, m ≥ 1. As m-Π_{3}^{0} determinacy is a Π_{3}^{1} sentence and strong Σ_{m+2}^{1}-DC_{0} is Π_{4}^{1} conservative over Π_{m+2}^{1}-CA_{0} by Simpson [2009, VII.6.20], we assume strong Σ_{m+2}^{1}-DC_{0} as well as Π_{m+2}^{1}-CA_{0}. In particular, we fix an m-Π_{3}^{0} set A given by the nested sequence A_{0} ⊇ A_{1} ⊇ ⋯ ⊇ A_{m} = ∅ of Π_{3}^{0} sets. We let A_{i} = ∩A_{i,k} for A_{i,k} ∈ Σ_{2}^{0} and A_{i,k} = ∪A_{i,k,j} for A_{i,k,j} ∈ Π_{1}^{0}.

We note that this proof does not use any determinacy beyond open determinacy, that (as we have seen) can be proved in systems much weaker than those we are using here.

We consider strings s ∈ ω^{≤m} (so of length at most m) and subgame trees S of the full binary tree. When s is specified, we let l = m − |s| and frequently make definitions and proofs depend on the parity of l (or equivalently of m when s = ∅ or |s| is otherwise fixed).

Definition 4.1. We define relations P^{s}(S) by induction on |s| ≤ m:

(1) P^{∅}(S) ⇔ there is a winning strategy for I (II) if l (or equivalently m) is even (odd) in G(A, S).

For |s| = n + 1 we also divide into cases based on the parity of l.

(1)

(2) If l is even, P^{s}(S) ⇔ there is a quasistrategy U for I in S such that (a) [U] ⊆ A ∪ A_{m−n−1,s(n)} and

(b) P^{s↾n}(U) fails.

(3) If l is odd, P^{s}(S) ⇔ there is a quasistrategy U for II in S such that (a) [U] ⊆ Ā ∪ A_{m−n−1,s(n)} and

(b) P^{s↾n}(U) fails.

A quasistrategy U witnesses P^{s}(S) if U is as required in the appropriate clause ((1), (2) or (3)) of the above definition.

It is not hard to show that for any s, if l is even (odd), and I (II) has a winning strategy in G(A, S), then P^{s}(S) holds. The converse is also true, but we would need to use m-Π_{3}^{0} determinacy to prove it. Our first goal is to prove that for every s of length n + 1 and any S, either P^{s}(S) holds or P^{s↾n}(S) holds (Lemma 4.9). Then, in the proof of Theorem 1.1, we will use this result to show that, if P^{∅}(T) does not hold, we can build a winning strategy for II (I) in the case when m is even (odd).

Definition 4.2. A quasistrategy U locally witnesses P^{s}(S) if, |s| = n + 1 and U is a quasistrategy for I (II) if l is even (odd) and there is a D ⊆ S such that for every d ∈ D there is a quasistrategy R^{d} for II (I) if l is even (odd) in S_{d} such that

(i) ∀d ∈ D ∩ U(U_{d} ∩ R^{d} witnesses P^{s}(R^{d}))

(ii) [U]\ ∪_{d∈D} [R^{d}] ⊆ A (Ā) if l is even (odd)

(iii) ∀p ∈ S∃^{≤1}d ∈ D(d ⊆ p & p ∈ R^{d})

Remark 4.3. Simple quantifier counting shows that the relations P^{s}(S), U witnesses P^{s}(S) and U locally witnesses P^{s}(S) are Σ_{|s|+2}^{1}, Π_{|s|+1}^{1} and Σ_{|s|+2}^{1}, respectively.

We now prove a number of Lemmas in Π_{m+2}^{1}-CA_{0} + strong Σ_{m+2}^{1}-DC_{0} to establish our theorem. Note that when we perform inductions on something like |s| we do not have to worry about what induction axioms we need as |s| ≤ m ∈ ω.

Lemma 4.4. If U locally witnesses P^{s}(S) then U witnesses P^{s}(S).

Proof: Suppose l is even. We show that clause (2a) of Definition 4.1 is satisfied. Consider x ∈ [U]. If x ∈ A there is nothing to prove. If not, by Definition 4.2(ii), x ∈ [R^{d}] for some d ∈ D. Then by (i) U_{d} ∩ R^{d} witnesses P^{s}(R^{d}) and so by Definition 4.1 (2a) x ∈ A_{m−n−1,s(n)} as required. If l is odd, the same argument with Ā in place of A and clause (3a) in place of (2a) shows that clause (3a) is satisfied as required.

We now proceed by induction on |s| = n+1 ≤ m to show that part (b) of clause (2) or (3) of Definition 4.1 holds. We begin with n = 0. Suppose that m is odd and so the associated l with s in the definitions of P^{s}(S) and U locally witnessing P^{s}(S) is even. If (2b) does not hold, i.e. P^{∅}(U) holds, there is a winning stratgey τ for II in G(A, U) (as m is odd). We claim there is a d ∈ D consistent with τ such that every x ⊇ d in [U] and consistent with τ is in [R^{d}]. Suppose not. Now note that every e ∉ ∪_{d∈D,d⊂e}R^{d} in U and consistent with τ has a d̂ ⊇ e in D (and so a minimal one) consistent with τ, for if not then, for any x ⊇ e in [U] and consistent with τ, x ∉ ∪_{d∈D}R^{d}. By Definition 4.2(ii) we would then have x ∈ A contradicting our choice of τ as a winning stratgey for II in G(A, U). Next, note that, by our assumption, any such d̂has a (minimal) extension ê consistent with τ and not in Rd̂. By Definition 4.2(iii), no e′ ⊃ d̂ with e′ ⊂ ê is in D and so ê has the same properties assumed about e. We can continue this procedure to build a sequence e_{j} each consistent with τ such that ∪e_{j} = x ∉ ∪_{d⊂x,d∈D}R^{d} and so x ∈ U \ ∪_{d∈D}R^{d} ⊆ A for the same contradiction to our choice of τ.

So we have a d ∈ D consistent with τ such that every x ⊇ d in [U] and consistent with τ is in [R^{d}]. Thus the natural restriction of τ is a winning strategy for II in G(A, U_{d} ∩ R^{d}), i.e. P^{∅}(U_{d} ∩ R^{d}) contradicting Definition 4.2(i) and so establishing (2b) of Definition 4.1 as required.

If m is even and so the associated l for s in the definition of P^{s}(S) is odd, the same proof works with the following pairs interchanged: I and II; 2 and 3; A and Ā (except that G(A, U) is unchanged).

Next, we consider n > 1 and assume for definiteness that m − n (= m − |s ↾ n|) is odd and, for the sake of a contradiction, that P^{s↾n}(U) holds. Let Ŝ be II’s quasistrategy in U witnessing P^{s↾n}(U). We will build Û, D̂ and {R̂^{d} : d ∈ D̂} locally witnessing P^{s↾n−1}(Ŝ). By the induction hypothesis this would imply P^{s↾n−1}(Ŝ), contradicting that Ŝ witnesses P^{s↾n}(U). Roughly speaking, to build I’s quasistrategy Û, player I would try to fall out of ∪_{d∈D}[R^{d}] and hence end up in A. For the d ∈ D such that I has no strategy to exit R^{d}, we will add d ∈ D̂ and define R̂^{d} ⊆ R^{d} such that P^{s↾n−1}(R̂^{d}).

Let D̂ = \{d ∈ Ŝ ∩ D|G(\overline{[R^{d}]}, Ŝ_{d}) is a win for II\} (a Σ_{2}^{1} set). For d ∈ D̂ we let R̂^{d} be II’s nonlosing quasistrategy in G(\overline{[R^{d}]}, Ŝ_{d}) (each a Π_{2}^{1} set and so the indexed collection is given by Π_{3}^{1}-CA_{0}) so, of course, R̂^{d} ⊆ R^{d} and R̂^{d} is a quasistrategy for II in U_{d}. As Ŝ witnesses P^{s↾n}(U), [Ŝ] ⊆ Ā ∪ A_{m−n,s(n−1)} and so [R̂^{d}] ⊆ Ā ∪ A_{m−n,s(n−1)}. By Definition 4.2(i), U_{d} ∩ R^{d} witnesses P^{s}(R^{d}) and so, in particular, P^{s↾n}(U_{d} ∩ R^{d}) fails and R̂^{d} is not a witness for it. As condition (3a) has already been verified for [U] ⊇ [R̂^{d}], (3b) must fail with R̂^{d} and so there is a witness Û^{d} for each P^{s↾n−1}(R̂^{d}). The indexed sequence {Û^{d} : d ∈ D̂} then exists by Σ_{|s|}^{1}-AC_{0} by Remark 4.3. Finally, we use Σ_{2}^{1}-CA_{0} and Σ_{2}^{1}-AC_{0} to define the sequence σ_{q,d} of winning strategies for I in G(\overline{[R^{d}]}, Ŝ_{q}) for d ∈ D and q ∉ R̂^{d} (which is taken to be ∅ for d ∈ D\D̂) when one exists.

We now (arithmetically in the above parameters) define a quasistrategy Û for I in Ŝ:

(1) If p ∈ Û and there is no d ∈ D such that d ⊆ p and p ∈ R^{d} then the immediate extensions of p in Û are the same as those in Ŝ.

(2) For each q ∈ Û and d ∈ D such that q is a minimal extension of d in R^{d}\R̂^{d}, the play in Û following q agrees with that of σ_{q,d} until we reach a p ∉ R^{d}.

(3) For d ∈ D̂ ∩ Û, let Û_{d} ∩ R̂^{d} = Û^{d}.

We claim that Û (with D̂ and R̂^{d}) locally witnesses P^{s↾n−1}(Ŝ). Property (i) of Definition 4.2 follows from (3) in the definition of Û and our choice of Û^{d} for d ∈ D̂. For (ii), note that, by (2) in the definition of Û, [Û] ∩ [R^{d}] ⊆ [R̂^{d}] while Û is a quasistrategy in Ŝ which is one in U. Thus [Û]\ ∪_{d∈D} [R̂^{d}] ⊆ [U]\ ∪_{d∈D} [R^{d}] ⊆ A by Definition 4.2(ii) as required. Property (iii) is immediate from the definitions and the corresponding condition for U being a local witness for P^{s}(S) as D̂ = D ∩Ŝ and R̂^{d} ⊆ R^{d}. Thus by induction, Û witnesses P^{s↾n−1}(Ŝ) for the desired contradiction (with clause (3b) in the definition of Ŝ being a witness for P^{s↾n(U)}).

Finally, when n = 1 (still assuming that m − n is odd), the proof is much the same as when n > 1 except that when we choose a witness Û^{d} for P^{s↾n−1}(R̂^{d}) we must take a winning strategy for I in G(A, R̂^{d}) and we need to show that [Û] ⊆ A to see that it witnesses P^{∅}(Ŝ) for the desired contradiction (with clause (3b) in the definition of Ŝ being a witness for P^{s↾n(U)}). The point here is that if we stay in some R̂^{d} then we follow Û^{d} which is a winning strategy for I in G(A, R̂^{d}). If we leave R̂^{d} then we leave R^{d} by (2) in the definition of Û. If we leave every R^{d}, we follow Ŝ and so stay in U and also wind up A by clause (ii) of the definition of U being a local witness for P^{s}(S).

For m − n even, the proof is the same except that we interchange I and II, clauses (2) and (3) of Definition 4.1, A and Ā and G(\overline{[R^{d}]}, Ŝ_{d}) and G([R^{d}], Ŝ_{d}). □

Definition 4.5. P^{s}(S) fails everywhere if P^{s}(S_{p}) fails for every p ∈ S. By Remark 4.3, this relation is Π_{|s|+2}^{1}.

Lemma 4.6. If P^{s}(S) fails then there is a quasistrategy W for I if l is odd (for II if l is even) in S such that P^{s}(W) fails everywhere.

Proof: For |s| = 0, if l is odd (even), II (I) does not have a winning strategy in G(A, S). Let W be I’s (II’s) nonlosing quasistrategy in this game. It exists by Π_{2}^{1}-CA_{0} and, by definition, II (I) does not have a winning strategy in G(A, W_{p}) for any p ∈ W_{p} and so P^{s}(W) fails everywhere.

Now suppose |s| = n+1 and, for definiteness, that l is even. Let D be the Σ_{|s|+2}^{1}∧Π_{|s|+2}^{1} set of minimal d ∈ S for which P^{s}(S_{d}). (If there are none, then P^{s}(S) already fails everywhere.) By Σ_{|s|+2}^{1}-AC_{0} let U^{d} witness P^{s}(S_{d}) for every d ∈ D.

Consider now the game G(B, S) where B = {x ∈ [S]|∃d ∈ D(d ⊆ x)}. We claim that I has no winning stratgey in this game. If there were one σ, then we could define a quasistrategy U for I in S by following σ until a position d ∈ D is reached at which point we move into U^{d}. With D and R^{d} = S_{d} for d ∈ D, it is easy to see that U locally witnesses P^{s}(S) which by the previous Lemma is the desired contradiction.

Thus we can let W be II’s nonlosing quasistrategy in G(B, S) and σ_{p} be a winning strategy for I for p ∈ S\W. (These exist as above.) If W is not as required, there is a q ∈ W and a witness Û that P^{s}(W_{q}). Define a quasistrategy U for I in S_{q} by U ∩ W_{q} = Û. If we ever reach a position p ∉ W, we switch to following σ_{p} until we reach a position d ∈ D at which point we switch to U^{d}. If we now let D̂ = D ∪ {q}, R^{q} = W_{q} and R^{d} = S_{d} for d ∈ D, it is easy to see that together with U we have a local witness for P^{s}(S_{q}). By the previous Lemma then P^{s}(S_{q}) and so by the definition of D there is a p ⊆ q in D contradicting the choice of W as a nonlosing strategy for II in G(B, S).

The argument for s = n + 1 and odd l is the same except that we interchange I and II and G(B, S) and G(B̄, S). □ Definition 4.7. For n + 1 = |s|, W strongly witnesses P^{s}(S) if, for all p ∈ W, W_{p} witnesses P^{s}(S_{p}), i.e. W witnesses P^{s}(S) and P^{s↾n}(W) fails everywhere. By Remark 4.3, this relation is Π_{|s|+1}^{1}.

Lemma 4.8. If P^{s}(S) then there is a W that strongly witnesses it. Proof: Assume, for definiteness, that l is even. Let U witness P^{s}(S). By Definition 4.1(2b), P^{s↾n}(U) fails. By Lemma 4.6, let W be a quasistrategy for I in U such that P^{s↾n}(W) fails everywhere. As [W] ⊆ [U], Definition 4.1(2a) holds of W and so it strongly witnesses P^{s}(S) as required. The proof for l odd is the same except that we interchange I and II as well as clauses (2) and (3) of Definition 4.1. □ Lemma 4.9. If |s| = n + 1 then at least one of P^{s}(S) and P^{s↾n}(S) holds. Proof: We prove the Lemma by reverse induction on n < m. Suppose for definiteness that m − n is odd. If P^{s}(S) fails we define by induction on the length of positions (using strong Σ_{m+2}^{1}-DC_{0}) a quasistrategy U for II in S along with D ⊆ S and R^{d} for d ∈ D locally witnessing P^{s↾n}(S) if n > 0 and witnessing P^{∅}(S) if n = 0. Thus, by Lemma 4.4 when n > 0, P^{s↾n}(S) holds as required. We will decide which q are in U by recursion on the length of q, starting with ∅ ∈ U and going up the tree S. Along the way we will enumerate some of these q into D and define a quasistrategy R^{q} for I. Inside each R^{q} we have to make sure to define U such that U ∩ R^{q} witnesses P^{s↾n}(R^{q}). For x ∈ [U] \ ⋃_{d∈D}[R^{d}] we need to make sure x ∈ Ā, and we will do this as follows. On the one hand, we will define U so that x belongs to Ā ∪ A_{m−n−2,j} for every j ∈ ω, and hence x ∈ Ā ∪ A_{m−n−2}. On the other hand, we will make sure that x ∉ A_{m−n−1,s(n),j} for any j, and hence x ∉ A_{m−n−1}. Then we use that Ā ∪ A_{m−n−2} \ A_{m−n−1} ⊆ Ā to show that x ∈ Ā. We will go along the path x satisfying the requirements x ∈ Ā ∪ A_{m−n−2,j} and x ∉ A_{m−n−1,s(n),j} one j at the time. To keep track of which requirements need to be satisfied, along the construction we will define the notion of a position q ∈ U marking a j ∈ ω (with the j’s marked in order along any path). Simultaneously we also define certain auxiliary quasistrategies W^{q} and R̂^{q}.

Of course, ∅ ∈ U and we say that it marks 0. If n = m − 1, by lemma 4.6, we let W^{∅} be a quasistrategy for II in S such that P^{s}(W^{∅}) fails everywhere. If n < m − 1, we know by (reverse induction) that P^{sˆ 0}(S) holds. In this case we apply Lemma 4.8 (and strong Σ_{m+2}^{1}-DC_{0}) to choose a W^{∅} strongly witnessing this fact (a Π_{|s|+2}^{1} and so at worst Π_{m+1}^{1} relation). (Note that in this case, P^{s}(W^{∅}) also fails everywhere by Definition 4.7.)

Now assume by induction (on positions in U) that q ∈ U marks j and that q belongs to a quasistrategy W^{q} for II in S_{q} such that P^{s}(W^{q}) fails everywhere and if n < m − 1 then W^{q} strongly witnesses P^{sˆ j}(S_{q}).

Recall that A_{m−n−1,s(n),j} is a closed set. If G(A_{m−n−1,s(n),j}, W^{q}) is not a win for II (a Π_{2}^{1} relation), put q in D and let R̂^{q} be I’s nonlosing quasistrategy in this game (a Π_{2}^{1} set in the parameters). Define R^{q} to be R̂^{q} on W^{q} and to agree with S elsewhere in S_{q}. Now [R̂^{q}] ⊆ A_{m−n−1,s(n),j} since it is a nonlosing quasistrategy for this closed set. Next note that, by definition, A_{m−n−1,s(n),j} ⊆ A_{m−n−1,s(n)}. Thus if P^{s↾n}(R̂^{q}) fails, R̂^{q} would witness P^{s}(W^{q}) contrary to our assumption that P^{s}(W^{q}) fails everywhere. So we may take U^{q} to be a witness for P^{s↾n}(R̂^{q}) (a Π_{|s|}^{1} relation) . We now continue to define U by letting it agree with U^{q} on R̂^{q} and let no p ∈ R̂^{q} into D nor mark any j′.

If beginning in this way with q we ever first reach a p ∉ R̂^{q} (which we take to be q if G(A_{m−n−1,s(n),j}, W^{q}) is a win for II), we continue in U by following a winning strategy τ_{p} for II in G(A_{m−n−1,s(n),j}, W^{q}) (a Π_{1}^{1} relation) until we first reach a q′ ⊃ p with [W_{q′}^{q}]∩A_{m−n−1,s(n),j} = ∅. We must reach such a q′ since τ_{p} is a winning strategy for II in G(A_{m−n−1,s(n),j}, W^{q}) and A_{m−n−1,s(n),j} is a closed set. We do not mark any q^{∗} with p ⊆ q^{∗} ⊂ q′ nor put any such into D. We now say that q′ marks j + 1. P^{s}(W_{q′}^{q}) fails everywhere since P^{s}(W^{q}) does. If n = m − 1, we let W^{q′} = W_{q′}^{q}. If n < m − 1, P^{sˆ j+1}(W_{q′}^{q}) holds by our reverse induction on n and we let W^{q′} strongly witness this fact (a Π_{|s|+2}^{1} and so at worst Π_{m+1}^{1} relation). Of course, it also strongly witnesses P^{sˆ (j+1)}(S_{q′}) as required for our inductive definition of U.

We now prove that, if n > 0, U (with D and R^{d}) locally witnesses P^{s↾n}(S). First note that, by our definitions, U_{d} ∩ R^{d} = U_{d} ∩ R̂^{d} = U^{d} for d ∈ D. Thus condition (i) of Definition 4.2 holds as U^{d} witnesses P^{s↾n}(R̂^{d}). As we never put any q ⊃ d ∈ D into D until we have left R̂^{d}, condition (iii) holds as well. We now turn to condition (ii) and consider any x ∈ [U]. Let ∅ = q_{0} ⊂ q_{1} … ⊂ q_{i} ⊂ … be the strictly increasing sequence of q’s contained in x such that q_{j} marks j. By construction, each q_{j} ∈ D. If the sequence terminates at some d = q_{k}, then, by definition, x never leaves R̂^{d} and so x ∈ [R^{d}] and (ii) holds trivially for this x. If not, then, for every j, x ∉ A_{m−n−1,s(n),j} as x ∈ [W_{q_{j+1}}^{q_{j}}] and [W_{q_{j+1}}^{q_{j}}] ∩ A_{m−n−1,s(n),j} = ∅. Thus x ∉ A_{m−n−1,s(n)} = ∪_{j}A_{m−n−1,s(n),j}. As A_{m−n−1,s(n)} ⊇ A_{m−n−1}, x ∉ A_{m−n−1}. Now if n + 1 = m, x ∉ A_{0} and so x ∉ A and condition (ii) is satisfied. If n + 1 < m then, as W^{q_{j}} witnesses P^{sˆ j}(S_{q_{j+1}}), x ∈ Ā∪A_{m−n−2,j} for each j. (Note that as m−n is odd so is m−|sˆ j| and we are in case (3) of Definition 4.1.) Thus x ∈ Ā ∪ A_{m−n−2} as A_{m−n−2} = ∩_{j}A_{m−n−2,j}. As, by our case assumptions, m − n − 1 is even, A_{m−n−2}\A_{m−n−1} ⊆ Ā by the definition of A in terms of the sequence A_{i}. Thus x ∈ Ā and condition (ii) is again satisfied.

Finally, if n = 0 we argue that U is a wining quasistrategy for II in G(A, S). Consider any x ∈ [U]. If there is a d ∈ D such that x ∈ [R̂^{d}] then x ∈ [U^{d}] by construction. Now U^{d} is a witness for P^{∅}(R̂^{d}) (as n = 0, s ↾ n = ∅), i.e. U^{d} is a winning strategy for II in G(A, R̂^{d}). Thus x ∈ Ā as required. On the other hand, if leaves every R̂^{d} then, by the argument above, x ∈ Ā as well.

For m−n even we interchange I and II as well as G(A_{m−n−1,s(n),j}, W^{q}) and G(Ā_{m−n−1,s(n),j}, W^{q}) in the definition of U. In the verification that U is as desired note that the case that n+1 = m cannot occur. Otherwise, we interchange I and II, cases (2) and (3) of Definition 4.1, even and odd as well as A and Ā. □

Proof: (of Theorem 1.1) If G(A, T) is not a win for II (I) if m is odd (even), P^{∅}(T) fails. By Lemma 4.6, there is a quasistrategy W^{∅} for I (II) such that P^{∅}(W^{∅}) fails everywhere. We define a quasistrategy U for I (II) in W^{∅} by induction on |p| for p ∈ U. For |p| = j + 1, we simultaneously define (using strong Σ_{3}^{1}-DC_{0}) a quasistrategy W^{p} for I (II) which strongly witnesses P^{⟨j⟩}(W_{p}^{p↾j}). Of course, ∅ ∈ U and we already have W^{∅}. Suppose then that p ∈ U, |p| = j + 1, and W^{p} has been defined. The immediate successors q of p in U are precisely its immediate successors in W^{p}. By our choice of W^{p}, P^{∅}(W^{p}) fails everywhere and so, in particular, P^{∅}(W_{q}^{p}) fails for each immediate successor q of p in U. By Lemma 4.9, then P^{⟨j⟩}(W_{q}^{p}) holds and, by Lemma 4.8 (and strong Σ_{3}^{1}-DC_{0}) we may choose a W^{q} that strongly witnesses it to continue our induction.

Consider now any play x ∈ [U]. By construction x ∈ [W^{x↾j+1}] for every j and W^{x↾j+1} witnesses P^{⟨j⟩}(W_{x↾j+1}^{x↾j}). By Definition 4.1 (2a) (4.1 (3a)) if m is odd (even), x ∈ A ∪ A_{m−1,j} (Ā ∪ A_{m−1,j}) for every j. As ∩_{j}A_{m−1,j} = A_{m−1} ⊆ A (Ā) (by the definition of A in terms of the sequence A_{i}), x ∈ A (Ā). Thus U is a winning quasistrategy for I (II) in G(A, T) as desired. □

5. The Game: Failures of Determinacy in L

This section is dedicated to proving Lemma 1.8. Let T_{n} consist of KP + Σ_{n}-admissibility + V=L + ∀α ∈ Ord(L_{α} is not Σ_{n}-admissible ). So L_{α_{n}} is the only wellfounded model of T_{n}. Each player will have to play the characteristic function of a complete consistent extension of T_{n}, or otherwise they loose. The goal now is to be able to identify the player playing the true theory of L_{α_{n}} using a Boolean combination of Π_{3}^{0} formulas.

To define G we first define 2n + 4 many Π_{3}^{0} conditions in order:

(R_{I}0), (R_{II}0), (R_{II}1), (R_{II}1), ...., (R_{II}(n + 1)), (R_{II}(n + 1)).

Then, if the first condition satisfied by the play is of the form (R_{I}k), I wins, and if it is of the form (R_{II}k), then II wins. If no condition is ever satisfied, we will let one of the two players win; for now it does not matter which.

We now define these conditions one at a time, so we can make the motivations and the pertinent definitions along the way. We will later rearrange the conditions to reduce the level of the game in the Π_{3,n}^{0} hierarchy. Every time we define a new pair of conditions (R_{I}k) and (R_{II}k) we will show that they are Π_{3}^{0}, and that if any of these conditions is the first one to be satisfied, the choice of the winner is compatible with (1) and (2) of Lemma 1.8. At the end, we will show that, if one of the players is actually playing T h_{α_{n}}, then some condition along the way will have to be satisfied, and hence (1) and (2) of Lemma 1.8 hold.

We begin with Conditions (R_{::}0).

(R_{I}0): II does not play a complete consistent extension of T_{n}
(R_{II}0): I does not play a complete consistent extension of T_{n}

Claim 5.1. Conditions (R_{I}1) and (R_{II}1) are Σ_{1}^{0}.

Proof: Saying that the set of sentences played form a complete and consistent theory is Π_{1}^{0}. Saying that the axioms of T_{n} are included in these sets is also Π_{1}^{0}. □

If either of these conditions are satisfied, the game ends and a player playing T h_{α_{n}} cannot loose at this stage. In this case it does not matter what the rest of the conditions say. So, from now on, when we describe the rest of the conditions, we will assume neither of these two conditions apply.

The term model of a complete theory T consistent with T_{n} is built as follows: Consider the set of formulas with one free variable φ(x) such that T ⊢ ∃!xφ(x). Think of this formula φ as a term t_{φ} representing the unique element satisfying φ. So, given two such formulas φ and ψ, we say that t_{φ} = t_{ψ} if T proves that φ and ψ are equivalent. Also, we let t_{φ} ∈ t_{ψ} if T proves that the witness of φ belongs to the witness of ψ. This defines the term model of T. Since T_{n} proves that every nonempty class has a <_{L}-least element, every sentence ∃xφ(x) in T has a term witnessing it. So, this term model we just built is a model of T and, furthermore, from T we can compute its full elementary diagram. Note that the term model of T h_{α_{n}} is isomorphic to L_{α_{n}} because very element of L_{α_{n}} is definable without parameters by Lemma 3.6.

Let M_{I} be the term model of the theory built by I and M_{II} the one built by II. So, from the play, we can compute the full elementary diagrams of M_{I} and M_{II}. These models might be wellfounded or not. But recall that the only wellfounded model of T_{n} is L_{α_{n}}. All the other models of T_{n} are ill-founded. We now continue with the next pair of conditions.

(R_{I}1): M_{II} is not an ω-model.
(R_{II}1): M_{I} is not an ω-model.

Claim 5.2. Conditions (R_{I}1) and (R_{II}1) are Σ_{2}^{0}.

Proof: To say that a term model M is an ω-model, we have to say that for every term t, if M ⊨ t ∈ ω, then there exists a number n such that M ⊨ t = 1 + 1 + .... + 1, where 1 is added n times. This is a Π_{2}^{0} formula about M. □

We remark that the proof of the claim above works when both players have actually played complete consistent extensions of T_{n}. Formally, we think of (R_{II}1) and (R_{II}1) as the Σ_{2}^{0} formulas given in the proof of the claim. The interpretation of these Σ_{2}^{0} formulas will match what we first called (R_{I}1) and (R_{II}1) above the claim, when conditions (R_{I}0) and (R_{II}0) are not satisfied, but that is the only case where we care. Similar remarks will apply to the conditions (R_{::}k) below. That is, we supply an intuitive description of sets in our list and then a formal Π_{3}^{0} definition that makes the intuition true in the cases of interest. As we continue to define more conditions on the winning set, keep in mind that our goal as we go along is to guarantee for each condition that if I plays the theory of L_{α_{n}} then he does not loose. If he does not play T h_{α_{n}} and II does, then II does not loose. At the end we will prove that someone wins the game.

L_{α_{n}} is an ω-model, so a player playing T h_{α_{n}}, cannot loose at this step either. From now on assume (for the intuitive descriptions of our clauses) that both M_{I} and M_{II} are ω-models of T_{n} and that at least one of them is L_{α_{n}}. Let us move on to the third pair of conditions.

(R_{I}2): ℝ_{M_{I}} ⊆ ℝ_{M_{II}}.
(R_{II}2): ℝ_{M_{II}} ⊆ ℝ_{M_{I}}.

If both players are playing T h_{α_{n}}, then (R_{I}2) holds, and hence I wins as needed for (1) of Lemma 1.8. So, from now on, let as assume that one player is playing T h_{α_{n}} and the other one is not. Next, note that L_{α_{n}} has no proper sub-models satisfying T_{n}, and hence the player playing T h_{α_{n}} cannot loose by either of these conditions.

Claim 5.3. Conditions (R_{I}2) and (R_{II}2) are Π_{3}^{0}.

Proof: For (R_{I}2), it is enough to say that every ordinal in M_{I}, is also an ordinal in M_{II}: If a linear ordering α belongs to both On^{M_{I}} and On^{M_{II}}, it has to actually be wellfounded as we are assuming one of M_{I} or M_{II} is wellfounded. So, by transfinite induction, this implies that L_{α} also belongs to both M_{I} and M_{II}. Now, note that since every ordinal α in M_{I} is countable in M_{I} (Lemma 3.5) there is always a real representing a linear ordering that is isomorphic to α.

To say that two ordinals α and β (even in different models) are the same, we say that there is a real x coding α in M_{I} and a real y coding an ordinal β in M_{II}, such that x = y. Even if x and y belong to different models, we can say they represent the same real by saying that for every natural number n, M_{I} ⊨ n ∈ x ⟺ M_{II} ⊨ n ∈ y. Therefore, the Π_{3}^{0} sentence we need is

∀α ∈ On^{M_{I}} ∃x ∈ ℝ^{M_{I}}, y ∈ ℝ^{M_{II}}, β ∈ On^{M_{II}}[(M_{I} ⊨ x codes α)
(5.1)  ∧(M_{II} ⊨ y codes β) ∧ ∀n ∈ ω(M_{I} ⊨ n ∈ x ⟺ M_{II} ⊨ n ∈ y)].
□

We remark again, that the claim should actually say: If M_{I} and M_{II} are ω-models of T_{n} and at least one of them is wellfounded, then (R_{I}2) and (R_{II}2) are equivalent to Π_{3}^{0} properties. In any other case, we think of (R_{I}2) and (R_{II}2) as given formally by these Π_{3}^{0} properties, which, in cases not of interest, might not have the intended meaning.

To this point, our proof follows the ideas in Martin [1974a] and [n.d., Ch. 1] where he shows that Σ_{4}^{0}-determinacy is not true in the least β-model of second order arithmetic ℝ∩L_{β_{0}}. These, in turn, are based on those of H. Friedman’s [1971] proof that Σ_{5}^{0} determinacy fails in ℝ ∩ L_{β_{0}}. The ideas in the rest of the proof are new.

From now on, we assume that no condition listed so far holds and so, in particular, not both of M_{I} and M_{II} are well founded. Again, we are interested in the plays where one is well founded and so actually L_{α_{n}}.

Definition 5.4. We use M to denote the wellfounded model of the pair M_{I} and M_{II} and N for the ill-founded one. The player playing M ≅ L_{α_{n}} should win the game but we do not know which one it is. There is a least ordinal α ∈ On^{M} that is not in N. Let A be the well founded part of N. So, we have that L_{α} ≅ A. Let us call A_{I} and A_{II} the initial segments of M_{I} and M_{II} that correspond to L_{α} and A in M and N.

M = L_{α_{n}}  N L_{α} − A

We abuse notation slightly by using A to also denote the isomorphism between A_{I} and A_{II}. That is, A is the set of pairs of terms (z, w) ∈ M_{I} × M_{II} representing elements z ∈ A_{I} and w ∈ A_{II} which are the same set under the isomorphism A_{I} ≅ A_{II}.

Claim 5.5. A is a Σ_{2}^{0} set. Also, A_{I} and A_{II} are Σ_{2}^{0} sets.

Proof: For A we have the following Σ_{2}^{0} definition.

(z, w) ∈ A ⟺ ∃x ∈ ℝ^{M_{I}}, y ∈ ℝ^{M_{II}} (M_{I} ⊨ x codes z ∧ M_{II} ⊨ y codes w ∧

∀n ∈ ω(M_{I} ⊨ n ∈ x ⟺ M_{II} ⊨ n ∈ y)).

For A_{I} we have that z ∈ A_{I} ⟺ ∃w ((z, w) ∈ A), and analogously for A_{II}. □

(At this point, Martin’s proof ([1974a] and [n.d., Ch. 1]) that Σ_{4}^{0}-DET fails in L_{β_{0}} has a Σ_{4}^{0} winning condition that says that there exists a α ∈ M_{I} such that L_{α}^{M_{I}} = A_{I}. )

The next n − 1 pairs of conditions all have basically the same form. The conditions (R_{::}3) are a bit simpler than the rest and we describe them first. We will then generalize them and define the conditions (R_{::}(2 + k)) for k > 2 all at once.

We start by defining the sets of ordinals in one model that have witnesses for Σ_{1} formulas with parameters in A that have no witnesses in the other model. The expectation is that the witnesses are in the nonwellfounded model N. We will show later that either there are many such witnesses and the set of witnesses shows that the On^{N} \ A has no least element; or there are few such witnesses and there is an ordinal β ∈ N such that A ≼_{1} L_{β}^{N}. In the former case, we have identified the nonwellfounded model and we can end the game. In the latter case, we continue with the next pair of conditions, now assuming the existence of such a β.

Let

C_{M_{II},1} = {β ∈ On^{M_{II}} : ∃(x_{1}, x_{2}) ∈ A, φ ∈ Δ_{0},

((∃z ∈ L_{β}^{M_{II}} M_{II} ⊨ φ(z, x_{2})) ∧ (M_{I} ⊨ ¬∃yφ(y, x_{1})))}.

Note that this condition says more than that A is not a Σ_{1} substructure of L_{β}^{M_{II}} as it asserts that there are no witnesses for the formula φ even in M_{I}. Thus its negation does not imply that A is a Σ_{1} substructure of L_{β}^{M_{II}}. C_{M_{I},1} is defined analogously. These sets are Σ_{2}^{0} because, as we noted before, A is Σ_{2}^{0} and the second line of the definition is computable form the elementary diagrams of M_{I} and M_{II}. We are now ready to define the next pair of conditions.

(R_{I}3): C_{M_{II},1} has no least element.
(R_{II}3): C_{M_{I},1} has no least element.

Clearly a player playing a wellfounded model cannot loose because of these conditions. Also, these conditions are Π_{3}^{0} as they say, for example, that ∀β(β ∉ C_{M_{II},k} ∨ ∃γ < β(γ ∈ C_{M_{II},k})) and C_{M_{II},k} is Σ_{2}^{0}.

Suppose now that neither of these conditions is satisfied.

Claim 5.6. There is a β ∈ On^{N} ∖ A such that A ≼_{1} L_{β}^{N}.

Proof: Suppose not, that is, for every γ ∈ On^{N} ∖A, there is a Σ_{1} formula with parameters in A, that is true in L_{γ} but not in A. Since conditions (R_{I}3) and (R_{II}3) are not satisfied, C_{N ,1} has a least element δ. Notice that δ cannot be in A because if the witness z for a Δ_{0} formula φ(z, x_{2}) is in L_{N_{δ}} ⊆ A, then ∃yφ(y, x_{1}) also holds in M. Let δ > γ_{0} > γ_{1} > γ_{2} > ... be a descending sequence in On^{N} ∖ A, converging down to the cut (On^{A}, On^{N} ∖ A). For each i, there is a Δ_{0} formula φ_{i} with parameters from A and a <_{L}-least witness z_{i} ∈ L_{γ_{i}} such that N ⊨ φ_{i}(z_{i}) but A ⊨ ¬∃yφ_{i}(y). By thinning out the sequence if necessary, we may assume that z_{i} ∈ L_{γ_{i}} but z_{i} ∉ L_{γ_{i+1}}. So {z_{i} : i ∈ ω} is an <_{L}^{N} -descending sequence. Since γ_{i} ∉ C_{N ,1}, M ⊨ ∃yφ_{i}(y). Let y_{i} be the <_{L}^{M}-least such witness. Since M is wellfounded, the sequence {y_{i} : i ∈ ω} cannot be a <_{L}^{M}-descending sequence. So, there exists i < j such that z_{j} <_{L}^{N} z_{i} but y_{i} <_{L}^{M} y_{j}. Therefore, L_{γ_{j}} is a witness in L_{γ_{j}+1} for x showing the truth in N of the Δ_{0} formula

ψ(x) ≡ ∃z ∈ xφ_{j}(z) ∧ ∀z ∈ x¬φ_{i}(z)

but there is no witness for ψ(x) in M. This shows that γ_{j} + 1 is in C_{N ,1}, contradicting our choice of δ as the least element of C_{N ,1}. □

We now turn to defining the rest of the conditions. Again, the idea is to define conditions such that they hold only if they have identified the nonwellfounded model, and if they do not hold, they give us information about the models that we can assume when we define the following conditions. We will show that if for some k, none of the conditions (R_{::}1), ..., (R_{::}(2+ k)) is satisfied, then α is (k + 1)-admissible. Since L_{α_{n}} has no n-admissible ordinals, we will be able to argue that some condition (R_{::}(2 + k)) will have to be satisfied for some k < n. This will be proved, of course, by induction on k, but the induction hypothesis needs to be stronger. We show that if no condition (R_{::}1), ..., (R_{::}(2 + k)) holds then there exists β_{1} and β_{2} such that

(⋆_{k})(β_{1}, β_{2}) : β_{1} ∈ On^{M_{I}} ∖ A_{I} ∧ M_{I} ⊨ β_{1} is (k − 1)-admissible∧

β_{2} ∈ On^{M_{II}} ∖ A_{II} ∧ M_{II} ⊨ β_{2} is (k − 1)-admissible∧
L_{β_{1}}^{M_{I}} ≡_{k,A} L_{β_{2}}^{M_{II}}.

Here ≡_{k,A} means Σ_{k}-elementary equivalence with parameters from A. In other words, L_{β_{1}}^{M_{I}} ≡_{k,A} L_{β_{2}}^{M_{II}} means that for every Σ_{k} formula φ(z), and every x_{1} ∈ A_{I} and x_{2} ∈ A_{II}, if x_{1} and x_{2} represent the same set (i.e. (x_{1}, x_{2}) ∈ A), then M_{I} ⊨ φ(x_{1}) ⟺ M_{II} ⊨ φ(x_{2}).

By Claim 5.6, we already know there are ordinals satisfying (⋆_{1}): Just let β_{1} = α ∈ M and let β_{2} ∈ N be such that A ≼_{1} L_{β_{2}}^{N}.

Property (⋆_{k}) is useful because, on the one hand, it is simple to define (it is Π_{2}^{0} as we prove below) and, on the other hand, it has strong consequences as we will show in Lemma 5.10. For instance, we will show that the existence of β_{1} and β_{2} satisfying it implies that α is (k + 1)-admissible.

Lemma 5.7. (⋆_{k}) is a Π_{2}^{0} property.

Proof: We already showed that β_{1} ∉ A_{I} ∧ β_{2} ∉ A_{II} is a Π_{2}^{0} relation. Whether β_{i} is (k − 1)- admissible is just one sentence in the theory of the structure. To check that L_{β_{1}}^{M_{I}} ≡_{k,A} L_{β_{2}}^{M_{II}}, we need to say that, for every Σ_{k} formula φ(x), and for every pair of parameters (x_{1}, x_{2}) ∈ A, M_{I} ⊨ φ(x_{1}) ⟺ M_{II} ⊨ φ(x_{2}). Recall that A is Σ_{2}^{0} (Claim 5.5). Counting quantifiers we see that (⋆_{k}) is Π_{2}^{0}. □

Definition 5.8. S_{k} is the set of formulas that are Boolean combinations of formulas of the form (∀x ∈ z) ψ(z, ȳ), where ψ is Σ_{k}.

Lemma 5.9. If L_{β_{1}}^{M_{I}} ≡_{k,A} L_{β_{2}}^{M_{II}}, then L_{β_{1}}^{M_{I}} and L_{β_{2}}^{M_{II}} satisfy the same S_{k}-sentences with parameters from A substituted for the free variables z and ȳ.

Proof: Let φ be a sentence of the form ∀x ∈ z ψ(x, z, ȳ) with parameters from A where ψ is Σ_{k}. Since φ has no free variables, z and ȳ are parameters from A, and so every x ∈ z is also in A. Since L_{β_{1}}^{M_{I}} ≡_{k,A} L_{β_{2}}^{M_{II}}, we have that for every x ∈ z, L_{β_{1}}^{M_{I}} ⊨ ψ(x, z, ȳ) ⇔ L_{β_{2}}^{M_{II}} ⊨ ψ(x, z, ȳ). So, of course, L_{β_{1}}^{M_{I}} ⊨ φ ⇔ L_{β_{2}}^{M_{II}} ⊨ φ. Finally, if ϕ is a Boolean combination of sentences of this form, then we also have L_{β_{1}}^{M_{I}} ⊨ ϕ ⇔ L_{β_{2}}^{M_{II}} ⊨ ϕ. □

Now we define sets that generalizes C_{M_{I},1} and C_{M_{II},1}. This time, the sets consist of the ordinals in one model (N) that have witnesses for S_{k} formulas with parameters in A that have no witnesses in the other model (M). We will show later that: either there are lots of such witnesses and the set C_{N ,k}^{β_{1},β_{2}} shows that On^{N} \ A has no least element, in which case we have identified the nonwellfounded model, or there are few such witnesses and we can find ordinals satisfying (⋆_{k}).

For β_{1} ∈ M_{I} and β_{2} ∈ M_{II}, let

C_{M_{II},k}^{β_{1},β_{2}} = {β ∈ β_{2} : ∃(x_{1}, x_{2}) ∈ A, ∃φ ∈ S_{k−1}

(∃z ∈ L_{β}^{M_{II}} L_{β_{2}}^{M_{II}} ⊨ φ(z, x_{2})) ∧ (L_{β_{1}}^{M_{II}} ⊨ ¬∃yφ(y, x_{1}))}.

and define C_{M_{I},k}^{β_{1},β_{2}} analogously. As in the case k = 1, these sets are Σ_{2}^{0}.

(R_{I}(2 + k)): For every β_{1}, β_{2}, if (⋆_{k−1})(β_{1}, β_{2}), then C_{M_{II},k}^{β_{1},β_{2}} has no least element.
(R_{II}(2 + k)): For every β_{1}, β_{2}, if (⋆_{k−1})(β_{1}, β_{2}), then C_{M_{I},k}^{β_{1},β_{2}} has no least element.

The conditions (R_{II}3) and (R_{II}3) are Π_{3}^{0}: We already showed that (⋆_{k−1}) is a Π_{2}^{0} property, and, as for k = 1, C_{M_{II},k}^{β_{1},β_{2}} having no least element is Π_{3}^{0} because C_{M_{II},k}^{β_{1},β_{2}} is Σ_{2}^{0}. Also observe that if there are β_{1}, β_{2} satisfying (⋆_{k−1}), then the player playing T h_{α_{n}} cannot loose by a condition (R_{::}(2 + k)).

Lemma 5.10. Suppose that β_{1}, β_{2} satisfy (⋆_{k}). For the sake of definiteness, suppose that β_{1} ∈ M and β_{2} ∈ N. Then

(1) L_{α} ≼_{k} L_{β_{1}} and A ≼_{k} L_{β_{2}}.

(2) α is (k + 1)-admissible.

(3) There exists a descending sequence of N ordinals γ converging down to On^{A} such that L_{γ} ≼_{k} L_{β_{2}}.

Proof: First, we note that {α} is not Σ_{k} definable in L_{β_{1}} with parameters from L_{α}. Suppose otherwise. Since α ∈ M ⊨ T, α is not Σ_{n}-admissible and every β ∈ M is countable in M. Thus there is a Σ_{n}/L_{α} map from ω onto α (possibly with parameters). This defines in L_{α}, a Σ_{n} ordering of ω of order type α. This ordering cannot belong to N as it would then define its wellfounded part. In L_{β_{1}} we can define this ordering with a Σ_{k} formula using the Σ_{k} definition of α and quantification over L_{α}. Since L_{β_{1}}^{M_{I}} ≡_{k,A} L_{β_{2}}^{M_{II}}, this ordering is definable in L_{β_{2}} by the same formula, and hence belongs N. Contradiction.

Now for part (1), since β_{1} is (k-1)-admissible, L_{β_{1}} has a Σ_{k}-Skolem function without parameters (Lemma 3.1). Let H be the Σ_{k}-Skolem hull of L_{α} in L_{β_{1}}. We show that H = L_{α}. Note that this implies that L_{α} ≼_{k} L_{β_{1}} (as desired) and also A ≼_{k} L_{β_{2}} since L_{β_{1}}^{M_{I}} ≡_{k,A} L_{β_{2}}^{M_{II}}.

Suppose that H ⊋ L_{α}. Let L_{γ} be the Mostowski collapse of H, so α < γ ≤ β_{1}. Let α′ be the ordinal in H that is sent to α ∈ L_{γ} by the collapse. As α′ is in the image of the Σ_{k} Skolem function, {α′} is Σ_{k} definable in H with parameters from L_{α} . The same formula then gives a definition of {α} in L_{γ} as the collapse is the identity on members of L_{α}. Thus {α} is Σ_{k} definable in L_{γ} with parameters from L_{α} but clearly

L_{γ}^{M} ≡_{k,A} H ≡_{k,A} L_{β_{1}}^{M}.

So {α} would be Σ_{k} definable in L_{β_{1}}^{M} contradicting our first observation.

(2) Suppose α is not (k + 1)-admissible and so (since every ordinal is countable in M) there is a Π_{k}/L_{α} function f from ω onto α. Since A ≼_{k} L_{β_{2}}, the same formula defining f over L_{α} defines a function from ω onto α in L_{β_{2}}. But then, in N we could define its wellfounded part, L_{α}, for a contradiction.

Now since α is (k + 1)-admissible, there are unboundedly many γ < α such that L_{γ} ≼_{k} L_{α} (Lemma 3.3). For all these γ we also have L_{γ}^{N} ≼_{k} L_{β_{2}}^{N}. The set of γ < β_{2} such that L_{γ}^{N} ≼_{k} L_{β_{2}}^{N} is definable in N. If for some δ ∈ On^{N} ∖ A, the set of γ < δ such that L_{γ}^{N} ≼_{k} L_{β_{2}}^{N} had supremum α, then α would be definable in N and we know it is not. So for every δ ∈ On^{N} ∖ A, there exists γ < δ, γ ∈ On^{N} ∖ A such that L_{γ}^{N} ≼_{k} L_{β_{2}}^{N}. □

Lemma 5.11. If there is a play of our game such that for all i ≤ 2 + k, the resulting real does not satisfy any condition (R_{I}i) or (R_{II}i), then there are β_{1} and β_{2} satisfying (⋆_{k}).

Proof: We already showed that there are β_{1} and β_{2} satisfying (⋆_{1}). The proof now proceeds by induction, so, without loss of generality, we assume that there exists β_{1}, β_{2} satisfying (⋆_{k−1}). We fix such β_{1}, β_{2}.

We claim that no δ ∈ A is in C_{N ,k}^{β_{1},β_{2}}. Consider δ ∈ A and any S_{k−1} formula ∀x ∈ zφ(z, ȳ) and z_{2}, ȳ_{2} ∈ L_{δ}^{N} ⊆ A such that L_{β_{2}}^{N} ⊨ ∀x ∈ z_{2}φ(z_{2}, ȳ_{2}). Since L_{β_{1}} and L_{β_{2}} satisfy the same Σ_{k−1} formulas with parameters from A (by (⋆_{k−1})), L_{β_{1}}^{M} ⊨ ∀x ∈ z_{1}φ(z_{1}, ȳ_{1}), where z_{1} and ȳ_{1} are the images of z_{2}, ȳ_{2} in M. Thus δ ∉ C_{N ,k}^{β_{1},β_{2}} by its definition.

Since the conditions (R_{I}(2 + k)) and (R_{II}(2 + k)) are not satisfied, C_{N ,k}^{β_{1},β_{2}} has a least element δ, necessarily not in A. By clause (3) of the previous lemma, there is a descending sequence δ > γ_{0} > γ_{1} > γ_{2} > ... in On^{N}, converging down to α = On^{A}, such that for each i L_{γ_{i}}^{N} ≼_{k−1} L_{β_{2}}^{N}. We now argue much as for Claim 5.6. We claim that, for some i, L_{α} ≼_{k} L_{γ_{i}}^{N}. If not, there is, for each i, a Π_{k−1} formula φ_{i}(z) with parameters from A and a <_{L}^{N} -least z_{i} ∈ L_{γ_{i}} such that L_{γ_{i}} ⊨ φ_{i}(z_{i}) and z_{i} ∉ A. As L_{γ_{i}}^{N} ≼_{k−1} L_{β_{2}}^{N}, L_{β_{2}}^{N} ⊨ φ_{i}(z_{i}). By thinning out the sequence if necessary, we may assume that z_{i} ∈ L_{γ_{i}}^{N} but z_{i} ∉ L_{γ_{i+1}}^{N}. So {z_{i} : i ∈ ω} is an <_{L}^{N} -descending sequence. Since γ_{i} ∉ C_{N ,k}^{β_{1},β_{2}}, L_{β_{1}}^{M} ⊨ ∃yφ_{i}(y). Let y_{i} be the <_{L}^{M}-least such witness. Since M is wellfounded, the sequence {y_{i} : i ∈ ω} cannot be a <_{L}^{M}-descending sequence. So, there exist i < j such that z_{j} <_{L}^{N} z_{i} but y_{i} <_{L}^{M} y_{j}. Therefore, L_{γ_{j}}^{N} ∈ L_{γ_{j}+1}^{N}is a witness for x showing the truth in L_{β_{2}}^{N}of the S_{k−1} formula

ψ(x) ≡ ∃z ∈ xφ_{j}(z, x) ∧ ∀z ∈ x¬φ_{i}(z, x)

while there is no such witness for the corresponding formula in L_{β_{1}}^{M}. This contradicts our choice of δ as the least element of C_{N ,k}^{β_{1},β_{2}}. Thus we have an i such that L_{α} ≼_{k} L_{γ_{i}}^{N} ≼_{k−1} L_{β_{2}}^{N}.

Now L_{γ_{i}}^{N} is Σ_{k−1} admissible by Lemma 3.4 as L_{β_{2}}^{N} is Σ_{k−2} admissible by (⋆_{k−1}) while α is (even) Σ_{k} admissible by our induction hypothesis and the previous Lemma and so (⋆_{k})(α, γ_{i}) as required. □

Lemma 5.12. The game G satisfies (1) and (2) of Lemma 1.8.

Proof: Since α ∈ M ⊨ T h_{α_{n}}, α cannot be n-admissible. We now know, by Lemma 5.10, that there are no β_{1}, β_{2} satisfying (⋆_{n−1}). So, by Lemma 5.11, there is a k < n such that either (R_{I}(2 + k)) or (R_{II}(2 + k)) holds. Suppose (R_{I}(2 + k)) is the first condition that holds and that I wins the game. Since ∀i < 2 + k, no condition (R_{::}i) holds, there are β_{1}, β_{2} satisfying (⋆_{k−1}). So, (R_{I}(2 + k)) implies that M_{II} is not wellfounded. An analogous argument works if (R_{II}(2 + k)) is the first condition that holds and II wins the game. □

To complete the proof of Lemma 1.8 and so of our main result, Theorem 1.2, we need to show that we can get the same results with a Π_{3,n−1}^{0} game. As now defined, the game is clearly Π_{3,2n+4}^{0} as there are six sets at the beginning and then 2(n − 1) sets of the form R_{I}(2 + k) or R_{II}(2 + k) for k < n. So we need to modify the game a bit. The conditions (R_{I}0), (R_{II}0), (R_{I}1) and (R_{II}1) are Σ_{2}^{0} and so can be absorbed into some later Π_{3}^{0} condition as indicated below. Thus, we first prove that the rest of the game is Π_{3,n−1}^{0}. To decrease the number of alternations, we will change the order of the conditions. We need to make a couple observations: First, if no condition (R_{::}i) for i < 2 + k holds, then only the player playing a nonwellfounded model can loose because of a condition (R_{::}(2 + k)). So it does not matter which of (R_{I}(2 + k)) and (R_{II}(2 + k)) comes first in the list and we can re-order this part of the list as:

..., (R_{I}3),  (R_{I}4), (R_{I}5),  (R_{I}6), ...
(R_{II}3), (R_{II}4),  (R_{II}5), (R_{II}6),

Second, independently of the outcomes of (R_{::}2), only the player playing a nonwellfounded model can loose with a condition (R_{::}3), so it does not matter in which order we place these conditions either. We can now optimize the number of alternations of Π_{3}^{0} conditions as follows:

..., (R_{I}2), (R_{I}3), (R_{I}4), (R_{I}5), (R_{I}6), ...
(R_{II}2), (R_{II}3), (R_{II}4),  (R_{II}5), (R_{II}6),

The first Π_{3}^{0} condition is now (R_{I}2)∨(R_{I}3) which makes I win. We add in the early conditions that are at most Σ_{2}^{0} to make our desired first condition (R_{I}0) ∨ (R_{I}1) ∨ (R_{I}2) ∨ (R_{I}3) which makes I win. The desired second condition is (R_{II}0) ∨ (R_{II}1) ∨ (R_{II}2) ∨ (R_{II}3) ∨ (R_{II}4) which makes II win. Then, for i > 1, the (2i-1)th condition is (R_{I}2i) ∨ (R_{I}(2i + 1)) which makes I win, and the 2ith condition is (R_{II}(2i + 1)) ∨ (R_{II}(2i + 2)) which makes II win. We end the list with (R_{I}(n + 1) if n is even and with (R_{II}(n + 1)) if n is odd. This gives us n many conditions. We finish the description of the game by adding on the the full space 2^{ω} as our nth and last set. The idea here is that this prescribes a win for I when n is even (and so II failed to win at the end by providing a descending chain in M_{I}) and a win for II when n is odd (and so I failed to win at the end by providing a descending chain in M_{II}). This provision includes the conditions for a win required at the last step of our arguments and then enlarges the winning set (for one player) but remember that once we have passed through all the conditions on our list we no longer care how the game is defined. Thus, we have a Π_{3,n−1}^{0} subset of 2^{ω} that defines our game as desired. This completes the proof of Lemma 1.8 and so of Theorem 1.2. □

6. No reversals from Σ_{4}^{1} sentences

In this section we will show that a true (or even consistent) Σ_{4}^{1} sentence T cannot imply Δ_{2}^{1}-CA_{0} over Π_{1}^{1}-CA_{0} even for β-models. At higher levels (n ≥ 2), even with the help of Π_{n}^{1}-CA_{0} or Δ_{n}^{1}-CA_{0} such a T does not imply Δ_{n+1}^{1}-CA_{0} or Π_{n}^{1}-CA_{0}, respectively, even for β-models. We also supply analogs for Σ_{m}^{1} sentences that are theorems of ZFC (or at least consistent with ZFC + V=L(X) for some X ⊆ ω).

Our models for the failure of such implications will all be β-models with second order part of the form ℝ ∩ 𝕃_{δ}. As before, we use the equivalences given by Simpson [2009, VII.5.3] between such models satisfying Π_{n+1}^{1}-CA_{0} or Δ_{n+1}^{1}-CA_{0} and L_{δ} being Σ_{n} nonprojectable or Σ_{n} admissible, respectively for n≥ 1 or n ≥ 2, respectively. The equivalence between Σ_{1} admissibility and Δ_{2}^{1}-CA_{0} works when L_{δ} is a limit of admissibles. In fact, as long as δ is a limit of admissibles (i.e. closed under the operation of going to the next admissible) then, in L_{δ}, any Σ_{n+1}^{1} sentence is equivalent to one that is Σ_{n} for n ≥ 1. (This is essentially Simpson [2009, VII.3.24].) Also note that a Σ_{n}^{1} sentence is true in L_{δ} if and only if it is true in (the β-model of second order arithmetic with sets in) ℝ ∩ 𝕃_{δ}.

Theorem 6.1. If T is a true Π_{3}^{1} sentence, then there is an ordinal δ such that L_{δ} ⊨ T & ∀γ∃β > γ(β is admissible) but L_{δ} is not Σ_{1} admissible and so ℝ∩L_{δ} ⊭ Δ_{2}^{1}-CA_{0}.

Proof: First note that by Shoenfield absoluteness (for Σ_{2}^{1} formulas between V and L), any true Π_{3}^{1} sentence is true in L. Suppose T is ∀A∃B∀CΦ(A, B, C) where Φ is arithmetic. Define functions f_{T} : ℝ^{L}→ON and f_{a} : ON → ON by f_{T} (A) = μα(∃B ∈ L_{α})∀CΦ(A, B, C) and f_{a}(α) = α^{+}, the least admissible greater than α. For any ordinal α closed under f_{a}, ℝ∩L_{α} is a β-model of Π_{1}^{1}-CA Simpson [2009, VII.1.8]. If α is also closed under f_{T} then L_{α} ⊨ T as well by the definition of a β-model (it is absolute for Π_{1}^{1} formulas). Thus there are α such that L_{α} ⊨ T & ∀γ∃β > γ(β is admissible). Let δ_{n} be the n^{th} such ordinal and let δ = ∪δ_{n}. It is clear that L_{δ} ⊨ T & ∀γ∃β > γ(β is admissible). The sequence δ_{n} is clearly Σ_{1} over L_{δ} and so L_{δ} is not Σ_{1} admissible as required to have ℝ ∩ 𝕃_{δ} ⊭ Δ_{2}^{1}-CA_{0}. □

Simpson pointed out that the above proof relativizes, of course, to any real X and so applies to Σ_{4}^{1} sentences by working in L(X) where X is the witness for the Σ_{4}^{1} sentence.

Corollary 6.2. 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}.

Proof: Let δ be defined in L(X) as it was on L in the Theorem but relativized to X where X is the witness to the first quantifier in T. As L_{δ}(X) is closed under the next admissible, ℝ∩L_{δ}(X) is a β-model of Π_{1}^{1}-CA_{0} + Π_{∞}^{1}-TI_{0} as well as T. □

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

Proof: Borel-DET is equivalent to a Π_{3}^{1} sentence over Π_{1}^{1}-CA_{0}. The sentence says that for every Borel code A there is a strategy f such that, for every C, the result of applying f to C is in the set coded by A. (The only thing to point out is that being a Borel code is Π_{1}^{1} and, assuming Π_{1}^{1}-CA_{0} (which actually follows in RCA_{0} from (Σ_{1}^{0} ∧ Π_{1}^{0})-DET), membership in the set coded is Δ_{1}^{1} by Simpson [2009, V.3.3-4]). □

Indeed, if a Σ_{4}^{1} sentence T is even consistent with ZFC then it is true in some model M of ZFC and so also in L^{M}(X) for some X ∈ M within which we can carry out the proof of Theorem 6.1. Thus all the proof theoretic nonimplications of Corollary 6.2 apply to such T as well.

An often used measuring rod for determinacy assumptions as in Martin [n.d.] and Welch [2009] is associating a class Γ with the least ordinal δ such that L_{δ} ⊨ Γ-DET. The proof of Theorem 6.1 shows that, by the standards of admissibility, such ordinals are not themselves large. The following Proposition captures this version of our results. It relativizes to Σ_{4}^{1} sentences true in L (e.g. theorems of ZFC) although not literally to all true ones.

Proposition 6.4. If T is a true Π_{3}^{1} sentence which implies Π_{1}^{1}-CA_{0} such as Γ-DET for any of the standard classes of the Borel hierarchy from Σ_{1}^{0} ∧ Π_{1}^{0} up to the class of all Borel sets, then, the least δ such that L ⊨ Γ-DET, while a limit of admissibles, is not itself Σ_{1} admissible. Indeed, the Δ_{1} projectum of δ is ω.

Proof: Let T be ∀x ⊆ ω∃y ⊆ ω∀z ⊆ ω[ϕ(x, y, z)]. First note that, in L_{δ}, every β is countable. If not, then there is a least β < δ which is not countable in L_{δ}. In particular no new subsets of ω appear between L_{β} and L_{δ}. Thus any Π_{∞}^{1} sentence true in L_{δ} is true in L_{β} for a contradiction to the leastness of δ. Thus every L_{β} for β < δ is coded as a subset of ω in L_{δ} and so the closure of ℝ ∩ 𝕃_{δ} under Π_{1}^{1} comprehension implies that L_{δ} is closed under the next admissible and so is a limit of admissibles.

Next, consider the function f which takes a subset x of ω in L_{δ} to the least ordinal γ such that there is an α < γ with α^{+} < γ as well and a subset y of ω in L_{α} such that L_{α}^{+} ⊨ ∀z ⊆ ω[ϕ(x, y, z)] (or equivalently ∀z ⊆ ω[ϕ(x, y, z)]). As L_{δ} ⊨ T and is closed under the next admissible, this function is total on L_{δ} and obviously Δ_{0}. We can then define the total Δ_{0} map h taking ν to the least γ such that f(x) ∈ L_{γ} for every x ⊆ ω in L_{ν}. If γ_{0} = ω and γ_{n+1} = h(γ_{n}) then γ = ∪γ_{n} ≤ δ. It is clear that L_{γ} ⊨ T and so γ = δ which is therefore, not only not admissible but actually has a total Σ_{1} map from ω cofinal in it. As every β < δ is countable in L_{δ}, these countings (of the γ_{n}) can be combined with the cofinal map n ↦ γ_{n} to produce the desired one-one Σ_{1} map from all of ω onto L_{δ}. □

We can actually say more than Theorem 6.1 about the reverse mathematical weakness of true Π_{3}^{1} (or Σ_{4}^{1}) sentences. True Π_{3}^{1} sentences T don’t help to prove higher levels of comprehension.

Proposition 6.5. If T is a true Π_{3}^{1} sentence then, for each n ≥ 1, there is an ordinal α which is Σ_{n} admissible, a limit of Σ_{n} admissibles, Σ_{n} projectable and satisfies T.

Proof: Choose α such that L_{α} is the Σ_{n} Skolem hull of ω in L_{ω_{1}} under the standard Σ_{n} Skolem function. (Note that any Σ_{n} hull of L_{ω_{1}} is transitive since every ordinal is countable in L_{ω_{1}}.) Thus L_{α} is a Σ_{n} elementary substructure of L_{ω_{1}} ⊨ T. It is Σ_{n} admissible by Lemma 3.4 and is the Σ_{n} Skolem hull of ω in L_{α} as well and so Σ_{n} projectable into ω.

If n ≥ 2, it is immediate that L_{α} satisfies the Π_{3}^{1} formula T. For n = 1 we have to be a bit more careful. Suppose T = ∀x∃y∀zϕ(x, y, z). Consider any x ∈ L_{α}. L_{ω_{1}} ⊨ ∃y(L_{δ} ⊨ ∀zϕ(x, y, z)) where δ is the second admissible after x and y appear in L. Thus there is such a y ∈ L_{α}. To conclude, note that if it is not the case that ∀zϕ(x, y, z) then there would be a counterexample z inside L_{δ} (actually definable over the first admissible after x and y). □

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

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

As before, the Proposition and its first Corollary hold for true Σ_{4}^{1} sentences by working in L(X) where X is the witness for the first existential quantifier.

We complete the picture of the powerlessness of true Π_{3}^{1} (Σ_{4}^{1}) sentences in the sense of reverse mathematics presented in Corollaries 6.2 and 6.6 by showing that they do not help Π_{n}^{1}-CA prove Δ_{n+1}^{1}-CA_{0} even for β-models.

Proposition 6.8. If T is a true Π_{3}^{1} sentence then, for each n ≥ 1, there is an ordinal α which is Σ_{n} nonprojectable, satisfies T but is not Σ_{n+1} admissible.

Proof: Let γ_{j} be the j^{th} ordinal δ such that L_{δ} ⪯_{n} L_{ω_{1}} and L_{δ} ⊨ T. Let γ = ∪γ_{j} and so L_{γ_{j}} ⪯_{n} L_{γ} ⪯_{n} L_{ω_{1}} for each j. In addition, L_{γ} ⊨ T as for any x ∈ L_{γ}, x ∈ L_{γ_{j}} for some j and the witness for x verifying T in L_{γ_{j}} is one in L_{γ} since, as Σ_{1} elementary substructures of L_{ω_{1}}, both are β-models. In particular, L_{γ} is Σ_{n} admissible by Lemma 3.4.

First note that L_{γ} is not Σ_{n} projectable. The point here is that if β < γ and θ defines a Σ_{n} subset of β over L_{γ} then for some j, γ_{j} is larger than β and all parameters in θ are also in L_{γ_{j}}. For such a j, the Σ_{n} definition θ defines the same subset of β over L_{γ_{j}} as over L_{γ}. The subset is then in L_{γ} as required.

Finally, γ is not Σ_{n+1} admissible as the sequence γ_{j} is definable by recursion over L_{γ} by a Σ_{n+1} formula. γ_{j} is the j^{th} ordinal δ such that L_{δ} ⪯_{n} L_{γ} (as L_{γ} ⪯_{n} L_{ω_{1}} and so this condition is the same as L_{δ} ⪯_{n} L_{ω_{1}}) and L_{δ} ⊨ T. To say that L_{δ} ⪯_{n} L_{γ} is to say that for every c ∈ L_{δ} and every Σ_{n} formula ϕ(cx), L_{γ} ⊨ ϕ(c) → L_{δ} ⊨ ϕ(c). By the Σ_{n} admissibility of L_{γ} this is equivalent to a Π_{n} formula and so its negation to a Σ_{n} one. Thus the sequence γ_{j} is Σ_{n+1} as required. □

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

Once again this Proposition and Corollary generalize to true Σ_{4}^{1} sentences by relativization. More generally, the results of this section can be suitably generalized to Σ_{m}^{1} formulas T which are theorems of ZFC or at least consistent with ZFC + V=L(X) for some subset X of ω as they are then true in a model M of V = L(X) and so in L_{(ω_{1})^{M}} (X). The proofs are essentially the same beginning with the fact that T is true in L_{ω_{1}}(X) (of a model M).

Corollary 6.10. If, for m > 4, T is a Σ_{m}^{1} theorem of ZFC (or is even consistent with ZFC +V = L(X) for some subset X of ω) and n ≥ m−2, then Π_{n−1}^{1}-CA + T + Π_{∞}^{1}-TI_{0} ⊬ Δ_{n}^{1}-CA_{0} and Δ_{n}^{1}-CA +T + Π_{∞}^{1}-TI_{0} ⊬ Π_{n}^{1}-CA_{0}. The proofs follow those of Theorem 6.1 (with Corollary 6.2) and Proposition 6.5 (with Corollary 6.6), respectively.

We close by pointing out that the results of this section are optimal in terms of the quantifier complexity of theorems that cannot imply Π_{n}^{1}-CA_{0} or even Δ_{n}^{1}-CA_{0}.

Remark 6.11. For n ≥ 1. there is a Π_{n+2}^{1} theorem T of second order arithmetic that implies Π_{n}^{1}-CA_{0} (and so Δ_{n}^{1}-CA_{0}) over RCA_{0}. The sentence T says that for every Π_{n}^{1} formula ∀Zψ(n, Z, A) and for every choice of parameter A, there is an X such that ∀n(n ∈ X^{[0]} → ∀Zψ(n, Z, A)) & ∀n(n ∉ X^{[0]} → ¬ψ(n, X^{[n+1]}, A)).

References

[1] Barwise, J. [1975], Admissible Sets and Structures, Perspectives in Mathematical Logic, Springer-Verlag, Berlin.

[2] Devlin, K. J. [1984], Constructibility, Perspectives in Mathematical Logic, Springer-Verlag, Berlin.

[3] Foreman, M. ed. [2000], Descriptive Set Theory and Dynamical Systems, Cambridge University Press, Cambridge.

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

[5] Friedman, H. [1975], Some systems of second order arithmetic and their use, Proceedings of the International Congress of Math., Vancouver 1974, v. 1, Can. Math. Congress, 1975, 235-242.

[6] Kechris, A. [1995], Classical Descriptive Set Theory, Graduate Texts in Mathematics 156, Springer-Verlag, New York.

[7] Kechris, A. and Becker, H. [1996], The Descriptive Set Theory of Polish Group Actions, Cambridge University Press, Cambridge.

[8] Kechris, A. and Louveau, A. [1987], Descriptive Set Theory and the Structure of Sets of Uniqueness, London Math. Soc. Lect. Notes 128, Cambridge University Press, Cambridge.

[9] Kechris, A. and Miller, B. D. [2004], Topics in orbit equivalence, Lecture Notes in Mathematics 1853, Springer, New York.

[10] Kuratowski, K. [1958], Topologie v.1, Państwowe Wydawnidwo Naukowe, Warsaw, English translation 1966.

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

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

[13] Martin, D. A. [1975], Borel Determinacy, Ann. Math. 102, 363-371.

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

[15] Martin, D. A and Steel, J. R. [1989], A proof of projective determinacy. Journal of the American Mathematical. Society 2, 71–125.

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

[17] 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., LNS, Institute for Mathematical Sciences, National University of Singapore, World Scientific, Singapore, 333-353.

[18] Moschovakis, Y. N. [2009], Descriptive Set Theory: Second Edition, Mathematical Surveys and Monographs 155, AMS, Providence.

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

[20] 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.

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

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

[23] Tanaka, K. [1990], Weak axioms of determinacy and subsystems of analysis I: Δ_{2}^{0} games), Zeitschr. f. math. Logik und Grundlagen d. Math. 36, 481-491.

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

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

[26] Woodin, H. [1988], Supercompact cardinals, sets of reals, and weakly homogeneous trees, Proceedings of the. National Academy of Sciences of the U.S.A. 85, 6587–6591.

Department of Mathematics, University of Chicago, 5734 S. University ave., Chicago, IL 60637, USA

E-mail address: antonio@math.uchicago.edu

Department of Mathematics, Malott Hall, Cornell University, Ithaca NY 14853 USA

E-mail address: shore@math.cornell.edu
URL: www.math.uchicago.edu/~antonio
URL: http://www.math.cornell.edu/~shore/