Solution (source code)

= Solution

Represent the arena by a pruned <set-theoretic tree> $T$ 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 $A$ be I's winning <open set>.

Define the <winning-position attractor in an infinite game> by <transfinite recursion>. Start with
$$
W_0=\{s\in T:[s]\subseteq A\}.
$$
At a successor stage retain $W_\alpha$ and add I-positions with at least one child in $W_\alpha$, and II-positions with every child in $W_\alpha$. 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 $W$ for the stable set. The rank of a position in $W$ is its first entry stage; any positive such rank is a successor <ordinal>.

If the initial position belongs to $W$, 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 $W_0$ after finitely many moves. Its complete branch then belongs to $A$. Hence this is a <winning strategy in an infinite game> for I.

If the initial position is outside $W$, every move of I stays outside $W$. At a II-position outside $W$ at least one child is outside $W$: 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 $W_0$. A resulting branch cannot belong to $A$, because $A$ is an <open set> and would therefore have a finite prefix whose whole cylinder lies in $A$, namely a member of $W_0$. Thus II wins. This proves \b[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 $\mathfrak c=2^{\aleph_0}$ strategies for each player, since a strategy is a binary-valued map on a countable set of positions. List I's strategies $\sigma_\alpha$ and II's strategies $\tau_\alpha$ for $\alpha<\mathfrak c$. Each strategy is compatible with $\mathfrak c$ different plays, obtained by varying all the opponent's binary moves.

At stage $\alpha$, choose a fresh play $x_\alpha$ following $\sigma_\alpha$ and then a different fresh play $y_\alpha$ following $\tau_\alpha$, avoiding every previously chosen play. Fewer than $\mathfrak c$ plays have been used at that stage, even when $\mathfrak c$ is singular, so these choices are possible. Let $B=\{y_\alpha:\alpha<\mathfrak c\}$. No I-strategy wins $B$, because its selected $x_\alpha$ is outside $B$; no II-strategy wins, because its selected $y_\alpha$ is inside $B$. Future choices avoid all earlier $x_\alpha$, so they never spoil the first assertion. This is the <choice diagonalization of an undetermined game>. Consequently \b[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.