The consistency strength of long projective determinacy
Juan P. Aguilera Sandra Müller



[2010]03E45, 03E60, 03E15, 03E55 

 


Juan P. Aguilera, Institut für diskrete Mathematik und
  Geometrie, Technische Universität Wien. Wiedner Hauptstrasse 8-10,
  1040 Wien, Austria. 
aguilera@logic.at
 
Sandra Müller, Kurt Gödel
  Research Center, Institut für Mathematik, UZA 1, Universität
  Wien. Augasse 2-6, 1090 Wien, Austria.
mueller.sandra@univie.ac.at 
The second-listed author, formerly known as Sandra Uhlenbrock, was
  partially supported by FWF grant number P 28157. 






  We determine the consistency strength of determinacy for projective
  games of length ω^2. Our main theorem is that
  ^1_n+1-determinacy for games of length ω^2 implies the
  existence of a model of set theory with ω + n Woodin
  cardinals. In a first step, we show that this hypothesis
  implies that there is a countable set of reals A such that
  M_n(A), the canonical inner model for n Woodin cardinals
  constructed over A, satisfies A = and the Axiom of
  Determinacy. Then we argue how to obtain a model with ω + n
  Woodin cardinal from this.
  
  We also show how the proof can be adapted to investigate the
  consistency strength of determinacy for games of length ω^2
  with payoff in ^^1_1 or with σ-projective
  payoff.


The consistency strength of long projective determinacy
    Sandra Müller
    December 30, 2023
=======================================================







§ INTRODUCTION

We study the consistency strength of determinacy for games of length
ω^2 with payoff in various pointclasses Γ.
Specifically, given a set A⊂ω^ω^2, i.e., a set of
sequences of natural numbers of length ω^2, with
A ∈Γ, consider the following game:

    [     I   n_0         n_2               n_ω            ;    II         n_1         n_3             n_ω+1       ]

 Players I and II alternate turns playing natural numbers to produce
 some
 x = (n_0, n_1, …, n_ω, n_ω+1, …) ∈ω^ω^2.  Player I wins such a run x of
 the game if, and only if, x ∈ A; otherwise, Player II wins. We
 study the strength of the statement that games of this form are
 determined, i.e., that one of 
 the players has a winning strategy. For all nontrivial classes
 Γ, this question is independent of Zermelo-Fraenkel set theory
 with the Axiom of Choice (); for some of them, however, it
 is known to follow from natural strengthenings of , namely, from assumptions
 on the existence of large cardinals. 

 Recall that the projective subsets of a Polish space are those
 obtainable from Borel sets in finitely many stages by applying
 complements and projections from a finite power of the space.  We are
 mainly interested in the case where Γ is a projective
 pointclass, i.e., ^1_n for some natural number n, but we will
 also consider the cases in which Γ is equal to
 ^^1_1 or a σ-projective pointclass.[The
   pointclass of all σ-projective sets is the smallest
   pointclass closed under complements, countable unions, and
   projections, where countable unions refer to sets which are subsets
   of the same product space. Moreover, we as usual identify  and
   .]
 
 The study of games of length ω^2 is motivated by the folklore
 result that projective determinacy for games of length ω
 implies projective determinacy for games of length α, for any
 α<ω^2. It is also not difficult to see that
 ^1_n+1-determinacy of length ω^2 follows from analytic
 determinacy for games of length ω·(ω+n), for 
 natural numbers n.[In fact, an argument as in
   <cit.> with a more careful analysis of the
   complexity of the payoff sets (using projective determinacy) shows
   that these two determinacy hypotheses are equivalent.]

 Analytic determinacy for games of length ω· (ω + n)
 was proved by Neeman <cit.> from a large cardinal
 hypothesis. Specifically, he assumed the existence of a weakly
 iterable model of set theory with ω + n Woodin cardinals,
 along with a sharp for the model. In fact, he proved this result for
 analytic games of any fixed countable length
 ω· (θ + 1), from corresponding assumptions. This
 naturally yields the question whether his results are optimal, i.e.,
 whether the determinacy of these long games implies the existence of
 models with certain numbers of Woodin cardinals. In light of this, we
 prove the following theorem:
  
  
    Suppose that ^1_n+1-determinacy for games of length
    ω^2 holds and let x ∈ be arbitrary. Then, there is a
    proper class model M of  with ω+n Woodin cardinals
    such that x ∈ M.
  

  The Woodin cardinals of the model we construct in the proof of
  Theorem <ref> are in reality countable. Moreover,
  the model is a premouse, i.e., fine structural, and we can in fact
  construct it such that it is active, i.e., it has a sharp on top. As
  a corollary of the theorem and the results from <cit.>, we
  obtain the following equiconsistencies, which also connect
  projective determinacy for games of length ω^2 to projective
  determinacy for games on reals.[We would like to thank the
    referee for asking whether (<ref>) and (<ref>) could be
    added to Corollary <ref>; see also <cit.>.]

  
    The following schemata are equiconsistent:
    
    
  *  + {“^1_n-determinacy for games of length
      ω^2 on ω” : n∈ω}. 
    
  *  +  +  + {“there are n Woodin
      cardinals”: n∈ω}. 
    
  *  + {“there are ω+n Woodin
      cardinals”: n∈ω}. 
    
  *  +  +  + {“^1_n-determinacy for games of length
      ω on ” : n∈ω}.
    
  *  +  +  +
      {“ V^(ω,)^1_n-determinacy for games
      of length ω on ω” : n∈ω}.
    
  

  The proof of Theorem <ref> has two main parts: in
  the first one, the hypothesis is shown to imply that for a closed
  and unbounded set of countable sets of reals A, there is a fine
  structural model of the Axiom of Determinacy with n Woodin
  cardinals whose set of real numbers is precisely A. In the second
  part we use a Prikry-like partial order to force over these models
  and obtain via a translation procedure an infinite sequence of
  Woodin cardinals below the already existing ones. The proof of
  Corollary <ref> is sketched in the final section of
  this paper.

  

  

  
Background The situation for games of length
  ω is well understood: There is a tight connection beween
  determinacy for these games and the existence of inner models with
  large cardinals. Martin <cit.> showed that Borel games are
  determined in . Contrary to that, determinacy for ^1_1
  (i.e., analytic) games cannot be proved in  alone. By theorems
  of Martin <cit.> and Harrington <cit.> ^1_1 games
  are determined if, and only if, x^♯ exists for every
  x∈. Martin and Steel <cit.> proved, for each
  n∈ω, that the existence of n Woodin cardinals with a
  measurable cardinal above implies the determinacy of all
  ^1_n+1 sets. Woodin (unpublished) improved this for odd
  n by showing that the existence of M_n^♯(x), the canonical
  active ω_1-iterable inner model with n Woodin cardinals
  constructed over x, for all reals x suffices to show
  ^1_n+1 determinacy. Afterwards, Neeman improved this in
  <cit.> even further and showed that for all n, the existence
  of M_n^♯(x) for all reals x implies determinacy of all
  ^n(<ω^2-^1_1) sets. Concerning the other direction,
  Woodin (see <cit.>) showed that if ^1_n+1 games are
  determined, then M_n^♯(x) exists for all reals x, thus
  establishing a level-by-level characterization of projective
  determinacy in terms of the existence of inner models with large
  cardinals. Similar characterizations are known for
  σ-projective games of length ω (see <cit.> and
  <cit.>). Determinacy for games of length ω with payoff in
  ^^1_1 is equivalent to ^L() (see
  <cit.>).

 

  Woodin showed that the existence of ω^2 Woodin cardinals
  under choice is equiconsistent with ^+ + and the existence
  of a normal fine measure on  (see Remark 9.98 in
  <cit.>). By this and a result of Trang (see <cit.>, case α = 2), determinacy of analytic games of
  length ω^3 implies the consistency of ω^2 Woodin
  cardinals under choice. In fact, a similar result holds for
  ω^α Woodin cardinals and determinacy of analytic games
  of length ω^1+α for all 1 < α < ω and all
  limit ordinals ω≤α < ω_1. For details see
  Theorems 2.2.1 and 2.3.11 in <cit.>, as well as <cit.> and
  <cit.>.


  

  
Further results The proof of Theorem
  <ref> uses game arguments based on techniques from
  Martin and Steel <cit.> and <cit.>, tracing back to
  arguments of H. Friedman <cit.> and Kechris and Solovay
  <cit.> as well as inner model theoretic methods based on the
  unpublished notes <cit.>. The method of the proof of Theorem
  <ref> can also be used to show the following two
  generalizations:

 
   Suppose that ^^1_1-determinacy for games of length
   ω^2 holds and let x ∈ be arbitrary. Then, there is a
   proper class model M of  with ω+ω Woodin
   cardinals such that x ∈ M.
 

 As above, it is not hard to show that determinacy of analytic games
 of length ω·(ω+ω) implies determinacy of
 ^^1_1 games of length ω^2. Our methods also
 generalize to games with σ-projective payoff and premice of
 class S_α (see <cit.> and <cit.>).


  Suppose that σ-projective determinacy for games of length
  ω^2 holds and let x ∈ be arbitrary. Then, for every
  α < ω_1, there is a proper class model M of 
  with ω Woodin cardinals with supremum λ which is of
  class S_α above λ and such that x ∈ M.




  
Outline In Section <ref>, we
establish conventions and recall some known facts about extender
models which will be used later on. Focusing first on the case
n = 1, Section <ref> contains the main argument and shows
that determinacy for games of length ω^2 with ^1_2 payoff
implies the existence of fine structural models of the Axiom of
Determinacy with one Woodin cardinal. In Section <ref>, we
argue that this fine structural model satisfies  and ^+. In
Section <ref>, we show how to obtain a model of
 with ω+1 Woodin cardinals from this model. Finally, in
Section <ref> we sketch the proof of Corollary
<ref> and explain how to carry out the modifications
needed to prove Theorems <ref> and
<ref>. 


We would like to thank John Steel for valuable discussions related to
this paper, in particular to Lemma <ref>, and for
making the unpublished notes <cit.> available to us. Moreover, we
would like to thank Grigor Sargsyan for his helpful comments on an
earlier version of this manuscript. Finally, we would like to thank
the referee for carefully reading our paper and making several
valuable suggestions.




§ PRELIMINARIES


For basic set theoretic definitions and results we refer to
<cit.> and <cit.>. Moreover, we work with canonical, fine
structural models with large cardinals, called premice. We
refer the reader to e.g., <cit.> for an introduction, and to
<cit.>, <cit.>, and <cit.> for additional
background. In particular, we will use Mitchell-Steel indexing for
extender sequences and the notation from <cit.>. As in
<cit.> we will consider relativized premice constructed over
arbitrary transitive sets X. Let
= {∈̇, Ė, Ḟ, Ẋ} denote the language of
relativized premice, where Ė is the predicate for the extender
sequence, Ḟ is the predicate for the top extender, and Ẋ
is the predicate for the set over which we construct the premouse.

For a transitive set X, we say an X-premouse
M = (J_α^E⃗, ∈, E⃗, E_α, X) for
E⃗ = (Ė)^M, E_α = (Ḟ)^M, and X = (Ẋ)^M
is active if E_α≠∅. Otherwise, we say M
is passive. We let
M | γ = (J_γ^E⃗, ∈, E⃗↾γ, E_γ, X) for γ≤ M ∩. Moreover, we
write M || γ for the passive initial segment of M of height
γ, i.e.
M || γ = (J_γ^E⃗, ∈, E⃗↾γ, ∅, X), for γ≤ M ∩. In particular,
M||^M denotes the premouse N which agrees with M except that
we let (Ḟ)^N = ∅. We say an ordinal η is a
(strong) cutpoint of M if there is no extender E on the
M-sequence with (E) ≤η≤(E).

