$F_σ$ Games and Reflection in $L(\mathbb{R})$
J. P. Aguilera


[2010]03D70, 03E15, 03E60; 91A44

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



We characterize the determinacy of F_σ games of length ω^2 in terms of determinacy assertions for short games. Specifically, we show that F_σ games of length ω^2 are determined if, and only if, there is a transitive model of + containing ℝ and reflecting Π_1 facts about the next admissible set.

As a consequence, one obtains that, over the base theory +  + ℝ exists,” determinacy for F_σ games of length ω^2 is stronger than , but weaker than + Σ_1-separation.


F_σ Games and Reflection in L(ℝ)
    J. P. Aguilera
    December 30, 2023 (compiled)
================================






§ INTRODUCTION

We study the consistency strength of F_σ-determinacy for games of length ω^2. We see that the situation here is tied with that of short games. For example, over the base theory 

    + + ℝ exists,”
 
F_σ-determinacy for games of length ω^2 is much stronger than ; however, it is much weaker than  + Σ_1-separation. Over , F_σ-determinacy for games of length ω^2 is stronger than the existence of a transitive model of  +  containing all reals; yet weaker than the existence of a transitive model of  +  + Σ_1-separation containing all reals.
The consistency strength of this theory is hard to describe in terms of large cardinals: determinacy assumptions for games of length ω^2 (over  or over + + ℝ exists”) for all pointclasses between the clopen sets and the Borel sets lie strictly between the existence of all finite amounts of Woodin cardinals (as a schema) and the existence of infinitely many Woodin cardinals, in terms of consistency strength (see <cit.>).

 Much like in the case of short F_σ games, long games are tied to reflection for set-theoretic formulae of a certain complexity, except that—rather than in L—one needs to consider reflection in the L(ℝ)-hierarchy. Given an admissible set, let A^+ denote the next admissible set, in the sense of Barwise-Gandy-Moschovakis <cit.>; i.e., A^+ is the smallest admissible set containing A. By convention, all admissible sets are transitive.


An admissible set A is Π^+_1-reflecting if for every Π_1 formula ϕ with parameters in A and one free variable, if A^+ϕ(A), then there is some B ∈ A with all parameters in ϕ such that B^+ϕ(B). 


Our main theorem is:

The following are equivalent:


  * ^0_2-determinacy for games of length ω^2;

  * There is a Π^+_1-reflecting model of  containing ℝ.



Precursors to this work include, on the side of long games, Blass' <cit.> theorem that determinacy for all games of length ω^2 is equivalent to _ℝ, Neeman's <cit.> work on games of countable length, Trang's <cit.> work on analytic games of additively indecomposable length, as well as previous work on games of length ω^2 that are open (see Theorem <ref> below), clopen <cit.>, Borel <cit.>, or projective <cit.>. On the side of F_σ games we mention Solovay's and Tanaka's <cit.> work in the contexts of subsystems of set theory and analysis, respectively, and Wolfe's <cit.> original proof of F_σ-determinacy.



§ PRELIMINARIES

In this section, we collect some preliminary definitions and results. 


 §.§ Games of transfinite length

We study two-player, perfect information games of length ω^2 which are F_σ, i.e., ^0_2-definable. These are games in which, given A∈𝒫(ℝ)∩^0_2, two players, Player I and Player II, alternate ω^2-many turns playing natural numbers, thus producing a sequence x ∈ℕ^ω^2. Since the spaces ℝ∖ℚ and ℕ^ω^2 are recursively homeomorphic, the sequence x may be identified with a(n irrational) real number. Player I wins if x ∈ A; otherwise, Player II wins.

As above, we will often identify sequences of natural numbers of length ω^2 with ω-sequences of reals and with single reals. We will denote by 

    x = ⟨ x_0, x_1, ⟩

the single real number coding the sequence (x_0, x_1,), via some fixed recursive coding. The precise coding used will be immaterial, except for the continuity property that the first n digits x should only depend on x_0, x_1,, x_n. Similarly, if s and t are infinite sequences, or reals coding them, we will denote by 

    s^⌢ t

the single real number coding the result of concatenating s and t.




 §.§ Reflection in L(ℝ)

We recall the definition of the L(ℝ) hierarchy: L_0(ℝ) is defined to be V_ω+1, the collection of all sets all of whose elements are hereditarily finite. L_α+1(ℝ) is the set of all subsets of L_α(ℝ) definable over L_α(ℝ) with parameters. At limit stages, L_λ(ℝ) is the union of all L_α(ℝ), for α<λ. The function

    α↦ L_α(ℝ)

is Δ_1 with ℝ as a parameter.
The first step towards proving Theorem <ref> is the observation that it suffices to restrict to admissible sets of the form L_α(ℝ). 

We will use the following non-standard notation:
 
Let α be an ordinal. We denote by 

    α^+

the least ordinal β such that α<β and L_β(ℝ) is admissible.



An ordinal α is Π^+_1-reflecting if L_α(ℝ) is Π^+_1-reflecting.



Suppose A is a Π^+_1-reflecting set and ℝ∈ A. Let α = ∩ A; then, α is Π^+_1-reflecting.

Let ϕ be a Π_1 formula with parameters in L_α(ℝ) such that 

    (L_α(ℝ))^+ϕ(L_α(ℝ)).

Clearly, (L_α(ℝ))^+ = L_α^+(ℝ). Moreover, A^+ is an admissible set containing L_α(ℝ), so L_α^+(ℝ)⊂ A^+.
Let ψ be the formula in the language of set theory with parameters in A ∪{A} asserting that for all β, if no γ∈ (α,β) is admissible, then L_β(ℝ)ϕ(L_α(ℝ)). Being admissible is expressible internally, α is Δ_1-definable from A, and—as remarked earlier—L_β(ℝ) is Δ_1-definable from β and ℝ (which belong to L_α(ℝ)). Hence, ψ is Π_1. Moreover, A^+ ψ(A), so, by reflection, there is B ∈ A such that B^+ψ(B) and B contains all parameters in ψ. In particular, ℝ∈ B.
Let β = ∩ B; since B ∈ A, β∈ A, so, in particular, β<α. L_β^+(ℝ)⊂ B^+. By choice of ψ, we obtain that L_β^+(ℝ)ϕ(L_β(ℝ)), as desired.



The following are equivalent:


  * There is a Π^+_1-reflecting model of  containing ℝ; and

  * There is a Π^+_1-reflecting ordinal α such that L_α(ℝ).


Suppose that A is a Π^+_1-reflecting model of  containing ℝ and let α = ∩ A. By Lemma <ref>, L_α(ℝ) is Π^+_1-reflecting. Moreover, it is a subset of A containing all reals, and thus all possible strategies for games; hence, L_α(ℝ). The converse is immediate.


This motivates the following definition:

We denote by σ_ℝ the least Π^+_1-reflecting ordinal.

σ_ℝ is the analog of the ordinal σ^1_1 for L(ℝ). Unlike σ^1_1, the set-theoretic properties of σ_ℝ are not decidable within . For instance,
under , σ_ℝ is big—it is a limit of weakly inaccessible cardinals. In contrast, if V = L, then σ_ℝ<ω_2.


