Solution (source code)

= Solution

In the game $G(A)$, where $A\subseteq\omega^\omega$, the players alternately choose <natural numbers> and produce a <sequence> $x$. Player I wins exactly when $x\in A$. 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
$$
\boxed{\mathsf{AD}:\quad \text{every }G(A),\ A\subseteq\omega^\omega,\ \text{is determined}.}
$$

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 $\omega^\omega$ its <product topology> of discrete move coordinates. If $A$ is open, let $W_0$ be the finite positions whose entire cylinder of extensions lies in $A$. 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 $W_0$: an infinite strictly descending <sequence> of <ordinals> cannot exist. The resulting play is in $A$, 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 $W_0$ forever. If its outcome were in the <open set> $A$, some finite prefix would have its entire cylinder in $A$, 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> $\mathfrak c=2^{\aleph_0}$, since a <strategy> is a <function> on a countably infinite <set> of positions. Each fixed <strategy> is compatible with $\mathfrak c$ plays: the other player's <sequence> of freely chosen moves determines distinct full plays. Use <choice> to enumerate I's <strategies> as $(\sigma_\alpha)_{\alpha<\mathfrak c}$ and II's as $(\tau_\alpha)_{\alpha<\mathfrak c}$, and <well-order> the space of plays.

Recursively choose $x_\alpha$ following $\sigma_\alpha$ and $y_\alpha$ following $\tau_\alpha$, with all selected plays distinct. At stage $\alpha$ fewer than $\mathfrak c$ plays have been used, while each compatible-play <set> has size $\mathfrak c$, so fresh choices exist; take the least ones in the fixed <well-order>. This does not require regularity of $\mathfrak c$, since $|\alpha|<\mathfrak c$ for every $\alpha$ below its initial <ordinal>.

Put $A=\{y_\alpha:\alpha<\mathfrak c\}$. Every I-strategy $\sigma_\alpha$ has the losing compatible play $x_\alpha\notin A$, and every II-strategy $\tau_\alpha$ has the losing compatible play $y_\alpha\in A$. Therefore neither player has a <winning strategy>. This <choice diagonalization of an undetermined game> proves
$$
\boxed{\mathsf{ZF}\vdash\mathsf{AC}\Rightarrow\neg\mathsf{AD}.}
$$
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>.