An arbitrary X-premouse might not satisfy the Axiom of Choice, but
it can be construed as an ordinary premouse which satisfies the Axiom
of Choice if a well-order of X is added generically. In particular,
every X-premouse M is well-ordered mod X, i.e., for every
set Y ∈ M there is an ordinal α and a surjection h in M
such that h  X ×α↠ Y. In this
article we shall mainly be interested in X-premice which satisfy the
Axiom of Determinacy (and hence not the full Axiom of Choice), where
X ∈, i.e., X is a countable set of reals.

Throughout this article, we work under the assumption that all premice
are tame, i.e., that there is no extender on the sequence of a
premouse overlapping a Woodin cardinal. This results in no loss of
generality, as otherwise the conclusions of the theorems in Section
<ref> hold.

In the rest of this section we summarize some facts about premice
which we are going to need later. Most of these can be found in
<cit.> and <cit.> for x-premice for a real x and they
straightforwardly generalize to X-premice for arbitrary countable
sets of reals X. Fix such a set X ∈ for the rest of this section.


  Let M be an X-premouse and let α<ω_1^L. Then we say
  that M is α-small if, and only if, for every ordinal
  κ≤ M ∩ such that there is an extender with
  critical point κ on the M-sequence, in M | κ there
  is no set of ordinals W of order-type α such that every
  ordinal in W is a Woodin cardinal in M | κ.


If it exists and is unique, we denote the ω_1-iterable,
countable, sound X-premouse which is not α-small, but all of
whose proper initial segments are α-small, by
M_α^♯(X). In this case M_α(X) denotes the result of
iterating the top most measure of M_α^♯(X) and its images
out of the universe.

We will now argue that under certain conditions there is a comparison
lemma for n-small X-premice. This will be used in the proof of
Theorem <ref>. For premice over a real x this can be
found for example in <cit.>; the argument there
generalizes to premice over countable sets of reals. For the reader's
convenience we will briefly sketch the main ideas and recall the
statements. The following notion will be important in what follows to
ensure that -structures exist.


  Let M be a sound X-premouse and let δ be a cardinal in M or
  δ = M ∩. We say that δ is not definably
    Woodin over M if, and only if, there exists an ordinal
  γ≤ M ∩ such that γ≥δ and either
  
  
  * over M|γ there exists an rΣ_n-definable set
    A ⊂δ for some n<ω such that for no
    κ < δ do the extenders on the M-sequence witness
    that κ is strong up to δ with respect to A, or

  * ρ_n(M|γ) < δ for some  n < ω.
  
 

For several iterability arguments to follow we need our premice to
satisfy the following property, which, as a fine structural argument shows,
is preserved during iterations. This in turn ensures that
-structures exist in iterations of a premouse M satisfying it. 


  Let M be a sound X-premouse. We say M has no definable Woodin
    cardinals if, and only if, for all δ≤ M ∩ we
  have that δ is not definably Woodin over M.


The proof of <cit.> generalizes to X-premice and
shows the following lemma. Here the hypothesis that M_n^♯(x)
exists for all x ∈ is used to compare the countable premice
M and N inside the model M_n^♯(x) for a real x coding M
and N. The fact that the iteration strategies for M and N are
guided by -structures ensures that their restriction to trees in
H^M_n^♯(x)_δ_x, where δ_x is the least Woodin
cardinal in M_n^♯(x), is in M_n^♯(x) and hence
ω_1^V-iterability suffices for comparison in this situation.


  Suppose that M_n^♯(x) exists for all x ∈. Let M and
  N be countable ω_1-iterable sound X-premice such that
  every proper initial segment of M and N is n-small and they
  both do not have definable Woodin cardinals. Then there are iterates
  M^* and N^* of M and N respectively such that one of the
  following holds:


  * M^* is an initial segment of N^* and there is no drop on the
  main branch in the iteration from M to M^*,

  * N^* is an initial segment of M^* and there is no drop on the
  main branch in the iteration from N to N^*.



      In the statement of Lemma <ref> the assumption
      that M and N do not have definable Woodin cardinals can be
      replaced by the assumption that M and N do not have Woodin
      cardinals; see the remark after the proof of Lemma 2.11 in
      <cit.>.

      There is a variant of this lemma for the case that one of the
      premice is only Π^1_n-iterable as introduced in Definitions
      1.4 and 1.6 in <cit.>. In this case, the last model of the
      iteration tree on that premouse need not be fully well-founded,
      but the argument from <cit.> (see also Corollary
      2.15 in <cit.>) yields that we still have a comparison
      lemma.


  Suppose that M_n^♯(x) exists for all x ∈. Let M and
  N be countable n-small sound solid X-premice which both do
  not have Woodin cardinals. Moreover, assume that M is
  ω_1-iterable and N is Π^1_n+1-iterable. Then there is
  an iteration tree  on M and a putative [We say that
     is a putative iteration tree if it satisfies all
    properties of an iteration tree, but we allow the last model, if
    it exists, to be ill-founded.] iteration tree  on N of
  length λ+1 for some limit ordinal λ such that one of
  the following holds:


  * _λ^ is an initial segment of _λ^ and
  there is no drop on the main branch through . In this case
  _λ^ need not be fully well-founded, but it is
  well-founded up to _λ^∩.

  * _λ^ is an initial segment of _λ^ and
  there is no drop on the main branch through . In this case
  _λ^ is fully well-founded and  is an iteration
  tree.



Finally, note that by a standard argument ^1_2-determinacy, or
equivalently that M^♯_1(x) exists and is
ω_1-iterable for all x ∈ℝ, implies that
M_1^♯(X) exists and is ω_1-iterable for any countable
set of reals X.


  Suppose ^1_2-determinacy holds and let
  A ∈𝒫_ω_1(ℝ). Then M_1^♯(A)
  exists and is ω_1-iterable.

 By a theorem of Woodin (cf. <cit.>), the hypothesis
  implies that M^♯_1(x) exists and is ω_1-iterable for
  all x ∈ℝ.

  Choose some x_A ∈ℝ such that A ∈ L[x_A]. Let
  κ be the critical point of the topmost extender F of
  M_1^♯(x_A) and let N be the result of a backgrounded
  L[E]-construction over A as in Mitchell-Steel <cit.>,
  carried out within M_1(x_A). We will add to (an initial segment
  of) N a suitable restriction of F so that the resulting
  structure P is an active, ω_1-iterable A-premouse which
  is not 1-small. We first detail the construction of P and then
  argue that this implies the existence and ω_1-iterability of
  M_1^♯(A).

Note that P needs to be defined in such a way that it satisfies the
initial segment condition. We use Jensen indexing and argue similarly
as in Fuchs-Neeman-Schindler <cit.>. Let α be
maximal such that, letting

    j: N|κ^+N→N|κ^+NF|α

be the ultrapower embedding,
N_P = (F|α)↾N|κ^+NF|α, and

    P = (N|κ^+NF|α, N_P),

then P satisfies the initial segment condition. We note that:


  * P| ^P is a
  passive premouse with a Woodin cardinal;

  * P is sound;

  * P| ^P is ω_1-iterable.

The last clause holds because P|^P inherits the ω_1-iterability from M_1(x_A) (cf. <cit.>). Since P is a subset of
M_1^♯(x_A), it follows that linear iterates of (P, N_P) by
N_P are wellfounded. Moreover, if P^* is any such iterate, then
P^*|κ = P|κ, so P^* also inherits the ω_1-iterability from M_1(x_A). It follows that P^*|^P^* is
ω_1-iterable. Therefore, P is ω_1-iterable by the main
theorem of Fuchs-Neeman-Schindler <cit.>, as desired.

Let N_0 and N_1 be two active, ω_1-iterable A-premice
which are not 1-small, all of whose proper initial segments are
1-small. Since all their proper initial segments are 1-small, both
N_0 and N_1 project to A.  Let y be a coding of the pair
(N_0,N_1) as a real number. By Lemma <ref> one of N_0 and N_1 must be
an initial segment of the other, which is impossible.  It follows that
there is a least active ω_1-iterable A-premouse which is not
1-small, so M_1^♯(A) exists and is ω_1-iterable.






§ MODELS OF THE AXIOM OF DETERMINACY WITH A WOODIN
  CARDINAL
  Recall that
𝒫_ω_1(ℝ) denotes the set of all countable
sets of reals. We consider models of the form M_n(A), where
n ∈ω and A ∈𝒫_ω_1(ℝ). It is
not hard to see that—provided they exist—many of these structures
are models of the Axiom of Choice. Our first theorem shows that, if
games of length ω^2 with ^1_n+1 payoff are determined,
then many of these structures are models of the Axiom of Determinacy
and we can in addition have that M_n(A) ∩ = A.
 

  Let n ∈ω and suppose that determinacy for ^1_n+1 games
  of length ω^2 holds. Then, there is a club
  𝒞⊂𝒫_ω_1(ℝ) such that
  for all A ∈𝒞, M^♯_n(A) exists, is
  ω_1-iterable, M^♯_n(A) ∩ = A, and
  
    M_n(A)  + .
 


To simplify the notation we will from this point on only consider the
case n=1. The general case n ∈ω can be shown by
straightforward modifications of the proof we give for n=1
below. For the rest of this section assume that V is a model of
 and Projective Determinacy, i.e., that M_n^♯(x) exists
for all reals x. Note that the hypothesis of Theorem
<ref>, determinacy for ^1_n+1 games of length
ω^2, trivially implies Projective Determinacy since after the
first ω moves the following rounds can be used to “play
witnesses for projections”. Whenever we are assuming a stronger
determinacy hypothesis, we will point it out explicitly.

Before moving on to the proof of Theorem <ref>, we recall
some basic model-theoretic facts we will need later. In addition to
the language of premice,
= {∈̇, Ė, Ḟ, Ẋ}, we will now also
consider the language  resulting from enhancing  with
constants ẋ_i, for i ∈ω. For an -model
= (M,∈, Ė^,Ḟ^,Ẋ^,{ẋ_i^
i < ω}) we write ↾ for the restriction
(M,∈,Ė^, Ḟ^, Ẋ^) of the model  to the
smaller language .

Let
ℳ = (M,∈, Ė^, Ḟ^, Ẋ^, {x_i
 i ∈ω}) for x_i = ẋ_i^, i ∈ω, be a
model in the enhanced language, so in particular
{x_i  i∈ω}⊆ M. The definable closure
of {x_i  i∈ω} in ℳ↾
is defined to be the submodel

    (M̅, ∈, Ė^∩M̅, Ḟ^∩M̅,
      Ẋ^∩M̅)
 of ℳ↾
where M̅ consists of all a∈ M such that for some k<ω
and some -formula ϕ(v,v_0, …, v_k),

    ↾“ϕ[a, x_0, …, x_k] and there is a
      unique x such that ϕ[x, x_0, …, x_k].”


For sufficiently nice theories T, the definable closure of a model
of T does not depend on the model itself but only on the theory. 


  Suppose T⊃ is a complete, consistent theory in the
  language  with the property that whenever

    ℳ = (M,∈, Ė^, Ḟ^, Ẋ^, {ẋ_i^ i ∈ω})
 
