Long Borel Games
J. P. Aguilera


[2010]Primary: 03E15, 03E60. Secondary: 03E45, 03E35, 03D60, 91A44

Institute of Discrete Mathematics and Geometry, Vienna University of Technology. Wiedner Hauptstraße 8–10, 1040 Vienna, Austria.
aguilera@logic.at




Long Borel Games





J. P. Aguilera











Institute of Discrete Mathematics and Geometry

Vienna University of Technology

Wiedner Hauptstrasse 8-10

1040 Vienna, Austria.





We study games of length ω^2 with moves in ℕ and Borel payoff.  These are, e.g., games in which two players alternate turns playing digits to produce a real number in [0,1] infinitely many times, after which the winner is decided in terms of the sequence belonging to a Borel set in the product space [0,1]^ℕ.

The main theorem is that Borel games of length ω^2 are determined if, and only if, for every countable ordinal α, there is a fine-structural, countably iterable model of Zermelo set theory with α-many iterated powersets above a limit of Woodin cardinals.



Long Borel Games
    J. P. Aguilera
    December 30, 2023 (compiled)
================================






§ INTRODUCTION

Given a Borel subset A of the Hilbert space ℓ^2, define a two-player perfect-information, zero-sum game in which Player I and Player II alternate turns playing digits x^0_i ∈{0,1,,9} infinitely often, giving rise to a real number 

    x^0 = ∑_i = 0^∞x^0_i/10^i+1.

Afterwards, they continue alternating turns to produce real numbers x^1, x^2, and so on. To ensure that the sequence belongs to ℓ^2,
we normalize, e.g., by setting

    y^i = x^i/i+1.

Player I wins the game if, and only if, y⃗∈ A; otherwise Player II wins.
These are games of transfinite length ω^2. (Recall that ω denotes the order-type of the natural numbers.)
It is a natural question whether these games are determined, i.e., whether one of the players has a winning strategy. 

Given A⊂ [0,1], the Gale-Stewart game on A is defined as follows: two players, I and II, alternate infinitely many turns playing digits x(0), x(1),, as before. This play gives rise to a real number x ∈ [0,1] as before.
Player I wins the game if, and only if, x ∈ A; otherwise, Player II wins. We say that a set A⊂ℝ is determined if the game associated to A ∩ [0,1] is determined.

Our games of length ω^2 can be recast in terms of Gale-Stewart games: given A ⊂ [0,1], players I and II alternate infinitely many turns playing digits x^0_0, x^0_1, x^0_2,; afterwards, they alternate infinitely many turns playing digits x^1_0, x^1_1, x^1_2,; and so on. Let 

    ρ:ℕ×ℕ→ℕ

be a Borel bijection, e.g., 

    (i,j)↦1/2(i+j)(i+j+1) + j.

Put

    x = ∑_j = 0^∞∑_i = 0^∞x^j_i/10^ρ(i,j)+1.

Player I wins the game if, and only if, x ∈ A; otherwise, Player II wins.

A third and most useful way of studying these games is in terms of the Baire space ℕ^ℕ: given a Borel A ⊂ℕ^ℕ, two players alternate ω^2 many turns playing elements of ℕ and produce an infinite sequence {x_i:i∈ℕ}, with x_i ∈ℕ^ℕ. As before, by means of a Borel bijection, this sequence is identified with an element x∈ℕ^ℕ. Player I wins the game if, and only if, x∈ A; otherwise, Player II wins. It is this the way in which we will speak of games of length ω^2 hereafter. Every Polish space is a continuous image of ℕ^ℕ and Borel sets have enough closure properties that  these forms of determinacy are all equivalent. 



——




Zermelo set theory (𝖹) was introduced in 1908 by E. Zermelo with the goal of reducing Cantor and Dedekind's theories to a small collection of principles. It, together with A. Fraenkel and T. Skolem's refinements, resulted in Zermelo-Fraenkel set theory (). In this article, 𝖹 consists of the axioms of extensionality, separation, power set, pairing, union, foundation, and infinity; and  consists of 𝖹, plus the axiom(s) of replacement. 𝖹𝖢 and  are the results of adding the Axiom of Choice to 𝖹 and , respectively.

Although 𝖹𝖢 is a powerful theory in which a great deal of mathematics can be formalized, there are many examples of theorems that cannot be proved without the use of the axiom of replacement. An early example of this was that of Borel determinacy, i.e., whether all Borel subsets of ℝ are determined.


Suppose A is Borel. Then A is determined.


Even before Martin's Borel determinacy theorem had been proved, it was known that any proof would need essential use of the axiom of replacement:


Borel determinacy is not provable in 𝖹𝖢.


Friedman's work showed that any proof of Borel determinacy would require the use of arbitrarily large countable iterations of the power set operator, and Martin's work showed that this suffices. A convenient slogan is that Borel determinacy captures the strength of countably iterated powersets. 

It is known that one cannot hope to prove the determinacy of any reasonable class of non-Borel games within ; however, one can extend  by very natural large cardinal axioms, or strengthenings of the axiom of infinity, and use them to prove the determinacy of games on the natural numbers. These connections between large cardinal axioms and infinite games have been the focus of extensive study for decades; some of the most famous results include Martin's <cit.> proof of analytic determinacy, Martin and Steel's <cit.> proof of projective determinacy, and Woodin's <cit.> proof of the Axiom of Determinacy in L(ℝ), the smallest model of  containing all reals and all ordinals. (Recall that the Axiom of Determinacy is the assertion that every Gale-Stewart game (of length ω) is determined. By a result of Mycielski and Steinhaus, it is inconsistent with the Axiom of Choice.)
More specifically, Woodin showed that if there are infinitely many Woodin cardinals and a measurable cardinal greater than them, then the Axiom of Determinacy holds in L(ℝ). The measurable cardinal is necessary, in the sense that the existence of infinitely many Woodin cardinals does not imply that the Axiom of Determinacy holds in L(ℝ).

Our main theorem shows that Borel determinacy for games of length ω^2 captures the strength of countably iterated powersets above a limit of Woodin cardinals.[In the interest of expedience, one may define  the statement there are infinitely many Woodin cardinals” to mean the following in 𝖹𝖢: there is an infinite sequence (δ_0,δ_1,) of cardinals such that for each i∈ℕ, V_δ_i is a model of  and δ_i is a Woodin cardinal in V_δ_j whenever i<j.]

The following are equivalent over :


  * Borel determinacy for games of length ω^2;

  * For every countable α, there is a countably iterable extender model of 𝖹𝖢 satisfying “V_λ+α exists, where λ is a limit of Woodin cardinals.”


Hence, Borel determinacy for games of length ω^2 is a natural example of a theorem whose strength can only be correctly gauged over  in terms of weaker set theories.
The models referred to in Theorem <ref> are fine-structural and built over some x∈ℝ.
As a consequence thereof, we obtain a result on the provability of Borel determinacy for games of length ω^2 similar to the one for short games:

Borel determinacy for games of length ω^2 is provable in the theory  + “there are infinitely many Woodin cardinals,” but not in the theory 𝖹𝖢 + “there are infinitely many Woodin cardinals.”

The first part of Corollary <ref> follows from Theorem <ref>, together with a theorem of Steel <cit.> and a reflection argument. Our proof of Theorem <ref> does not quite go through if one replaces  by 𝖹𝖢 in the statement, although we conjecture that the equivalence is still provable there. Nonetheless, the proof does go through if one replaces  by 𝖹𝖢, together with the assumption that there are enough ordinals[It suffices to assume that ϑ_α exists for all α<ω_1 (see below).] and, in particular, if one assumes that there are infinitely many Woodin cardinals. This yields the second part of Corollary <ref>.

The main step towards proving Theorem <ref> is a “shortening” result like the one in <cit.>.
It shows that Borel games of length ω^2 are determined if, and only if, those in a much more complicated class of games of length ω are. Recall the definition of Gödel's constructible hierarchy over ℝ: L_0(ℝ) is V_ω+1 (the collection of all sets of von Neumann rank ≤ω), L_α+1(ℝ) is the collection of all sets definable over L_α(ℝ) from parameters in L_α(ℝ), and L_λ(ℝ) = ⋃_α<λL_α(ℝ) if λ is a limit ordinal.


Let ϑ be the least ordinal such that for every countable ordinal α, there is ξ<ϑ such that L_ξ(ℝ) satisfies V_α exists.”
The following are equivalent:


  * Borel determinacy for games of length ω^2;

  * L_ϑ(ℝ) is a model of the Axiom of Determinacy.


It is independent of  whether L_ϑ(ℝ) is a model of the Axiom of Determinacy or of the Axiom of Choice (or neither), but it is never a model of Zermelo set theory, since 𝒫(ℝ) ∩ L_ϑ(ℝ)∉L_ϑ(ℝ).


The use of large cardinals is essential in proofs of determinacy by Gödel's second incompleteness theorem, for one can often prove the existence of inner models of set theory satisfying forms of the axiom of infinity from the determinacy of infinite games. 
Results of this form include Friedman's Theorem <ref> and Theorem <ref>, but also Harrington's <cit.> work on analytic determinacy and Woodin's work in projective determinacy and the Axiom of Determinacy (see e.g., <cit.> and <cit.>). More recent work in this direction includes that of Steel <cit.>, Montalbán-Shore <cit.>, Welch <cit.>, Trang <cit.>, and others. In order to obtain equivalences such as Theorem <ref>, as opposed to equiconsistency results, one needs to involve the techniques of the core model induction. Since we shall be confined within L(ℝ), the arguments we will need can be found in Steel-Woodin <cit.>. Other expositions include Schindler-Steel <cit.> and Wilson <cit.>.

The determinacy of games of countable length with analytic (or projective) payoff has been proved by Neeman <cit.> from assumptions that are very likely optimal. The optimality for games of sufficiently closed length has been verified by Trang <cit.> and by Woodin, in unpublished work.
Reversals of determinacy hypotheses for projective games of length ω^2 were obtained in <cit.> and for clopen games in <cit.>. Games of length ω^2 were first considered in print by Blass <cit.>. Let us finish this introduction with some open questions:


Is the equivalence in Theorem <ref> provable within 𝖹𝖢?



What is the consistency strength of Borel determinacy for games of length ω^2+ω?



