---
tag: B219KX1T9B
kind: statement
role: theorem
name: The Martin–Harrington theorem
sources:
  - wikipedia: en:2630881@r1361303671
    locator: Lightface analytic game, section The Martin–Harrington theorem
    note: adopted
    mention: wikipedia://en/2630881#1OHQ
    sections: [Statement]
inventory: [4A0Q98BHGN]
---

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