is a model of T and 𝒩^ is the definable closure of
{ẋ_i^ i∈ω} in ℳ↾, then


  * for each i∈ω, ẋ_i^∈ℝ,  

  * 𝒩^≺ℳ↾. 

Then 𝒩^ does not depend on ℳ, i.e., if
 is another model of T with properties
(<ref>) and
(<ref>), then ^ and ^ are
isomorphic.


Let T be as in the statement and let

    ℳ = (M,∈, Ė^, Ḟ^, Ẋ^,{ẋ^_i  i∈ω})

and

    𝒫 = (P,∈, Ė^, Ḟ^, Ẋ^,{ẋ^_i  i∈ω})
 be two models of T. Since T is
complete, ℳ and 𝒫 are elementarily equivalent
with respect to the language . If 𝒩^ and
𝒩^ are the respective definable closures of
↾ and ↾, the natural
function ρ given by

    the unique a ∈ M such that ↾ϕ[a, ẋ_1^, …, ẋ_k^]
    ↦ the unique b ∈ P such that ↾ϕ[b, ẋ_1^, …, ẋ_k^]
 
for some k < ω and some -formula
ϕ(x, v_1, …, v_k) is an isomorphism from 𝒩^ to
𝒩^. This follows from the following observations:


  * Since ẋ_i are constants interpreted by reals and T is
  complete, they have the same interpretation in ℳ and
  𝒫, i.e., for all i ∈ω, ẋ_i^ = ẋ_i^.

  * If x ∈𝒩^, then there is an -formula
  ψ(v,v_1,…,v_k) such that ↾ψ[x, ẋ_1^, …, ẋ_k^] and x is unique with
  this property in ↾. Thus, if x ∈Ė^, 

    “x is the unique element satisfying
      ψ[x,ẋ_1^,…, ẋ_k^]∧ x∈Ė^,”

and so by considering the -sentence “there exists a unique
x with ψ(x, ẋ_1,…, ẋ_k) ∧ x ∈Ė”,

    “ρ(x) is the unique element satisfying
      ψ[ρ(x), ẋ_1^, …, ẋ_k^] ∧ρ(x) ∈Ė^”,

hence ρ(x) ∈Ė^. If x ∉Ė^, we have
x ∉Ė^ by the same argument.

The argument for the other predicates is analogous; hence, all
predicates are interpreted the same way. Therefore, 𝒩^M
and 𝒩^P are indeed isomorphic.


We will now set a general context in which we prove the following two
lemmas, as we want to apply them in both the proof of Theorem
<ref> and the proof of Lemma <ref>
below, for different formulae φ.


  Let X ∈ and let  be a countable X-premouse. Let
  φ be an -formula without free variables.
  
  
  * We say  is a φ-witness if, and only if,
     is 1-small, sound, and solid, , there are no
    Woodin cardinals in , and φ.
  
  * We say  is a minimal φ-witness if, and
    only if,  is a φ-witness and no proper initial
    segment of  is a φ-witness, i.e., whenever  is a
    proper initial segment of  satisfying  + “there are no
    Woodin cardinals”, then ⊭φ.
  


 
  Let X ∈ and suppose that  is a countable
  Π^1_2-iterable X-premouse which is a minimal φ-witness
  for some -formula φ. Moreover, assume that there is
  another countable X-premouse  which is a φ-witness
  and ω_1-iterable. Then  is in fact ω_1-iterable.


 Let x be a real coding  and
   and consider the coiteration of  and  inside
  M_1^♯(x) in the sense of Lemma <ref> using
  ω_1-iterability for  and Π^1_2-iterability for
  . Let  and  be the resulting iteration trees on 
  and  with final models ^* and ^* respectively. We
  will show that  cannot win this comparison, i.e., 
  ^* ^* and there is no drop on the main branch through
  . This implies that  is elementarily embeddable into the
  ω_1-iterable premouse ^* and thus ω_1-iterable.

  Assume first that ^* = ^*, there is no drop on the main
  branch through , and there is at least one drop on the main
  branch through . Then ^* is (by elementarity) a model of
  , contrary to the fact that
  ρ_ω(^*) < ^* ∩.

  Finally assume, again towards a contradiction, that
  ^* ^* and there is no drop on the main branch through
  . The model ^* need not be fully well-founded, but this does
  not affect the rest of the argument as we shall work in the
  well-founded part of ^*.

  Notice that ^* is a proper initial segment of ^* which (by
  elementarity) satisfies , “there are no Woodin cardinals,”
  and φ. Therefore, it cannot be that there is no drop in
  model on the main branch through , by elementarity and the
  minimality of . Assume for simplicity that there is exactly one
  drop in model on the main branch through , say, at level
  β+1 < λ (the general case is similar: if there is more
  than one drop, we repeat the argument). Using the notation from
  <cit.>, the fact that there is a drop in model at
  stage β+1 implies that _β+1^* is a proper initial
  segment of _ξ^, where ξ is the U-predecessor of
  β+1 and _β+1^* is the model to which the next
  extender on the main branch through  is applied. So by
  elementarity between _β+1^* and ^*, there is an
  ordinal α^* witnessing the failure of the minimality property
  for _β+1^*, i.e., the following hold:
  
  
  * α^* < _β+1^* ∩ < _ξ^∩,
  
  * _β+1^*|α^* is a model of  with no Woodin
    cardinals, and
  
  * _β+1^*|α^* φ.
  
  But _β+1^* is an initial segment of _ξ^, so the
  same holds for _ξ^ | α^*. Now by elementarity
  again—this time between  and _ξ^—this failure of
  the minimality property also holds for , contradicting the fact
  that  is a minimal φ-witness.


  Let X ∈ and let
   and  be ω_1-iterable countable X-premice which
  are minimal φ-witnesses for some -formula
  φ. Then  and  have a common iterate and on both
  sides of the iteration there is no drop in model on the main branch
  through the iteration
  tree. 



  Let  and  be the iteration trees of length λ +1
  for some ordinal λ on  and  respectively obtained
  from a successful comparison in the sense of Lemma
  <ref>. Write ^* = _λ^ and
  ^* = _λ^ for the last models of the iteration
  trees. We cannot have ^* ^*, by the argument of Lemma
  <ref>. Similarly, the alternative
  ^* ^* leads to a contradiction, so we must have
  ^* = ^*.
  
  Only one side of the comparison can drop; assume that there is a
  drop in model on the main branch through . The case that the
  main branch through  drops is analogous. As in the proof of
  Lemma <ref>, we assume for simplicity that
  there is exactly one drop in model along the main branch through
  , say at stage β+1 < λ; the general case is dealt
  with similarly by repeating the argument. By elementarity,
  ^* = ^* and _β+1^* are
  φ-witnesses. Moreover, as  is a minimal
  φ-witness, by elementarity the same holds for _ξ^,
  where ξ is as in the proof of Lemma
  <ref> the U-predecessor of β+1. But
  _β+1^* _ξ^, contradicting the minimality
  property for _ξ^. Therefore, both sides of the comparison
  do not drop in model.


We are now going to define a collection of games of length
ω^2 which are generalizations of the game in
<cit.>. The argument there goes back to ideas in
<cit.> 
            
allowing one of the two players in the game to play the theory of a
model with certain properties in addition to the usual moves. In the
proofs of Theorem <ref> and Lemma
<ref> below we will consider two different
instances of games from this collection where Player I plays a
complete and consistent theory in the language of premice with
additional constant symbols.

Before we give the definition of the games, recall that if
X ∈ and  is an X-premouse, then analogously to
the existence of a definable well-order in L, there is a uniformly
definable X-parametrized family of well-orders the union of whose
ranges is  (cf. <cit.>). More
specifically, we can fix a formula θ(·,·,·) in the
language of premice  such that for any such X and any
X-premouse , the following hold:


  * for any x ∈, there is some α∈^ and
  some r ∈ X such that
  
    θ(α,r,x);


  * for all r ∈ X and α∈^ there is at most one
  x ∈ such that
  
    θ(α,r,x).



Moreover, fix recursive bijections m and n assigning an odd number
>1 to each -formula φ such that m and n have
disjoint recursive ranges and for every φ, m(φ) and
n(φ) are larger than
max{ i   ẋ_i  occurs in φ}.


  Let φ and ψ(x_0,a,b) be -formulae and let
  𝒢_φ,ψ denote the following game of length
  ω^2 on ω: Fix some enumeration
  (ϕ_i  i ∈ω) of all -formulae such that
  ẋ_i does not appear in ϕ_j if j ≤ i. Then a typical
  run of 𝒢_φ,ψ looks as follows:
  
    [              I            x_0              a       v_0, x_1                v_1,
          x_3                              ;             II                             b                           x_2                           x_4                ]

  
  
  * Player I starts by playing some parameter x_0 ∈;
  
  * Players I and II take turns playing natural numbers to
    construct reals a, b ∈;
  
  * Players I and II take turns, respectively playing sequences of
    natural numbers (v_i, x_2i+1) and x_2i+2 in , for
    i ∈ω. We ask that v_i ∈{0,1}.
  

  Here v_i will be interpreted as the truth value of the formula
  ϕ_i from the enumeration fixed above. This can be thought of as
  Player I either accepting or rejecting the formula ϕ_i. If so,
  the play determines a complete theory T in the language .

  Player I wins the game 𝒢_φ,ψ if, and only if,
  
  
  *   x_1 = a ⊕ b.
  
  *  For each i ∈ω, T contains the
    sentence ẋ_i ∈ and, moreover, for each
    j,m ∈ω, T contains the sentence ẋ_i(m) = j if,
    and only if, x_i(m) = j.
  
  *  For every formula ϕ(x) with one free
    variable in the expanded language , and m(ϕ) and
    n(ϕ) as fixed above, T contains the statements
    
    ∃ x ϕ(x) →∃ x ∃α 
          (ϕ(x) θ(α, ẋ_m(ϕ), x)),

    
    ∃ x  (ϕ(x)  x ∈Ẋ) →ϕ(ẋ_n(ϕ)).

    
    
    
  
  *  T is a complete, consistent theory such that
    for every countable model  of T and every model ^*
    which is the definable closure of {x_i : i < ω} in
    ↾, ^* is well-founded and if 
    denotes the transitive collapse of ^*,
    
    
  *  is an X-premouse, where
      X = {x_i  i ∈ω},
    
  *   is a minimal φ-witness,
    
  *  is Π^1_2-iterable in the sense of <cit.>, and
    
  *  ψ(x_0,a,b).
  

If Player I plays according to all these rules, he wins the game. In
this case there is a unique premouse _p as in (<ref>)
associated to the play p = (x_0,a ⊕ b,v_0, x_1, x_2, …) of
the game. Otherwise, Player II wins.



  Rule (<ref>) in the game 𝒢_φ,ψ
  ensures that if  is a model of the theory T, then the
  definable closure of {x_i:i∈ω} in
  ↾ is an elementary substructure of
  ↾ (by the Tarski-Vaught criterion) by the
  following argument: Suppose ∃ x ϕ(x) holds in . Then
  rule (<ref>) ensures that
  ∃ x ∃α  (ϕ(x) θ(α, ẋ_m(ϕ), x)). Now, the formula
  ϕ(x) ∧∃α (θ(α, ẋ_m(ϕ), x)
  ∧∀β∈α ∃ y(ϕ(y) θ(β, ẋ_m(ϕ), y))) uniquely defines a witness x
  for ϕ(x) (the minimal witness according to the well-order given
  by θ(·, ẋ_m(ϕ), ·)). Hence, rule
  (<ref>) can be followed by Player I by playing an
  appropriate theory T, as then the model  is uniquely determined
  by it, by Lemma <ref>.


