The Banach–Mazur category game on sequence spaces and the real line

Work in ZF. Let X be Baire space (Baire sequence space ${\mathbb{N}}^{\mathbb{N}}$ and its cylinder topology), Cantor space (Cantor sequence space) or $\mathbb{R}$, and let $A\subseteq X$. In the category game I and II alternate basic-open moves $V_0,V_1,\dots$, I first, with full-history strategies as in Gale–Stewart games and strategies.

In either sequence space moves are cylinders determined by finite words: the first word is nonempty and each subsequent word properly extends its predecessor. In $\mathbb{R}$ moves are nonempty bounded rational open intervals satisfying $\overline{V_{n+1}}\subseteq V_n$ and $\mathrm{length}(V_n)<1\mathrm{/}(n+1)$. A relative game on a fixed nonempty basic open V requires $V_0\subseteq V$ for cylinders, or $\overline{V_0}\subseteq V$ for intervals. All later rules remain the same.

Each legal full play determines one point. In sequence spaces it is the union of the strictly extending words. For intervals apply A nested sequence of nonempty closed bounded intervals has nonempty intersection, and the intersection is a single point exactly when the lengths tend to $0$ to their nonempty bounded nested closures, whose lengths tend to zero: the intersection is a singleton x. Because the next closure lies inside each V_n, this x belongs to every V_n. I wins precisely when x belongs to A.

For natural-number coding, code a finite word by its length and iterated pairing $⟨i,j⟩=(i+j)(i+j+1)\mathrm{/}2+j$; the intervals are coded by pairs in a fixed enumeration of the rationals from $\mathbb{Q}$ is countably infinite. Allow unused numbers as illegal codes. In sequence spaces one can always append a digit. In the real case The rationals embed densely in the reals supplies a rational interval with closure inside any prescribed nonempty open and as small as the next bound requires. Thus legal continuation sets are nonempty subsets of $\mathbb{N}$ and have least codes, without choice.

In the full coded natural-number game the first illegal move loses, regardless of later moves. More formally, I's payoff contains the plays with first illegal move by II, together with all wholly legal plays whose resulting point is in A. This is a subset of ${\mathbb{N}}^{\mathbb{N}}$. A winning coded strategy, restricted to its legal consistent histories, cannot make the first illegal move: a legal opponent continuation exists by least codes and would defeat it. Complete its values at inconsistent legal histories by least legal defaults. This gives a legal winning strategy. Neither determinacy nor AC is assumed by the definition.