Let A⊂ℝ×ℝ and write A_x = {y∈ℝ: (x,y)∈ℝ}. We write ^ℝ A for the set of all x∈ℝ such that Player I has a winning strategy for the game on ℝ with payoff A_x. We define

    ^ℝ^0_2 = {^ℝ A : A ∈^0_2}.



(Classes such as ^ℝ^0_1 or ^ℝ^0_1 are defined analogously.)
To prove Theorem <ref>, it suffices to prove that determinacy for F_σ games of length ω^2 is equivalent to the fact that L_σ_ℝ(ℝ). Following previous proofs of determinacy for games of length ω^2, our first goal is to locate winning strategies for ^0_2 games on ℝ. We shall show that

    𝒫(ℝ) ∩Σ_1^L_σ_ℝ(ℝ)= ^ℝ^0_2.


The main tool for this is the theory of inductive definitions on ℝ, the basics of which we recall next.




 §.§ Inductive definitions

Suppose that 
ϕ:𝒫(ℝ^m)→𝒫(ℝ^m)
is an operator. We define sets ϕ^λ⊂ℝ^m inductively by 

    ϕ^0    = ∅,
    ϕ^<λ   = ⋃_μ<λϕ(ϕ^<μ),
    ϕ^λ   = ϕ^<λ∪ϕ(ϕ^<λ),
    ϕ^∞   =⋃_λ∈ϕ^λ.


The least κ such that ϕ^∞ = ϕ^κ is called the closure ordinal of ϕ and denoted |ϕ|. If Γ is a class of operators, we write 
|Γ|

    |Γ| = sup{|ϕ|:ϕ∈Γ}.



Let Γ be a class of operators

    ϕ:𝒫(ℝ^m)→𝒫(ℝ^m).

We say that R⊂ℝ^n is Γ-inductive inductive (relation) if there is b ∈ℝ^m-n such that for all a ∈ℝ^n,

    a ∈ R  if, and only if,  (a,b) ∈ϕ^∞.


An operator ϕ is defined by a formula ψ(x,X) if, and only if, 

    ϕ(X) = {a ∈ℝ^m: ψ(a,X)}.

Thus, it is natural to consider classes of operators specified in terms of definability. Let Γ be a pointclass; we say that an operator ϕ is in Γ if it is defined by a formula in Γ with an additional predicate symbol X. We say that an operator is positive positive operator if this additional predicate symbol appears only positively, i.e., not in the scope of any negations (or in the antecedent of implications).
An operator is monotonemonotone operator if X⊂ Y⊂ℝ implies ϕ(X)⊂ϕ(Y). Every positive operator is monotone, of course. We may also speak of a formula defining an operator being positive under the obvious circumstances.


Let Γ be a pointclass.


  * Γ- is the pointclass of all Γ-inductive sets. 

  * Γ^pos- is the pointclass of all (positive-Γ)-inductive sets. 

  * Γ^mon- is the pointclass of all (monotone-Γ)-inductive sets.




A subset of ℝ is inductive if it is positive analytical inductive, i.e., letting  be the class of all inductive sets, we have

    = ⋃_n∈ℕ(^1,pos_n-).

A subset of ℝ is co-inductive if its complement is inductive. We write  for the class of co-inductive sets.
inductive (pointclass)


Pointclasses of the form ^1_n (or of other forms) can be relativized by allowing sets of reals as parameters. This leads to a relativized version of the inductive sets:

Let X⊂ℝ. A subset of ℝ is inductive on X if it is positive analytical-on-X inductive, i.e., letting (X) be the class of all sets inductive on X, we have

    (X) = ⋃_n∈ℕ(^1,pos_n(X)-).


In the definition above, “positive” refers to the variable on which the induction is carried out, not to the parameter X.

Let κ be the closure ordinal of the inductive sets, i.e., the supremum of closure ordinals of positive analytical inductive definitions. Then L_κ(ℝ) is the smallest model of  containing ℝ and 

    = 𝒫(ℝ)∩Σ_1^L_κ(ℝ),

where Σ_1-definability in the equation above allows for parameters.
Subsets of ℝ that are both inductive and co-inductive are called hyperprojective. By Δ_1-separation, these are the sets of reals in L_κ(ℝ). 

In general, let α be an ordinal and suppose that α is smaller than the least non-ℝ-projectible ordinal, i.e., that there is a surjection

    ρ:ℝ→ L_α(ℝ)

which is Σ_1-definable over L_α(ℝ) (this restriction can be relaxed, but all ordinals relevant to this article will be of this form). Let X be a set of reals coding L_α(ℝ) this way. Then, if κ_X is the closure ordinal of the X-inductive sets, we have that L_κ_X(ℝ) is the smallest model of  containing L_α(ℝ) and 

    (X) = 𝒫(ℝ)∩Σ_1^L_κ_X(ℝ).


An alternate definition of the inductive sets is given by the following theorem:

The following are equivalent:


  * A⊂ℝ is inductive,

  * there is a projective (or even analytic) set B⊂ℝ such that for all x∈ℝ,

    x ∈ A ↔∃ x_0 ∀ x_1 ∃ x_2 ∃ n  (x,⟨ x_0, , x_n⟩) ∈ B.




Moschovakis' theorem has the following easy consequence:

(X) = ^ℝ^0_1(X).

Assume X = ∅ for simplicity. To see that 

    ⊂^ℝ^0_1,

it suffices to notice that a statement of the form

    ∃ x_0 ∀ x_1 ∃ x_2 ∃ n  (x,⟨ x_0, , x_n⟩) ∈ B

can be decided by an open (in our sense) game on ℝ (the details can be verified e.g., as in <cit.>). Conversely, let U ∈^0_1∩𝒫(ℝ^2). 
Write 

    U = ⋃_i∈ℕU_i

as a countable union of basic clopen sets.
Thus, 

    x ∈^ℝU  if, and only if, ∃ x_0∈ℝ ∀ x_1∈ℝ  ∃ n∈ℕ  (x,⟨ x_0,x_1,⟩) ∈ U_n.

Since U_n is basic open, it is of the form

    O(s,t) = {(x,y)∈ℝ: (s,t)⊏ (x,y)}.

Let k_n be the length of s and t. By our choice of coding of infinite sequences of real numbers by real numbers, the first k_n digits of a sequence ⟨ x_0,x_1,⟩ depend only on x_0,, x_k_n.
Clearly, the set

    U_n^*    = {(x, ⟨ k, x_0,, x_k⟩) : k is greater than or equal to the length of the 
          unique finite  sequences s and t such that U_n = O(s,t), and 
           ∃ x_k+1 ∃ x_k+2  (x,⟨ x_0,x_1,⟩) ∈ U_n)};

is projective. Let

    A = {x∈ℝ: ∃ x_0∈ℝ ∀ x_1∈ℝ  ∃ n, m∈ℕ  (x,⟨ n, x_0,x_1,, x_n⟩) ∈ U^*_m}.