To prove Theorem <ref>, we first need to show the
following lemma. We thank John Steel for pointing out to us that it
can be proved via a modification of our argument for Theorem
<ref>.


  Suppose that ^1_2 games of length ω^2 are
  determined. Then there is a club 𝒞^* ⊂𝒫_ω_1(ℝ) such that for all A ∈𝒞^*, 
  
    ℝ∩ M_1(A) = A.




  Assume towards a contradiction that the statement of the lemma
  fails. Thus, there is a stationary set of sets
  A ∈𝒫_ω_1(ℝ) such that
  
    A ⊊ℝ∩ M_1(A).
 Let
  
    φ≡“there is a real  y  which is not in
        Ẋ”
 and
  
    ψ(x_0,a,b) ≡“there is a real definable from  x_0
         which is not in Ẋ and 
     if  z_0
         is the least
          real definable from  x_0  which is not in Ẋ, 
         then
          its  b_0th digit is  a_1”,

  where a = (a_0, a_1, …) and b = (b_0, b_1, …) with
  a_i,b_i ∈ω for all i ∈ω. This will only be
  applied in X-premice  for some X ∈ with
  x_0 ∈ X and “least” refers to the least real in the well-order
  of elements of  definable from x_0 which is given by
  θ(·, x_0, ·).
  
  Consider the game 𝒢_φ,ψ, i.e., after Player I
  plays the parameter x_0, the only relevant moves are the
  following: Player II plays a natural number b_0 asking Player I
  for the b_0th digit of the least real definable from x_0 which
  is not going to be in X and Player II answers by playing
  a_1. Afterwards they continue playing the rest of
  X = { x_0, x_1, …} and the theory of a φ-witness.

  The winning condition in this game 𝒢_φ,ψ is
  Π^1_2, so it is determined and we can distinguish the following
  two cases to obtain a contradiction by arguing that no player can
  have a winning strategy.



  
Case 1:Player I has a winning strategy
σ in 𝒢_φ,ψ.

Let W be the transitive collapse of a countable elementary
substructure Y of some large V_κ such that σ∈ Y and
let π denote the inverse of the collapse embedding, i.e.,

    π W ≅ Y ≺ V_κ.


Since ℝ^W is countable, it follows that
M_1^♯(ℝ^W) exists and is ω_1-iterable. Since
the set of ℝ^W for such elementary substructures W is a
club in 𝒫_ω_1(ℝ), we may assume that

    ℝ^W ⊊ℝ∩ M_1(ℝ^W).


The game _φ,ψ can be defined in W. Let
σ̅∈ W be such that π(σ̅) = σ, i.e.,
σ̅ = σ∩ W. By elementarity,

    W “σ̅ is a winning strategy for Player I in
        𝒢_φ,ψ.”


Let h be a well-ordering of ℝ^W in V of order-type
ω. Consider a play of the game 𝒢_φ,ψ in
V in which Player II plays some b∈ and x_2, x_4, …
according to h and Player I plays according to the winning strategy
σ. Every proper initial segment of the play is in the domain of
σ̅. It follows that the real part (x_0, x_1, x_2, …)
of the play, say p, enumerates ℝ^W. Furthermore, p is
consistent with σ, whereby p is won by Player I. This means
that p determines a Π^1_2-iterable ℝ^W-premouse
_p which is a minimal φ-witness.

Let δ_^W denote the Woodin cardinal in M_1(^W). Since
we chose W so that
ℝ^W ⊊ℝ∩
M_1(ℝ^W)|δ_ℝ^W and since satisfying
φ for the ^W-premice _p and
M_1(^W)|δ_^W means having a real which is not in
^W, we have that M_1(ℝ^W)|δ_^W is an
ω_1-iterable φ-witness. Thus, Lemma
<ref> implies that _p is
ω_1-iterable as well.

Let x_0 ∈ be the first move given by σ (so x_0 is
also the first move given by σ̅). Moreover, let
a_0 ∈ω be the first move of Player I after x_0 given by
σ (and σ̅). Let τ be the real defined by

    τ(n) = σ̅(x_0, a_0, n),
 for all possible moves n ∈ω
of Player II for b_0. We claim that τ is the least real in
_p not in ℝ^W which is definable from x_0. This will
be a contradiction, since τ∈ W as σ̅∈ W and
x_0∈ W.

Let τ^' be the least real in _p not in ℝ^W
which is definable from x_0. Assume that τ^'≠τ and
choose some n_0 ∈ω such that
τ(n_0) ≠τ^'(n_0). Let q be the play of the game
𝒢_φ,ψ in which Player I plays according to
σ̅ and Player II plays some b ∈ with first digit
n_0 and then h as above. As Player I plays according to
σ̅ and hence according to σ, this is a winning play
for Player I. Let _q be the corresponding model. In particular,
_q ψ(x_0,a,b), i.e. the least real in _q not in
ℝ^W which is definable from x_0 has
a_1 = σ̅(x_0, a_0, n_0) as n_0th digit.

By the rules of the game, _q is a Π^1_2-iterable
^W-premouse which is a minimal φ-witness. Hence, Lemma
<ref> yields (as in the case of _p) that
_q is in fact ω_1-iterable. So Lemma
<ref> implies that _p and _q coiterate to
a common model and there is no drop in model on the main branch
through the trees on both sides of the coiteration. By definition,
both _p and _q are pointwise definable from
^W. Therefore it is easy to see that in fact _p = _q. In
particular, _p and _q have the same least real τ^'
definable from x_0 which is different from all reals in ^W and
by choice of q,
τ^'(n_0) = σ̅(x_0, a_0, n_0) = τ(n_0), which is
the desired contradiction.



  
Case 2:
Player II has a winning strategy σ in
𝒢_φ,ψ.

Let W be the transitive collapse of a countable elementary
substructure Y of some large V_κ such that σ∈ Y and
let π denote the inverse of the collapse embedding. Moreover, let
σ̅∈ W be such that π(σ̅) = σ, i.e.,
σ̅= σ∩ W. Since ℝ^W is countable, it
follows that M_1^♯(ℝ^W) exists and is
ω_1-iterable in V. As before, by our hypothesis we may assume
that

    ℝ^W ⊊ℝ∩ M_1(ℝ^W).


Let = M_1(^W)|α, where α is least such that
+ “there are no Woodin cardinals” and 
contains a real which is not in ℝ^W. Let ^*, be
the definable closure of ^W in  and ^ the transitive
collapse of ^*,. Then ^≺. Thus, there is
some real z in ^ which is not in ^W such that z is
definable in ^ from some real x_0 ∈^W. We shall ask
Player I to begin every play of the game 𝒢_φ,ψ
by playing this real x_0. Assume without loss of generality that z
is the least real in ^∖^W definable from x_0
according to the well-order defined by θ(·, x_0, ·).

Consider the play p in 𝒢_φ,ψ in which Player
II plays according to σ̅ (and hence according to the winning
strategy σ) and Player I plays:


  * x_0 ∈^W, in the first round,

  * a_1 = z(b_0), in response to Player II playing b_0 ∈ω according to σ,

  * other, arbitrary, natural numbers a_0, a_2, a_3, …,

  * some enumeration h of ℝ^W in order-type ω
  with h∈ V as in Case 1, together with the theory of  in the
  language , where the constants ẋ_i are interpreted
  by the reals x_i ∈^W according to p, satisfying rules
  (<ref>), (<ref>), and (<ref>) of the
  game 𝒢_φ,ψ.
 
Arguing as before, one shows that the reals in played in p enumerate
^W. It follows that the model ^ witnesses that p is
a winning play for Player I, which contradicts the fact that σ
is a winning strategy for Player II. This proves the lemma.



  It is also possible to prove Lemma <ref> with
  the following variant of the argument we gave above. Instead of
  playing a code for a theory via v_i ∈{0,1} for
  i ∈ω, we could ask Player I to play a (fine structural)
  code for a premouse  projecting to ω digit by digit via
  v_i ∈ω for i ∈ω. In addition, we can let Player
  I play w_i ∈ω together with v_i for each i ∈ω
  to play another real w digit by digit. Then we say Player I wins
  if, and only if, the premouse  he codes satisfies (a)-(c) in
  Definition <ref> where we no longer require  in
  the definition of φ-witness, but ask that w is the minimal
  (in the natural order on formulae and ordinal parameters) real
  definable from x_0 over  which is not in
  X = {x_i  i ∈ω} and that no proper initial segment
  of  satisfies this property. Then a similar argument as in
  Lemma <ref> shows that if there is an
  ω_1-iterable model with this property,  is in fact
  ω_1-iterable as well. Now a similar argument as in the proof
  of Lemma <ref> above shows that this game
  works. Moreover, the same idea can be used to phrase the proof of
  Theorem <ref> below differently.


Finally, we are ready to prove Theorem <ref>.


Assume towards a contradiction that we have

    M_1(B)|δ_B
 for a stationary set of sets
B ∈𝒫_ω_1(ℝ), where δ_B denotes
the Woodin cardinal in M_1(B). Let
  
    φ≡“Ẋ =  + ”
 and
  
    ψ(x_0,a,b) ≡“there is a non-determined set of
          reals definable from x_0  and 
    if  Z  is
          the least such set in the well-order relative to Ẋ, 
         then  a ⊕ b ∈ Z ”.

  This will only be applied in X-premice  for some
  X ∈ with x_0 ∈ X and as in the proof of Lemma
  <ref> “least” refers to the least set in the
  well-order of elements of  definable from x_0 which is given
  by θ(·, x_0, ·).

  In this case, the game _φ,ψ is a variant of the
  Kechris-Solovay game in <cit.> (see also the game in
  <cit.>) adapted as a model game. The winning
  condition is Π^1_2, so the game _φ,ψ is
  determined. We will obtain a contradiction by arguing that no player
  can have a winning strategy.



  
Case 1:Player I has a winning strategy
σ in 𝒢_φ,ψ.

Let W be the transitive collapse of a countable elementary
substructure Y of some large V_κ with σ∈ Y and let
π denote the inverse of the collapse embedding, i.e.

    π W ≅ Y ≺ V_κ.

 
Since ℝ^W = ∩ W is countable, it follows that
M_1^♯(ℝ^W) exists and is ω_1-iterable (in
V). By Lemma <ref>, the set of ^W for W
as above with the additional property that
M_1(^W) ∩ = ^W is club in
𝒫_ω_1(ℝ). By assumption, we may thus
choose W so that M_1(^W) ∩ = ^W and in addition

    M_1(ℝ^W)|δ_ℝ^W.


Note that the game _φ,ψ can be defined in W and let
σ̅∈ W be such that π(σ̅) = σ, i.e.,
σ̅ = σ∩ W. By elementarity,

    W “σ̅ is a winning strategy for Player I
        in 𝒢_φ,ψ.”