What is the consistency strength of determinacy for games of length ω with payoff in the smallest σ-algebra containing the projective sets?





——




The article is structured as follows: Theorem <ref> is proved in Section <ref>.
The proof is purely descriptive-set– and recursion-theoretic. It involves the use of model games which incorporate elements from the constructions in Martin and Steel <cit.>, Friedman <cit.>, and Martin (see <cit.>).
A tool used in the proof (Lemma <ref>) is a method of describing  initial segments of the L(ℝ)-hierarchy by games in which two players determine the truth of a statement in L(ℝ) by challenging each other's claims with auxiliary games. This lemma is proved in Section <ref>.
The article ends with Section <ref>, in which localizations of arguments from inner model theory are shown to imply Theorem <ref>, starting from Theorem <ref>.




  
Acknowledgements We would like to thank Sandra Müller, Grigor Sargsyan, and Hugh Woodin for engaging in fruitful discussions with us. This work was partially suported by a grant from the Austrian Science Fund.



§ PRELIMINARIES

We shall use notions from descriptive set theory and ordinal recursion theory freely. We refer the reader to Moschovakis' book <cit.> and to Barwise's book <cit.> for background. Additional background, as well as history, can be found in the chapters from the Handbook of Set Theory by Schindler-Zeman <cit.>, Steel <cit.>, and Koellner-Woodin <cit.>.

Our notation is standard.
Among the usual abuses of notation in which we shall engage are the identification of ℝ with the Baire space ℕ^ℕ, as well as the identification of Gale-Stewart games with other infinite zero-sum games without explicitly transforming the payoff set into that of a Gale-Stewart game. We also identify ℝ with V_ω+1. In particular, natural numbers are real numbers. 

If σ is a strategy for a short game (i.e., one of length ω) on ℕ, then we may alternately regard σ as a real, as a function on ℕ^ℕ, or as the function on ℝ which to each x∈ℝ assigns the unique y which results by playing against x in a way consistent with σ. If σ and τ are two strategies, σ*τ denotes the result of facing them off against each other.

