The Martin–Harrington theorem

Statement

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.

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.

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).