Let h be a well-ordering of ℝ^W in V of order-type
ω. Clearly, every proper initial segment of h is in
W. Consider a play of the game 𝒢_φ,ψ in V
in which Player II plays some arbitrary b^* ∈ and
x_2, x_4, … according to h and Player I plays according to the
winning strategy σ. Every proper initial segment of the play is
in the domain of σ̅. It follows that the real part
(x_0, x_1, x_2, …) of the play, say p, enumerates
ℝ^W. Futhermore, p is consistent with σ, whereby
p is won by Player I. This means that p determines a
Π^1_2-iterable ℝ^W-premouse _p which is a minimal
φ-witness. In particular, _p ∩ = ^W. Since both
_p and M_1(ℝ^W)|δ_^W are
ℝ^W-premice and M_1(ℝ^W)|δ_^W is a
φ-witness, _p is ω_1-iterable by Lemma
<ref>.

Let x_0 ∈ be the first move given by σ (so x_0 is
also the first move given by σ̅). Let Z = Z(x_0,_p)
denote the least non-determined set of reals in _p which is
definable from x_0. This exists since
_p ψ(x_0,a^*,b^*), where a^* is the sequence of
natural numbers Player I plays after x_0 in response to b^*
according to σ. There is a natural strategy τ for Player I
in G(Z)—the Gale-Stewart game with winning condition Z played in
_p—which is induced by σ̅. Let τ be the unique
strategy such that for a,b ∈∩_p,

    a = τ(b)  if, and only if,  (x_0,a) = σ̅(b).

Note that τ∈ W as σ̅, x_0 ∈ W and, since the reals
of _p are those of W, we also have τ∈_p.

We claim that τ is a winning strategy for Player I (in the game
G(Z) in _p), which will contradict the fact that the set Z is
non-determined in _p. Let a ⊕ b∈ℝ^W be a play
by τ. Let q be the play of the game
𝒢_φ,ψ in which Player I plays according to
σ̅ and Player II plays b and then h as above. As Player
I plays according to σ̅ and hence according to σ,
this is a winning play for Player I. Let _q be the corresponding
model. In particular, _q ψ(x_0,a,b), i.e.
a ⊕ b ∈ Z(x_0,_q), where Z(x_0,_q) denotes the least
non-determined set of reals in _q which is definable from x_0.

By the rules of the game, _q is a Π^1_2-iterable
^W-premouse which is a minimal φ-witness. Hence Lemma
<ref> yields that _q is in fact
ω_1-iterable. So we can apply Lemma <ref> to
_q and _p. In fact, _p = _q as both are pointwise
definable from ^W. Therefore, Z = Z(x_0,_p) = Z(x_0,_q)
and a ⊕ b ∈ Z. Hence, τ is a winning strategy for Player
I, contrary to the fact that Z is non-determined in _p.



  
Case 2: Player II has a winning strategy
σ in 𝒢_φ,ψ.

As before, let W be the transitive collapse of a countable
elementary substructure Y of some large V_κ with
σ∈ Y and let π denote the inverse of the collapse
embedding, i.e.

    π W ≅ Y ≺ V_κ.

Then M_1^♯(ℝ^W) exists and is ω_1-iterable in V.
As before, we may choose W so that

    M_1(ℝ^W) ∩ = ^W  and 
      M_1(ℝ^W)|δ_ℝ^W.
 Let
σ̅= σ∩ W, so that σ̅∈ W and

    W“σ̅ is a winning strategy for Player II in
        𝒢_φ,ψ.”


Let = M_1(^W)|α, where α is least such that there
are no Woodin cardinals in  and +. Let
^*, be the definable closure of ^W in  and
^ the transitive collapse of ^*,. Then
^≺ and ^ is ω_1-iterable because it is
elementary embedded in the ω_1-iterable premouse
. Moreover, there is some non-determined set in ^
definable from some real x_0 ∈^W. We shall ask Player I to
play this real x_0 followed by some real a and some enumeration
h ∈ V of ^W in order-type ω together with the theory
of  (of course, organized in such a way that he satisfies rules
(<ref>), (<ref>), and (<ref>) of the
game). Let Z(x_0,^) be as before.

Since σ̅ is a winning strategy for Player II in the game
𝒢_φ,ψ in W, in particular σ̅ wins
against all plays in which Player I begins by playing x_0. As
before, there is a natural strategy τ∈^ for Player II
for the Gale-Stewart game inside ^ with payoff set
Z(x_0,^), namely, the unique strategy such that

    b = τ(a)  if, and only if,  b = σ̅(x_0, a).
 A
similar argument as in Case 1, using that Player I cannot lose a play
p as above because of having played the wrong theor, but only
because a⊕ b ∉ Z(x_0,_p), gives that τ is a
winning strategy for Player II in ^. This finishes the proof
of Theorem <ref>.







§ DEPENDENT CHOICES, SCALES, AND MOUSE
  CAPTURING


By Theorem <ref> we obtain a countable set of reals A
such that M_1(A) is an A-premouse constructed over its reals and
M_1(A)  + from the assumption that all ^1_2 games
of length ω^2 are determined. We aim to show that there is a
model with ω+1 Woodin cardinals from this hypothesis. Before we
do that in the next section, we first show some structural properties
of this model.

First, we have that in fact M_1(A) by the following
theorem, which is a special case of <cit.> (building
on <cit.> and <cit.>).


  Let A ∈ be a countable set of reals such that
  M_1(A) ∩ = A and M_1(A)  +. Then
  M_1(A).


In what follows we argue that, in M_1(A), Σ^2_1 has the scale
property and Θ = θ_0, i.e. the Solovay sequence is
trivial. Assuming , recall that

    Θ = sup{β : there is a surjection  f →β},
 and

    θ_0 = sup{β : there is an  surjection
       f →β}.


These properties of M_1(A) have proofs similar to those for
L(). E.g., using <cit.> the scale analysis of L() from
<cit.> can be done inside M_1(A) and yields that
Σ_1^M_1(A) has the scale property. Moreover, as in L(),
it is easy to see that (Σ^2_1)^M_1(A) =
Σ_1^M_1(A). Similarly, (Θ = θ_0)^M_1(A). In
fact, by generalizing the arguments used for L(), we can also get
that ^+ holds in M_1(A) but we will not need that. We summarize
this in the next theorem.


  Let A ∈ be a countable set of reals such that
  M_1(A) ∩ = A and M_1(A)  +. Then
  M_1(A) “Σ^2_1 has the scale property” +
  Θ = θ_0.


Finally, we also have that M_1(A) satisfies Mouse Capturing
(), i.e., that for any two countable transitive sets x and y
such that x ⊆ y and x ∈_y ∪{y}, x is
contained in an ω_1-iterable y-premouse. This follows from
<cit.> (due to Woodin).


  Let A ∈ be a countable set of reals such that
  M_1(A) ∩ = A and M_1(A)  +. Then
  M_1(A).






§ Ω+1 WOODIN CARDINALS
 


In this section we will use the results from the previous sections to
construct a premouse with ω +1 Woodin cardinals. More
precisely, we prove the following theorem:


  Suppose there is some A ∈ such that 
  
  
  * M_1^♯(A) exists,
  
  * M_1(A) ∩ = A, and
  
  * M_1(A).
  
  Then there is an active premouse with
  ω+1 Woodin cardinals.


Using Section <ref>, for the rest of this section, we fix a
countable set of reals A such that M_1(A) is an
ω_1-iterable A-premouse with M_1(A) ∩ = A and

    M_1(A)  +  +  + “Σ^2_1 has the
        scale property” + Θ = θ_0 + .


The rest of this section is devoted to the proof of Theorem
<ref>. Most of the proof in this section closely
follows ideas from Section 3 in the unpublished notes <cit.>. See
also Sections 6.5 and 6.6 in <cit.> for a similar argument
applied to L() or <cit.>. We start by introducing some
notation, generalizing ideas from <cit.> and
<cit.> to our context. Suppose that A is as in the statement
of Theorem <ref> and work inside V = M_1(A).

The proof of Theorem <ref> can be split in several
parts. After we recall a useful standard fact, we define suitable
premice. From these we will, by pseudo-comparison and
pseudo-genericity iteration, obtain models which we can use in a
Prikry-like forcing to construct a model with ω Woodin
cardinals. Then we argue that this model can be rearranged into a
premouse on top of which we can perform a -construction to add
one more Woodin cardinal.
 
The following standard lemma will be useful later on:

  There is a Σ^2_1 scale
  ϕ⃗ on a Σ^2_1 set which is universal for
  ^2_1 such that, letting T be the tree obtained from
  ϕ⃗, we have for any countable transitive set a,
 
    𝒫(a)∩ L[T,a]
                                                   = 𝒫(a)∩_a ∪{a}
       = {b∈ H(ω_1): b
                                                   belongs to an
                                                  ω_1-iterable
                                                 a-premouse}.




  The second equality easily follows from . For the first
  equality, let U⊂^2 be any Σ^2_1 set that is
  universal for ^2_1. Σ^2_1 has the scale property, so
  let T be a tree on ω×ω×δ^2_1 obtained
  from a Σ^2_1-scale on U (thus T projects to
  U). 

  Now, suppose b ∈𝒫(a)∩_a ∪{a}. Let z be
  a real coding a. Then the set B of all _a ∪{a}
  subsets of a (coded as a real relative to z) is
  Σ^2_1(z). By the Mansfield-Solovay Theorem (see for example
  <cit.>), either B ⊆ L[T,z], or B contains a perfect
  subset. But since B is countable, it is thin. Therefore b_z, the
  real coding b relative to z, is in L[T,z] and hence
  b ∈ L[T,z]. Since this holds for all z which are
  (ω,a)-generic over L[T,a], it follows that
  b ∈ L[T,a].
  
  Conversely, every real in L[T,a] is definable from a and ordinal
  parameters. This is because the reals of L[T,a] do not depend on
  the choice of the universal set U nor on the scale on U (this
  follows e.g., from <cit.>, see also
  <cit.>).


Fix a Σ^2_1 set U which is universal for ^2_1 in
V = M_1(A) and a tree T as above for the rest of this section.




 §.§ Suitable premice


We begin by isolating a class of models suitable for our purposes.


Suppose b is a countable transitive set. We write

    Lp(b) = ⋃{M: M is a sound ω_1-iterable
        b-premouse such that ρ_ω(M) = b }.
 Moreover, we
inductively define Lp^1(b) = Lp(b),

    Lp^n+1(b) = Lp(Lp^n(b)),
 and

    Lp^ω(b) = ⋃_n<ω Lp^n(b).




  Recall that we are working inside M_1(A), which is a model of
  , so the club filter is an ultrafilter on ω_1. This can
  be used to show that ω_1-iterability already implies
  ω_1+1-iterability (see e.g. <cit.> for
  details), so that any two ω_1-iterable b-premice M and
  N as in the definition of Lp(b) can be successfully compared and
  line up, i.e M  N or N  M. Therefore, Lp(b) is a
  well-defined premouse.


In the definitions below, let a be an arbitrary countable transitive
set. 


  We say that an a-premouse M is suitable if, and only if,
  there is an ordinal δ such that


  * M is a model of  - “Replacement” and
  M ∩ = sup_n<ω (δ^+n)^M,

  * δ is the unique Woodin cardinal in M, and

  * M is full, i.e. for every cutpoint[In the case
    where η is not a cutpoint, we refer to the *-transformation
    in <cit.>.] η in M, Lp(M|η)  M.