We claim that A is inductive. To see this, first notice that the collection of all pairs (x,⟨ n, x_0,x_1,, x_n⟩) belonging to some U^*_m is projective. Moreover, the real ⟨ n, x_0,x_1,, x_⟨ n, m⟩⟩ coding the tuple (n, x_0,x_1,, x_⟨ n, m⟩) agrees on the first n digits with the real ⟨ n, x_0,x_1,, x_n⟩ coding the tuple (n, x_0,x_1,, x_n). Thus, it follows from the definition of U_m^* that

    (x,⟨ n, x_0,x_1,, x_n⟩) ∈ U^*_m

implies

    (x,⟨⟨ n, m⟩, x_0,x_1,, x_⟨ n, m⟩⟩) ∈ U^*_m.

Hence, A is inductive. Finally, writing k_n for the length of the finite sequences s and t such that U_n = O(s,t),

    x∈ A iff    ∃ x_0∈ℝ ∀ x_1∈ℝ  ∃ n,m∈ℕ  (x,⟨ n, x_0,x_1,, x_n⟩) ∈ U^*_m
     iff    ∃ x_0∈ℝ ∀ x_1∈ℝ  ∃ n,m∈ℕ k_m≤ n ∧
           ∃ y_n+1 ∃ y_n+2  (x,⟨ x_0,x_1,, x_n, y_n+1, ⟩) ∈ U_m
     iff    ∃ x_0∈ℝ ∀ x_1∈ℝ  ∃ m∈ℕ  (x,⟨ x_0,x_1,⟩) ∈ U_m

Here, the first and second equivalences hold by definition. The third equivalence holds because whether (x,⟨ x_0,x_1,⟩) belongs to U_m depends only on the first k_m digits of ⟨ x_0,x_1,⟩ (by definition of k_m), which in turn depend only on x_0, x_1, , x_k_m.


We mention some results on the relation between inductive definitions, monotone inductive definitions, and positive inductive definitions.[We would like to thank A. S. Kechris for sharing the notes <cit.> with us.]
 
Let ℱ be a collection of operators containing Π^1_1 and closed under ∧,∨,∃^ℝ and recursive substitutions. Suppose that


  * WF∈ℱ̆, and

  * ℱ̆∈ℱ^mon-.

Then ℱ^mon- = ℱ-.


We state the following theorem without defining all notions involved, and afterwards state the instance in which we will be interested:

Let Q be a quantifier on ℝ. Let Γ be the pointclass of all sets which are positive Q-inductive and let Γ' be the pointclass dual to Γ. Then,

    Γ'- = Γ'^pos-.


In particular, letting Q be the quantifier ∃^ℝ, we have Γ = and Γ' =, and thus:



    - = ^pos-.



We mention that Harrington and Moschovakis' theorem as stated in <cit.> is more general and e.g., implies the following classical result:

Σ^1_1- = Σ_1^1,pos-.



We finish by recalling the definition of a Spector class (on ℝ).


A pointclass Γ is called[This differs from the notion of Spector pointclass” in Moschovakis <cit.>.] a Spector class on ℝ if the following conditions hold:


  * Γ is closed under ∧, ∨, ∃^ℝ, ∀^ℝ;

  * Γ contains all analytical relations;

  * Γ is parametrized by ℝ;

  * Γ has the prewellordering property.

Spector class (on ℝ)




 §.§ Short F_σ games

In order to locate winning strategies for ^0_2 games on ℝ within the L(ℝ)-hierarchy, it might be helpful to recall the location of winning strategies for Σ^0_2 games on ℕ in the L-hierarchy. This is a result of Solovay and is obtained by combining three theorems in recursion theory. 

The first one of them is also due to Solovay:

Σ^1,pos_1- = Σ^0_2.

A proof of Solovay's theorem can be found in <cit.> or in <cit.>. It will adapt to prove the analog for games on ℝ later, as well as the fact that ^ℝ^0_2-determinacy implies determinacy for ^0_2 games of length ω^2.
The second theorem is Grilliot's Theorem <ref> which, together with Theorem <ref> implies that

    Σ^1_1- = Σ^0_2.


The final theorem is due to Aczel and Richter. Recall that σ^1_1 denotes the least Σ^1_1-reflecting  ordinal.

|Σ^1_1| = σ^1_1, where |Σ^1_1| refers to closure under inductive operators on ℕ.


Combining everything, one sees that, in order to know which player wins a (lightface) Σ^0_2 game on ℕ, one needs not search beyond L_σ^1_1 for a winning strategy.
Our plan for locating Player I's winning strategies for ^0_2 games on ℝ will be to follow the same steps as in the argument for games on ℕ.


 



§ COINDUCTIVE OPERATORS


^ℝ^0_2 = ^pos-

We begin by quoting Wolfe's proof of Σ^0_2-determinacy and Solovay's proof of Theorem <ref> to prove that

    ^ℝ^0_2 ⊂^pos-.

Although the argument for this inclusion is very similar to the one for games on ℕ, a variation of it will be used below in the proof of Lemma <ref> below, so we prefer to include all the details.

Let A⊂ℝ^2 be a Σ^0_2 set (where we assume no parameter is needed; the general result follows by relativization). Say A is given by 

    (x,y)∈ A ↔∃ n ∀ m  (n,x↾ m,y↾ m) ∈ P,

where P is recursive. 
The proof proceeds by showing that winning a certain game G^*(⟨⟩) equivalent to A_x is equivalent to the membership of x in a set in ^pos-. For s a finite sequence of real numbers of even length, define G^*(s) to be the following game:


  * Players I and II alternate turns playing real numbers α_n.

  * After infinitely many rounds have taken place, Player I wins if, letting 

    t(m) = s^⌢⟨α_0,α_1,,α_m⟩
 
(i.e., letting t be the real coding the result of concatenating s with the first m moves of the play (α_0,α_1,)), 
we have

    ∃ n ∀ m ∀ m'<m  (n,x↾ m', t(m)↾ m') ∈ P.


Note that by our conventions on coding sequences of reals by single reals, we have

    s^⌢⟨α_0,α_1,⟩↾ m 
    = t(m)↾ m.
 
This implies that Player I has a winning strategy for the game on A if, and only if, she has one for the game on G^*(⟨⟩). The game G^*(s) is like G^*(⟨⟩), except that we assume that s has already been played. We shall show that Player I having a winning strategy is in ^pos-.


Let s be a finite sequence of real numbers of even length and X be a set of reals. Consider the following game, G(X,s):


  * Players I and II alternate turns playing real numbers α_n.

  * After infinitely many rounds have taken place, Player I wins if, and only if, letting 

    t(2m) = s^⌢⟨α_0,,α_2m⟩,
 
one of the following holds for each m∈ℕ:


  * there is n≤(s) such that
we have

    ∀ m' < m  (n, x↾ m', t(2m)↾ m') ∈ P.


  * t(2m) ∈ X.


The formula

    ϕ(s,X) = s has even length and Player I has a winning strategy in G(X,s)”

is clearly in ^ℝΠ^0_1 with an additional predicate for X and X appears positively in it. Since Π^0_1 games on ℝ are determined by the Gale-Stewart theorem <cit.>, the dual pointclass of ^ℝΠ^0_1 is ^ℝΣ^0_1. By Corollary <ref>, (<ref>) is in ^pos. The claim is now that

    s ∈ϕ^∞↔ Player I has a winning strategy in G^*(s)”


