Borel Determinacy (Martin)

Martin's Borel determinacy theorem is one of the most important results provable in ZFC, establishing that all Borel games are determined without any large cardinal assumptions.

Statement

Theorem9.6Borel determinacy (Martin, 1975)

For every Borel set $A \subseteq \omega^\omega$ , the Gale-Stewart game $G_A$ is determined: either player I or player II has a winning strategy.

Proof Outline

Proof

The proof proceeds by induction on the Borel complexity of $A$ .

Base case ( $\boldsymbol{\Sigma}^0_1$ and $\boldsymbol{\Pi}^0_1$ ): Gale and Stewart (1953) proved that open and closed games are determined. For a closed set $A$ : the game tree has a natural ranking by ordinals. Player I wins iff the rank of the initial position is "infinite" (reaches a winning terminal state). Player II wins by always moving to decrease the rank.

Inductive step: The key difficulty is handling countable unions and complements simultaneously. Martin's proof uses an auxiliary game technique called unraveling.

For $A \in \boldsymbol{\Sigma}^0_{\alpha+1}$ , write $A = \bigcup_n B_n$ where each $B_n \in \boldsymbol{\Pi}^0_\alpha$ . Define an auxiliary game where players also declare which $B_n$ they are aiming for (or avoiding). The auxiliary game has simpler payoff (at level $\boldsymbol{\Pi}^0_\alpha$ ), determined by induction. A winning strategy in the auxiliary game can be "pulled back" to a winning strategy in the original game.

The technical core requires iterating this construction through all countable ordinal levels, using the axiom of replacement (to form the necessary transfinite sequences of games) and the power set axiom. Friedman showed that the proof inherently requires these axioms: Borel determinacy is not provable in second-order arithmetic. $\blacksquare$

■

Proof-Theoretic Strength

RemarkReverse mathematics of Borel determinacy

Borel determinacy is the prime example of a "natural" theorem requiring strong set-theoretic axioms:

$\boldsymbol{\Sigma}^0_1$ determinacy is provable in weak arithmetic.
$\boldsymbol{\Sigma}^0_2$ determinacy requires $\omega$ iterations of the power set.
$\boldsymbol{\Sigma}^0_\alpha$ determinacy requires $\alpha$ iterations of the power set.
Full Borel determinacy requires $\omega_1$ iterations and is not provable in Zermelo set theory (Z) or in any system weaker than about $\omega_1$ iterations of the power set axiom.

Friedman proved: for each $n$ , there exists a Borel set of finite level whose determinacy is not provable in $Z_n$ ( $n$ -th order arithmetic).

ExampleStrategy for an open game

Let $A = \{x \in \omega^\omega : \exists n,\, x(0) + \cdots + x(n) > 100\}$ (open: the condition is witnessed in finite time).

Player I wins by choosing large numbers (e.g., $a_0 = 101$ ). This illustrates open determinacy: once the open condition is achieved, player I wins regardless of future moves.