In 1971, before the theorem was proved, Harvey Friedman showed that any proof of the theorem in Zermelo–Fraenkel set theory must make repeated use of instances of the axiom schema of replacement.
On each turn, each player chooses a single element of A to play.
The players are aware, from the beginning of the game, of a fixed payoff set (a.k.a.
If the infinite sequence created by a play of the game is in the payoff set, then player I wins.
More specifically, a winning strategy for player I is a function f that takes as input sequences of elements of A of even length and returns an element of A, such that player I will win every play of the form
A winning strategy for player II is a function g that takes odd-length sequences of elements of A and returns elements of A, such that player II will win every play of the form
For a given set A, whether a subset of Aω will be determined depends to some extent on its topological structure.
The tree consists of all finite sequences of elements of A, and the children of a particular node σ of the tree are exactly the sequences that extend σ by one element.
For each of the finite sequences σ in the tree, the set of all elements of Aω that begin with σ is a basic open set in the topology on A.
The Borel sets of Aω are the smallest class of subsets of Aω that includes the open sets and is closed under complement and countable union.
The Borel sets are classified in the Borel hierarchy based on how many times the operations of complement and countable union are required to produce them from open sets.
Gale and Stewart (1953) proved that if the payoff set is an open or closed subset of Aω then the Gale–Stewart game with that payoff set is always determined.
Over the next twenty years, this was extended to slightly higher levels of the Borel hierarchy through ever more complicated proofs.
This led to the question of whether the game must be determined whenever the payoff set is a Borel subset of Aω.
It was known that, using the axiom of choice, it is possible to construct a subset of {0,1}ω that is not determined (Kechris 1995, p. 139).
Harvey Friedman (1971) proved that any proof that all Borel subsets of Cantor space ({0,1}ω ) were determined would require repeated use of instances of the axiom schema of replacement, an axiom not typically required to prove theorems about "small" structures such as Cantor space that are not explicitly "set-theoretic" (that is, constructed for the purposes of exploring axiomatic set theory).
Donald A. Martin (1975) proved that for any set A, all Borel subsets of Aω are determined.
In his review of Martin's paper, Drake describes the second proof as "surprisingly straightforward."
However, the last two properties can be more easily proved without using Borel determinacy, by showing that the σ-algebras of measurable sets or sets with the Baire property are closed under Suslin's operation
The Borel determinacy theorem is of interest for its metamathematical properties as well as its consequences in descriptive set theory.
Determinacy of closed sets of Aω for arbitrary A is equivalent to the axiom of choice over ZF (Kechris 1995, p. 139).
When working in set-theoretical systems where the axiom of choice is not assumed, this can be circumvented by considering generalized strategies known as quasistrategies (Kechris 1995, p. 139) or by only considering games where A is the set of natural numbers, as in the axiom of determinacy.
One way it differs from ZF is that Z does not prove that the power set operation can be iterated infinitely many times beginning with an arbitrary infinite set.
In particular, Vω + ω, a particular level of the cumulative hierarchy with countable rank, is a model of Zermelo set theory.
The axiom schema of replacement, on the other hand, is only satisfied by Vκ for significantly larger values of κ, such as when κ is a strongly inaccessible cardinal.
Friedman's theorem of 1971 showed that there is a model of Zermelo set theory (with the axiom of choice) in which Borel determinacy fails, and thus Zermelo set theory alone cannot prove the Borel determinacy theorem.
[1] The existence of all beth numbers of countable index is sufficient to prove the Borel determinacy theorem.
It is known to be unprovable in ZFC but relatively consistent with it and implied by certain large cardinal axioms.
The existence of a measurable cardinal is enough to imply over ZFC the result that all analytic subsets of Polish spaces are determined, which is weaker than full projective determinacy.
The axiom of determinacy states that all subsets of all Polish spaces are determined.