As in Solovay's proof, it is first shown that if s ∈ϕ^ξ, then Player I has a winning strategy in G^*(s), by induction on ξ. 
Suppose that this holds for ϕ^<ξ and that s ∈ϕ^ξ, so that Player I has a winning strategy in G(ϕ^<ξ,s), say, σ. A winning strategy for G^*(s) is obtained as follows:
Player I begins by playing G^*(s) by σ so long as the first winning condition of G(s,X) is satisfied, i.e., so long as after round m, letting t(m) = s^⌢⟨α_0,α_1,,α_m⟩, we have

    ∃ n≤(s) ∀ m' < m  (n, x↾ m', t(2m)↾ m') ∈ P.

If after some round this condition is not satisfied, then (since σ is a winning strategy), we must have 

    ∃ζ<ξ (s^⌢⟨α_0,,α_2m⟩∈ϕ^ζ),

in which case the induction hypothesis yields a winning strategy for the game G^*(s^⌢⟨α_0,,α_2m⟩) which should now be followed.

Conversely, if Player I has a winning strategy σ in G^*(s) then s must belong to ϕ^∞, for otherwise (by monotonicity of ϕ and determinacy of closed games) Player II has a winning strategy τ in G(s,ϕ^∞). If so, we could face off the strategies σ and τ against each other. Since τ is winning for Player II, after finitely many rounds, one will reach a partial play t(2m_1) = s^⌢⟨α_0,,α_2m_1⟩ such that the following hold:


  * ∀ n≤(s) ∃ m' < m_1  (n, x↾ m', t(2m_1)↾ m') ∉P; and

  * t(2m_1) ∉ϕ^∞.

The second condition yields a new strategy τ_1 for Player II that can now be played against σ in G(t(2m_1), ϕ^∞) until some stage m_2 at which the two conditions above hold again, etc. Continuing this process infinitely often yields a play

    t = s^⌢⟨α_0,α_1,⟩

such that for each k,

    ∀ n≤(t(2m_k)) ∃ m' < m_k  (n, x↾ m', t(2m_k+1)↾ m') ∉P,

so that

    ∀ n ∃ m'(n, x↾ m', t↾ m') ∉P,

contradicting the fact that σ was a winning strategy for Player I in G(s). This completes the proof of (<ref>). 

The second step consists in showing that

    ^pos-⊂^ℝ^0_2.

Let ϕ(s,X) be a positive  operator.

By a theorem of Kechris and Moschovakis (see <cit.>) and since ^0_2 is  parametrized by ℝ and has the prewellordering property, ^ℝ^0_2 is a Spector class on ℝ. By the Main Lemma” of Moschovakis <cit.> (see also <cit.>), in order to see that ϕ^∞∈^ℝ^0_2, it suffices to show that ^ℝ^0_2 is closed under ϕ, i.e., that for all A ∈^ℝ^0_2, the set

    A_ϕ = {(x,z) : ϕ(x, {y:(y,z) ∈ A})}

is in ^ℝ^0_2. 
Let us put

    A_z = {y∈ℝ:(y,z)∈ A}

and verify that

    {(x,z) : ϕ(x, A_z)}∈^ℝ^0_2.

Since ϕ is in , it follows from Moschovakis <cit.> that there is a ^1_1 formula ψ such that 

    ϕ(x,X) ↔∃ y_0 ∀ y_1  ∀ n ψ(x,⟨ y_0,, y_n⟩,X),

say,

    ϕ(x,X) ↔∃ y_0 ∀ y_1  ∀ n ∀ w ψ_0(w, x,⟨ y_0,, y_n⟩,X),

for some arithmetical ψ_0.

To verify that A_ϕ is in ^ℝ^0_2, fix x and z; we play the natural game given by the equation above:


  * Players I and II begin by playing real numbers y_0, y_1, until Player II decides to move on to the next stage after turn n. If this never happens, Player I wins.

  * Player II plays w ∈ℝ. Let θ_0 = ψ_0(w, x,⟨ y_0,, y_n⟩,A_z) and assume without loss of generality that θ_0 has been rewritten without implications and without negations whose scope is not only an atomic formula.

  * If θ_k has been defined and is a formula in the language of second-order arithmetic with an additional predicate A_z, we proceed by cases:


  * If the outermost logical connective of θ_k is a disjunction, then Player I chooses one of the disjuncts; we set θ_k+1 equal to this choice.

  * If the outermost logical connective of θ_k is a conjunction, then Player II chooses one of the conjuncts; we set θ_k+1 equal to this choice.

  * If θ_k is atomic then either it is an atomic formula not involving X, in which case the game ends and Player I wins if, and only if, θ_k holds; or it is of the form a ∈ A_z (since ϕ is positive). In the latter case, the game continues. 

  * Let B ∈^0_2 be such that A_z = ^ℝB. Players I and II alternate infinitely many turns playing reals w_0, w_1, w_2,. At the end, Player I wins if, and only if, (⟨ w_0, w_1, ⟩, w, a, z) ∈ B.


Clearly the winning condition for the game is ^0_2. It is easy to verify that Player I has a winning strategy in this game if, and only if (x,z) ∈ A_ϕ. This proves (<ref>).


Together with Harrington and Moschovakis's Theorem <ref>, the previous result yields:


- = ^ℝ^0_2.




§ COINDUCTIVE OPERATORS AND REFLECTION

Let ≼ be a binary relation. As a convention, we will use ≺ to denote the strict part of ≼ (i.e., x≺ y whenever x≼ y and y⋠x) and ≡ to denote ≼-equivalence (i.e., x≡ y whenever x ≼ y and y≼ x).  Similar conventions shall apply to variations of ≼, e.g., by subscripts. Notice that any two of ≼, ≺, and ≡ determine the other one.

Given a binary relation ≼ and an equivalence relation E with the same field, ≼ is said to commute with E if x≼ y, xEa, and yEb imply a≼ b, and similarly for the strict part ≺. A binary relation ≼ commutes with itself if it commutes with ≡; this follows from transitivity. An induction on the complexity of formulae shows that if ≼ is a binary relation that commutes with itself, then any first-order formula in the vocabulary {≺, =} holds of some tuple (x_1,, x_n) of objects in field(≼) if, and only if, it holds of any tuple (y_1,, y_n) such that x_i is ≡-equivalent to y_i for each i, so long as equality is interpreted as ≡.

We define in the natural way the notion of a  preorder on ℝ coding an initial segment of L(ℝ):

Let α be an ordinal. A coding of L_α(ℝ) is a preorder ≼ on a subset of ℝ such that

    (L_α(ℝ), ∈, =) ≅
    (field(≼), ≺, ≡)/≡.


The right-hand side of the displayed equation is the quotient structure of the structure  (field(≼), ≺, ≡) by ≡. The relation ≡ becomes equality in this quotient. If ≼ is a coding of some L_α(ℝ), then ≺ induces a wellfounded transitive relation on ≡-equivalence classes and there is a surjection ρ from field(≼) to L_α(ℝ) such that x ≺ y if, and only if, ρ(x) ∈ρ(y). If so then in this section only, let us denote ρ(x) by |x|_≼.


|| = σ_ℝ.


The proof of Theorem <ref> will be divided into two lemmata:


|| is Π^+_1-reflecting.
 
The lemma will be proved by an argument similar to the one of <cit.>. We have not checked whether the results of <cit.> (e.g., the lemma proved in the appendix) hold in full in the context of recursion on ℝ but, since we are only interested in proving Lemma <ref> (and are not analizing, e.g., ordinals of the form |Σ^1_n|), we do not need to be very careful with issues of definability, which greatly simplifies the situation.


Given an inductive definition ϕ, there is a natural way of associating to it a prewellordering on ℝ, namely, letting

    w(x) =
    least ξ such that x∈ϕ^ξ+1,     if it exists,
    ∞,     otherwise;

we put

    x≼_ϕ y  if, and only if,  w(x)≤ x(y).


Let ϕ be a universal coinductive operator, i.e., a coinductive operator such that whenever ψ is a coinductive operator, we have

    ψ(X) = {x∈ℝ: (x,a) ∈ϕ(X)}

for some a∈ℝ. (See Moschovakis <cit.> for a proof of the existence of universal coinductive sets; they can be defined uniformly in X.)
Below, we will define a coinductive operator Θ which simultaneously applies ϕ, defines the prewellordering associated to ϕ, and codes initial segments of L_α(ℝ) along the prewellordering given by ϕ. Given X⊂ℝ, write

    (i,X) = {(i,x):x∈ℝ}.

Conversely, we write

    X_i = {x∈ℝ:(i,x) ∈ X}.


Let X ⊂ℝ and ≼ be a binary relation on X. Suppose moreover that U is a set of real numbers and that X consists only of tuples of real numbers none of whose first coordinate belongs to U. We define a set (X,≼) and a binary relation ≼^+ such that if ≼ has field X and codes L_α(ℝ), then ≼^+ is a relation on X ⊕(X,≼)  which codes L_α+1(ℝ). The reason for mentioning U at all will become clear soon; roughly, it contains indicators which we will use to identify which reals belong to (X,≼) and which do not.

(X,≼) is the set of all tuples (x_0, φ, b⃗), where x_0 ∈ U, φ is a formula of arity (b⃗) + 1 in the vocabulary {=, ≺} and b⃗ is a finite tuple of elements of X. For x,y ∈ X⊕(X,≼), we put x ≺^* y if, and only if, one of the following holds:


  * x, y ∈ X and x≺ y;

  * y ∈(X,≼) is of the form (x_0, φ, b⃗) and (X, ≺, ≡) φ(b⃗, x).

Afterwards, let xEy if, and only if x and y have exactly the same ≺^*-predecessors, and put
x ≼^+ y if, and only if, xEy or there are aEx and bEy such that a ≺^* b. Hence, the relation ≺^* is a first approximation to ≺^+. It extends ≺ by specifying which of the elements of X are smaller than which of the new elements. It may thus be that an element x of (X,≼) turns out to have exactly the same ≺^*-predecessors as some other element y of (X,≼) or of X. We would then like to force these x and y to be ≡^+-equivalent, which is what we do. Note that this definition depended on U, so when in need of precision, we may write (X, ≼, U) for (X, ≼) and ≼^+U for ≼^+. 
By inspecting the construction, one sees that both (X, ≼, U) and ≼^+ are, say, hyperprojective (in fact, much simpler) in X, U, and ≼. Another feature of this definition is that if {≼_ι}_ι is an increasing family of relations obtained this way, and ≼_0 is a coding of some L_α(ℝ) then ⋃_ι≼_ι is a coding of some L_β(ℝ) (this is  where the set U in the definition is used).

We now define the operator Θ. Given X⊂ℝ, Θ will map X to a set Y with four parts, Y_0, Y_1, Y_2, and Y_3 defined in terms of X_0, X_1, X_2, and X_3. If X is of the right form, Y_1 will be a prewellordering of some length α+1 and Y_3 will be a coding of L_α+1(ℝ) with field Y_2.


  * Y_0 = ϕ(X_0);

  * Y_1 = X_1 ∪{(x,y): x ∈ Y_0 ∪field(X_1)  and  y∈ Y_0∖field(X_1)};

  * Y_2 = X_2 ∪(X_2, X_3, U), where U = Y_0∖field(X_1);

  * Y_3 = X_3^+U, where U = Y_0∖field(X_1).

The class of coinductive operators is closed under Boolean connectives and real quantifiers, so Θ is coinductive. The operator generates the inductive definition ϕ^∞ on its first component, while simultaneously coding ≼_ϕ in its second component. At each stage ξ, all new elements added to the field of ≼_ϕ, i.e., those of ≼_ϕ-rank ξ+1, are used to define the new elements of the set (Θ^ξ)_2 which acts as the field of a relation (Θ^ξ)_3 that codes L_ξ+1(ℝ). 