If M is suitable, we denote its Woodin cardinal by δ_M.

  Let M be a countable
  a-premouse and x_M a real coding M. Then for any real
  z ≥_T x_M, the statement “M is suitable” is absolute
  between V and L[T,z].



  Suppose not, say M is suitable in L[T,z] but there is some
  η < M ∩ and a sound ω_1-iterable
  M|η-premouse N in V with ρ_ω(N) = M|η such
  that N ⋬ M. This statement is ^2_1 and
  hence such a counterexample would also exist in L[T,z]. By the
  same argument, if we suppose that M is suitable in V, every such
  ω_1-iterable M|η-premouse in L[T,z] is also
  ω_1-iterable in V. Hence the statement “M is suitable”
  is absolute between V and L[T,z].



  Let  be a normal iteration tree on a suitable a-premouse M
  of length < ω_1^V. Then we say that  is correctly
    guided if, and only if, for every limit ordinal λ < (), if b
  is the branch choosen through ↾λ in
  , then (b, ↾λ) exists and
  (b, ↾λ)  Lp((↾λ)).



  Let  be a normal iteration tree on a suitable a-premouse M
  of length < ω_1^V. Then we say that  is short if,
  and only if,  is correctly guided and if  has limit
  length, then () exists, and () 
  Lp(()). If  is correctly guided but not short, then it
  is said to be maximal.


As in <cit.>, we define the notion of being suitability-strict
in order to make the proofs of Lemmas
<ref> and <ref>
below work.


  Let M be a suitable a-premouse and let  be a normal
  iteration tree on M of length < ω_1^V. Then we say that
   is suitability-strict if, and only if, for all
  α < (),
  
  
  * if [0, α]_T does not drop then _α^ is
    suitable, and
  
  * if [0, α]_T drops then no _α^
    is suitable.
  



  Let M be a suitable a-premouse. Then we say that M is
  short tree iterable if, and only if, whenever  is a
  short tree on M of length < ω_1^V,
  
  
  *  is suitability-strict,
  
  * if  has a last model, then every putative iteration tree
     extending  such that () = () +1 has a
    well-founded last model, and
  
  * if  has limit length, then there exists a cofinal
    well-founded branch b through  such that
    (b,) = ().
  



  Suppose M is a suitable a-premouse. We say R is a
  pseudo-normal iterate of M if, and only if, R is suitable
  and there is a normal iteration tree  on M such that either
   has successor length and R is the last model of  or
   is maximal and R = Lp^ω(()).


As usual, this notion can easily be generalized to stacks of normal
trees, but we omit the technical details. The interested reader can
find them in a different setting for example in <cit.>,
<cit.>, or <cit.>. The following lemmas are the analogues of
Theorems 3.14 and 3.16 in <cit.>. The proofs are similar to the
ones in <cit.> and <cit.> and use absoluteness as in the
proof of Lemma <ref>; we omit further details.


  Suppose M and N are countable short tree iterable, suitable
  a-premice. Then, they have a common pseudo-normal iterate R such
  that R ∈ L[T,z], where z is a real coding M and
  N. Moreover,
  δ_R≤ (max{δ_M,δ_N}^+)^L[T,z] =
  ω_1^L[T,z]. 



  Let M be a countable, short tree iterable, suitable
  a-premouse. Then for a cone of reals z, M is countable in
  L[T,z], and there is a non-dropping pseudo-normal iterate R of
  M in L[T,z] such that z is generic over R for Woodin's
  extender algebra at δ_R, and
  δ_R = ω_1^L[T,z].




 §.§ The models ^x_a

As before, let a be an arbitrary countable transitive set. Let x
be a real such that a ∈ L[x].  We consider the simultaneous
pseudo-comparison of all short tree iterable, suitable a-premice
coded by some real z ≤_T x. We carry out this pseudo-comparison
while at the same time performing a pseudo-genericity iteration making
every z ≤_T x generic over the common part of the final
model. Note that there are only countably many reals z ≤_T x for
every fixed real x and let ^- = _a^x,- denote the
resulting model. I.e., either ^- is the common last model of the
iteration trees obtained by the process described above, or all of
these trees are maximal and ^- is the common part model of one
(and hence all) of these trees. Moreover, let
= _a^x = Lp(_a^x,-) and
δ = _a^x,-∩.

  We have the following properties.
  
  
  * As an ^--premouse, no level of  projects across
    δ,  
                                
  
  * δ_ = δ is a Woodin cardinal in
    , 
  
  * 𝒫(δ)∩ = 𝒫(δ) ∩_^-∪{^-}, 
  
  * 𝒫(a)∩ = 𝒫(a) ∩_a ∪{a},
     and
  
  * ω_1^L[T,x] = δ. 
  


 We carry out the pseudo-comparisons and
  pseudo-genericity iterations to obtain ^- within L[T,x] in
  the sense of Lemmas <ref> and
  <ref>.

  
    The pseudo-comparisons reach a limit stage in which all of the
    iteration trees are maximal.
  
  
    If the pseudo-comparisons reach a limit stage in which one
    iteration tree  is maximal, this already implies that all
    iteration trees are maximal since they agree on their common part
    model and thus a short iteration tree  would provide a
    -structure ()  Lp(()) = Lp(()) for
    , contradicting the maximality of .

    Therefore, we can suppose toward a contradiction that all
    iteration trees occuring in the pseudo-comparisons are short. Then
    the pseudo-comparisons are in fact comparisons and they end
    successfully using the short tree iteration strategies. They give
    rise to a last model ^* such that every z≤_T x is
    generic over ^* for Woodin's extender algebra. Moreover, the
    main branches through all iteration trees in the comparisons are
    non-dropping and we have elementary iteration embeddings
    
    j_→^*
 for each short tree iterable,
    suitable a-premouse  coded by some real z≤_T x.
    
    
    
    
    
    In particular, ^* is suitable, witnessed by a Woodin cardinal
    δ^* = δ_^*.

    The proof of the comparison lemma (cf. e.g., the claim in the
    proof of <cit.>) shows that, if a coiteration
    terminates successfully, the comparison process lasts at most
    countably many steps in L[T,x], and so ^* is countable in
    L[T,x]. By construction, x is generic over ^* for
    Woodin's extender algebra at δ^*, so we shall write
    ^*[x] for the corresponding generic extension.

    
      ℝ∩ L[T,x] ⊆ℝ∩^*[x].
    
    
      Recall that Woodin's extender algebra at δ^* has the
      δ^*-c.c. and hence
      ((δ^*)^+)^^* = ((δ^*)^+)^^*[x]. Let
      γ = ((δ^*)^+)^^*. Consider the countable set
      ^*[x]|γ and the model L[T, ^*[x]|γ]. Since
      x ∈^*[x]|γ, we have that
      L[T,x] ⊆ L[T, ^*[x]|γ]. Now, Lemma
      <ref> implies that every real y in
      L[T, ^*[x]|γ], belongs to an ω_1-iterable
      ^*[x]|γ-premouse N^y. By taking an initial segment
      if necessary, we can assume that N^y is sound and
      ρ_ω(N^y) ≤γ. Since
      L[T, x] ⊆ L[T, ^*[x]|γ], it suffices to show
      that every real y in an ω_1-iterable
      ^*[x]|γ-premouse N^y belongs to ^*[x].

      Let N̅^y = ^N^y(^*|γ) be the
      ^*|γ-premouse obtained as the result of a
      -construction above ^*|γ inside N^y in the
      sense of <cit.> or <cit.>. As the size
      of the extender algebra at δ^* is small, N̅^y is
      again a premouse and by definability of the forcing
      ρ_ω(N̅^y) ≤γ (see for example
      <cit.> for a similar argument). Therefore, the
      suitability of ^* yields N̅^y ^* and hence
      N^y = N̅^y[x] ^*[x], where N̅^y[x] and
      ^*[x] are construed as ^*[x]|γ-premice. Thus
      y ∈^*[x], as desired.
    

    Since ^* is countable in L[T,x], in particular δ^*,
    the Woodin cardinal in ^*, is countable in L[T,x]. Using
    the subclaim, this implies that δ^* is countable in
    ^*[x]. But the extender algebra at δ^* in ^* has
    the δ^*-c.c., so δ^* remains a cardinal in
    ^*[x]—a contradiction.
  

  Since all iteration trees are maximal, we have ^- = (),
  where  is an iteration tree of limit length on a suitable
  a-premouse coded by some real z ≤_T x. Then = Lp(^-)
  satisfies (<ref>) and (<ref>).

  For (<ref>), note that
  𝒫(δ) ∩_^-∪{^-} is the set
  of all subsets of δ which belong to an ω_1-iterable
  ^--premouse. Since = Lp(^-) these correspond to
  initial segments of .

  This also implies that every subset of a in _a ∪{a}
  belongs to  since
  _a ∪{a}⊆_^-∪{^-}. For
  the other inclusion in (<ref>), suppose that b is a
  subset of a and b ∈. As no new subsets of a are added
  during the iteration,
  
  b ∈ N for some short tree iterable, suitable a-premouse N
  coded by some real z ≤_T x. But then N | η is
  ω_1-iterable for every ordinal η such that
  ρ_ω(N|η) = a as, in these cases, -structures
  exist. Hence, b belongs to an ω_1-iterable a-premouse and
  hence to _a ∪{a}.

  Finally, (<ref>) follows by the same argument as in
  the proof of the subclaim since the assumption that
  δ < ω_1^L[T,x] together with (<ref>)
  and (<ref>) suffices to derive the contradiction.


The construction of _a^x depends only on the Turing degree of
x, i.e., x ≡_T y implies _a^x = _a^y. Therefore, we will
also write _a^d for _a^x, if d = [x]_T.



 §.§ Prikry-like forcing a premouse

We define a Prikry-like partial order  to add a premouse with
infinitely many Woodin cardinals. Let 𝒟 denote the set of
all Turing degrees and let μ denote the Martin measure on
𝒟. Further, let ^m be the set of all increasing
sequences of Turing degrees of length m and μ_m be the measure
on ^m induced by the product of μ. More precisely, let
μ_0 = μ and assume inductively that μ_k is already defined
on ^k for some k < m. Then we let for any X ∈^k+1,
μ_k+1(X) = 1 if, and only if, for μ_0-a.e. d_0 and
μ_k-a.e.  (d_1, …, d_k), (d_0, …, d_k) ∈ X.

To define the Prikry-like partial order , we first define a
sequence of premice along an increasing sequence of Turing
degrees. For d⃗ = (d_0, …, d_m) ∈^m+1, we let

    ^d⃗_0(a) = _a^d_0
 if d_0 is large enough
so that _a^d_0 is defined, and recursively

    ^d⃗_i+1(a) = _^d⃗_i(a)^d_i+1
 for
i < m, if d_i+1 is large enough so that
_^d⃗_i(a)^d_i+1 is defined.

Recall that U is a Σ^2_1 set which is universal for
^2_1 in V = M_1(A). Now, the conditions in  are of the
form (s, X⃗), where


  * s = (_0, …, _n) is a sequence of premice such that
  for some d⃗_s ∈^n+1, _i= _i^d⃗_s(∅)
  for all i ≤ n; and

  * X⃗ = (X_k  k < ω) ∈ L(U,A)[The reason for
    requiring X⃗∈ L(U,A) will become apparent in the proof of
    Lemma <ref>.] is a sequence of sets such that for
  all k < ω,
  
  
  * X_k is a collection of (k+1)-sequences of premice, and
  
  * (^d⃗_0(_n), …, ^d⃗_k(_n)) ∈
    X_k for μ_k+1-a.e. d⃗∈𝒟^k+1.
   


