Borel Determinacy

Origin. Martin (1975). Infinite games with Borel winning sets are determined. One player has winning strategy. Beyond Borel: requires large cardinals. Foundation for descriptive set theory.

Models. Two players alternate choosing naturals. Infinite play: sequence in ℕ^ω. Winning condition: Borel set A. Determined: one player has winning strategy.

Formalism.

Gale-Stewart game G(A): Players I and II alternate: a₀, b₀, a₁, b₁, ... Play: x = (a₀, b₀, a₁, b₁, ...) ∈ ℕ^ω Player I wins iff x ∈ A.

Strategy: σ for I: (history) → next move τ for II: (history) → next move σ * τ: unique play when both follow strategies

Winning strategy: σ winning for I in G(A) iff ∀τ. σ * τ ∈ A τ winning for II iff ∀σ. σ * τ ∉ A

Determinacy: G(A) determined iff I or II has winning strategy. Det(Γ): all games with Γ payoff determined.

Borel hierarchy: Σ⁰₁: open, Π⁰₁: closed Σ⁰_α: countable unions of sets drawn from ∪{β<α} Π⁰_β; Π⁰_α: complements of Σ⁰_α Borel: ∪{α<ω₁} Σ⁰_α = ∪_{α<ω₁} Π⁰_α The union runs to ω₁, not to ω. Stopping at the finite levels does not give the Borel sets, because those levels are not jointly closed under countable union: take one set from each of Σ⁰₁, Σ⁰₂, Σ⁰₃, … and their union already sits at Σ⁰_ω. On an uncountable Polish space the hierarchy is strictly increasing at every countable ordinal, so every level below ω₁ is needed and none above is.

Martin's theorem: All Borel games are determined. Det(Borel) provable in ZFC.

Beyond Borel: Analytic (Σ¹₁): projections of Borel. Det(Analytic) requires large cardinals. Projective determinacy: from large cardinals.

Symbols.

Symbol	Unicode	Name	Meaning
σ	U+03C3	Sigma	A strategy for player I; also the boldface Borel classes
τ	U+03C4	Tau	A strategy for player II
Σ	U+03A3	Sigma, capital	The existential side of a hierarchy level
Π	U+03A0	Pi, capital	The universal side of a hierarchy level
α, β	U+03B1, U+03B2	Alpha, beta	Countable ordinals indexing the hierarchy
ω	U+03C9	Omega	The first infinite ordinal; ω₁ is the first uncountable one
ℕ	U+2115	Double-struck N	The naturals, from which moves are drawn
∈	U+2208	Element of	x ∈ A: player I wins the play x
∉	U+2209	Not an element of	Player II's winning condition
∀	U+2200	Universal quantifier	Quantification over opposing strategies
∪	U+222A	Union	Union over the levels of the hierarchy
<	—	Less than	Ordinal order in the hierarchy definitions
*	—	Play operator	σ * τ is the play produced by both strategies
G(A)	—	Gale–Stewart game	The game with payoff set A
Det	—	Determinacy	Det(Γ): every game with payoff in Γ is determined
A	—	Payoff set	The set of plays winning for player I

Metatheory. Gale and Stewart (1953) proved open and closed games determined by an elementary argument, after which progress was level by level: Wolfe (1955) for Σ⁰₂, Davis (1964) for Σ⁰₃, Paris (1972) for Σ⁰₄. Martin (1975) proved that every Borel game is determined, in ZF plus dependent choice, by unravelling a Borel payoff set into a clopen one on an auxiliary tree of higher type and pulling the resulting strategy back. The proof's cost is exactly measured: Friedman (1971) showed that Borel determinacy cannot be proved without uncountably many iterations of the power set operation, so it is not a theorem of Zermelo set theory and is the standard example of an ordinary mathematical statement whose proof needs the full replacement schema. Above Borel the strength is calibrated by large cardinals rather than by the hierarchy: analytic determinacy is equivalent to the existence of sharps for all reals (Martin, Harrington), and Martin and Steel derived projective determinacy from infinitely many Woodin cardinals.

Applies to. Descriptive set theory. Set theory foundations. Infinite games. Automata theory. Large cardinals.

Limitations. Determinacy stops where it does for a reason: the Axiom of Choice supplies an undetermined payoff set by transfinite recursion over the continuum many strategy pairs, so full determinacy is inconsistent with AC and the Axiom of Determinacy can only be adopted in models where choice fails. Even the theorem that holds is expensive — by Friedman's result the whole cumulative hierarchy up to ω₁ is needed — so Borel determinacy has no proof in any weak or predicative system and no constructive content. Everything past the Borel sets is unprovable in ZFC outright and requires large cardinal hypotheses that are themselves unprovable. The strategies produced are arbitrary functions on finite sequences, with no bound on their complexity, which is why the theorem gives existence but nothing computational; the finite-state analogues used in verification need separate positional determinacy results.