Any fixed point of Θ will contain a fixed point of ϕ in its first component. Because ϕ is universal coinductive,
an argument as in <cit.> (but using continuous reducibility in place of many-one reducibility[A proof of the Kleene's Recursion Theorem in this context can be found e.g., in <cit.>.]) shows that 

    |Θ| = |ϕ| = ||.

Hence, we need to show that |Θ| is Π^+_1-reflecting (although, to show that there is a Π^+_1-reflecting ordinal ≤||—which is really the point of this lemma—, we do not need the argument from <cit.>). Recall that, given a coding ≼ of some L_α(ℝ), in this section we write |x|_≼ for the element of L_α(ℝ) coded by x, if any.


Let ψ be a Π_1 formula in the language of set theory. Then, there is a coinductive operator Ψ, such that whenever λ≤ |Θ|,


  * for all c_1,, c_l ∈ (Θ^λ)_2,

    L_λ^+(ℝ)ψ(|c_1|_(Θ^λ)_3, , |c_l|_(Θ^λ)_3)↔ (c_1,, c_l) ∈Ψ(Θ^λ).


  * for all c_1,, c_l ∈ℝ, if there is some i < l+1 such that c_i ∉(Θ^λ)_2, then

    (c_1,, c_l) ∉Ψ(Θ^λ).



The main observation is that by Barwise-Gandy-Moschovakis <cit.>, for every admissible set A, a relation P on A is coinductive on A with parameters if, and only if, it is Π_1 over A^+, with parameters in A ∪{A}. Moreover,   this correspondence is uniform, in that the definition of the coinductive relation depends only on the Π_1 formula and its parameters, and not on the admissible set A (as long as it contains the parameters),[This can be shown directly for admissible sets of the form L_α(ℝ): given such a set, one defines an operator, elementary in L_α(ℝ), that successively outputs extensions of L_α(ℝ), like Θ does. To ensure that the operator is elementary, one can have it e.g., add only Σ_1-definable sets at each stage, instead of all first-order–definable sets. One can ask the operator to also check at each limit stage whether the Π_1 fact with parameters in L_α(ℝ) holds of the structure it outputs. Like we did with Θ, this operator can be ensured to have closure ordinal α^+ by asking it to generate a universal Σ_1(L_α(ℝ)) inductive definition in parallel. The operator for that can be obtained e.g., from the universal Σ_1(P) subset of ℝ, where P is a subset of ℝ coding L_α(ℝ). The set P can be obtained uniformly in a Σ_1(L_α(ℝ)) way (for multiplicatively indecomposable α; see Steel <cit.>).] and vice-versa.

Hence, given a Π_1-formula ψ, the set of all a_1,,a_l ∈ L_λ(ℝ) such that 
    L_λ^+(ℝ)ψ(a_1,,a_l )

is a coinductive subset of L_λ(ℝ) (and thus of L_λ+1(ℝ)).
Since (Θ^λ)_3 is a coding of L_λ+1(ℝ), there is a surjection

    ρ:(Θ^λ)_2 → L_λ+1(ℝ),

such that a pair (x,y) belongs to the strict part of (Θ^λ)_3 if, and only if, ρ(x) ∈ρ(y).
It follows that the preimage of a coinductive subset of L_λ+1(ℝ) under ρ is coinductive on ℝ from the parameters (Θ^λ)_2 and (Θ^λ)_3. Hence, there is a coinductive operator Ψ' such that 


  * for all c_1,, c_l ∈ (Θ^λ)_2,

    L_λ^+(ℝ)ψ(|c_1|_(Θ^λ)_3, , |c_l|_(Θ^λ)_3)↔ (c_1,, c_l) ∈Ψ'((Θ^λ)_2⊕ (Θ^λ)_3).


  * for all c_1,, c_l ∈ℝ, if there is some i < l+1 such that c_i ∉(Θ^λ)_2, then

    (c_1,, c_l) ∉Ψ'((Θ^λ)_2⊕ (Θ^λ)_3).




Now, both (Θ^λ)_2 and (Θ^λ)_3 reduce to Θ^λ continuously, and this reduction is uniform in λ, so 
there is an operator Ψ as desired.


Let ψ be a Π_1 sentence and let Ψ be given by the sublemma, so that for all λ≤|Θ| and all c_1,, c_l ∈ (Θ^λ)_2, we have

    L_λ^+(ℝ)ψ(|c_1|_(Θ^λ)_3, , |c_l|_(Θ^λ)_3)↔ (c_1,, c_l) ∈Ψ(Θ^λ).

Since ϕ was chosen to be a universal coinductive operator, Θ(X) is complete coinductive for all X, so there is a continuous function

    g:ℝ^l↦ℝ

such that for all c_1,, c_l ∈ℝ and all X⊂ℝ do we have

    (c_1,, c_l) ∈Ψ(X) ↔ g(c_1,, c_l)∈Θ(X).

Hence,

    L_λ^+(ℝ)ψ(|c_1|_(Θ^λ)_3, , |c_l|_(Θ^λ)_3)↔ g(c_1,, c_l) ∈Θ(Θ^λ).

Suppose then that there are elements γ_1,,γ_l of L_λ(ℝ) such that

    L_|Θ|^+(ℝ)ψ(γ_1,, γ_l).

By construction, (Θ^<λ)_3 is a coding of L_λ(ℝ) for each λ, so (Θ^∞)_3 is a coding of L_|Θ|(ℝ)
with field (Θ^∞)_2. Thus, there is a surjection 

    ρ:(Θ^∞)_2 → L_|Θ|(ℝ)
 
such that the pair (x,y) belongs to the strict part of (Θ^∞)_3 if, and only if, ρ(x) ∈ρ(y). Pick c_1,, c_l such that for each 0<i<l+1, ρ(c_i) = γ_i. Then,

    L_|Θ|^+(ℝ)ψ(|c_1|_(Θ^∞)_3, , |c_l|_(Θ^∞)_3).

By (<ref>),

    g(c_1,, c_l) ∈Θ(Θ^∞) ⊂Θ^∞.
 
|Θ| is a limit ordinal, so there is some λ<|Θ| such that 

    g(c_1,, c_l) ∈Θ(Θ^λ),

so that, by (<ref>),

    L_λ^+(ℝ)ψ(|c_1|_(Θ^λ)_3, , |c_l|_(Θ^λ)_3).
 
Notice that the sequence of sets {(Θ^λ)_2:λ<|Θ|}, as well as the sequence of isomorphisms witnessing that each (Θ^λ)_3 is a coding of L_λ+1(ℝ) are strictly increasing, and this implies that 

    |c_i|_(Θ^λ)_3 = |c_i|_(Θ^∞)_3

for each 0<i<l+1, which yields the result. This proves the lemma.



If κ is Π^+_1-reflecting, then ||≤κ.

This proof is like that of <cit.>.
Suppose κ is Π^+_1-reflecting and let ϕ be a coinductive operator. Since κ is Π^+_1-reflecting, it is  ℝ-recursively inaccessible. Because coinductive relations are universal relations on the next admissible set, it follows that if A ∈𝒫(ℝ) ∩ L_α(ℝ), then L_α^++1(ℝ) can compute coinductive relations on A.
Now, L_κ(ℝ) can compute the sequence {ϕ^λ:λ<κ} in a Π_1 way (with parameters): x 
is the λth element of this sequence if every transitive set of the form L_α(ℝ) containing an increasing (λ + 1)-sequence of ℝ-admissible sets believes that x is the λth element of the sequence. Moreover, this definition is uniform on  ℝ-recursively inaccessible ordinals.
Thus, letting ψ be a Π_1 formula such that

    a ∈ϕ^<κ↔ L_κ(ℝ)∃λ ψ(a,λ),

the question of whether a belongs to ϕ(ϕ^<κ) is coinductive over ϕ^<κ, hence over L_κ(ℝ), hence universal over L_κ^+(ℝ), so, by Π^+_1-reflection, ϕ(ϕ^<κ)⊂ϕ^<κ, as desired.


This concludes the proof of Theorem <ref>. The main consequence of interest to us is:

𝒫(ℝ) ∩Σ_1^L_σ_ℝ(ℝ) = ^ℝ^0_2.

By Theorems <ref> and <ref>,
we need to show that 

    𝒫(ℝ) ∩Σ_1^L_||(ℝ) = -.

That the class on the right-hand side is contained in the one on the left is clear. The converse follows from the proof of Lemma <ref>: one can use a coinductive operator to inductively generate codes for initial segments of L(ℝ) below ||, so an existential statement about L_||(ℝ) can be rephrased in terms of membership in the least fixed point of a coinductive operator.




§ F_Σ-DETERMINACY


Suppose that all sets in ^ℝ^0_2 are determined. Then, all ^0_2 games of length ω^2 are determined.

Note that ^0_2 games of length ω with moves in ℝ are determined.
Suppose that all sets in ^ℝ^0_2 are determined and let A∈^0_2. We show that the game of length ω^2 with payoff A is determined. Let us refer to this game as G. The proof begins very much like that of Theorem <ref>: we begin by replacing G with a game G^*(⟨⟩). Without loss of generality we shall assume that there is a recursive set P such that A is given by 

    x∈ A ↔∃ n ∀ m  (n,x↾ m) ∈ P,


For s a finite sequence of real numbers of even length, define G^*(s) to be the following game:


  * Players I and II alternate ω^2-many turns playing natural numbers to produce a countable sequence {α_n:n∈ℕ} of real numbers.

  * After ω^2-many rounds have taken place, Player I wins if, letting 

    t(m) = s^⌢⟨α_0,α_1,,α_m⟩,
 
we have

    ∃ n ∀ m ∀ m'<m  (n, t(m)↾ m') ∈ P.


As before, Player I has a winning strategy for G if, and only if, she has one for G^*(⟨⟩). Moreover, Player II has a winning strategy for G if, and only if, she has one for G^*(⟨⟩). The game G^*(s) is like G^*(⟨⟩), except that we assume that s has already been played.


Let n_s be a natural number, s be a sequence of natural numbers of even length ω· n_s and X be a set of sequences of natural numbers of length <ω^2. Consider the following game, G(X,s):


  * Players I and II alternate ω^2-many turns playing natural numbers to produce digits corresponding to a countable sequence {α_n:n∈ℕ} of real numbers.

  * After ω^2-many rounds have taken place, Player I wins if, and only if, letting 

    t(m) = s^⌢⟨α_0,,α_m⟩,
 
one of the following holds for each m∈ℕ:


  * there is n≤ n_s such that
we have

    ∀ m' < m  (n, t(m)↾ m') ∈ P.


  * t(m) ∈ X.


