In descriptive set theory, a lightface analytic game is an infinite two-player game of perfect information whose payoff set is a lightface analytic (Σ11) subset of Baire space. The determinacy of all lightface analytic games is equivalent, over ZFC, to the existence of 0#, a result known as the Martin–Harrington theorem.
Background
Infinite games The games studied here are Gale-Stewart games. Two players, conventionally called Player I and Player II, alternate choosing natural numbers, with Player I going first:
Player I chooses a0, Player II chooses a1, Player I chooses a2, ... After infinitely many rounds, the two players have together produced an infinite sequence (a0, a1, a2, ...) in Baire space ωω — the set of all infinite sequences of natural numbers equipped with the product of the discrete topology. A payoff set A ⊆ ωω is fixed in advance; Player I wins if the resulting sequence belongs to A, and Player II wins otherwise. A strategy for Player I is a function σ that maps each finite sequence of even length (representing the moves played so far) to a natural number (Player I's next move). A strategy for Player II is defined analogously for sequences of odd length. A strategy is a winning strategy if following it guarantees a win regardless of the opponent's play. A game is determined if one of the two players has a winning strategy.
The determinacy hierarchy Not all infinite games are determined: using the axiom of choice one can construct an undetermined game. However, determinacy holds for payoff sets of low descriptive complexity. The classical results form a hierarchy:
Lightface versus boldface The lightface/boldface distinction is central to this subject. A set A ⊆ ωω is boldface analytic (Σ11) if it is the projection of a closed set in a product space, equivalently if there exists a tree T on ω × ω such that A is the set of first coordinates of infinite branches through T. The lightface version adds an effectivity constraint: A is lightface analytic (Σ11) if T can be taken to be a computable (recursive) subset of (ω × ω)<ω. Equivalently, a set is lightface analytic if it is recursively enumerable relative to no oracle — it can be described without any real-number parameters. Boldface analytic sets may require real-number parameters; the lightface class is strictly smaller. This distinction has a direct consequence for determinacy: boldface analytic determinacy follows from the existence of a measurable cardinal, a relatively strong large-cardinal assumption. Lightface analytic determinacy requires only the weaker assumption that 0# exists. Conversely, Leo Harrington showed that lightface analytic determinacy cannot be proved in ZFC alone, and in fact implies the existence of 0#.
The Martin–Harrington theorem The central result of the subject is:
Theorem (Martin–Harrington, 1978). The following are equivalent over ZFC: All lightface analytic games are determined. 0# exists.
Forward direction: 0# implies determinacy Donald A. Martin proved that if 0# exists then all lightface analytic games are determined. The key tool is the sequence of Silver indiscernibles encoded by 0#. These indiscernibles provide a uniform way to build winning strategies for lightface analytic games: the computable tree defining the payoff set can be analyzed using the indiscernibles, and the resulting structure allows one to determine which player wins and to explicitly construct a winning strategy.
Reverse direction: determinacy implies 0# Leo Harrington proved the converse in 1978: if all lightface analytic games are determined, then 0# exists. This direction is considerably harder. Harrington's proof uses the theory of admissible sets and admissible ordinals (in particular, Barwise compactness) to show that determinacy of a certain lightface analytic game forces the existence of a model of set theory with a non-trivial elementary embedding j : L → L, which is equivalent to the existence of 0#. A later forcing-free proof of this direction was given by Sami (1999).
0# and the constructible universe 0# (zero sharp) is a real number — formally a subset of ω — that encodes the complete first-order theory of Gödel's constructible universe L with respect to its Silver indiscernibles. The Silver indiscernibles are a club class of ordinals that are indistinguishable from one another by any first-order formula of set theory with parameters from lower in the indiscernible sequence. The existence of 0# is independent of ZFC. If 0# exists then L ≠ V (the constructible universe is a proper inner model of the true universe), and every uncountable cardinal of V is a measurable cardinal in L[0#]. The existence of a measurable cardinal implies that 0# exists, but not conversely; 0# is a strictly weaker assumption.
Relativization The theorem relativizes to arbitrary reals. For any real x, Π11(x) determinacy — determinacy of all games whose payoff set is lightface co-analytic relative to x as an oracle — is equivalent to the existence of x#, the sharp for the inner model L[x]. The original Martin–Harrington theorem is the special case x = ∅.
See also Analytic set Analytical hierarchy Borel determinacy theorem Descriptive set theory Projective determinacy Zero sharp
References
Further reading Moschovakis, Yiannis N. (2009). Descriptive Set Theory (2nd ed.). American Mathematical Society. ISBN 978-0-8218-4813-5. Kanamori, Akihiro (2003). The Higher Infinite (2nd ed.). Springer. ISBN 3-540-00384-3. Ahmed, Shehzad (2014). Π11-Determinacy and Sharps (PDF) (Master's thesis). Boise State University.