We call s the stem of the condition (s, X⃗). For two
conditions (s, X⃗) and (r, Y⃗) in  with
s = (_0, …, _n) and r = (_0, …, _m), we let
(s, X⃗) ≤ (r, Y⃗) if, and only if, one of the following holds:


  * s = r and X_i ⊆ Y_i for
all i<ω; or 

  * for some k < ω and a sequence
  (^d⃗_0(_m), …, ^d⃗_k(_m)) ∈ Y_k
  given by some d⃗∈^k+1,


  * s = r^⌢ (^d⃗_0(_m), …, ^d⃗_k(_m)), and

  * for all i < ω and sequences e⃗∈^i+1 such
  that
  (^e⃗_0(_n), …, ^e⃗_i(_n)) is
  defined and belongs to X_i, we have
  
  
  
    (^d⃗^⌢e⃗_0(_m), …, ^d⃗^⌢e⃗_k(_m), ^d⃗^⌢e⃗_k+1(_m), …, ^d⃗^⌢e⃗_k+i+1(_m)) ∈ Y_k+i+1.




 We can actually restrict to the following dense suborder of
  . We call a condition (s, X⃗) ∈ a measure-one
    tree if, and only if, X⃗ = (X_k  k < ω), where each
  X_k is a set of stems each of which is compatible with
  s = (_0, …, _n) and the following hold:


  * X⃗ is closed under initial segments in the following sense:
whenever (x_0, …, x_k) ∈ X_k for some k < ω,
  then (x_0, …, x_i) ∈ X_i for all i < k; and

  * for all k<ω and all x ∈ X_k, 
  
    {d∈𝒟:x^⌢(__n^d) ∈ X_k+1}∈μ.



The next lemma shows that  has the Prikry property. As the proof
is analogous to e.g., the proof of Corollary 6.39 in <cit.>, we
omit it.


  Let (s, X⃗) ∈ be a condition and Λ a countable
  set of sentences in the forcing language. Then there is some
  (s, Y⃗) ≤ (s, X⃗) such that (s, Y⃗) decides
  ϕ, for all ϕ∈Λ. 


Now fix a G which is -generic over M_1(A) and let
= (_n  n < ω) be the union of the stems of
conditions in G. Write δ_n for the largest cardinal in
_n. By definition, all _n are such that
_n = Lp(_n|δ_n) and Lp^ω(_n|δ_n) is a
suitable premouse, so δ_n is a Woodin cardinal in _n. Let

    _∞ = ⋃_n<ω_n.



  The following hold:
   
  
  * for all n<ω, (δ_n) ∩ L[] ⊆_n, 
  
  * for all n < ω, δ_n is a Woodin cardinal in
    L[], 
  
  * _n = _∞ | (δ_n^+)^_∞; hence,
    L[_∞] = L[]. 
  



  We show (<ref>), from which (<ref>) and
  (<ref>) follow.  Let us first show that
  (δ_n) ∩_n+1⊆_n; a consequence of
  this is that (δ_n) ∩_m ⊆_n whenever
  n<m.  To see this, suppose there is a subset a of δ_n
  which is in _n+1. By Lemma <ref>(<ref>),
  (δ_n) ∩_n+1 = (δ_n) ∩__n ∪{_n}.
 
 
 
 
  Lemma <ref>(<ref>) implies that
  (δ_n) ∩_n = (δ_n) ∩__n^- ∪{_n^-}, but this is equal to
  (δ_n) ∩__n ∪{_n} by definability of
  _n = Lp(_n^-). Hence, we have a ∈_n, as desired.

 
 
 
 
 
 

  To prove (<ref>), let
  a ∈(δ_n) ∩ L[]. Let ȧ be a term
  defining a from  and an ordinal parameter in
  M_1(A)[G]. The Prikry property (Lemma <ref>)
  yields a k<ω and a condition (s, X⃗) with s of the
  form (s_0, …, s_k), with n<k, which decides all statements
  of the form “ξ∈ȧ”. By genericity we can choose
  (s, X⃗) ∈ G, so that, in particular, s_i = _i for all
  i ≤ k.
   We have ξ∈ a if, and only if,
    
    ∃ t ∃Y⃗ (t  is of
          the form  (t_0, …, t_k)  ∧  t_i = _i  for all 
        i ≤ k  ∧  (t, Y⃗)  ⊩ ξ∈ȧ).
 
  
  
    If ξ∈ a, then the condition (s, X⃗) is a witness for
    the displayed equation. Conversely, suppose there is some
    condition (t, Y⃗) as in the displayed equation, but
    ξ∉ a. Then we must have
    (s, X⃗)  ⊩ ξ∉ȧ. Note that t =
    s. Define Z⃗ by Z_i = X_i ∩ Y_i for all i <
    ω. Then (s, Z⃗) ≤ (s, X⃗) and
    (s, Z⃗) = (t, Z⃗) ≤ (t, Y⃗). Now, let H be
    -generic over M_1(A) such that H contains (s, Z⃗). Then, in M_1(A)[H], both ξ∈ a and ξ∉ a
    hold, a contradiction.
  
  The claim yields that a ∈__k ∪{_k} and thus
  a ∈__k^- ∪{_k^-}∩(δ_k) = _k
  ∩(δ_k), by Lemma
  <ref>(<ref>). So in particular
  a ∈_k ∩(δ_n). By the remark at the beginning of
  the proof, this implies a ∈_n, as desired.


Write λ = sup_n<ωδ_n and fix any premouse
 extending _∞ in which λ remains a
cardinal. We form a derived model of . More precisely, working in
M_1(A)[G], let  be the partial order consisting of sequences
(h_0, …, h_k) such that for all 0 ≤ n ≤ k,
h_n ∈ M_1(A) is (ω, δ_n)-generic over
_n. The order on  is sequence extension. Fix ĥ
-generic over M_1(A)[G], let (h_n  n < ω) be the
induced sequence, and let h be given by h(n,m) = h_n(m). We may
abuse notation and identify ĥ with h and with the
corresponding (ω, <λ)-generic filter over
M_1(A)[G], since (δ_n  n < ω) is definable from
_∞ by the previous lemma.

Using this h, we can build the derived model of : Write

    ^*_h = ⋃_n∈ω∩[h↾δ_n],
 and

    Hom^*_h = { p[S]    ∩^*_h | ∃ n < ω ([h
      ↾δ_n]  S  is a 
       <λ-absolutely complemented tree)}.


Note that ^*_h, and ^*_h only depend on _∞ and
h, not on the full premouse , so this notation makes sense. For
this reason, we sometimes do not distinguish between  and
_∞ in what follows.



 §.§ Preparation for adding extenders on
  top


Our next goal is to add the extenders of M_1(A) on top of
_∞ while preserving the Woodin cardinals of _∞ to
obtain a model with ω +1 Woodin cardinals.  This will be done
via a -construction. For this, some preparation is needed— we
need to show e.g.,

    L_ξ[_∞][h] = (M_1(A)|ξ)[G][h]
 for some ordinal ξ
below the Woodin cardinal of M_1(A).

We first need the following lemmas which again essentially can be
found also in <cit.>. Recall that we have V = M_1(A) and write
^V = M_1(A) ∩ = A.


ℝ^*_h = ℝ^V.


  ℝ^*_h ⊆ℝ^V is easy to see as each pair
  (_n, h_n) is in M_1(A), so let x ∈^V for the other
  inclusion. Let (s, X⃗) ∈ be an arbitrary condition in
  the Prikry-like forcing defined above, say
  s = (_0, …, _k). For each n<ω consider
  
    Y_n = { t ∈ X_n |∃d⃗∈^n+1 (x ≤_T
        d_0 ∧ t = (_0^d⃗(_k), …, _n^d⃗(_k)))}
 and note that (s, Y⃗) ≤ (s, X⃗). Moreover, since pseudo-genericity iterations are included in
  the construction of the premice _a^d, it follows by density
  that for all i >k, x is generic over _i for Woodin's
  extender algebra at δ_i. Hence x ∈^*_h.



  Hom^*_h = ^2_1. 


  We first show ^2_1⊆ Hom^*_h. Let B ∈^2_1,
  so that B is, since ^2_1 has the scale property, Suslin
  and co-Suslin. More precisely, choose z∈ℝ such that
  B ∈Δ^2_1(z) and choose i ∈ω large enough so that
  z ∈_i[h_i] (this exists by the previous lemma). From T and
  z, one can construct trees S_0 and S_1 on
  ω×κ, for some ordinal
  κ<δ^2_1, such that S_0 and S_1 project to
  B and ℝ∖ B, respectively.  We have
  
    S_0, S_1 ∈ L[T, _j, h_i]
 for every j≥ i. Moreover, by
  the absoluteness of well-foundedness, if
  x ∈ L[T, _j, h_i]∩ℝ, then
  
    L[T, _j, h_i] x ∈ p[S_0]∪ p[S_1].


  Moreover, if ℚ is a small partial order in
  L[T, _j, h_i] (say, of size strictly less than δ_j) and
  g is ℚ-generic over L[T, _j, h_i], then
  
    L[T, _j, h_i][g]ℝ = p[S_0]∪ p[S_1],
 for
  (since δ_j is countable in V) otherwise there is a
  ℚ-generic g over L[T, _j, h_i] with g∈ V such
  that
  
    L[T, _j, h_i][g]∃ x∈ℝ (x ∉p[S_0]∪ p[S_1]).
 However, such an x does belong to one
  of p[S_0] or p[S_1] in V and thus it must do too in
  L[T, _j, h_i][g] (by the absoluteness of well-foundedness).

  We have shown that in L[T, _j, h_i] there are
  <δ_j-absolutely complementing trees S_0 and S_1 that
  project to B ∩ L[T, _j, h_i] and
  (ℝ∖ B) ∩ L[T, _j, h_i], respectively.

  The trees S_0 and S_1 might be big (in principle κ might
  be of arbitrarily large size below δ^2_1). Let M
  be an elementary substructure of some large L_α[T,_j,h_i]
  such that
  
  
  * M ∈ L[T,_j,h_i],
  
  * L[T,_j,h_i]  |M| = δ_j,
  
  * L_δ_j[T,_j,h_i] ⊆ M, and
  
  * S_0, S_1 ∈ M.
  
  Let S_0^j and S_1^j be the images of S_0 and S_1 under the
  collapse embedding for M. Then, S_0^j and S_1^j are also
  <δ_j-absolutely complementing and S_0^j projects to
  B ∩ L[T, _j, h_i][g] whenever g is ℚ-generic
  over L[T, _j, h_i] for a partial order ℚ in
  L[T,_j,h_i] of size strictly less than δ_j.

  
    For all j >i, S_0^j, S_1^j ∈_∞[h_i].
  
  
    Note that h_i is (ω, δ_i)-generic over
    _j+1.
    
    
    Recall that by definition, _j+1 = ^d__j for some
    Turing degree d. Therefore we have, for such a d, by an
    argument similar to that in the proof of Subclaim
    <ref> that
    
    _j+1[h_i] = ^d__j[h_i].


    Now, by Lemma <ref>, every subset of _j in
    L[T,_j,h_i] is definable from _j, h_i, and ordinal
    parameters in V. S_0^j and S_1^j are essentially subsets of
    δ_j in L[T,_j,h_i], so they are definable in V from
    _j, h_i, and ordinal parameters. By Lemma
    <ref>(<ref>),
    
    𝒫(_j[h_i])∩^d__j[h_i] =
          𝒫(_j[h_i])∩__j[h_i] ∪{_j[h_i]}.
 This implies that S_0^j and S_1^j
    belong to Q_j+1[h_i], which proves the claim.
  

  It follows that S_0^j and S_1^j are <δ_j-absolutely
  complementing trees in _∞[h_i] since by an argument as in
  the proof of Lemma <ref>, for every g which is generic
  for a partial order of size strictly less than δ_j,
  _∞[g] ∩(δ_j) ⊆_j[g]. In
  particular, B ∩_∞[h_i] is <λ-universally
  Baire in _∞[h_i]. The canonical extension B^* of
  B ∩_∞[h_i] to a set in Hom^*_h is in fact unique and
  consistent with the trees (S_0^j,S_1^j) for all
  i<j<ω. Therefore B = B^*. This proves
  ^2_1⊆ Hom^*_h.

  We now assume towards a contradiction that ^2_1≠ Hom^*_h,
  i.e., that the ^2_1 sets form a proper Wadge initial segment
  of Hom^*_h. Since Hom^*_h is closed under continuous
  reducibility and the Σ^2_1 set U which is universal for
  ^2_1 is minimal in the Wadge hierarchy above the pointclass
  ^2_1, it follows that U ∈ Hom^*_h.

  By definition of Hom^*_h, there is some i∈ω and a
  <λ-absolutely complemented tree S in _∞[h_i]
  such that, since ^V = ^*_h by Lemma <ref>,
  p[S] ∩^V = ^V ∖ U.

  By Lemma <ref>, the relation
  
    x ∉_{y}
 is Π^2_1, so it appears in a section of
  the complement of U. Using S, we can get a real x such that
  x ∉_{(_i|δ_i, h_i)} but
  x ∈_∞[h_i]. Then in fact x ∈_i[h_i] by the
  argument in the proof of Lemma <ref>. However,
  _i = Lp(_i|δ_i), so every real in _i[h_i] is
  definable from _i|δ_i, h_i, and ordinal parameters,
  which is a contradiction. This completes the proof of the lemma.


