Long Games and -Projective Sets
Abstract.
We prove a number of results on the determinacy of -projective sets of reals, i.e., those belonging to the smallest pointclass containing the open sets and closed under complements, countable unions, and projections. We first prove the equivalence between -projective determinacy and the determinacy of certain classes of games of variable length (Theorem 2.4). We then give an elementary proof of the determinacy of -projective sets from optimal large-cardinal hypotheses (Theorem 4.4). Finally, we show how to generalize the proof to obtain proofs of the determinacy of -projective games of a given countable length and of games with payoff in the smallest -algebra containing the projective sets, from corresponding assumptions (Theorems 5.1 and 5.4).
Key words and phrases:
Infinite Game, Determinacy, Inner Model Theory, Large Cardinal, Long Game, Mouse2010 Mathematics Subject Classification:
03E60, 03E45, 03E15, 03E30, 03E551. Introduction
Let denote the space of infinite sequences of natural numbers with the product topology, i.e., the topology generated by basic (cl)open sets of the form
where . As usual, we will refer to the elements of as reals. Given a subset of , the payoff set, we consider the Gale-Stewart game of length as follows:
for .
Two players, I and II, alternate turns playing to produce an element of . Player I wins if and only if ; otherwise, Player II wins. One can likewise define longer games by considering subsets of , where is a countable ordinal. If so, we will again regard as a product of discrete spaces. A game is determined if one of players I and II has a winning strategy. A set is said to be determined if the corresponding game is.
These games have been studied extensively; under suitable set-theoretic assumptions, one can prove various classes of them to be determined. One often studies the determinacy of pointclasses given in terms of definability (a general reference is Moschovakis [Mos09]). A pointclass central to this article is the following:
Definition 1.1.
The pointclass of -projective sets is the smallest pointclass closed under complements, countable unions,111Of course, one only considers unions of sets in the same space, as is usual. and projections.
In this article, we consider the following classes of games, and their interplay:
-
(1)
games of fixed countable length whose payoff is -projective;
-
(2)
games of variable length whose payoff is a pointclass containing the clopen sets and contained in the -projective sets;
-
(3)
games of countable length with payoff in other -algebras.
Neeman extensively studied long games and their connection to large cardinals in [Nee04]. These results are based on his earlier work in [Nee95] and [Nee02] on games of length , where he started connecting moves in long games with moves in iteration games. He showed in [Nee04] for example that the determinacy of games with fixed countable length and analytic payoff set follows from the existence of Woodin cardinals. Moreover, he also analyzed games of continuously coded length (see also [Nee05]) and games of length up to a locally uncountable ordinal. In [Nee07] he even showed determinacy for open games of length , indeed for a larger class of games of length , from large cardinals. That the determinacy of arbitrary games of length is inconsistent is due to Mycielski and has been known for a long time (see [Myc64]).
As for the converse, the determinacy of infinite games implies the existence of inner models with large cardinals (cf. e.g., [Har78, KW10, Tra13, Uhl16, MSW20] and others).
Summary of results
We begin in Section 2 by introducing a class of games of variable length below . We call these games -simple, where is a pointclass. We show that -projective determinacy implies the determinacy of -simple games of length where is the pointclass of all -projective sets. In Section 3 we introduce a class of games we call decoding games. These are used to show that -projective determinacy follows from simple clopen determinacy of length . The proof also shows directly that simple -projective determinacy of length follows from simple clopen determinacy of length
In Section 4, we prove simple clopen determinacy of length (and thus -projective determinacy of length ) from optimal large cardinal assumptions. The proof is level-by-level. An alternative, purely inner-model-theoretic proof of -projective determinacy can be found [Agu]; our proof, however, requires little inner model theory beyond the definition of the large-cardinal assumption. Roughly, it consists in repeatedly applying a theorem of Neeman [Nee04] to reduce a simple clopen game of length to an iteration game on an extender model with many partial extenders. The difference here is that players are allowed to drop gratuitously in the iteration game finitely many times to take advantage of the partial extenders in the model.
Finally, in Section 5, we exhibit some additional applications of the proof in Section 4. Specifically we prove from (likely optimal) large cardinal assumptions that -projective games of length are determined, where is a countable ordinal. We also prove, from a hypothesis slightly beyond projective determinacy, that games in the smallest -algebra containing the projective sets are determined.
2. Simple games of length
We begin by noting a result on the determinacy of games of length222Here and below, we identify the spaces , and , as well as and . :
Theorem 2.1 (folklore).
The following are equivalent:
-
(1)
All projective games of length are determined.
-
(2)
All projective games of length are determined, for all .
-
(3)
All clopen333In the product topology on . games of length are determined, for all .
Instead of providing a proof of Theorem 2.1, we refer the reader to the proof of Theorem 2.4 below, an easy adaptation of which suffices (cf. Remark 2.5).
Our first result is the analog of Theorem 2.1 for -projective games. Although the equivalence between the first two items remains true if one replaces “projective” with “-projective,” the one between the last two does not. Instead, one needs to consider a larger class of games that are still decided in less than rounds, in the sense that for any there is such that for all , if , then
Note that every game of length can be seen as a game of this form, for any . For the definition below, we adapt the convention that if , then a subset of can be identified with
Definition 2.2.
Let be a collection of subsets of (each identified with a subset of for some as above). A game of length is -simple if it is obtained as follows:
-
(1)
For every , games that are decided after moves such that their payoff restricted to sequences of length is in are -simple.
-
(2)
Let and for each let be a -simple game. Then the game obtained as follows is -simple: Players I and II take turns playing natural numbers for moves, i.e., rounds in games of length . Afterwards, Player I plays some . Players I and II continue playing according to the rules of (keeping the first natural numbers they have already played, but not ).
-
(3)
Let and for each let be a -simple game. Then the game obtained as follows is -simple: Players I and II take turns playing natural numbers for moves, i.e., rounds in games of length . Afterwards, Player II plays some . Players I and II continue playing according to the rules of (keeping the first natural numbers they have already played, but not ).
We are mainly interested in games of length which are simple clopen, i.e., which are -simple for the collection of clopen sets. Let us start by noting that every simple clopen game has in fact a payoff set which is clopen in (this fact will not be needed, but it justifies our terminology).
Lemma 2.3.
Let be a simple clopen game of length with payoff set . Then is clopen in .
Proof.
We prove this by induction on the definition of simple clopen games. In the case that is a clopen game of fixed length it is clear that is clopen. So suppose that we are given simple clopen games , with payoff sets . Moreover, suppose for notational simplicity that , i.e., the players play one round of length before Player I plays to decide which rules to follow. Inductively, we can assume that every is clopen in . Let be the game obtained by applying (2) in Definition 2.2. For , write for
Then is a winning run for Player I in iff
Each is open, so the payoff set of is open. Additionally, if, and only if,
Each is closed, so is closed. Therefore, is clopen.
The main fact about simple clopen games is that their determinacy is already equivalent to determinacy of -simple games where is the pointclass of all -projective sets:
Theorem 2.4.
The following are equivalent:
-
(1)
All -projective games of length are determined.
-
(2)
All simple -projective games of length are determined.
-
(3)
All simple clopen games of length are determined.
The proof of -projective determinacy of length from simple clopen determinacy, i.e., , will take place in the next section (Proposition 3.1). For now, we content ourselves with showing that -projective determinacy of length implies simple clopen determinacy of length , i.e., (see Proposition 2.7), although the proof we give easily adapts to show simple -projective determinacy of length from the same hypothesis, i.e., (see Proposition 3.7). Note that is obvious. It will be convenient for the future to introduce the definition of the game rank of a simple clopen game.
To each simple clopen game of length we associate a countable ordinal , the game rank of , by induction on the definition of simple clopen games. If is a game of fixed length , then . If is obtained from games , and from an ordinal as in Definition 2.2, we let
Remark 2.5.
The proof of Theorem 2.4 is local. We leave the computation of the precise complexity bounds to the curious reader, but we mention that e.g., the proof shows the equivalence among
-
(1)
the determinacy of games of length which are for some ;
-
(2)
the determinacy of simple clopen games of length of rank
-
(3)
the determinacy of simple games of rank which are for some .
The reason why we have chosen to define the game rank this way is that it will make some arguments by induction easier later on. Let us consider some examples: if , then is essentially a game in which an infinite collection of games, each of bounded length, are given, and one of the players begins by deciding which one of them they will play. If , then the game is similar, except that the player does not decide which game they will play until the first moves have been played. More generally, a game has limit rank if and only if it begins with one player choosing one among a countably infinite collection of games that can be played.
Remark 2.6.
Let be a simple clopen game of rank and be a partial play of . Denote by the game that results from after has been played. Then is a simple clopen game of rank .
Clearly, every simple clopen game has a countable rank. Now we turn to the proof of in Theorem 2.4.
Proposition 2.7.
Suppose that all -projective games of length are determined. Then all simple clopen games of length are determined.
Proof.
Let us say that two games and are equivalent if the following hold:
-
(1)
Player I has a winning strategy in if and only if she has one in ; and
-
(2)
Player II has a winning strategy in if and only if she has one in .
We prove the proposition by induction on the game rank of a simple clopen game . In the case that the game rank is a successor ordinal, we additionally show that the game is equivalent to a -projective game of length (this is clear in the limit case). Suppose that is a limit ordinal and this has been shown for games of rank . Let be the rank of , where . If , then the result follows easily: by the definition of game rank, the rules of dictate that one player must begin by choosing one amongst an infinite sequence of games . If that player has a winning strategy in any one of them, then choosing that game will guarantee a win in ; otherwise, the induction hypothesis yields a winning strategy for the other player in each game and thus in .
If , say, , then one argues as follows. Given a partial play of , we denote by the game after has been played. Consider the following game, :
-
(1)
Players I and II alternate many turns to produce a real number .
-
(2)
Afterwards, the game ends. Player I wins if and only if
Player I has a winning strategy in , where .444Here, denotes the result of facing off the strategies coded by the reals and .
Claim 1.
is equivalent to .
Granted the claim, it is easy to prove the proposition, for, letting be as above, the rules of dictate that one of the players must choose one amongst an infinite sequence of games . Assume without loss of generality that this is Player I. By induction hypothesis, the set of such that there exists so that Player I has a winning strategy in is -projective. Hence, the payoff set of is -projective, as was to be shown.
It remains to prove the claim. Thus, let and consider the following game :
-
(1)
Players I and II alternate many turns to produce real numbers .
-
(2)
Afterwards, the game ends. Player I wins if and only if
Player I has a winning strategy in the game , where .
Thus, . By induction on (i.e., by downward induction on ), we show that is equivalent to . A simple modification of the argument shows that is equivalent to , for each and each ; this is possible because is a simple clopen game of rank . We will use the equivalence between and as part of the induction hypothesis.
We have shown (by the induction hypothesis for the proposition) that is equivalent to . The same argument applied to shows that is equivalent to for every and thus that is determined. Moreover, Player I wins a run of if and only if she has a winning strategy in and Player II wins a run of if and only if Player I does not have a winning strategy in ; however, is determined for every , as it is a -projective game of length (this follows from an argument as right after the statement of Claim 1). Moreover, the induction hypothesis (for the claim) shows that a player has a winning strategy in if and only if she has one in . This shows that a player has a winning strategy in if and only if she has one in , as was to be shown. ∎
3. Decoding games
Our first goal in this section is to prove the following proposition, i.e., in Theorem 2.4.
Proposition 3.1.
Suppose simple clopen games of length are determined. Then -projective games of length are determined.
In order to prove Proposition 3.1, we introduce a representation of -projective sets.
Definition 3.2.
Fix an enumeration
of all basic open and basic closed sets in each , for . Suppose is -projective. A -projective code of is defined inductively as follows:
-
(1)
If is basic open, then , where .
-
(2)
If is basic closed, then , where .
-
(3)
If , then .
-
(4)
If , then .
-
(5)
If for some , then .
-
(6)
If , then .
-
(7)
If , then .
Here, denotes the dual of the projection,
A -projective code of a given set is not unique. In fact,
Lemma 3.3.
Let be -projective.
-
(1)
has a -projective code in which no complements and no basic open sets appear.
-
(2)
has a -projective code in which no complements and no basic closed sets appear.
Proof.
Given a -projective code for , one obtains, by a simple application of de Morgan’s laws, a -projective code in which complements are only applied to basic open sets or to basic closed sets. Since every basic open set is clopen, basic open sets can be replaced by a countable intersection of basic closed sets in the projective code; similarly, basic closed sets can be replaced by a countable union of basic open sets. ∎
Definition 3.4.
Suppose for some is -projective and fix a code for . The decoding game for (with respect to ) is a game of length according to the following rules: In the first rounds, which we will call the preparation, Players I and II start by alternating turns playing natural numbers to obtain reals . Afterwards, they proceed according to the -projective code of via the following recursive definition:
-
(1)
If is basic open, say , then the game is over, i.e., further moves are not relevant. Player I wins if and only if .
-
(2)
If is basic closed, say , then the game is over, i.e., further moves are not relevant. Player I wins if and only if .
-
(3)
If , so that , then Player I plays some . The game continues from the current play (without the last move, ) with the rules of the decoding game with respect to .
-
(4)
If , so that , then Player II plays some . The game continues from the current play (without the last move, ) with the rules of the decoding game with respect to .
-
(5)
If for some , so that , then the game continues from the current play with the rules of the decoding game with respect to , except that the roles of Players I and II are reversed.
-
(6)
If , so that , then Player I plays some in moves of the game, where the moves of Player II are not relevant. The game continues from the current play, together with , using the rules of the decoding game with respect to .
-
(7)
If , so that , then Player II plays some in moves if the game, where the moves of Player I are not relevant. The game continues from the current play, together with , using the rules of the decoding game with respect to .
Clause (5) of the preceding definition will not be used below, but we have defined it in the natural way nonetheless.
Lemma 3.5.
Let for some be -projective and fix a code for . A player has a winning strategy in the game with payoff set if and only if the player has a winning strategy in the decoding game for with respect to .
Proof.
Assume first that Player I has a winning strategy in the game with winning set . Then the following describes a winning strategy for Player I in the decoding game for with respect to . In the first rounds of the game, Player I follows the strategy . Since is a winning strategy in , the players produce a sequence of reals . In the following rounds, Player I follows the rules of the decoding game according to , playing witnesses to the fact that . This means that, e.g., if , i.e., , then Player I plays such that . The strategy for the other cases is defined similarly. This yields a winning strategy for Player I in the decoding game for with respect to .
Now assume that Player I has a payoff strategy in the decoding game for with respect to . Then the restriction of to the first rounds of the game is a winning strategy for Player I in the game . Similarly for Player II. ∎
Lemma 3.6.
Let be -projective, for some . Then, for every -projective code for in which no complements appear, the decoding game given by is simple clopen.
Proof.
Choose a code for in which no complements appear. We will show by induction on the definition of simple clopen games, that the game obtained as in (6) or (7) in Definition 3.4 is simple clopen again. This will finish the proof as games obtained by clauses (1)-(4) in Definition 3.4 are clearly simple clopen, by the definition of simple clopen games.
Let us introduce some notation for this proof. If , we write for the sequence of digits of in even positions, and for the sequence of digits of in odd positions. Thus, if results from a run of a Gale-Stewart game, then is the sequence of moves of Player I and that of Player II.
So let be a simple clopen game with payoff set and consider the game which is defined as follows. Players I and II start by alternating turns playing natural numbers to define reals . Then players I and II alternate moves to play some real . Finally, Players I and II alternate again to produce reals so that and we say that is a winning run for Player I in iff . That means if denotes the payoff set of , we have iff . We aim to show that is simple clopen again.
Suppose first that is a clopen game of some fixed length , i.e., we consider as a game of length but only the first moves are relevant for the payoff set. Fix some . In particular, is a clopen set in . We can naturally write for clopen sets , and . By definition, the payoff set for the game is , where
which is clopen. Moreover, in again only the first moves are relevant, so is a clopen game of fixed length and in particular simple clopen.
Now suppose that is a simple clopen game obtained by condition (2) in Definition 2.2, i.e., we are given simple clopen games , , and after Player I and II take turns producing , Player I plays some natural number and the players continue according to the rules of (keeping the moves which produced ). That means for every , some sequence is a winning run for Player I in iff is a winning run for Player I in . We can assume inductively that the games for (obtained as above) are simple clopen and we aim to show that is simple clopen. Consider the simple clopen game which is obtained by applying (2) in Definition 2.2 to the games and the natural number . Suppose Players I and II produce in a run of . Then
where the first equivalence holds by definition of , the second equivalence holds by inductive hypothesis, the third equivalence by choice of , and the fourth equivalence by definition of . Hence and are equal and is a simple clopen game, as desired.
With Lemmata 3.5 and 3.6, Proposition 3.1 is proved. To finish the proof of Theorem 2.4 one needs to show the following proposition. This is and in Theorem 2.4.
Proposition 3.7.
Suppose either that simple clopen games of length are determined or that -projective games of length are determined. Then simple -projective games of length are determined.
Proposition 3.7 can be proved directly either by the method of the proof of Proposition
3.1, or by that of Proposition 2.7. In the second case, one need only carry out a straightforward adaptation.
In the first case,
a simple -projective game is reduced
to the simple clopen game in which two players play the game ,
producing a sequence for some
such that there is a -projective set
with the property that Player I
wins iff , no matter how the players continue playing the
rest of . After this, the players play the decoding game for to
determine who the winner is in a clopen way.
We close this section with a useful characterization of the -projective sets, although it will not be used.
Proposition 3.8 (Folklore).
A set is -projective if and only if it belongs to .
Proof.
Clearly, is closed under countable sequences and is closed under projections.
Conversely, by induction on , one sees that and the satisfaction relation for are coded by -projective sets of reals:
-
(1)
is coded by itself. The satisfaction relation for is given by
for a formula in the language of set theory and a finite sequence of reals. Since every formula in the language of set theory is in the class for some , belongs to the pointclass (i.e., the pointclass of countable unions of projective sets) and is thus -projective.
-
(2)
Suppose that a -projective code for has been defined and that a -projective satisfaction predicate for relative to has been defined. Suppose that and
(where is a quantifier and is ) is a -formula with free variables. Then, letting
a -projective code for can be defined by the disjointed union
where is a real number coding555E.g., it could be the tuple . the set . A satisfaction relation can be defined from this: for atomic formulae, we set
For other formulae, this is done as above, so the satisfaction relation is seen to belong to the pointclass and is thus by using the inductive hypothesis -projective.
-
(3)
Suppose that a -projective code for has been defined and that a -projective satisfaction predicate for has been defined for every , where is a countable limit ordinal. Then can be defined as the disjoint (countable) union of , for . Thus is -projective. The satisfaction relation can be defined as above.
This completes the proof. ∎
4. Determinacy from large cardinals
In this section, we prove level-by-level that the existence of certain iterable inner models with Woodin cardinals implies simple clopen determinacy of length , which in turn implies -projective determinacy of length . A different proof of this latter result can be found in [Agu], but the proof we give here has the advantage that it requires almost no inner-model-theoretic background. Another advantage is that it easily generalizes to yield further results (cf. the next section).
The idea of this proof is to enhance a simple clopen game of length by presenting each player with a fine-structural model that can be manipulated to obtain information about the game. This method of proof is due to Neeman [Nee04]; the difference in our context is that the models considered will contain many partial measures and, in addition to taking iterated ultrapowers, we will allow the players to remove end-segments of their models during the game so as to make the measures total and obtain new information. Although this determinacy proof could have been framed directly in terms of (the decoding game for) -projective sets, it seems somewhat more natural to consider simple clopen games of length instead and proceed by induction on the game rank.
Before we start with the proof, let us recall the relevant inner model theoretic notions we will need. In what follows, we will work with premice and formulae in the language of relativized premice , where is a predicate for a sequence of extenders, is a predicate for an extender, and is a predicate for a real number over which we construct the premouse.
For some real , a potential -premouse is a model where is a fine extender sequence666See Definition in [Ste10], which goes back to Section in [MS94] and [SSZ02]. and an ordinal or (see Section in [Ste10] for details). We say that such a potential -premouse is active iff . If , we write for the corresponding initial segment of . A potential -premouse is called an -premouse if every proper initial segment of is -sound. If it does not lead to confusion, we will sometimes drop the and just call a premouse. Informally, an -mouse is an iterable -premouse. We will avoid this term as the notion of iterability is ambiguous, but -iterability suffices for all our arguments.777We will only need weak iterability, in the sense of [Nee04]. Here we say that an -premouse is -iterable if it is iterable for countable stacks of normal trees of length (see Section of [Ste10] for a formal definition).
We consider premice belonging to various smallness classes:
Definition 4.1.
Let be an -iterable premouse and .
-
(1)
We say is of class above if is a proper class or active.
-
(2)
We say is of class above if there is some ordinal and some with such that is of class above and is Woodin in .
-
(3)
Let be a countable limit ordinal. We say is of class above if and is of class above for all .
Moreover, we say is of class if it is of class above .
Example 4.2.
Let and recall that a premouse is called -small if for every which is a critical point of an extender on the sequence of extenders of , . Moreover, we say is -small if is an initial segment of . Let denote the unique countable, sound, -iterable premouse which is not -small, but all of whose proper initial segments are -small, if it exists and is unique. If exists and is unique for all , then – in particular – every has a sharp. Let denote the smallest active premouse extending
Then is of class . If there is a premouse of class , then it contains and in fact is countable in it.
Note that if is a premouse of class , then is aware of this, since is countable in . If is of class and not a proper class, then is active and we can obtain a proper class model by iterating the active extender of and its images out of the universe. By convention, we shall say that this proper class model is also of class .
We recall the definition of the game rank of a simple clopen game. If is a game of fixed length , then . If is obtained from games , and from an ordinal as in Definition 2.2, we let
Remark 4.3.
For every simple game and initial play of , let denote the rest of the game after has been played. Let be a sequence of initial plays of starting with the empty sequence such that end-extends , and either is a successor ordinal with or is a limit ordinal. Then this sequence has to be of finite length and we can choose large enough such that .
Theorem 4.4.
Suppose that and for every there is an such that there is a proper class -premouse of class which is a model of . Then every simple clopen game such that is determined.
In the proof, we are going to use premice of class to apply the following theorem of Neeman multiple times.
Theorem 4.5 (Neeman, Theorem 2A.2 in [Nee04]).
There are binary formulae and in the language of set theory such that the following hold for any transitive, weakly iterable888As defined in Appendix A, Iterability in [Nee04]. Note that -iterability implies weak iterability. premouse which is a model of :
Let be a Woodin cardinal in and let and be -names for a subset of . Then,
-
(1)
If , there is a strategy for Player I in a game of length such that whenever is a play by , there is a non-dropping iterate of with embedding and an -generic such that and .
-
(2)
If , there is a strategy for Player II in a game of length such that whenever is a play by , there is a non-dropping iterate of with embedding and an -generic such that and .
-
(3)
Otherwise, there is an -generic and an such that and .
We now proceed to:
Proof of Theorem 4.4.
We may as well assume that is infinite, since otherwise has fixed length , so it is determined by the results of [Nee95] and [Nee02] (see also the introduction of [Nee04]).
Let be a simple clopen game with , say . We assume that is a successor ordinal, since the limit case is similar. Let code all parameters used in the definition of . We may as well assume that belongs to the Turing cone given by the hypothesis of the theorem.
To each non-terminal play of corresponds a game
Clearly, is a simple game and . Given , a -premouse , we select and define formulae and , and two sets and , each of which is either a -name for a set of real numbers or a set of natural numbers. The definition is by induction on (not on !). Formally, these names and sets of course depend on the model in which they are defined, so we sometimes write and to make this explicit. But for simplicity and readability we will omit this whenever it does not lead to confusion.
At the same time, we show that there are names, names for names, etc., for these sets such that their interpretation with respect to generics for some for collapsing Woodin cardinals of is a set of the same form with respect to the model instead of . More precisely, if is a model as above and has (at least) Woodin cardinals, then let be the forcing iteration of length collapsing the ordinals to one after the other, where is the least Woodin cardinal in and is the least Woodin cardinal in above for all , i.e., and for all ,
where is the canonical -name for . This is of course equivalent to the product and to the , but we are interested in the step-by-step collapse.
We consider nice -names for finite sequences of reals with the property that the game rank of is decided by the empty condition.999Note that the game rank of depends only on and finitely many digits of . By induction on the game rank of , we will specify for every such that has at least Woodin cardinals and every such -name , a -name in such that whenever is -generic over ,
where . We will call this name the good -name for . We will also define analogous names for . We now proceed to the recursive definition of , , , , , and .101010For every , will be one of three formulae (there is one possibility for the successor case and two for the limit case). We will however use the notation to make the presentation uniform. Similarly for .
Case 1.
(this is the base case).
Let and let be any -premouse which is a model of and of class . Assume without loss of generality that is minimal, in the sense that no proper initial segment of is a model of of class . Let be the least Woodin cardinal in , so that is of class above , and let . We define the -names for sets of reals and by111111Here and below, all names for real are assumed to be nice.
and
Let and be the formulae given by Neeman’s theorem (Theorem 4.5) such that the following hold:
-
(1)
If , there is a strategy for Player I in a game of length such that whenever is a play by , there is an iterate of , an elementary embedding and an -generic such that and .
-
(2)
If , there is a strategy for Player II in a game of length such that whenever is a play by , there is an iterate of , an elementary embedding and an -generic such that and .
-
(3)
Otherwise, there is an -generic and an such that and .
Now, we specify the good -names as claimed above, for models with enough Woodin cardinals below so that is defined. For , suppose that is a premouse with Woodin cardinals and is of class above and minimal above .121212A case of interest will be that of such which are initial segments of a model of some class which is minimal above . In such an , need not be a cardinal. Let be a nice -name for a finite sequence of reals and set
The good -names for and similar names for are defined analogously.
Case 2.
for some .
Let and let be any -premouse which is a model of of class . Assume without loss of generality that is minimal, in the sense that no proper initial segment of is a model of of class . Let be the least Woodin cardinal in , so that is of class above , and let . Then let
where is the good -name with respect to , so that whenever is -generic over , , where . We also let
for analogous as above. Note that is a good name for or respectively and hence already defined since for every real , . Let and be the formulae given by Neeman’s theorem (Theorem 4.5) such that the following hold:
-
(1)
If , there is a strategy for Player I in a game of length such that whenever is a play by , there is an iterate of , an elementary embedding and an -generic such that and .
-
(2)
If , there is a strategy for Player II in a game of length such that whenever is a play by , there is an iterate of , an elementary embedding and an -generic such that and .
-
(3)
Otherwise, there is an -generic and an such that and .
Now, we specify the good -names . For , suppose is a premouse with Woodin cardinals and that is of class above and minimal above . Let be a nice -name for a finite sequence of reals. Set
where is a good -name for . That means is such that whenever is -generic over , , where . The -names for and similar names for are defined analogously.
Case 3.
is a limit ordinal and the rules of dictate that, after , it is Player I’s turn.
Let and let be any -premouse which is a model of and of class . Let . Then let be the set of all such that there is an such that is an active -premouse of class which is minimal, in the sense that no proper initial segment thereof is of class , and, if we let be the result of iterating the active extender of out of the universe, then
This makes sense because for all , , so the set has been defined for all as above. Moreover, belongs to , since the formulae , together with their parameters , are definable131313Recall that the structure includes a predicate for its extender sequence. uniformly in , , and , as can be shown inductively by following this construction and the proof of Theorem 4.5 (cf. the proof of [Nee04, Theorem 1E.1]).
We let be the formula asserting that is non-empty. Similarly, let be the set of all such that whenever is such that is an active -premouse of class which is minimal, then
for defined as above. We let be the formula asserting that is equal to . As before, the set belongs to .
The good -names and are defined as before, for premice which are of class above finitely many Woodin cardinals.
Case 4.
is a limit ordinal and the rules of dictate that, after , it is Player II’s turn.
Let and let be any -premouse which is a model of and of class . Let . Then let be the set of all such that there is an such that is an active -premouse of class which is minimal, in the sense that no proper initial segment of is of class , and, if we again let be the result of iterating the active extender of out of the universe, then
Again, is in . We let be the formula asserting that is equal to . Similarly, let be the set of all such that whenever is such that is an active -premouse of class which is minimal, then
for defined as above. We let be the formula asserting that is non-empty.
The good -names and are defined as before, for premice which are of class above finitely many Woodin cardinals.
This completes the definition of the names , , , , and the formulae and . Continuing with the proof of Theorem 4.4, we prove a technical claim which shows that these names behave well under elementary embeddings.
Claim 1.
Suppose is a successor ordinal, let be a proper class premouse which is a model of of class and minimal, in the sense that no proper initial segment of is a model of of class .141414Since is a successor ordinal and is minimal, has a Woodin cardinal. Let be an elementary embedding. Let be a finite sequence of reals in . Then
and, analogously,
Proof.
Let denote the least Woodin cardinal of . We will in fact show that whenever is a -name for a finite sequence of reals such that is decided by the empty condition, we have
and
i.e., if is a good -name such that whenever is -generic over ,
then is a good -name such that whenever is -generic over ,
and similarly for .
This will yield the claim if applied to , as, by definition,
Hence,
and similarly for .
By the definition of simple games, depends only on , the length of , and finitely many values of (those in which the players determine the subgames played). Thus, if is a -name in for a finite sequence of reals such that for some countable ordinal and if is a -name for a real, then
The claim is proved simultaneously for all premice and all , by induction on the game rank of . We prove it for the names for Player I; the other part is similar. We proceed by cases:
First suppose that and let and be a -name for a finite sequence of reals such that . Let , so that whenever is -generic over ,
By definition,
By elementarity,
But this implies that is a good -name such that whenever is -generic over ,
This finishes the case .
If , where , let again , be a -name for a finite sequence of reals such that and let , so that whenever is -generic over ,
This means that
where is a good -name such that whenever is -generic over ,
By inductive hypothesis, and using that , we have that is a good -name such that whenever is -generic over ,
Since, by elementarity,
it follows that is a good -name such that for every -generic over ,
as desired.
If is a limit ordinal, let again , be a -name for a finite sequence of reals such that . Let , so that whenever is -generic over ,
This means that
where is a good -name such that whenever is -generic over ,
By inductive hypothesis, is a good -name such that whenever is -generic over ,
Since, by elementarity,
it follows that is a good -name such that for every -generic over ,
as desired.
The argument for is analogous. This completes the proof of the claim. ∎
Now we turn to the proof of the following claim, from which the theorem follows. Recall that .
Claim 2.
Let be an -premouse which of of class but has no proper initial segment of class . Let denote the least Woodin cardinal in . Then
-
(1)
If , then Player I has a winning strategy in .
-
(2)
If , then Player II has a winning strategy in .
-
(3)
.
Proof.
If is active, then we may identify it with the proper class sized iterated ultrapower by its top extender and its images, so we may assume that is a model of . Note that always has a Woodin cardinal, as is a successor ordinal. We first prove (3). Suppose that and . We inductively construct a run of the game by its initial segments together with reals , -premice which are proper class models of and ordinals . Let be the empty play, , and . Inductively, suppose that , , and have been defined and that
and let be the least Woodin cardinal of , if it exists.
If is a successor ordinal for some , then, by Neeman’s theorem (Theorem 4.5), there is an -generic and a such that and . This means that
Let , . Here can be rearranged as a -premouse for some real coding and as collapses a cutpoint of the -premouse . We will always consider as such a -premouse.
Suppose that is a limit ordinal and the rules of dictate that after , it is Player I’s turn. By inductive hypothesis we have , so there is no active initial segment , , of of class which is minimal and satisfies , for any . Moreover, . Hence, there is some and an active initial segment of of class which is minimal and does not satisfy , where is defined analogous as above. Fix such a and such an active initial segment of and let be the proper class model resulting from iterating the active extender of out of the universe. Set and . Then,
The case that is a limit ordinal and the rules of dictate that it is Player II’s turn after is similar.
Finally, suppose that . By Neeman’s theorem (Theorem 4.5), there is some -generic and some such that and . This means that
-
(1)
“Player I does not have a winning strategy in ”, and
-
(2)
“Player II does not have a winning strategy in ”.
However, , so is a clopen game of length . This is a contradiction, as is a model of , so it certainly satisfies clopen determinacy. This proves (3).
Let be as in the statement of the claim and suppose . We will describe a winning strategy for Player I in (in ) as a concatenation of strategies for different rounds of . Playing against arbitrary moves of Player II, we will for inductively construct plays for initial segments of according to together with
-
•
reals such that and ,
-
•
-premice which are proper class models of of class , none of whose initial segments are of class , and such that ,
-
•
premice together with iteration embeddings ,
-
•
if has a Woodin cardinal and is the least Woodin cardinal in , -generics over .
In case does not have a Woodin cardinal, we will let be undefined and let . In the other case, we let . Finally, we will stop the construction after finitely many steps when .
Let be the empty play and . We will inductively argue that
where is the -name or set of natural numbers in defined above.
Assume inductively that and with are already constructed for all and that . To construct and we distinguish the following cases.
Assume first that for some . Since
it follows from Neeman’s theorem (Theorem 4.5) that there is a strategy for Player I in a game of length such that whenever is a play by , there is an iterate of , an elementary embedding and an -generic such that and . Hence, by Claim 1, . By definition,
Let , , and . Note that and as before can be rearranged as a -premouse for some real coding and . Again, we will always consider as such a -premouse.
Now suppose that is a limit ordinal and the rules of dictate that, after , it is Player I’s turn. By assumption, . So
Hence, there is a natural number and an ordinal such that is an active initial segment of of class and is minimal, and, if we let be the result of iterating the active extender of out of the universe, then Let , , and . Moreover, let be the strategy which tells Player I to play .
For the other limit case suppose that is a limit ordinal and the rules of dictate that, after , it is Player II’s turn. In this case we can let as Player I is not playing, i.e., we only have to react to what Player II is playing in the next round. Suppose that Player II plays some natural number and let . Since , we have
In particular, . Thus there is an ordinal such that is an active initial segment of , minimal of class , and if we let denote the result of iterating the active extender of out of the universe, then Let , and .
Finally, assume that . Since , by Neeman’s theorem (Theorem 4.5), there is a strategy for Player I in a game of length such that whenever is a play by , there is an iterate of , an elementary embedding and an -generic such that and . Then, by Claim 1, . Therefore,
We let and stop the construction. Since , is a clopen game of length . As is a proper class model of , we can use absoluteness of winning strategies for clopen games of length to obtain that Player I has a winning strategy in in . Let be a strategy for Player I witnessing this.
This process describes a winning strategy for Player I in by concatenating the strategies for , as desired. ∎
This finishes the proof of Theorem 4.4. ∎
5. Further applications
In this section, we present some additional applications of the proof of Theorem 4.4. Since the proofs are similar, we simply sketch the differences.
5.1. Longer games
We begin by noting that the results presented so far generalize to longer games. In particular:
Theorem 5.1.
Let be a countable ordinal. Suppose that for each and each there is some and an -premouse of class above some below which there are Woodin cardinals in . Then -projective games of length are determined.
The theorem is a consequence of a more general result akin to Theorem 4.4, namely, the determinacy of simple -projective games of length , in the following sense:
Definition 5.2.
Let be a collection of subsets of (with each identified with a subset of for some as in Definition 2.2). A game of length is -simple if it is obtained as follows:
-
(1)
For every , games in of fixed length are -simple.
-
(2)
Let and for each let be a -simple game. Then the game obtained as follows is -simple: Players I and II take turns playing natural numbers for moves, i.e., rounds in games of length . Afterwards, Player I plays some . Players I and II continue playing according to the rules of (keeping the first natural numbers they have already played).
-
(3)
Let and for each let be a -simple game. Then the game obtained as follows is -simple: Players I and II take turns playing natural numbers for moves, i.e., rounds in games of length . Afterwards, Player II plays some . Players I and II continue playing according to the rules of (keeping the first natural numbers they have already played).
The notion of game rank in this context is defined as before: if is a game of fixed length , then . If is obtained from games , and from an ordinal as in Definition 5.2, we let
Theorem 5.3.
Let be a countable ordinal. Suppose that for each and each there is some and an -premouse of class above some below which there are Woodin cardinals in . Then, simple -projective games of length are determined.
Proof Sketch.
The theorem is proved like Theorem 4.4: first, by arguing as in Proposition 3.7, one sees that is suffices to prove determinacy for simple clopen games of length . Let be a game of successor rank definable from a parameter . Given and an active -premouse of class , one defines sets and and formulae and by induction on as in the proof of Theorem 4.4, provided .
The difference is as follows: in the proof of Theorem 4.4, occurs when ; here, it happens when is a -sequence of reals. Instead of defining in this case, we define only and . These are names for sets of -sequences of reals and are defined as in Case 2 in the proof of Theorem 4.4; namely,
where is a name for a -sequence of reals, is the least Woodin cardinal of above , and is the second Woodin cardinal of above , if it exists, and , otherwise. (Note that exists since, by assumption, is a successor ordinal). is defined similarly. Once these names have been defined, one applies Theorem 2A.2 of [Nee04] (the general version of Theorem 4.5) so that (using the fact that has Woodin cardinals below ) one obtains formulae and with parameters and , such that one of the following holds:
-
(1)
If , there is a strategy for Player I in a game of length such that whenever is a play by , there is a non-dropping iterate of with an embedding and an -generic such that and .
-
(2)
If , there is a strategy for Player II in a game of length such that whenever is a play by , there is a non-dropping iterate of with an embedding and an -generic such that and .
-
(3)
Otherwise, there is an -generic and an such that and .
An argument as in the proof of Theorem 4.4 yields the following claim:
Claim 1.
Let be an -premouse and be an ordinal such that has Woodin cardinals below . Suppose that is of class above and no proper initial segment of is of class above , where is a successor ordinal. Let denote the least Woodin cardinal of above . Then
-
(1)
If , then Player I has a winning strategy in .
-
(2)
If , then Player II has a winning strategy in .
-
(3)
.
The theorem is now immediate from the claim. ∎
5.2. -algebras
The proof of Theorem 4.4 adapts to prove the determinacy of various -algebras. As an example, we consider the smallest -algebra containing all projective sets. We show that a sufficient condition for its determinacy is the existence of -premice of class for every .
Theorem 5.4.
Suppose that for each there is an -premouse of class . Then, every set in the smallest -algebra on containing the projective sets is determined.
Proof Sketch.
Let belong to the -algebra in the statement. Let
denote the Borel hierarchy built starting from sets which are countable intersections of projective sets, i.e., consists of all countable intersections of projective sets and consists of all countable unions of sets each of which is the complement of a set in for some . Standard arguments show that these pointclasses constitute a hierarchy of sets in the smallest -algebra containing the projective sets. It follows that there is and such that , i.e., such that belongs to and that has a -projective code (in the sense of Section 3) which is recursive in .
Let be a -projective code for which is recursive in and in which no complements appear. To show that is determined, it suffices to show that the decoding game for is determined. Let us denote this game by . It is a simple clopen game; it is not quite of rank , so determinacy does not follow immediately from Theorem 4.4, but it follows from the proof:
Given a partial play of the game and a model , we define sets and , formulae and , and names and as in the proof of Theorem 4.4. The cases where are exactly as in the proof of Theorem 4.4. The remaining cases are very slightly different—for this, let us define the notion of subrank. Recall that has the following rules:
-
(1)
Players I and II begin by alternating many rounds to play a real number .
-
(2)
Afterwards, they alternate a finite amount of turns as follows: letting and supposing has been defined, is a -projective code for a union or an intersection of sets, say , with each of smaller (Borel) rank. By the rules of the decoding game, one of the players needs to play a natural number , thus selecting a -projective code for ; we let .
-
(3)
Eventually, a stage is reached in which is a code for a projective set; at this point the players continue with the rules of the decoding game for .
Given a play of in which a player needs to play a natural number and has been defined as above, we say that the game subrank of is the least such that or .
We now continue the definition of the sets and , formulae and , and names and . Assume is such that , so that the sets have not been defined already; we proceed by induction on the subrank of :
Case 5.
The subrank of is defined and nonzero and the rules of dictate that, after , it is Player I’s turn.
Let and let be any -premouse which is a model of and of class . Let . Then let be the set of all such that
This makes sense because for all , the subrank of is smaller than the subrank of , so the set has been defined. Moreover, belongs to , since is recursive in and the formulae , as well as the sets , are definable uniformly in , as can be shown inductively by following this construction and the proof of Theorem 4.5 (cf. the proof of [Nee04, Theorem 1E.1]).
We let be the formula asserting that is non-empty. Similarly, let be the set of all such that
We let be the formula asserting that is equal to . As before, the set belongs to .
The good -names and are defined as in the other cases.
Case 6.
The subrank of is defined and nonzero and the rules of dictate that, after , it is Player II’s turn.
This case is similar to the preceding one.
Case 7.
is the empty play.
Let be any -premouse which is a model of and of class and let be the smallest Woodin cardinal of . In this case, is the canonical -name for all reals such that holds, where is a good -name with respect to , so that whenever is -generic over , , where .
The name is defined analogously. The formulae and are obtained by applying Neeman’s theorem to and .
This completes the definition of the names and formulae. After this, an argument as in the proof of Theorem 4.4 yields the following claim:
Claim 1.
Let be an -premouse which is of class but has no proper initial segment of class . Let denote the least Woodin cardinal in . Then
-
(1)
If , then Player I has a winning strategy in .
-
(2)
If , then Player II has a winning strategy in .
-
(3)
.
The theorem is now immediate from the claim. ∎
The following remains an interesting open problem:
Question 5.5.
What is the consistency strength of determinacy for sets in the smallest -algebra containing the projective sets?
Acknowledgements
The first-listed author was partially suported by FWO grant number 3E017319 and by FWF grant numbers I4427 and I4513-N. The second-listed author, formerly known as Sandra Uhlenbrock, was partially supported by FWF grant number P 28157 and in addition gratefully acknowledges funding from L’ORÉAL Austria, in collaboration with the Austrian UNESCO Commission and in cooperation with the Austrian Academy of Sciences - Fellowship Determinacy and Large Cardinals. This project has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No 794020 of the third-listed author (Project IMIC: Inner models and infinite computations). The third-listed author was partially supported by FWF grant number I4039.
References
- [Agu] J. P. Aguilera. -Projective Determinacy. Submitted. Available at https://www.dropbox.com/s/g853hj5ern1kkyb/SPReversal.pdf?dl=0.
- [Har78] L. Harrington. Analytic Determinacy and . Journal of Symbolic Logic, 43:685–693, 1978.
- [KW10] P. Koellner and W. H. Woodin. Large Cardinals from Determinacy. In M. Foreman and A. Kanamori, editors, Handbook of Set Theory. Springer, 2010.
- [Mos09] Y. N. Moschovakis. Descriptive set theory, second edition, volume 155 of Mathematical Surveys and Monographs. AMS, 2009.
- [MS94] W. J. Mitchell and J. R. Steel. Fine structure and iteration trees. Lecture notes in logic. Springer-Verlag, Berlin, New York, 1994.
- [MSW20] S. Müller, R. Schindler, and W.H. Woodin. Mice with finitely many woodin cardinals from optimal determinacy hypotheses. Journal of Mathematical Logic, 20, 2020.
- [Myc64] Jan Mycielski. On the axiom of determinateness. Fundamenta Mathematicae, 53(2):205–224, 1964.
- [Nee95] I. Neeman. Optimal Proofs of Determinacy. Bulletin of Symbolic Logic, 1(3):327–339, 09 1995.
- [Nee02] I. Neeman. Optimal Proofs of Determinacy II. Journal of Mathematical Logic, 2(2):227–258, 11 2002.
- [Nee04] I. Neeman. The Determinacy of Long Games. De Gruyter series in logic and its applications. Walter de Gruyter, 2004.
- [Nee05] Itay Neeman. An introduction to proofs of determinacy of long games, pages 43––86. Lecture Notes in Logic. Cambridge University Press, 2005.
- [Nee07] Itay Neeman. Games of length . Journal of Mathematical Logic, 07(01):83–124, 2007.
- [SSZ02] R. Schindler, J. R. Steel, and M. Zeman. Deconstructing inner model theory. Journal of Symbolic Logic, 67:721–736, 2002.
- [Ste10] J. R. Steel. An Outline of Inner Model Theory. In M. Foreman and A. Kanamori, editors, Handbook of Set Theory. Springer, 2010.
- [Tra13] N. D. Trang. Generalized Solovay Measures, the HOD analysis, and the Core Model Induction. 2013. PhD Thesis. UC Berkeley.
- [Uhl16] Sandra Uhlenbrock, now Müller. Pure and Hybrid Mice with Finitely Many Woodin Cardinals from Levels of Determinacy. PhD thesis, WWU Münster, 2016.