Thus G(X,s) is a game on ℕ of length ω^2. Write

    ϕ(s,X) =  Player I has a winning strategy in G(X,s).”

The argument from Theorem <ref> shows that if s ∈ϕ^∞, then Player I has a winning strategy in G^*(s). To complete the proof, it remains to show that if s∉ϕ^∞, then Player II has a winning strategy in G^*(s).

Notice that G(X,s) is a game of length ω^2 with moves in ℕ and payoff in Π^0_1 (using X as a second-order oracle). We consider the following auxiliary game, which we shall denote by H(X,s):

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

Here, σ_i and τ_i are real numbers coding strategies for games on ℕ of length ω. Player I wins the game if, and only if, the sequence

    (s, σ_0*τ_0*, σ_1*τ_1,)

satisfies the winning condition of G(X,s). Here, σ*τ denotes the result of facing off the strategies σ and τ against each other. Thus, H(X,s) is a game of length ω with moves in ℝ and payoff in Π^0_1(X).
We will need a sublemma:

Suppose that all subsets of ℝ in ^ℝ^0_1(X) are determined. Then, the following are equivalent:


  * Player I has a winning strategy in H(X,s); and

  * Player I has a winning strategy in G(X,s).

Moreover, the games are determined.

[Proof Sketch]
The equivalence is proved by arguing as in the proof of <cit.>. This is possible because the game H(s,X) is Π^0_1(X). The proof of <cit.> uses determinacy of sets in ^ℝ^0_1; in this case, we need determinacy of sets in ^ℝ^0_1(X), which we are assuming.
H(X,s) is closed and thus determined by the Gale-Stewart theorem. The proof of <cit.> also shows that if Player II has a winning strategy in H(X,s), then she has one in G(X,s), so that this game is also determined.



Sublemma <ref> essentially states that Lemma <ref> holds if one replaces ^0_2 by ^0_1.
The part of the proof of <cit.> used in the proof of Sublemma <ref> goes through for ^0_1 games. It would also go through for ^0_1 games if one switched the order in which the players move in the definition of H(X,s). The proof, however, does not go through for more complicated games. 
By different arguments (involving the theory of scales in L(ℝ)), one can prove analogues of Lemma <ref> for more complicated pointclasses, up to ^1_1 (see <cit.>). The result of replacing ^0_2 by ^1_1 in the statement of Lemma <ref> is not provable in .


It follows from Corollary <ref> that if X ∈ L_α(ℝ), then all winning strategies for games on ℝ with payoff in ^0_1(X) are definable over L_α^+(ℝ), so ^ℝ^0_1(X) belongs e.g., to L_α^++(ℝ).

^ℝ^0_2 is closed under the open-game-on-ℝ quantifier; i.e.,
if X ∈^ℝ^0_2, then ^ℝ^0_1(X)⊂^ℝ^0_2.

This can be proved directly by an argument like the one of (<ref>) in Theorem <ref>. Alternatively, one can also appeal to
the Main Lemma” of Moschovakis <cit.> (as in the proof of Theorem <ref>): since operators definable from X by an open game quantifier are X-inductive (by Corollary <ref>) and ^ℝ^0_2 is a Spector class, it suffices to show that ^ℝ^0_2 is closed under the inductive step. But the inductive step is positive analyical on X and a real parameter, so clearly ^ℝ^0_2 is closed under it. 
Write

    ϕ'(s,X) =  Player I has a winning strategy in H(X,s).”

Clearly, ϕ'(s,X) is an operator in ^ℝ^0_1 and thus in  (by Corollary <ref>). By Theorem <ref>, there is some η≤σ_ℝ such that ϕ'^∞ = ϕ'^η. By Corollary <ref> and the hypothesis of the lemma,

    L_σ_ℝ(ℝ).