Recall that ^V = A. Define ξ_0 to be the least
ξ > Θ^L(U,A) such that L_ξ(U, A). Since
V | ξ_0 is a countably iterable A-premouse, it is easy to see
that

    V|ξ_0 = L_ξ_0(U, A).


Finally, we have the following agreement between L[_∞][h]
and L(U, A)[G][h] (as classes). Here we will use the extra condition
“X⃗∈ L(U,A)” in the definition of the Prikry-like forcing
 defined in Section <ref> to ensure that
∈ L(U,A).


  L[_∞][h] = L(U, A)[G][h].


  In L[_∞][h], one can easily compute the derived model of
  L[_∞] associated to h. Thus, using Lemma
  <ref>, it follows that
  U ∈ L[_∞][h]. By Lemma <ref>,
  A = ℝ^V ∈ L[_∞][h] and, using L(U,A) and
  _∞, one can easily define ℙ and
  G. Conversely, from G one can easily recover _∞.


This, together with the observation above, has the following
corollary:


  L_ξ_0[_∞][h] = V|ξ_0[G][h].




 §.§ Adding extenders on top


Finally, we use a -construction (see for example <cit.> or <cit.>) to add extenders witnessing another
Woodin cardinal on top of _∞. In Lemma
<ref>, we first extend Corollary <ref>
to ordinals ξ > ξ_0 in order to obtain an appropriate background
universe W for the -construction. Using the fact that V[G][h]
is a forcing extension of the A-premouse V = M_1(A) by a small
forcing, the proof of this lemma is straightforward and similar to the
argument in <cit.>, so we omit it.


  There is a proper class (_∞, h)-premouse W such that for
  any ξ≥ξ_0, 
  
  
  * W|ξ has the same universe as V|ξ[G][h],
  
  * for any k < ω, ρ_k(W|ξ) = ω if, and only if,
    ρ_k(V|ξ) = A, and
  
  * for any k < ω, if ρ_k(W|ξ) > ω, then
    ρ_k(W|ξ) = ρ_k(V|ξ) and
    p_k+1(W|ξ) = p_k+1(V|ξ).
  


Let = ^W(L_ξ_0[_∞]) be the result of a
-construction above L_ξ_0[_∞] performed inside W
and let _ξ for ξ≥ξ_0 denote the levels of the
-construction. The following lemma shows that  is as
desired.


The following hold:
  
  
  * For ξ≥ξ_0, if X ⊆_ξ is definable
    over _ξ with parameters from _ξ, then
    X ∩_∞ | δ_n ∈_∞ for all
    n < ω. 
  
  * For all ξ≥ξ_0, ρ_ω(_ξ) ≥λ. 
  
  *  is a premouse and [h] =
    W. 
  
  *  has ω+1 Woodin
    cardinals. 
  



  For the proof of (<ref>) note that _ξ
  is 
  definable over V|ξ[G] from _∞ since the translation
  between V|ξ[G][h] and W|ξ is definable and h is generic
  over V|ξ[G] for a homogeneous forcing. Hence, if
  X ⊆_ξ is definable over _ξ with parameters
  from _ξ, then X ∈ V[G]. We can assume without loss of
  generality that X is a set of ordinals and let Ẋ_n for
  every n < ω be a term defining X ∩δ_n from
  _∞ and the ordinal parameter ξ. Now we can argue as in
  the proof of Lemma <ref> to obtain
  X ∩δ_n ∈_∞, as desired.

  Suppose (<ref>) fails and let ξ≥ξ_0
  be least such that ρ_ω(_ξ) = ρ < λ. Say this
  is witnessed by some set of ordinals X ⊆ρ, which is
  definable over _ξ with parameters from _ξ, but
  X ∉_ξ. Since λ = ⋃_n < ωδ_n,
  there is some n < ω such that ρ < δ_n. This means
  that X = X ∩δ_n ∈_∞ by
  (<ref>). But _∞⊆_ξ, a
  contradiction.

  Finally, (<ref>) and
  (<ref>) now follow from this and standard
  properties of the -construction, see for example
  <cit.>.


This finishes the proof of Theorem <ref> and, by
putting the active extender of M_1^♯(A) on an initial of ,
e.g., as in <cit.>, also the proof of Theorem
<ref>.




§ APPLICATIONS


We sketch a proof of the equiconsistencies of the schemata stated in
Corollary <ref>. 


  We start with the equiconsistency of (<ref>), (<ref>),
  and (<ref>). Theorem <ref> together with Theorem
  <ref> immediately gives that the consistency of
  (<ref>) implies the consistency of (<ref>). Now suppose
  that (<ref>) is consistent, say there is a model M of
  +  + with n+5 Woodin cardinals. Using a fully
  backgrounded extender construction as in <cit.>, it is easy to
  see that M_n^♯(^M) exists in M and
  M_n(^M) ∩ = ^M. Moreover, as winning strategies for
  games of length ω on ω can be coded by reals,
  M_n(^M). Therefore the argument in Section
  <ref> shows that there is a model of 
  with ω + n Woodin cardinals. The direction from (<ref>)
  to (<ref>) follows from <cit.>, where Neeman argues in
  Appendix A, using results of <cit.>, that the existence of a
  model with ω+n Woodin cardinals and a measurable cardinal
  above them all implies the existence of a sufficiently iterable
  active premouse with ω+n Woodin cardinals to which Theorem
  2A.3 in <cit.> applies.

  Next, we argue that (<ref>) is equiconsistent with (<ref>)
  and (<ref>). First, suppose that there is a model V of
  +  + and, say, ^1_n+5-determinacy for games of
  length ω on  and work in this model. The methods of
  Section <ref> can be used to conclude from
  ^1_n+5-determinacy for games of length ω on reals that
  M_n^♯() exists and is countably iterable (see <cit.>
  for details). Since M_n^♯() contains all the reals, it in
  particular contains codes for all winning strategies for games on
  natural numbers of length ω which exist in V. Therefore
  M_n^♯() witnesses (<ref>). For the other
  direction, suppose there is model of  in which, say,
  ^1_n+5-determinacy holds for games of length ω^2 on
  ω. By the results in Section <ref>, there a
  countable set of reals A such that
  M_n+4(A) “ = A” +. Now work inside
  V = M_n+4(A) and write = A. Note that V is a model of
  + (see e.g., <cit.>). Since M_n+3^♯() exists
  in V, it follows from the proof of projective determinacy in
  <cit.> that ^1_n-determinacy holds for games of length
  ω on  (see <cit.> for details).

  Finally, we argue that (<ref>) is equiconsistent with the other
  schemata. Suppose there is model of  in which, say,
  ^1_n+5-determinacy holds for games of length ω^2 on
  ω. Then again by the results in Section <ref>
  there a countable set of reals A such that
  M_n+4(A) “ = A” + and we can work
  in V = M_n+4(A). As V has sufficiently many Woodin cardinals,
  every (ω, )-generic extension V[g] is closed under
  x ↦ M_n^♯(x) for all reals x and hence satisfies
  ^1_n+1-determinacy for games of length ω on
  ω. For the other direction we show the consistency of
  (<ref>). Suppose that there is a model V of ++
  such that, say, ^1_n+5-determinacy for games of length
  ω on ω holds in every (ω,)-generic
  extension of V[g] of V. As ^V is a countable set of reals
  in V[g], M_n+1^♯(^V) exists in V[g]. By homogeneity
  of the forcing, this implies that in V there is a set of reals
  coding a model with n+1 Woodin cardinals which contains
  ^V. This suffices to run the argument in <cit.> mentioned
  above which yields ^1_n-determinacy for games of length
  ω on .



We finish this article by sketching the modifications which are needed
to prove Theorems <ref> and
<ref>.


  Instead of Theorem <ref>, we now aim to obtain a
  countable set of reals A such that M_ω(A) ∩ = A and
  M_ω(A)  +. For this purpose, we replace
  1-smallness in the definition of φ-witness (see Definition
  <ref>) by ω-smallness. Moreover, we replace
  Π^1_2-iterability in the definition of the game
  _φ,ψ (see Definition <ref>) by the
  notion of weak iterability (also called
  ^Π^1_1-iterability) as in <cit.>. Note that determinacy of games of length ω^2 with
  ^Π^1_1 payoff suffices to show that this game is
  determined. Furthermore, Theorem 7.10 in <cit.> suffices to
  carry out the comparison arguments used to prove Theorem
  <ref>. The proofs in Sections <ref> and
  <ref> straightforwardly generalize to this
  context.



  Instead of Theorem <ref>, we now aim to obtain a
  countable set of reals A such that there is an A-premouse M of
  class S_α such that M ∩ = A and
  M  +. For this purpose, we replace 1-smallness in
  the definition of φ-witness (see Definition
  <ref>) by not being of class S_α. Moreover, we
  replace Π^1_2-iterability in the definition of the game
  _φ,ψ (see Definition <ref>) by the
  notion of Π^1_α-iterability as in <cit.>. Note that determinacy of games of length ω^2 with
  σ-projective payoff suffices to show that this game is
  determined. Furthermore, Lemmas 2.19 and 4.3 in <cit.> suffice to
  carry out the comparison arguments used to prove Theorem
  <ref>. The proofs in Sections <ref> and
  <ref> straightforwardly generalize to this
  context.







abstract