We will often need to consider games of length ω with moves in ℝ. These can be considered as games of length ω^2 on ℕ in which Player I's moves are ignored throughout the (2n+1)th block of ω-many moves, and Player II's moves are ignored throughout the (2n)th block of ω-many moves. In particular, if Borel games of length ω^2 are determined, then so too are Borel games of length ω with moves on ℝ; the converse is not true, as the latter statement is provable in  (by Martin's proof of Borel determinacy). 

At no point other than Section <ref> will we need any inner model theory, but we will make use of simple fine-structural facts about L(ℝ). We make use of the Jensen hierarchy over the reals (see <cit.>). Recall its definition given by:

    J_0(ℝ) 
       = V_ω+1
    
    J_α+1(ℝ) 
       = closure of J_α(ℝ) ∪{J_α(ℝ)} under rudimentary functions
    
    J_λ(ℝ) 
       = ⋃_α<λJ_α(ℝ),  for limit λ.


The following definition is perhaps not standard, but will suffice for our purposes:

Let α and β be ordinals. We say that the projectum of J_α(ℝ) is V_β if β<α and β is the least ordinal such that

    V_β+1∩(J_α+1(ℝ) ∖ J_α(ℝ))≠∅.


Let β be such that V_β is the projectum of J_α(ℝ). We say that J_α(ℝ) projects to V_β. Since ℝ always belongs to J_α(ℝ), β is at least ω+1. If β = ω+1, we say that J_α(ℝ) projects to ℝ. If J_α(ℝ) does not project to ℝ, then every subset of ℝ definable over 𝒫(ℝ)^J_α(ℝ) belongs to J_α(ℝ), so

    (ℕ,ℝ,𝒫(ℝ) ∩ J_α(ℝ))

is a model of third-order arithmetic.

If the projectum of J_α(ℝ) is not defined, then J_α(ℝ) contains all definable subsets of V_β^J_α(ℝ) for all β<α, and so 

    J_α(ℝ).



Suppose that the projectum of J_α(ℝ) is V_β and ω+1<β. Then, there is a surjection

    ρ:V_β∩ J_α(ℝ)↠ J_α(ℝ)

in J_α+1(ℝ).

This proof is similar to those in <cit.> and <cit.>. 
Suppose that the projectum of L_α(ℝ) is V_β, with ω+1<β, and let ϕ be a formula in the language of set theory such that for some a ∈ J_α(ℝ), we have

    {x ∈ J_α(ℝ): J_α(ℝ)ϕ(a,x)}∈ V_β+1∩(J_α+1(ℝ) ∖ J_α(ℝ)).

Call the set just defined A. 
Suppose that ϕ is Σ_n. In L(ℝ), every set is definable from a real and ordinal parameters, in fact, by Lemma 1.4 of <cit.>, there are surjections 

    f_β: [ω·β]^<ω×ℝ↠ J_β(ℝ)

which are uniformly Σ_1 over J_β(ℝ). Thus, we may assume that a ∈ℝ by replacing n with a bigger natural number if necessary, and replacing ϕ(a,x) with the formula

    ϕ(f_α(β⃗,a),x) holds for the least tuple β⃗ such that the set 
    {x: ϕ(f_α(β⃗,a),x)} does not exist.


Since ω+1 < β, Lemma 1.7 and Theorem 1.16 of <cit.> imply that J_α(ℝ) has a _n Skolem function, i.e., that there is a partial map

    h: J_α(ℝ)×ℝ→ J_α(ℝ)

which is Σ_n in a parameter p ∈ J_α(ℝ) such that whenever S is a nonempty Σ_n set over J_α(ℝ) with a parameter q ∈ J_α(ℝ), then

    h(q,x) ∈ S  for some  x∈ℝ.

Thus, one can define the Σ_n Skolem hull of J_α(ℝ) with a Σ_n formula using parameters from J_α(ℝ). Let p be the parameter defining h and

    ℋ = Hull^J_α(ℝ)_Σ_n(V_β∩ J_α(ℝ), {p}).

By Lemma 1.9 of <cit.>,


  * ℋ is a Σ_n-elementary substructure of J_α(ℝ), and

  * ℋ = f[X^<ω] for some partial map f which is Σ_n over ℋ with parameters in ℋ, where X = (V_β∩ J_α(ℝ)) ∪{p}.

The latter conclusion easily implies that in fact 

    ℋ = f[X^<ω]
 
for some partial map f as above, where X = V_β∩ J_α(ℝ).

Since ω+1<β, ℋ contains all reals, so, by condensation, there is γ≤α such that the transitive collapse of ℋ is J_γ(ℝ). Let

    π:J_γ(ℝ) ↠ℋ

be the collapse embedding, which has critical point ≥β. By definition, A ∈ V_β+1, so

    if J_α(ℝ)ϕ(a,x), then x ∈ V_β.

Since V_β∩ J_α(ℝ)⊂ J_γ(ℝ) and a ∈ℝ, we have for every x∈ J_γ(ℝ),

    J_α(ℝ)ϕ(a,x) 
        if, and only if,  J_α(ℝ) x ∈ V_π(β)∧ϕ(a,x),
        if, and only if,  J_γ(ℝ) x ∈ V_β∧ϕ(a,x).

This is not entirely straightforward, as V_β∩ J_α(ℝ) need not be an element of J_γ(ℝ) (or of J_α(ℝ)), but for each η, the set

    {x ∈ J_η(ℝ): x  has rank β}

is uniformly Δ^J_η(ℝ)_1(β) (provided β<η). Thus, the set A is definable over J_γ(ℝ), which implies that γ = α.  Using π and the function f from above, one obtains a partial surjection from V_β∩ J_α(ℝ) onto J_α(ℝ) which is definable over J_α(ℝ) by a Σ_n formula with parameters. This easily translates into a Π_n+1 (with parameters) total surjection f^* from V_β∩ J_α(ℝ) onto J_α(ℝ). Clearly f^* belongs to J_α+1(ℝ), which completes the proof.





§ DETERMINACY AND L(ℝ)

If A⊂ℝ×ℝ is a set and x∈ℝ, we define
A_x = {y∈ℝ: (x,y) ∈ A}
and

    ^ℝA 
       = {x∈ℝ:  Player I has a winning strategy in the game 
              with payoff A_x and moves in ℝ}.

The set ^ℝA is defined similarly for A a subset of other spaces, such as ℝ^n. Letting
^ℝ^1_1 = {^ℝA: A is Borel},
we write

    γ^1_1 = sup{α:  there is a prewellordering of ℝ in ^ℝ^1_1 of rank α}.

The ordinal γ^1_1 is usually denoted by δ_^ℝ^1_1. ^ℝ^1_1 γ^1_1[Note that ^ℝΔ^1_1 is a much smaller class than Δ_1^L(ℝ) = Δ_^ℝΠ^1_1, the class of all sets A such that both A and its complement belong to ^ℝΠ^1_1.]

 
𝒫(ℝ)∩ L_γ^1_1(ℝ)⊂^ℝ^1_1.

The proof of Lemma <ref> will be delegated to the following section. For now, let us assume that it is true.


Under determinacy, Lemma <ref> can be proved easily by appealing to general Wadge theory. The proof that we shall provide, however, is direct, and goes through in e.g., +.



ϑ_α
We denote by ϑ_α the least ordinal ξ such that
L_ξ(ℝ) is a model of 

    + Separation +  V_α exists.”

We also define 

    ϑ = sup_α<ω_1ϑ_α.



The main result of this section is the following: 


The following are equivalent:


  *  Borel determinacy for games of length ω^2;

  *  L_ϑ(ℝ).



We need some preliminaries. We will work with structures in the language of set theory with additional constants {ẋ_i:i∈ℕ} (which will be interpreted as real numbers). We fix:


  * a formula θ(·,·,·) in the language of set theory defining in L(ℝ) an ℝ-parametrized sequence of wellorderings the union of whose domain is L(ℝ) (e.g., the one given by Lemma 1.4 of <cit.>), and

  * injective functions n(·) and m(·) assigning natural numbers to formulae in the extended language in such a way that their ranges are recursive and disjoint and whenever ẋ_i occurs in a formula ϕ, then i < m(ϕ) and i<n(ϕ).


Let us begin with an observation:



Suppose that M is a model of  and M contains an ordinal a isomorphic to α. Then (V_a)^M (which need not belong to M) is wellfounded.

Let us identify the wellfounded part of M with its transitive collapse. In particular, we write α for the ordinal a in the statement of the lemma. Although (V_α)^M need not belong to M, it is Δ_1-definable (with parameters) over M, so given x ∈ (V_α)^M, M can determine the rank of x. Thus, if x ∈^M y and y ∈^M (V_α)^M, then

    rank^M(x) < rank^M(y) < α.

Since α is wellfounded, (V_α)^M must be too.



For every α<ω_1, let T_α be the set of all (real numbers coding) complete and consistent theories T in the language of set theory with additional constants {ẋ_i:i∈ℕ} such that 


  * T extends + ℝ exists” + V = L(ℝ) + {ẋ_i ∈ℝ:i∈ℕ},

  * T contains Skolem schemata of the forms

    ∃ x∈ℝ ϕ(x) 
       →ϕ(ẋ_n(ϕ)),
    ∃ x ϕ(x) 
       →∃ x ∃β∈ (θ(β,ẋ_m(ϕ), x) ∧ϕ(x));


  * all models of T contain an ordinal isomorphic to α.

Then T_α is a Borel subset of ℝ.

Given a complete and consistent theory T in the language of set theory extending , we say that M is a term model of T if M is the natural =-quotient of the collection of all formulae ϕ with one free variable such that

    there is a unique x satisfying ϕ(x)”∈ T,

with the membership predicate and the constants ẋ_i having the obvious interpretations. Suppose that T is as in the statement of the lemma and let M be the term model of T. It follows from the Tarski-Vaught criterion and the fact that M satisfies the Skolem schemata that M is in fact a model of T. Moreover, it embeds into every model of T, so every model of T contains an isomorphic copy of α+1 if, and only if, M does.

Fix some wellordering ≼ of ℕ of length α+1. Thus, the following are equivalent:


  * T ∈ T_α;

  * there is a term model M of T, and a function f such that


  * the range of f is the field of ≼,

  * the domain of f is the set of ∈^M-predecessors of an ordinal of M,

  * for all y∈(f), f(y) is the ≼-least number greater than f(x) for every x ∈^M y;


  * for all term models M of T, there is an M-ordinal m ∈ M such that for all functions f, if


  * the range of f is contained in the field of ≼,

  * the domain of f is the set of ∈^M-predecessors of (m+1)^M,

  * for all y∈(f), f(y) is the ≼-least number greater than f(x) for every x ∈^M y,

then f(m) is the ≼-largest number.


Therefore T_α is Borel.



ϑ is least such that

    L_ϑ(ℝ) Borel games on ℝ are determined.”


Clearly ϑ has this property, for L_ϑ(ℝ) has initial segments with enough iterated powersets of the real numbers for Martin's proof <cit.> to go through; moreover, the existence of winning strategies for games on ℝ is upwards absolute between transitive sets that contain ℝ. 

Let us verify that ϑ is the least such ordinal. We need to employ model games such as the one of <cit.>.
A similar application of the techniques of <cit.> was used in <cit.> to produce iterable models of  with Woodin cardinals. Fortunately, our situation is simpler inasmuch as we do not need to construct models with large cardinals (yet); the drawback is that we cannot even ask for wellfoundedness in the payoff. One deals with this issue as in Martin's reversal of Borel determinacy (unpublished, but see the exercise in pp. 53–54 of <cit.> for the case of Π^0_4 games on ℕ).

Let α<ω_1 be an infinite successor ordinal. We consider the following game:

    [        I x_0, u_0          x_2, u_1                  ;       II          x_1, v_0          x_3, v_1          ]

Here, Players I and II play a countable sequence of reals {x_i}_i∈ℕ, as well as two countable sequences u,v ∈ 2^ℕ. Fix an enumeration {ϕ_i:i∈ℕ} of all formulae in the language of set theory with added constants {ẋ_i:∈ℕ}. 
We ask of the players that:


  * T_I := {ϕ_i: u_i = 1} is a complete, consistent theory in the expanded language, satisfying the following conditions:


  * T_I extends the theory  + Separation + ℝ exists” +  + V = L(ℝ);

  * T_I contains the statement ẋ_i ∈ℝ for each i∈ℕ, and it contains the statement ẋ_i(n) = m if, and only if, x_i(n) = m;

  * T_I contains the Skolem schemata

    ∃ x∈ℝ ϕ(x) 
       →ϕ(ẋ_n(ϕ)),
    ∃ x ϕ(x) 
       →∃ x ∃β∈ (θ(β,ẋ_m(ϕ), x) ∧ϕ(x));


  * We ask that all models of T_I contain an ordinal isomorphic to α. If so, then by the proof of Lemma <ref>, there must be a formula ϕ_α in the expanded language that defines the αth ordinal in every model of T_I. We demand then that T_I contain the axiom 

    if ϕ_α(x) holds, then V_x exists,”
 
as well as 

    ϕ_α(x) ∧ϕ(a)→ L_a(ℝ) + Separation + V_x exists,”

whenever ϕ is a formula and the formula the unique a satisfying ϕ(a) is an ordinal smaller than α” belongs to T_I.


  * T_II := {ϕ_i: v_i = 1} is a complete, consistent theory in the expanded language with the same requirements as above.

If T_I satisfies the properties above and ℳ is a model of T_I, then the definable closure of {x_i^ℳ:i∈ℕ} in ℳ is an elementary substructure of ℳ isomorphic to the term model of T_I. Denote this model by N_I. In particular, N_I satisfies  + Separation + “V_α exists” and no proper initial segment of N_I does. Similarly for Player II. If the above conditions are met, Player I wins if, and only if, one of the following holds:


  *  N_I is isomorphic to an initial segment of N_II; or

  *  there is an ordinal a of N_I such that L_a(ℝ)^N_I is isomorphic to an initial segment of N_II, but L_a+1(ℝ)^N_I is not.


In either clause, we do not demand that the initial segment of N_II be an element of N_II.


The winning condition is Borel.

Let us momentarily reason in  

    + Separation + ℝ exists” +  + V = L(ℝ).
 
Suppose that J_ξ(ℝ)V_α exists,” for every ordinal ξ. Thus, for every ξ, the projectum of J_ξ(ℝ) is strictly smaller than V_α. By Proposition <ref>, whenever ξ is an ordinal, there is some 

    a ∈ V_α∩ J_ξ+1(ℝ)

such that a
codes J_ξ(ℝ). Now, let N_I and N_II be as in the definition of the game (i.e., suppose that T_I and T_II satisfy the conditions necessary in order for N_I and N_II to be defined). Now, N_I and N_II might have initial segments that satisfy V_α exists,” but they certainly do not have any initial segments satisfying V_α+1 exists,”
so for every initial segment N of either of N_I or N_II of (internal) limit length greater than α, we have

    for all ξ∈^N, there is  a∈ (V_α+1)^N coding  (J_ξ(ℝ))^N.

(One could easily get around this issue by removing the condition that the theories satisfy  + Separation, but we have adpoted the rule because this is the theory used in the definition of ϑ_α.)

Back in the real world, we verify that conditions (<ref>) and (<ref>) are Borel. We will show that it is Borel to check whether the elements of (V_α)^N_I are (up to isomorphism) those of (V_α)^N, for some initial segment N of (V_α)^N_II. This suffices for (<ref>), by the above remark and by replacing α with α+1.
As in the proof of Proposition <ref>, one should bear in mind that (V_α)^N need not be an element of N, but it is definable over N in a Borel way by defining an initial segment of the rank function along a Borel presentation of α; viz., a set x∈ N has rank α in N if, and only if, f(x) = α for some (all) function(s) f such that


  * the range of f is α+1,

  * the domain of f is a subset of N containing x and is transitive (so, in particular, ∈^N is wellfounded in (f)),

  * for all y∈(f), f(y) = sup{f(z):z ∈^N y}. 


Let f_I (in V) be a function assigning to each set in (V_α)^N_I its rank in N_I and f_II be defined similarly. Consider the following Ehrenfeucht-Fraïssé–like game:


  * Player II begins by selecting an ordinal a ∈ N_II. Define N = (J_a(ℝ))^N_II. For the rest of the game, the players attempt to determine whether (V_α)^N_I is equal to (V_α)^N up to isomorphism.

  * During turn 1, Player I selects some x_0 ∈ (V_α)^N_I or some y_0 ∈ (V_α)^N. In the first case, let ξ_0 be least such that x_0 ∈ (V_ξ_0)^N_I; Player II needs to respond with some y_0 ∈ (V_ξ_0)^N. In the second case, let ξ_0 be least such that y_0 ∈ (V_ξ_0)^N; Player II needs to respond with some x_0 ∈ (V_ξ_0)^N_I.

  * During turn n+1, assuming x_n, y_n, and ξ_n have been defined, Player I plays some ξ_n+1 < ξ_n and either some x_n+1∈ (V_ξ_n+1)^N_I such that x_n+1∈^N_I x_n or some y_n+1∈ (V_ξ_n+1)^N such that y_n+1∈^N_II y_n. In the first case, Player II must respond with some y_n+1∈ (V_ξ_n+1)^N such that y_n+1∈^N_II y_n; in the second case, Player II must respond with some x_n+1∈ (V_ξ_n+1)^N_I such that x_n+1∈^N_I x_n.

  * The first player who cannot make a legal move loses the game.

This game can easily be coded by a clopen game of length ω on ℕ with parameters α, N_I,N_II,f_I, and f_II; let us denote it by EF_0(N_I,N_II,f_I,f_II) to emphasize this. If there is an ordinal a ∈ N_II such that (V_α)^N_I = (V_α)^J_a(ℝ)^N_II, then clearly Player II has a winning strategy. Moreover, if there is no such ordinal, then one can easily use the fact that (V_α)^N_I and (V_α)^N_II are wellfounded to construct a winning strategy for Player I. 

There is a problem with this game, viz., that one may also want to consider initial segments of N_II not of the form J_a(ℝ) for a an ordinal of N_II. For this, we define a game EF(N_I,N_II,f_I,f_II) which is like EF_0(N_I,N_II,f_I,f_II), except that Player I begins by selecting an ordinal a_0 of N_I, after which Player II selects a ∈ N_II and they continue as before to determine whether 

    (V_α)^J_a_0(ℝ)^N_I = (V_α)^J_a(ℝ)^N_II.
 An argument like the preceding one shows that Player II has a winning strategy in EF(N_I,N_II,f_I,f_II) if, and only if, (V_α)^N_I = (V_α)^N for some initial segment N of N_II.

Now, one sees that the following are equivalent:


  * the elements of (V_α)^N_I are those of (V_α)^N, for some initial segment N of (V_α)^N_II,

  * there is sequence of surjective functions {f_β:β≤α}  and an initial segment N of N_II such that, identifying the wellfounded parts of N_I and N with their transitive collapses,


  * f_0 maps the empty set to the empty set,

  * for all β≤α, f_β+1: (V_β)^N_I→ (V_β)^N maps each set b to the set {f_β(a): a ∈^N_I b}, in the sense of N,

  * for all limit β≤α, f_β = ⋃_γ<βf_γ


  * for every pair of functions f_I and f_II assigning respectively to each set in (V_α)^N_I and  (V_α)^N_II its rank in N_I and N_II, Player I does not have a winning strategy in the game EF(N_I,N_II,f_I,f_II).

Since EF(N_I,N_II,f_I,f_II) is a clopen game, Player I not having a winning strategy is a ^1_1 condition. It follows that condition (<ref>) is Borel.


Similarly, to prove that (<ref>) is Borel, it suffices to show that it is Borel to check whether there is a ∈ N_I such that 


  * (V_α)^J_a(ℝ)^N_I⊂ (V_α)^N_II

  * (V_α)^J_a+1(ℝ)^N_I⊄(V_α)^N_II

An argument as above shows that the conjunction of these two statements is Borel. This proves the sublemma.


We have shown that the payoff set of the game is Borel. Moreover, it is easily won by Player I in V, for she can play the theory of J_ϑ_α(ℝ) = L_ϑ_α(ℝ) and, e.g., only recursive reals. Recall that ϑ_α is least such that

    J_ϑ_α(ℝ) + Separation + V_α exists.”

Moreover, as long as Player II plays by copying the theory chosen by Player I (and plays arbitrary reals), then every strategy that ensures that Player I will win demands that she play the theory of J_ϑ_α(ℝ). Thus, the theory of J_ϑ_α(ℝ) can be easily computed from ℝ and any winning strategy for Player I. 

Now let ξ be an ordinal such that the game is determined in J_ξ(ℝ). Then J_ξ(ℝ) contains a winning strategy τ for some player. Since J_ξ(ℝ) contains all plays of the game, τ is also a winning strategy in V, so it must be a winning strategy for Player I. Hence, we must have ϑ_α<ξ, since τ cannot belong to J_ϑ_α(ℝ).
Therefore, if J_ξ(ℝ) contains strategies for the game above for each α<ω_1, then it contains every ordinal below ϑ, which is what was to be shown.



Let ξ<ϑ. Then there is a prewellordering of ℝ of length greater than ξ definable by a set in ^ℝ^1_1.

Choose α<ω_1 such that ξ<ϑ_α and let (i,x), (j,y) be two pairs in ℕ×ℝ. The ordinal ϑ_α will play no role in the game other than bounding the complexity of the payoff set.
We consider a two-player game G(α, i,x,j,y) given by

    [        I x_0, u_0                            x_2, u_1                  ;       II                   x_1, v_0                            x_3, v_1                  ;        I                            y_1, t_0                            y_3, t_1         ;       II          y_0, s_0                            y_2, s_1                   ]

Here, I and II play two runs of the game from Lemma <ref> in parallel, except that their roles are reversed in the second game. As before, we suppose fixed an enumeration {ϕ_i:i∈ℕ} of all formulae in the language of set theory with added constants {ẋ_i:i∈ℕ}.  The rules are:


  *  If ϕ_j is not a formula with one free variable and with no constant symbols other than ẋ_0, then Player II loses. 

  *  If ϕ_i is not a formula with one free variable and with no constant symbols other than ẋ_0, then Player I loses. 

  *  Both players have to obey the rules in each subgame.

  *  If so, then Player II has to win the second subgame. Moreover, she must set y_0 = y and the theory played must contain the formula there is a unique ordinal satisfying ϕ_j.”

  *  If so, then Player I has to win the first subgame. Moreover, she must set x_0 = x and the theory played must contain the formula there is a unique ordinal satisfying ϕ_i.”

If all rules thus far have been obeyed, then we declare the winner according to the following rules (here, we identify the theories played with their term models):



  *  Every real played in the first subgame must be played in the second subgame by Player II; otherwise, Player I wins.

  *  Every real played in the second subgame must be played in the first subgame by Player I; otherwise, Player II wins.

  *  If no winner has been declared thus far, let N_I be the winning model from the first subgame and N_II be the winning model from the second subgame (both with α in their wellfounded parts). Then,


  * We demand that N_I be isomorphic to an initial segment of N_II; otherwise, Player II wins. 

  * Let a_I be the unique ordinal in N_I satisfying ϕ_i and let a_II be the unique ordinal in N_II satisfying ϕ_j. Then,
Player I wins if for every (some) isomorphism j from N_I to an initial segment N of N_II, we have 

    N_II j(a_I) < a_II.
 
If not, then Player II wins.


Let ϑ_α^* be the order-type of the set of ordinals definable in L_ϑ_α(ℝ) from a real. Given pairs (i,x), (j,y) as above, if there is not a unique ordinal η<ϑ_α such that 

    L_ϑ_α(ℝ)ϕ_j(y,η),

then Player I has a winning strategy in the game obtained by playing the theory of L_ϑ_α(ℝ) in both subgames. This way, Player I is guaranteed to win the first subgame and Player II is forced to play the theory of L_ϑ_α(ℝ) in the second subgame, which will cost her the game. Similarly, if η above exists and there is not a unique ordinal γ<ϑ_α such that 

    L_ϑ_α(ℝ)ϕ_i(x,γ),

then Player II has a winning strategy in the game.
Otherwise, let γ and η be as above. We claim that

    γ≤η if, and only if, Player I has a winning strategy in the game.

If so, then the game defines a prewellordering of ℝ of length greater than ϑ_α^*, in which the pairs of highest rank are those whose first coordinate fails the syntactic condition (<ref>)–(<ref>) and the pairs of second-highest rank are those
not defining an ordinal in L_ϑ_α(ℝ), i.e., those failing conditions (<ref>)–(<ref>). The facts that condition (<ref>) is checked before condition (<ref>) and that condition (<ref>) is checked before (<ref>) will ensure that the game defines a reflexive relation.
Let us now proceed to the proof of equation (<ref>). 

Suppose γ≤η. A winning  strategy for Player I is defined by setting x_0 = x as appropriate and playing the theory of L_ϑ_α(ℝ) in the first subgame together with all reals played in the second subgame. In the second subgame, Player I also plays the theory of L_ϑ_α(ℝ). This strategy ensures that Player  I will win the first subgame, as in Lemma <ref>. Moreover, if Player II wishes to have any chance of winning the second subgame, she must also play the theory of L_ϑ_α(ℝ). If so, then this will define two models N_I and N_II as in the rules of the game, both wellfounded. Either there will be a real played in the first game and not in the second—in which case Player I wins—or both plays will contain the same reals. If so, the models N_I and N_II both embed into L_ϑ_α(ℝ) and are hence wellfounded, so their transitive collapses are of the forms L_α_I(σ) and L_α_II(σ), for some countable set of reals σ. Since each model satisfies the formulae:


  *  + Separation,

  * V_α exists,” and

  * for all η∈, L_η(ℝ)  + Separation + V_α exists,' ”

they must be equal. If Player II has not lost at this point, then we must have y_0 = y. The fact that L_α_I(σ) embeds elementarily into L_ϑ_α(ℝ) implies that the ordinal defined by ϕ_i and x must be at most the ordinal defined by ϕ_j and y in those models, as desired.

Conversely, suppose that Player I has a winning strategy in the game. We consider a run of the game by that strategy in which Player II plays the theory of L_ϑ_α(ℝ) in the first subgame, as well as in the second, where she also plays all reals from the first subgame. This ensures winning the second subgame and losing the first one. As before, this forces Player I to play the theory of L_ϑ_α(ℝ) in the first game, so the play defines two wellfounded models with the same reals and the same theory, whose transitive collapses must therefore be equal. Since the play must be won by Player I, the ordinal defined by ϕ_i and x must be at most the ordinal defined by ϕ_j and y.

This proves the claim and, together with the remark following equation (<ref>) shows that the relation ≼ given by

    (i,x) ≼ (j,y)  if, and only if, Player I has a winning strategy in G(α,i,x,j,y)

is a prewellordering of length greater than ϑ_α^*. A standard Skolem-hull argument shows that if β<α, then ϑ_β<ϑ_α^*.
Using the fact that the game from Lemma <ref> is Borel, one sees that for every α, G(α,i,x,j,y) is uniformly in Δ^1_1(α, ⟨ i,x ⟩, ⟨ j, y⟩), which completes the proof.


Before proving the theorem, we need two more lemmata.


Let ω+1< α<ω_1. The pointclass (^2_1)^L_ϑ_α(ℝ) has the scale property.

Let γ = ϑ_α. Since L_γ(ℝ) is a model of Σ_1-separation, γ is ℝ-nonprojectible, in the sense that there is no total function which is (Σ_1)^L_γ(ℝ) with parameters in L_γ(ℝ) and which maps γ injectively into some β<γ. The usual argument for L (see Barwise <cit.>) shows that γ is recursively ℝ-inaccessible, i.e., ℝ-admissible and a limit of ℝ-admissibles. 

To prove the lemma, we first verify that
the proof of Martin-Steel <cit.> goes through in L_γ(ℝ) and shows that
every (^ℝ^1_1)^L_γ(ℝ) set[In the choiceless context, ^ℝ is to be understood in terms of quasi-strategies.] admits a closed game representation in L_γ(ℝ). To see this, first observe that every wellfounded tree T in L_γ(ℝ) has a rank, since γ is a limit of ℝ-admissibles. This observation ensures that the proof of the claim in the proof of <cit.> holds in L_γ(ℝ) so that (using the notation from <cit.>) Player I has a winning strategy in G_x if, and only if, she has one in G^*_x,ξ for some ξ. Now, each G^*_x,ξ is a closed game and G^*_x,ξ∈ L_ξ+1(ℝ). By standard arguments, if Player I has a winning strategy in G^*_x,ξ, she has one in L_ξ^*+1(ℝ) whenever ξ<ξ^* and ξ^* is ℝ-admissible. 
Clearly, Θ^L_γ(ℝ) is also recursively ℝ-inaccessible and, by the Löwenheim-Skolem theorem,

    L_Θ^L_γ(ℝ)(ℝ)≺_1 L_γ(ℝ),

so it follows that
if x∈ℝ and ξ is least such that Player I has a winning strategy in G^*_x,ξ, then 

    ξ<Θ^L_γ(ℝ).

Denote this least ξ by ξ_x and let λ be the supremum of all ξ_x such that ξ_x is defined; thus, λ≤Θ^L_γ(ℝ). This shows that the map x↦ G^*_x,λ belongs to L_γ(ℝ). One finishes the argument as in <cit.>.

The statement of <cit.> also holds true in L_γ(ℝ), i.e.,

    (^ℝΠ^1_1)^L_γ(ℝ) = Σ_1(L_γ(ℝ), {ℝ}).

Here, the proof needs no modifications other than weakening condition (2) to only require that the model satisfy (say) , as opposed to ^-. This shows, using the proof of <cit.>, that the pointclass 

    Σ_1(L_γ(ℝ), {ℝ})

has the scale property. Now the proof of Solovay's basis theorem (e.g., the one in Section 2 of Koellner-Woodin <cit.>, replacing their T_0 with some strong-enough theory that holds in L_Θ^L_γ(ℝ)(ℝ)) shows that

    Σ_1(L_γ(ℝ), {ℝ}) = (Σ^2_1)^L_γ(ℝ),

from which the lemma follows.



Suppose that sets in ^ℝ^1_1 are determined. Then, Borel games of length ω^2 are determined.

This argument is a local version of the one in Blass <cit.>.
Consider the game on ℝ of length ω in which two players alternate turns playing strategies for games of length ω:

    [   I σ_0     σ_1        ;  II     τ_0     τ_1     ]

Player I wins if, and only if,

    (σ_0*τ_0, σ_1*τ_1,) ∈ A,

where σ*τ denotes the result of playing the strategies σ and τ against each other.

Call this game G. It is a Borel game (on ℝ), so it is determined. If it is Player I who wins this game, then Player I also wins the game of length ω^2 with payoff A. Suppose that it is Player II who wins this game; we shall construct a winning strategy for the game of length ω^2 with payoff A for Player II.

Let Σ denote the winning strategy for Player II in G. Σ is essentially a set of reals. By the remark at the beginning of the proof of Lemma <ref>, we may assume 

    Σ∈ L_ϑ(ℝ).

Recall that ϑ = sup{ϑ_α:α<ω_1}. By the minimality of ϑ_α and the ℝ-stability of δ^2_1, we have

    ϑ_α < (δ^2_1)^ϑ_α+1

for each α<ω_1. This implies by Lemma <ref> that 𝒫(ℝ)∩ L_ϑ(ℝ) has the scale property. Since it is closed under quantification by ℝ, Theorem D of <cit.> implies that it has the uniformization property.

Denote by A^* the set of all sequences p of natural numbers of length ω· n, for some n ∈ℕ, such that there is a sequence 

    τ⃗∈ℝ^n

such that p results from applying Σ to τ⃗. Put

    A^*_n = A^*∩ℝ^n.

For any given p ∈ A^*_1, there might be many strategies τ for Player I witnessing p ∈ A^*; however, A^*_1 is definable from Σ, so it belongs to L_ϑ(ℝ). Applying the uniformization property, one finds a function 

    f_1:A^*_1→ℝ

such that for each p ∈ A^*_1, f_1(p) is a strategy τ witnessing p ∈ A^* and, moreover, f_1 ∈ L_ϑ(ℝ). Inductively, suppose f_n has been defined. For any given p ∈ A^*_n+1, there might be many strategies τ such that f_n(p↾ω· n)^⌢τ witnesses p ∈ A^*, or none at all; however, A^*_n+1 is definable from Σ, so it belongs to L_ϑ(ℝ). Applying the uniformization property, one finds a function 

    f_n+1:A^*_n+1→ℝ^n+1

with f_n+1∈ L_ϑ(ℝ) and such that the following hold for each p ∈ A^*_n+1 for which such a τ exists:


  * f_n+1(p) is a sequence τ⃗ witnessing p ∈ A^*; and

  * f_n+1(p)↾ m = f_m(p↾ω· m)
for every m≤ n+1.

Let us also define a partial function f_ω: ℝ^ℕ→ℝ^ℕ by

    f_ω(p) = ⋃_n∈ℕ f_n(p↾  n),

if the right-hand side is defined, and put

    f = ⋃_n≤ωf_n.


Let us call a sequence p of natural numbers of length ω· n, with n∈ℕ, promising if  for every m ≤ n, p↾ω· m ∈ A^* and this is witnessed by f(p)↾ m.
Given a promising sequence p, we shall construct a strategy σ^* for Player II (for a game of length ω on ℕ) such that for every
x∈ℝ, p^⌢(σ^*(x)) is promising. 
Thus, if p^* is a run of a game of length ω^2 all of whose initial segments of limit length were obtained in this way, then it is a play all of whose initial segments are promising. This means that

    p^* = f(p^*) * Σ(f(p^*)),

which implies that p^* ∈ A.

Now, let p ∈ℝ^n be promising and consider the game G^* on ℕ of length ω:

    [    I x(0)      x(2)          ;   II      x(1)      x(3)      ]

Player II wins if, and only if, p^⌢ x is promising. We first show that Player I cannot have a winning strategy. Suppose towards a contradiction that τ is a winning strategy for Player I.  Thus, if Player I begins a run of G by playing

    f(p)^⌢τ,

during the first n+1 moves and Player II plays by Σ, then
she will begin by responding with n moves according to Σ, resulting in a sequence of strategies σ_0,, σ_n-1 so that

    p = (f(p)(0)*σ_0, , f(p)(n-1)*σ_n-1)

and continue responding with one last move by Σ, say σ. Put x = τ*σ. Since the play of G just described is consistent with Σ, we have p^⌢ x ∈ A^*. Although it need not be the case that f(p^⌢ x)(n) = τ,
the construction of f ensures that f(p^⌢ x) is a sequence τ⃗ witnessing p^⌢ x∈ A^* and f(p^⌢ x)↾ n = f(p). Thus, the run of G^* in which Player I plays by τ and Player II plays by σ results in a play x such that p^⌢ x is promising, which is a contradiction. Hence, Player I cannot have a winning strategy in G^*. We will show that the payoff set of G^* belongs to ^ℝ^1_1; this will imply that it is determined and thus that Player II has a winning strategy, which will finish the proof.

The payoff set of G^* (for Player II) consists of all x∈ℝ such that p^⌢ x is promising. A sequence being promising is defined in terms of Σ and f. Now, each f_n belongs to L_ϑ(ℝ) and, since

    (ϑ) = ω_1,

there is some α<ω_1 such that  each f_n belongs to L_ϑ_α(ℝ). Since 

    (L_Θ^L_ϑ_α(ℝ)(ℝ))^ω⊂ L_ϑ_α(ℝ),

we have f ∈ L_ϑ_α(ℝ). By choosing α large enough so that Σ∈ L_ϑ_α(ℝ), we ensure that

    {p ∈ℝ^n: p  is promising and  n∈ℕ}∈ L_ϑ_α(ℝ).

By Lemma <ref>, ϑ≤γ^1_1, so that, by Lemma, <ref>, the set in the displayed equation belongs to ^ℝ^1_1, which completes the proof.


Woodin has shown that ℝ^♯ exists and  holds in L(ℝ) if, and only if, there is a countably iterable proper-class model of  with infinitely many Woodin cardinals. Neeman <cit.> has shown that if such a model exists, then all analytic games of length ω^2 are determined (incidentally, the converse follows from a theorem of Trang <cit.> and a theorem of Martin-Steel <cit.>, after appealing to Woodin's theorem). 
Let us remark that the argument just given yields a direct proof of analytic determinacy for games of length ω^2 which involves no inner model theory.

(Neeman-Woodin)
Suppose that ℝ^♯ exists and L(ℝ). Then, analytic games of length ω^2 are determined.

Given an analytic set A, let G be the game defined as in the proof of Lemma <ref>. It is an analytic game on ℝ and, if won by Player I, then the game of length ω^2 with payoff A is also won by Player I. 
Since ℝ^♯ exists, then analytic games on ℝ are determined, by the argument in Martin <cit.>, so if Player I does not win A, then Player II does. 

Since  holds in L(ℝ), all sets in ^ℝ^1_1 are determined. Moreover, the pointclass ^ℝ^1_1 is correctly computed in L(ℝ), so if Player II wins an analytic game on ℝ (this is a ^ℝ^1_1 fact), then she has a winning strategy which is (^2_1)^L(ℝ). Hence, the game G^* defined as in the proof of the preceding lemma belongs to L(ℝ) and is thus determined. The rest of the argument is as before.


Theorem <ref> now follows: if Borel games of length ω^2 are determined, then all sets in 
^ℝ^1_1
are determined (in the usual sense). By Lemma <ref>, ϑ≤γ^1_1, so 

    L_ϑ(ℝ)

by Lemma <ref>. Conversely, suppose (<ref>) holds. By Lemma <ref> and the fact that the existence of winning strategies for games on ℝ is upwards absolute from initial segments of L(ℝ) (since they contain all possible plays of the game), we have 

    ^ℝ^1_1 ⊂ L_ϑ(ℝ).

Thus, sets in ^ℝ^1_1 are determined (in the usual sense). By the previous lemma, this implies that games of length ω^2 with Borel payoff are determined.
Theorem <ref> is thus proved.


γ^1_1 = ϑ.

Immediate from Lemma <ref>, Lemma <ref>, and the observation that Lemma <ref> implies equation (<ref>). Note that the three lemmata were proved under no determinacy hypotheses.




§ PROOF OF LEMMA <REF>


Let α<γ^1_1 be an ordinal; we show

    𝒫(ℝ)∩ L_α+1(ℝ)⊂^ℝ^1_1.

The proof consists in defining a game that determines membership in a set definable over L_α(ℝ); we call it the definability game. Readers familiar with Tanaka's <cit.> proof of Steel's <cit.> classical result on the equivalence between arithmetical transfinite recursion and clopen determinacy should find similarities.

Fix some prewellordering ≼ of ℝ in ^ℝ^1_1 of length α+1 or greater. To ease notation, assume that ≼ is defined without real parameters.
The definability game will involve playing representations of elements of L_α(ℝ). These are defined inductively: pairs (0, x), where x∈ℝ, are representations for x. Let β+1≤α, b ∈ L_β(ℝ) and

    B = {x∈ L_β(ℝ): L_β(ℝ)ϕ̂(x,b)}

be an element of L_β+1(ℝ). If x_b codes a representation (ψ, y, y_b) of b and |y|_≼ < β, then the triple

    (ϕ̂,x_β, x_b),

is a representation of B, whenever x_β is any real of rank β in ≼.[Strictly speaking, we should allow x_b to code finite tuples of representations, but we shall generally abuse notation by assuming that these tuples have length 1.]


Let α and ≼ be as above. Then, every set in L_α(ℝ) has a representation.

By induction on ordinals β≤α.


Let us also inductively define a proto-representation to be either a pair (0,x) as above, or a triple as in (<ref>)
whose first coordinate is a formula and third coordinate is a proto-representation, i.e., one drops the requirement on the ≼-rank of the second coordinate.

Being a proto-representation is easy to check—the class of all proto-representations is Σ^0_1. Being a genuine representation, on the other hand, is more complicated, as, if (ϕ̂, x_β, x_b) is as in (<ref>), then one needs to check that x_b in fact codes a representation for an element of L_β(ℝ).

In principle, one can have highly inefficient representations in which one defines simple objects in a complicated way. We will denote by _α the set of codes of all representations of the form (0,x) and of the form (ϕ̂, x_β, x_b), where x_β has rank <α in ≼. Belonging to _α does not guarantee that a representation is optimal, but it guarantees that, in a sense, it is not more complicated than α.”


Let α<γ^1_1, ≼, and _α be as above. If x_α has rank α in ≼, then _α∈^ℝΔ^1_1(x_α).

It is easy to determine whether a real number codes a representation of the form (0,y), so let us consider only proto-representations which are triples.

For a triple (ψ, x, y) to be a representation of an element of L_α(ℝ) in _α, it is necessary and sufficient that the following two conditions hold:


  *  x ≺ x_α,

  *  y codes a representation (ψ̂, x_γ, x_c) and x_γ≺ x.

Given a ∈ℝ, we define a game G(a) on reals with payoff in Δ^1_1(x_α). In this game, Player I claims that a codes a representation, and Player II claims otherwise. 

If a does not code a triple, the game ends immediately and Player I loses. Otherwise, suppose a codes a triple (ψ, x, y) as above.
Player II must begin by challenging one of the two conditions (<ref>) or (<ref>) above. If Player II decides to challenge condition (<ref>), then they must play the game with payoff in Δ^1_1(x,x_α) determining whether 

    x ≺ x_α;

if so, the winner of this subgame is the winner of G. If Player II decides to challenge condition (<ref>), then Player II must provide one of the following three reasons:


  * y does not code a triple nor a pair (0,ŷ), where ŷ∈ℝ;

  * y codes a triple (ψ̂, x_γ, x_c), but x≼ x_γ;

  * y codes a triple (ψ̂, x_γ, x_c), but x_c is not a representation.

If Player II claims that y does not code a triple or a pair (0,ŷ), then the game ends and Player I wins if, and only if, y codes a triple or a pair (0,ŷ). If Player II claims that x≼ x_γ, then, as above, they must play the game with payoff in Δ(x,x_γ) determining whether

    x_γ≺ x.

Finally, if Player II claims that y codes a triple (ψ̂, x_γ, x_c), but x_c is not a representation, then she again must provide a reason, and so on. 
If Player II correctly identifies the problems with Player I's purported representations throughout the game, then she must initiate a subgame after finitely many turns (because ≺ is wellfounded). Hence, we add as a rule that if the game finishes after infinitely many turns without Player II having initiated a subgame, she loses. We note that, although different subgames can be initiated by Player II, they are all Borel, and in fact they are so in a uniform way, i.e., they are all instances of the same game (namely, the one for determining whether u ≺ v), and only their parameters vary. This uniformity is necessary for ensuring that the payoff of G(a) is also Borel.

Now, Player I wins a run p of the game if, and only if, one of the following holds:


  * One of the players violates a rule and the first one to do so is Player II; 

  * The players obey the rules and for all n, Player II does not initiate a subgame in the nth turn; 

  * The players obey the rules, there is a least n such that Player II initiates a subgame in the nth turn, and p↾(n,∞) is a win for Player I in this game.

The first condition is Σ^0_1(a,p, x_α), the second one is Π^0_1(a,p), and the third one is Δ^1_1(a,p). Thus, the winning condition is in Δ^1_1(a,p,x_α). Moreover, if (ψ, x, y) is a representation of an element of L_α(ℝ), then any challenge raised by Player II can easily be overcome by Player I, so she must have a winning strategy. Similarly, if (ψ, x, y) is not a representation of an element of L_α(ℝ), then Player II can identify the reason why this is the case and pose a challenge Player I cannot overcome. Therefore, Player I has a winning strategy in this game if, and only if, a indeed codes a representation of an element of L_α(ℝ) in _α. We have shown that the set of codes of representations of elements of L_α(ℝ) is the set of all a for which Player I has a winning strategy in the Borel game G(a), as was to be shown.



The fact that all auxilary games were  Borel in a uniform way was crucial in the proof of Lemma <ref>. In fact, the set ⋃_α<γ^1_1Rep_α is not in ^ℝ^1_1. 




The order of a proto-representation is defined inductively: the order of a proto-representation of the form (0,x) is 0; the order of a proto-representation of the form (ϕ,x_β, x_b) is the maximum of |x_β|_≺ and the order of x_b.

Thus, if x ∈_α, then the order of x is strictly less than α.


We now proceed to the definability game and, with it, to the proof of Lemma <ref>. The idea of the game is very simple: two players argue whether a formula holds of some sets in a given level of the L(ℝ)-hierarchy. However, its description is lengthy. This is due to two complications that arise: the first one is that we need the payoff of the game to be ^1_1. This requires us speaking about representations of sets instead of sets directly. The second one is that many rules need to be put into place to ensure that the players are honest in their moves.

Fix some n∈ℕ, a parameter x_A∈ L_α(ℝ), and a set 

    A ∈Σ_n(L_α(ℝ),x_A),

say, A = {y∈ L_α(ℝ): L_α(ℝ)ϕ(y,x_A)}.
In the definability game, Player I attempts to show that a given y ∈ L_γ^1_1(ℝ) belongs to the set A above, i.e., that

    L_α(ℝ)ϕ(y,x_A)

We assume that the scopes of all negations in ϕ (and in all formulae appearing below) are atomic formulae. We also assume that no implications appear in ϕ. The game will involve Players I and II playing purported representations of sets in L_α(ℝ). 
Fix some representation (ϕ,x_α, x_a) for A and some real x^* coding it. Let a∈ℝ; we define the game D_A(a). If a does not code a pair (0,y) or a triple (ϕ_y, x_y, x_c), the game ends immediately and Player I loses. Otherwise, the game begins. We will describe the rules in the case that a codes a triple; the rules in the case that a codes a pair (0,y) are analogous; soon, we will restrict our attention to reals a of order <α (as the reader will soon realize, this restriction postpones a certain complication in the definition of the game). 
Player I's goal is to convince Player II that the triple coded by a is a representation for some y such that equation (<ref>) is satisfied. The game is defined from x^* and a (as well as the parameters defining ≼, which we assumed for simplicity to be non-existent). 

The rules of the game give the players opportunities to initiate subgames in which they challenge the other's moves. If this happens at any point, the definability game will end and the winner will be declared to be the winner of the subgame. We do not need to speak about winning strategies for the subgame—we can simply ask the players to play it. All subgames will have Borel payoff and real moves; this allows the players to check during the game whether a given ^ℝ^1_1 fact holds.


At the beginning of of D_A(a), Player II has the oportunity to claim that

    (ϕ_y, x_y, x_c) is not a representation of an element of L_α(ℝ),

i.e., that (ϕ_y, x_y, x_c)∉_α.
If this happens, then the game is over and Player I wins if, and only if, the challenged object is indeed a representation; otherwise Player II wins. If Player II does not claim either of the two statements above, the game proceeds.

At the beginning of turn k, Players I and II have defined a proto-representation (ϕ_k, x_β^k, x_b^k) for some set B^k and finitely many proto-representations (ψ_w^k_i, x_w^k_i, x_d^k_i) for some sets w^k_i. Player I claims that w⃗^k ∈ B^k, i.e., that

    L_β^k(ℝ)ϕ_k(w⃗^k,b^k);

Player II claims otherwise.
Below, we write w⃗ = w⃗^k and b = b^k for notational simplicity; as before, we might abuse notation by assuming w⃗ is a tuple of length 1 and simply writing w.
We define the order of the game at turn k to be the maximum of the orders of w and b.
Let us describe the rules of the game by cases:



  * If ϕ_k is of the form ψ∨χ, then Player I selects either ψ or χ. We set ϕ_k+1 equal to that choice and leave the rest of the objects unchanged.

  * If ϕ_k is of the form ψ∧χ, then Player II selects either ψ or χ. We set ϕ_k+1 equal to that choice and leave the rest of the objects unchanged.

  * If ϕ_k(w, b) is of the form ∃ z ψ(w, b, z), then Player I must play a proto-representation x_z which is allegedly a representation in _β^k of some z∈ L_β^k(ℝ) such that

    L_β^k(ℝ)ψ(w,b,z).

At this point, Player II has the opportunity to object to the fact that x_z belongs to _β^k. If so, the game ends and Player I wins if, and only if, x_z ∈_β^k. If Player II does not challenge Player I's move, then the game continues with ϕ_k+1 = ψ and z added to w⃗; the rest of the objects remain unchanged.

  * If ϕ_k(w, b) is of the form ∀ z ψ(w, b, z), then Player II must play a proto-representation x_z which is allegedly a representation in _β^k of of some z∈ L_β^k(ℝ) such that

    L_β^k(ℝ)ψ(w,b,z).

As before, Player I has the opportunity to object to the fact that x_z belongs to _β^k. If so, the game ends and Player I wins if, and only if, x_z∉_β^k. If Player I does not challenge Player II's move, then the game continues with ϕ_k+1 = ψ and z added to w⃗; the rest of the objects remain unchanged.

  *  If ϕ_k is a non-negated atomic formula, then it is of the form 
u ∈ v, where u and v are any of b or some w_i; both u and v have associated proto-representations that have been played in one of the previous turns, or given by the initial data. There are three subcases that we need to distinguish: 


  * Suppose that the proto-representation associated to v is of the form (0, x), for some x∈ℝ, and the proto-representation associated to u is of the form (0, y), for some y∈ℝ; then the game ends. Player I wins if, and only if, y ∈ x; otherwise, Player II wins. 

  *  Suppose that the proto-representation associated to v is of the form (0, x), for some x∈ℝ, but the one associated to u is of the form

    (ϕ_u, x_η_u, x_u).

The problem is that—in principle—(ϕ_u, x_η_u, x_u) might be a complicated (true) representation of a simple set.[Originally introduced into the game by either player.] The game proceeds as follows: since the proto-representation associated to v is of the form (0, x), it is a true representation of some real number. 
Player I must thus play a natural number n ∈ x and claim that (ϕ_u, x_η_u, x_u) is a representation of n, i.e., that, there is u' ∈ L_η_u(ℝ) represented by x_u such that

    L_η_u(ℝ)ϕ_u(u',m)  if, and only if,  m<n.

Player II must object by playing some m_0 ∈ℕ such that one of the following holds:


  * m_0 < n but L_η_u(ℝ)ϕ_u(u',m_0); or

  * n < m_0 and L_η_u(ℝ)ϕ_u(u',m_0).


During the remainder of the game, the two players must determine whether 

    L_η_u(ℝ)ϕ_u(u',m_0).

We know how to do this: namely, we set B^k+1 equal to

    {m∈ℕ: L_η_u(ℝ)ϕ_u(u',m)}

or

    {m∈ℕ: L_η_u(ℝ)¬ϕ_u(u',m)},

according to which objection was raised by Player II, and work with the canonical representation for B^k+1; and w⃗^k+1 = (0, m_0).

  * Suppose that v has an associated proto-representation of the form

    (χ, x_η, x_a_v).

This case is similar to the previous one: Player I claims u ∈ v, i.e., 

    L_η(ℝ)χ(u,a_v).

The problem (as before) is that the proto-representation

    (ϕ_u, x_η_u, x_u)

associated to u
might be unnecessarily complicated. We ask Player I to decide whether
x_η_u≺ x_η.
To ensure that Player I tells the truth, we then ask Player II to decide whether 
x_η_u≺ x_η.
If the two players disagree on this, the game ends, with the winner being declared as the winner of the subgame that determines whether x_η_u≺ x_η.

Otherwise, suppose first that the players both believe that x_η_u≺ x_η. 
At this point, Player II can claim that the proto-representation (ϕ_u, x_η_u, x_u) associated to u does not belong to Rep_η. If so, then—as above—the game ends, and the winner of the game is the winner of the game given by Lemma <ref> applied to x_η and the proto-representation associated to u.[Note that this proto-representation could have been played by Player II at an earlier turn; this does not matter.] If Player II chooses not to make that claim, the game continues with ϕ_k+1 = χ, x_β^k+1 = x_η, x_b^k+1 = x_a_v, and w⃗^k+1=u.

If the players both believe that x_η≼ x_η_u, then we need to argue as above. If u truly is an element of v, then u must have a representation of order strictly less than η. Player I must play such a representation, say, (ϕ_u', x_η_u', x_u'). As usual, Player II may object by claiming that (ϕ_u', x_η_u', x_u') ∉_η, in which case the game ends and the winner is declared according as whether (ϕ_u', x_η_u', x_u') ∈_η or not; or by claiming that (ϕ_u', x_η_u', x_u') is not in fact a representation of the same object as (ϕ_u, x_η_u, x_u). Let u' be the object represented by (ϕ_u', x_η_u', x_u') (if any). This is now treated much like the case (<ref>). Player II must claim one of the following:


  * u' ⊄u; or

  * u⊄u'.
 
Assume without loss of generality that it is the first alternative that is claimed. Player II must play a proto-representation (ϕ_v', x_η_v', x_v') for a set v' witnessing that u' ≠ u. Player I can make the usual objection that (ϕ_v', x_η_v', x_v')∉_η'_u, in which case the game proceeds as usual. Otherwise, Player I may claim that v' ∉u' or that v' ∈ u. In the former case, the game proceeds with the proto-representation (ϕ_u', x_η_u', x_u') for u' = B^k+1 and w^k+1 equal to the proto-representation (ϕ_v', x_η_v', x_v'). The other case is similar.



  *  Finally, if ϕ_k is a negated atomic formula, then it is of the form 
u ∉v, where u and v are any of b or some w_i; both u and v have associated proto-representations that have been played in one of the previous turns. One distinguishes three subcases and proceeds as in case (<ref>).



The hope is that
both players play only real representations when they should play proto-representations and that the initial triples are also real representations. 
Let us say that a (partial) play in which these conditions are satisfied is honest.

A key remark is that, if a play p is honest, then the order of p decreases after each time the players find themselves in one of situations (<ref>) or (<ref>) (assuming the game does not end).
This implies that an honest play in which both players
accept each other's moves will end after finitely many turns by one of the winning conditions in clauses (<ref>)–(<ref>) and the winner will be defined then. 


If our expectations on the honesty of the players are not realized, the game will end in one of two possible ways: by means of a subgame initiated by a player challenging the other player's choice, in which case the winner of the definability game will be the winner of the subgame; or perhaps after infinitely many turns, if a player made improper moves and was not challenged by the opponent (or perhaps if one of the initial triples was not a real representation and this was not noticed by Player II). In this latter case, we declare Player I as the winner.[This choice will not be very consequential. Such an outcome will not occur in any case of interest, but it needs to be considered to make the game zero-sum.] 

There are three types of subgames that can be initiated: the one given by Lemma <ref>, its dual—that in which the roles of Player I and Player II are reversed—, and the game associated to the prewellordering ≺. Games of each of those three types are uniformly in ^1_1, and defined using the initial parameters, as well as parameters played during the (main) game.
 
Thus, Player I wins a run p of the game if, and only if, a codes a triple and


  * There is some k such that a player breaks a rule during turn k and the first player to do so is Player II;

  * There is some k such that a player initiates a challenge during turn k and p↾(k,∞) is a win for Player I in the subgame;

  * The game ends at a finite stage k by Player I fulfilling the condition in case (<ref>) or case (<ref>) above; or

  * After infinitely many steps, no player has won or initiated a challenge.

The first condition is Σ^0_1(x^*,a,p). The second condition is Δ^1_1(x^*,p). Lastly, the third condition is Σ^0_1(p) and the fourth condition is Π^0_1(p). Hence, the payoff set is in Δ^1_1(x^*,a,p). 

Player I has a winning strategy in D_A(a) if, and only if, a codes a representation in _α of some set y ∈ L_α(ℝ) such that

    L_α(ℝ)ϕ(y,x_A).


Clearly it is necessary that a code a representation in _α for some set y ∈ L_α(ℝ) in order for Player I to have a winning strategy.
Suppose it does and that (<ref>) holds.
The strategy for Player I is simple—essentially, she will always tell the truth. This will ensure that the intuitive interpretation of the game in terms of Player I claiming that a formula holds in an initial segment of L(ℝ) and Player II claiming otherwise is accurate.

If Player I's assertions are ever challenged by Player II, the subgame can be won as in Lemma <ref>. Otherwise, at a given turn k, if (ϕ_k, x_β^k,x_b^k) and (ψ_w^k, x_w^k,x_d^k) are as in the definition of the game, then they will be true representations. If ϕ_k is a disjunction, then one of the disjuncts will hold in L_β^k(ℝ) and Player I will choose it. If ϕ_k is a conjunction, then both conjuncts will hold in L_β^k(ℝ) and so it will not matter which one Player II chooses. If ϕ_k is of the form ∃ z ψ, then there really must be a witness to ψ in L_β^k(ℝ), and Player I will play a true representation of this witness, say, of minimal order. If ϕ_k is of the form ∀ z ψ and Player II plays a proto-representation which is not a representation of an element of L_β^k(ℝ), or has order higher than that permissible by the rules of the game, then Player I will challenge Player II's move and win the game as in Lemma <ref>. Otherwise, Player II will play a representation of an element of L_β^k(ℝ) and ψ will hold of this element. 
If ϕ_k is atomic or negated atomic, then it will be true, so that either the game will end and be won by Player I or continue according to the form of the representations relevant to the turn of the game the players are in. As remarked earlier, the order of every honest play of the game decreases after each time the players find themselves in one of situations (<ref>) or (<ref>).
Hence, the strategy just described  ensures that either a player will initiate a challenge that will end by Player I winning, or that the game will end after finitely many turns and be won by Player I.

Similarly, if Player I has a winning strategy, then (<ref>) must hold, for otherwise essentially the same strategy for Player II will be a winning strategy. The point is that if Player II plays properly, every play will end either after finitely many turns or with a subgame.


Thus, given a set of reals A ∈ L_α+1(ℝ)
and a code x^* of a representation for A (which exists by Lemma <ref>), one has

    A = {y∈ℝ:  Player I has a winning strategy in  D_A(⟨ 0, y⟩)}.

Since D_A(⟨ 0, y⟩) is in Δ^1_1(x^*, ⟨ 0, y⟩), we have

    𝒫(ℝ)∩ L_α+1(ℝ)⊂^ℝ^1_1.

Therefore, the proof of Lemma <ref> is complete.



§ DERIVED MODEL THEOREMS
 

In this section, we prove two lemmata that tie determinacy in L_ϑ(ℝ) to the existence of countably iterable extender models of Zermelo set theory with infinitely many Woodin cardinals. The first lemma is proved just like its analogue for L(ℝ). The second lemma is also similar to its analogue for L(ℝ) but has some differences.
We will assume some familiarity with the theory of extender models, e.g., as presented in Mitchell-Steel <cit.> or Steel <cit.>.

We note that every interval of the form [(δ^2_1)^L_ϑ_α(ℝ),ϑ_α] is a gap (cf. the proof of Lemma <ref> above).


Suppose that for every α<ω_1, there is a countable, countably iterable extender model of

    𝖹 + V_λ+α exists and λ is a limit of Woodin cardinals.”

Then L_ϑ(ℝ).

Let α<ω_1 be large. We show that

    L_ϑ_α(ℝ).


Let M be an extender model as in the statement and let {δ_i:i∈ℕ} enumerate the first infinitely many Woodin cardinals of M. As usual, M is a model of the Axiom of Choice. 
Since M is a model of Powerset, we have

    M  for every κ, κ^+ exists.”


A consequence of this is that M; thus M can define the class (L(A))^M for all A ∈ M.
Assume without loss of generality that M is minimal, in the sense that

    M  V = L(V_λ).

Since M 𝖹𝖢, it can form ultrapowers of itself in the usual (non-fine-structural) sense and realize them e.g., as the union of all ultrapowers of initial segments of its cumulative hierarchy. One can carry out the usual proofs of basic facts about the stationary tower ℚ_<δ, as well as the proof of Woodin's derived model theorem (e.g., the one in <cit.>) within M.[This is where we use the assumption that α is large. For instance, the proof in <cit.> involves building conditions for the stationary tower ℚ_<δ starting from elementary substructures of V_λ+ω. We have not attempted to prove (<ref>) from optimal hypotheses; it seems plausible that a more careful argument shows e.g., that L_ϑ_1(ℝ) if there is a countable, ω_1-iterable extender model of  - Powerset with a limit of Woodin cardinals.] 
Suppose g^* ⊂(ω,λ) is M-generic. Since M 𝖹𝖢 +, then 

    M[g^*] 𝖹𝖢 + ,

(this follows, e.g., from work of Mathias <cit.>) so that if ℝ^* is the set of reals of a symmetric collapse at λ, then

    L(ℝ^*)^M𝖹 +

(for the proof of this in the case of L, see Gostanian <cit.>.)
Since λ is a limit of Woodin cardinals in M,

    L(ℝ^*)^M + .

Now let g⊂(ω,ℝ) be V-generic. In V[g] let {x_i:i∈ℝ} enumerate ℝ and find a sequence M_i of extender models such that for each i∈ℕ,


  * M_i+1 is the direct limit of an iteration tree on M_i of length ω by extenders with critical point above the ith Woodin cardinal of M_i and length below the i+1th Woodin cardinal of M_i+1;

  * If j_i:M_0→ M_i+1 is the embedding, then j_i ∈ V and there is an M_i+1-generic g_i⊂(ω,j(δ_i)) such that x_i ∈ M_i+1[g_i]. 

If so, then, letting M_∞ be the direct limit of {M_i:i∈ℕ}, it follows by the restriction on the extenders allowed in the trees that M_∞ is wellfounded. If j is the embedding, then j(λ) = ω_1^V. By (<ref>) and the homogeneity of the symmetric collapse, 

    M ⊩ every set in L(ℝ̇) is determined and L(ℝ̇),”

where ℝ̇ is a name for the set of reals of the symmetric collapse. By elementarity, 

    L(ℝ^*)^M_∞+.

The symmetric collapse can be chosen (in V[g]) in such a way that it absorbs the generic g_i for each i∈ℕ, in which case (ℝ^*)^M_∞ = ℝ^V, so L(ℝ^*)^M_∞ is of the form L_ξ(ℝ). 

Suppose h⊂(ω,λ) is M_∞-generic and chosen so that the symmetric collapse induced by h absorbs g_i for each i∈ℕ. By the remark before equation (<ref>), we have

    M_∞[h] 𝖹𝖢.

Since (ω,λ) has the λ^+-chain condition, 

    M_∞[h] V_α exists.”

Now, clearly, we have

    L_ξ(ℝ)⊂ M_∞[h],
 
so L_ξ(ℝ) satisfies  by  (<ref>); it satisfies 𝖹 by (<ref>), and it satisfies V_α exists” by (<ref>). By minimality, ϑ_α<ξ, which completes the proof.




Suppose that L_ϑ(ℝ). Then, for each α<ω_1, there is an ω_1-iterable extender model of

    𝖹 + V_λ+α exists and λ is a limit of Woodin cardinals.”


Suppose that L_ϑ(ℝ). Let α<ω_1 be large and find some γ<ϑ such that


  * L_γ(ℝ) is a model of 𝖹 +V_α exists,”

  * if x,y∈ℝ and x is definable in L_γ(ℝ) from y and ordinal parameters, then there is γ'<γ such that x is definable in L_γ'(ℝ) from y and ordinal parameters.

For example, one could take γ to be least such that 

    V_α+ω^L_ϑ_α+ω(ℝ)⊂ L_γ(ℝ).

Clearly L_γ(ℝ) is a model of V_α exists.” Moreover, if a ∈ L_β(ℝ), with β<γ, then—by minimality—there is n∈ℕ such that 

    V_α+n^L_ϑ_α+ω(ℝ)⊄L_β(ℝ).

Thus, there is a stage β'+1 ∈ (β,γ) at which a new element of V_α+n is constructed and, by Proposition <ref>, there is a surjection from V_α+n∩ J_β'(ℝ) to J_β'(ℝ) in J_β'+1(ℝ). In particular, there is a surjection from V_α+n∩ J_β'(ℝ) to a. Hence, 𝒫(a)^L_ϑ_α+ω(ℝ)⊂ V_α+n+1^L_ϑ_α+ω(ℝ) and so 

    𝒫(a)^L_ϑ_α+ω(ℝ) = 𝒫(a)^L_γ(ℝ)∈ L_γ(ℝ),

so we have that L_γ(ℝ)𝖹.
Lastly, the definition implies that γ is a cardinal (in fact, the largest cardinal) of L_ϑ_α+ω(ℝ) greater than Θ^L_ϑ_α+ω(ℝ), so that (by the Löwenheim-Skolem theorem),
we have

    L_γ(ℝ) ≺_1 L_ϑ_α+ω(ℝ).

Hence, if x,y∈ℝ and x is definable in L_γ(ℝ) from y and ordinal parameters, then 

    L_γ(ℝ)∃γ' (x is definable in L_γ'(ℝ) from y and ordinal parameters),

so γ is as desired.

The first thing to verify is that 

    L_γ(ℝ) Mouse Capturing.”

Recall that Mouse Capturing” is the statement that for every pair of reals (x,y), x is definable from y and ordinal parameters if, and only if, x belongs to a countably iterable extender model over y. In Schindler-Steel <cit.>, it is shown that for all reals x,y, the following are equivalent:


  * x is definable from y and ordinal parameters in L_β(ℝ) for some β<γ,

  * x belongs to an extender model over y which is countably iterable by an iteration strategy in L_γ(ℝ).

The equivalence is stated modulo an inductive hypothesis W^*_α, but this hypothesis is proved (see the argument in pp. 157-158 of <cit.>) under the assumption of  (in L(ℝ), but the argument goes through in L_γ(ℝ)). By our choice of γ, this shows that L_γ(ℝ) satisfies Mouse Capturing.

The second thing to verify is that 

    L_γ(ℝ)^+;

this follows from the usual proof for L(ℝ): Ordinal Determinacy follows from the facts that by Kechris-Kleinberg-Moschovakis-Woodin <cit.>, (δ^2_1)^L_γ(ℝ) is a limit of cardinals with the strong partition property, and that by a theorem due independently to Moschovakis and Woodin (see Larson <cit.> for a proof), this implies <(δ^2_1)^L_γ(ℝ)-determinacy. Since

    L_(δ^2_1)^L_γ(ℝ)(ℝ)≺_1 L_γ(ℝ),

this implies Ordinal Determinacy in L_γ(ℝ).

That every set of reals is ∞-Borel in L_γ(ℝ) follows from the argument in <cit.>. (It uses the fact that (Σ^2_1)^L_γ(ℝ) has the scale property, which is proved by following the argument of <cit.> as in Lemma <ref>).

We have checked that L_γ(ℝ) satisfies ^+ and Mouse Capturing. Now, let β<α be arbitrary and let x_β be a real such that β is recursive in x_β. Define the theory

    S ≡𝖹 +  + ^+ +  + “Mouse Capturing” + “V_β exists.”

Let κ be least such that J_κ(ℝ) S; clearly κ<γ and, in fact, κ<(δ^2_1)^L_γ(ℝ).
We now run the proof of Steel-Woodin <cit.> for the theory S within L_γ(ℝ) (so that κ here takes the role of the ordinal denoted by γ therein), except that we consider the pointclass (Σ^2_1(x_β))^J_κ(ℝ), rather than (Σ^2_1)^J_κ(ℝ). Similarly, one replaces the L[E]-construction on p. 325 of <cit.> by an L[E](x_β)-construction.
Letting M, N, and ξ be as in <cit.>, and M_0 be set of all elements of M|ξ which are definable from x_β in M|ξ, the argument shows that M_0 has the form J_ζ(N_0), for some ζ and some extender model N_0 over x_β and, moreover, the following hold:


  * N_0 satisfies “there are infinitely many Woodin cardinals”;

  * no initial segment of M_0 projects to N_0;

  * M_0 has an (ω_1,ω_1)-iteration strategy Σ_0;

  * the derived model of M_0 at its limit of Woodin cardinals satisfies S.

Now, let λ be the limit of Woodin cardinals of M_0. Then, an ordinal η>λ is a cardinal of M_0 if, and only if, it is a cardinal of a generic extension of M_0 by (ω,λ) if, and only if, it is a cardinal of the derived model of M_0. Since this derived model satisfies S, it follows that M_0 has β-many cardinals above λ and, since M_0 is a model of the Generalized Continuum Hypothesis, we have M_0 “V_β exists.”
Since β<α was arbitrary and α was arbitrary, the result follows.


Theorem <ref> is immediate from Theorem <ref>,  Lemma <ref> and Lemma <ref>.



abstract