Since σ_ℝ is recursively ℝ-inaccessible, i.e., ℝ-admissible and a limit of ℝ-admissibles, it follows that for every ζ<η, every subset of ℝ in ^ℝ^0_1(ϕ'^ζ) is determined. Hence, an induction along ζ shows that

    ϕ'^ζ = ϕ^ζ

for all ζ<η. It follows that 

    ϕ^∞ = ϕ'^∞∈Σ_1^L_σ_ℝ(ℝ) = ^ℝ^0_2.
 
(In case η = σ^ℝ, the last step of the induction follows from Sublemma <ref>.)

Now, suppose that s ∉ϕ^∞. By definition, Player I does not have a winning strategy in G(ϕ^∞,s). By the two sublemmata, G(ϕ^∞,s) is determined. Thus, Player II has a winning strategy in G(ϕ^∞,s). But then, an argument as in the proof of Theorem <ref> shows how to turn this into a winning strategy for G^*(s). This concludes the proof of the lemma.


We are now led to the main theorem of the article.


The following are equivalent:


  * ^0_2-determinacy for games of length ω^2;

  * There is a Π^+_1-reflecting model of  containing ℝ.


If ^0_2 games of length ω^2 are determined, then clearly sets in ^ℝ^0_2 are determined, so that L_σ_ℝ(ℝ), by Corollary <ref>.

Conversely, suppose that there is a Π^+_1-reflecting model of  containing ℝ. By Corollary <ref>, L_σ_ℝ(ℝ). Since σ_ℝ is ℝ-admissible, 

    𝒫(ℝ)∩ L_σ_ℝ(ℝ) = 𝒫(ℝ)∩Δ_1^L_σ_ℝ(ℝ).

Let Γ be the pointclass of all sets of reals which are Σ_1-definable over L_σ_ℝ(ℝ) with parameters.
Using that L_σ_ℝ(ℝ), Steel <cit.> implies that Γ has the scale property. Since σ_ℝ is ℝ-admissible, Γ is closed under existential and universal real quantification and thus by Moschovakis <cit.>, it has the uniformization property.
Hence, the hypotheses for the Kechris-Woodin determinacy transfer theorem <cit.> are satisfied, and we may apply it to conclude that all sets in Σ_1^L_σ_ℝ(ℝ) are determined. By Corollary <ref>, all sets in ^ℝ^0_2 are determined. By Lemma <ref>, ^0_2-games of length ω^2 are determined.




§ CONCLUDING REMARKS

Let us remark that the proof of Theorem <ref> also yields the following result, which
was pointed out in <cit.>: 

The following are equivalent over :


  * ^0_1-determinacy for games of length ω^2,

  * There is a transitive model of + containing the reals.


To prove Theorem <ref>, repeat the proof of Theorem <ref>, using the least κ such that L_κ(ℝ) is admissible in place of σ_ℝ, Corollary <ref> in place of Corollary <ref>, and Sublemma <ref> in place of Lemma <ref>.


A classical theorem of Kripke states that, in L, the least α such that L_α is a model of + Σ_1-separation is the union of a chain of Σ_1-elementary substructures. The situation is analogous in L(ℝ).
This and Theorem <ref> imply the consistency results mentioned in the introduction. 


The following theories are strictly increasing in consistency strength:


  *  +  + ℝ exists” + ;

  *  +  + ℝ exists” + ^0_2-determinacy for games of length ω^2;

  * +  +ℝ exists” +  + Σ_1-separation.


Working in +  + ℝ exists,” assume that ^0_2 games of length ω^2 are determined. We show that there is a model of

    +  + ℝ exists”+.
 
Consider the following game of length ω^2:


  * Player I begins by choosing a ^0_1 game of length ω^2;

  * Player II decides which role she wants to have in the game;

  * Players I and II play the game chosen by Player I, taking the roles specified by Player II.

This game is perhaps not ^0_1, but it is certainly, say, Δ^0_2. It clearly cannot be won by Player I, and any winning strategy for Player II easily reduces continuously to a winning strategy for some player for any prescribed ^0_1 game of length ω^2. Since  ℝ exists, one may use collection to conclude that there is a set A containing winning strategies for all ^0_1 games of length ω^2. From A and ℝ one may use Σ_0-separation to conclude that there is a universal ^ℝ^0_1 set. Hence, there is a universal  set, from which one can easily compute a prewellordering of ℝ whose length is an ℝ-admissible ordinal κ. By collection, this ordinal exists, so L_κ(ℝ) + and

    = 𝒫(ℝ)∩Σ^L_κ(ℝ)_1.

Since all ^0_2 games of length ω^2 are determined, all ^ℝ^0_1 games of length ω are determined, and so 

    L_κ(ℝ).


For the remaining implication, suppose that  holds and Σ_1-separation holds. It follows that 

    L(ℝ) + Σ_1-Separation.

To see this, we assume without loss of generality that for no ordinal η do we have 

    L_η(ℝ) + Σ_1-Separation,

i.e., that the least non-ℝ-projectible ordinal does not exist. Thus, it suffices to show that every subset of ℝ which is Σ_1-definable (with parameters) over L(ℝ) belongs to L(ℝ). If not, then by Steel <cit.>, there is a partial surjection from ℝ onto L(ℝ) which is Σ_1-definable over L(ℝ) with parameters. However, L(ℝ) is a Σ_1-definable class and Σ_1-separation holds (in V), so this surjection is actually a set. But this is impossible, for its restriction to the ordinals is also a surjection. Thus,

    L(ℝ) + Σ_1-Separation

as claimed. Working in L(ℝ), there are arbitrarily large ℝ-stable ordinals. But it is immediate from the definition that if

    L_α(ℝ)≺_1 L_α^++1(ℝ),

(recall Definition <ref>) then σ_ℝ<α, so there is a (set) model of  in which all games of length ω^2 are determined (and  holds in this model, additionally).


We finish with some remarks.
Many questions are open in the realm of F_σ games. A very interesting question is the consistency strength of determinacy for F_σ games of length ω· 2. Using the fact that F_σ games of length ω are determined, this is seen to be equivalent to determinacy for games of length ω with payoff in ^0_2. By Solovay's Theorem <ref> and Grilliot's Theorem <ref>, this is equivalent to determinacy for games of length ω with payoff in ^1_1-. By a theorem of Aanderaa <cit.>, we have

    ^1_1-⊂^1_1-,

so a theorem of Welch <cit.> shows that determinacy for F_σ games of length ω· 2 implies the existence of an inner model with a strong cardinal.

A different family of questions concerns the study of || and related ordinals. Gostanian <cit.> proves that σ^1_1 is the least ordinal α such that 

    δ_α: = sup{δ: δ is the length of an α-recursive wellorder} < α^+.

This characterization obviously not true for ||, since 

    sup{δ: δ is the length of a Δ^1_1-prewellordering of ℝ} = ω_1,

and L_ω_1(ℝ) is not admissible. Is there a (somewhat) similar characterization of ||? Another question concerns the degree of stability of ||.
The fact that σ^1_1 is δ_σ^1_1-stable but not (δ_σ^1_1+1)-stable (see <cit.>) depends on Gostanian's characterization and thus does not immediately seem to generalize.


By a slightly more elaborate argument involving Inner Model Theory (one can e.g., use the results in Part II of Müller <cit.>), one can replace  by  in the statement of Theorem <ref>(<ref>) (and, in fact, by much stronger theories). Similarly, and using Theorem <ref>, one can replace Theorem <ref>(<ref>) by the theory  + ^0_1-determinacy for games of length ω^2. We omit the details.




The following theories are strictly increasing in consistency strength:


  * +  + ℝ exists” + ;

  *  + ^0_1-determinacy for games of length ω^2;

  *  + ^0_1-determinacy for games of length ω^2 + {“there are n Woodin cardinals”: n∈ℕ};

  *  +  + ℝ exists” + ^0_2-determinacy for games of length ω^2;

  *  + ^0_2-determinacy for games of length ω^2;

  *  + ^0_2-determinacy for games of length ω^2 + {“there are n Woodin cardinals”: n∈ℕ};

  *  + +ℝ exists” +  + Σ_1-separation


[Proof Sketch]
(<ref>) is equivalent over  to the existence of a transitive model of (<ref>) containing ℝ (this can be seen by arguing as in the proof of Theorem <ref>, using Corollary <ref> and Sublemma <ref>; cf. the remark in <cit.>).

It remains to show how to obtain a model of (<ref>) within (<ref>) and how to obtain a model of (<ref>) within (<ref>). We sketch the argument for the latter.

As in the proof of Theorem <ref>, we may work in L(ℝ). Let A be a complete Σ_1^L_σ_ℝ(ℝ) set, so that  every ^0_2 game on ℝ has  a winning strategy continuously reducible to A.
By a theorem of Müller <cit.>, there is an ω_1-iterable hybrid Σ-premouse N which captures A and with, say, one Woodin cardinal. Similarly, there is an ω_1-iterable hybrid Σ-premouse M which captures A and with, say, two Woodin cardinal. Thus, N is countable and ω_1-iterable in M. It follows that M is correct about which player wins each ^0_2 game on ℝ. By a theorem of Neeman <cit.>, the existence (and iterability) of N implies the determinacy of all sets in ^ℝ^0_2. Thus, these sets are determined in M and so M satisfies ^0_2-determinacy for games of length ω^2. The same argument yields such an M with any finite amount of Woodin cardinals, and thus the required model exists by compactness.





abbrv


