In the game , where , the players alternately choose natural numbers and produce a sequence . Player I wins exactly when . A strategy in an infinite game assigns a move to every finite position where its player is to move; it is winning if every play following it is won by that player. A game is determined if one player has a winning strategy. Both cannot have winning strategies, since their joint play would have to be won by both. The axiom of determinacy asserts
Without assuming AD, one can prove determinacy for finite games by backward induction, and for games with open or closed payoffs by the following argument. Give its product topology of discrete move coordinates. If is open, let be the finite positions whose entire cylinder of extensions lies in . Form a winning-position attractor in an infinite game by transfinite recursion: add an I-position if some child has already been added, and add an II-position if all its children have already been added. Take unions at limits. The process stabilizes because there are only set-many positions and each genuine successor change adds a new one.
An added nonterminal position receives its least entry ordinal. At an I-position in the stable attractor, choose a child of smaller rank; at an II-position every child has smaller rank. Thus every play following I's rank-decreasing strategy must reach : an infinite strictly descending sequence of ordinals cannot exist. The resulting play is in , so I wins from any position in the attractor.
Outside the attractor, every child of an I-position remains outside, and an II-position has some child outside. Otherwise the ranks of all its children would have a set-sized supremum and the parent would have been added at a later stage. II chooses such a child and keeps the play outside forever. If its outcome were in the open set , some finite prefix would have its entire cylinder in , contrary to this avoidance. Therefore II wins from outside. With natural-number moves the least suitable child may be chosen at each position, so no choice axiom is needed for these strategies. This proves open determinacy. For a closed payoff, apply the same argument to its open complement with the players' winning roles interchanged. Clopen payoffs are included in both results.
Now assume AC and construct an undetermined game. The set of strategies for either player has cardinality , since a strategy is a function on a countably infinite set of positions. Each fixed strategy is compatible with plays: the other player's sequence of freely chosen moves determines distinct full plays. Use choice to enumerate I's strategies as and II's as , and well-order the space of plays.
Recursively choose following and following , with all selected plays distinct. At stage fewer than plays have been used, while each compatible-play set has size , so fresh choices exist; take the least ones in the fixed well-order. This does not require regularity of , since for every below its initial ordinal.
Put . Every I-strategy has the losing compatible play , and every II-strategy has the losing compatible play . Therefore neither player has a winning strategy. This choice diagonalization of an undetermined game proves
The elementary determinacy proofs above concern specified definable payoff classes; the diagonal construction explains why extending them to every arbitrary subset of the play space is incompatible with choice.
In an infinite game of perfect information, the players alternately choose elements of a nonempty set , producing . Player I wins when belongs to the payoff set . A strategy in an infinite game chooses a move at each position where its player moves, and a winning strategy in an infinite game wins against every possible opposing play. The Gale-Stewart theorem states that such a game is determined when is open in the product topology of discrete . The same holds for closed payoff sets and, more strongly, for every payoff set.
For open determinacy, let be the positions and the prefixes certifying a win for I, where is the extension cylinder set. Form the winning-position attractor in an infinite game by transfinite recursion: start at , at a successor stage add I-positions with some successor already in and II-positions with all successors in , and take unions at limits. This increasing sequence stabilizes, since its positions form a set. Call the stable set .
Each position in has a least entry ordinal, necessarily a successor. I chooses a successor with smaller entry ordinal; every II successor has smaller entry ordinal. An infinite strictly decreasing sequence of ordinals is impossible, so play reaches in finitely many moves. This gives I a winning strategy in an infinite game from every position in . Outside , all I moves stay outside, while II can choose a move outside. The axiom of choice selects those moves simultaneously. Such a play never reaches , so it is outside the open payoff set. Thus II wins from the complement of , proving determinacy. Interchanging the players and complementing the payoff gives closed determinacy.
We prove the strengthening via Buchi games, including their determinacy argument. On a set of positions with nonempty successor sets, put
For a specified set of marked positions, I's objective is to visit infinitely often. For each , let be the least fixed point obtained by starting and iterating
with unions at limits. Its inner entry ranks let I force a visit to . The operation is monotone. Starting at , iterate with intersections at limits. This descending sequence stabilizes at .
From , the inner ranks force a marked position with a next move still in . I chooses such a move, and the construction repeats. At II-positions all necessary moves stay in the indicated inner attractor, or in at a marked position. Every round takes finitely many moves by decreasing inner ranks. I therefore forces infinitely many marked visits.
For , let be its removal rank: . Since , at I's turn all successors lie outside , and at II's turn there is a successor outside it. II chooses such successors. If also , then ; II can choose outside , or every I move lies outside . Along this strategy removal ranks never increase and strictly decrease after each marked visit. Infinitely many visits would give an infinite ordinal descent, so II wins. This proves Buchi game determinacy on a set-sized arena without any countability restriction.
Now write the original payoff as , with each open. Add a deterministic monitor to the finite position, initially . At each new prefix, if its cylinder is contained in , increment the monitor and mark that step. For a play , the monitor increments infinitely often exactly when . In one direction every increment certifies the next required open set. In the other, after the monitor reaches , openness of supplies a later certifying prefix, so it eventually reaches . The expanded game is a Buchi game; its monitor is determined by the observed finite play, so its winning strategy transfers directly to the original game. Consequently
Complementing and interchanging players also gives determinacy for payoff sets. These arguments work on pruned game subtrees as well, and assigned terminal winners can be incorporated by replacing each terminal position by an absorbing position with the corresponding outcome.
Represent the arena by a pruned set-theoretic tree of legal finite positions. Players I and II alternate; every position has a legal continuation. The usual terminal-position convention can also be handled by adding terminal wins and losses at the initial stage. Give the branches the product topology generated by finite-position cylinders, and let be I's winning open set.
Define the winning-position attractor in an infinite game by transfinite recursion. Start with
At a successor stage retain and add I-positions with at least one child in , and II-positions with every child in . At a limit stage take the union. The increasing sequence stabilizes because the positions form a set: strict increases at arbitrarily many stages would select too many distinct positions. Write for the stable set. The rank of a position in is its first entry stage; any positive such rank is a successor ordinal.
If the initial position belongs to , at every I-position of positive rank choose a child that was present at the preceding stage. Every move by II also leads to a child of smaller rank, by the rule for II-positions. There is no infinite strictly decreasing sequence of ordinals, so every play following this strategy in an infinite game reaches after finitely many moves. Its complete branch then belongs to . Hence this is a winning strategy in an infinite game for I.
If the initial position is outside , every move of I stays outside . At a II-position outside at least one child is outside : otherwise the entry ranks of its set of children have a common ordinal bound, and that position would enter at the next stage. Choose such a child. This gives II a strategy in an infinite game that never enters . A resulting branch cannot belong to , because is an open set and would therefore have a finite prefix whose whole cylinder lies in , namely a member of . Thus II wins. This proves the Gale-Stewart theorem for an arbitrary set-sized arena, in the ordinary metatheory with choice. Countability of the move set was never used.
The restriction on the payoff is essential. Under the axiom of choice, already for binary moves there is an undetermined game. There are strategies for each player, since a strategy is a binary-valued map on a countable set of positions. List I's strategies and II's strategies for . Each strategy is compatible with different plays, obtained by varying all the opponent's binary moves.
At stage , choose a fresh play following and then a different fresh play following , avoiding every previously chosen play. Fewer than plays have been used at that stage, even when is singular, so these choices are possible. Let . No I-strategy wins , because its selected is outside ; no II-strategy wins, because its selected is inside . Future choices avoid all earlier , so they never spoil the first assertion. This is the choice diagonalization of an undetermined game. Consequently determinacy for all payoff sets is incompatible with the axiom of choice. The attractor still makes sense for a nonopen payoff, but an avoiding play may then enter the payoff without ever having a winning finite prefix.