Gale–Stewart games and strategies

Let $E$ be a nonempty set, $T\subseteq E^{<\omega }$ a nonempty pruned tree (Trees and their bodies), and $A\subseteq [T]$. In $G(A;T)$, player I moves at even-length positions and player II at odd-length positions. A legal move at $s$ is $e\in E$ such that $s^{⌢}e\in T$. A full play is a branch $x\in [T]$. Player I wins it when $x\in A$; otherwise player II wins.

A strategy for player $P$ assigns a legal move to every position at which $P$ moves, including positions inconsistent with its earlier prescriptions. A branch $x$ is consistent with $\sigma$ when $x(n)=\sigma (x\upharpoonright n)$ at each coordinate of that player's parity. The strategy is winning if every consistent branch is won by that player. The game is determined if at least one player has a winning strategy. These are definitions in ZF; a legal move exists individually at each position, but no simultaneous strategy-existence assertion for arbitrary $E$ is implicit.

For $s\in T$ put $[T{]}_s=\{x\in [T]:s\subseteq x\}$. These cylinders, including $[T{]}_{\mathrm{\varnothing }}=[T]$, form a basis: two cylinders intersect in the longer one when the words are comparable, and are disjoint otherwise. Unions of cylinders therefore satisfy the topology axioms in Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison. Moreover

$[T]\setminus [T{]}_s=\bigcup \{[T{]}_t:t\in T,\mathrm{\mid }t\mathrm{\mid }=\mathrm{\mid }s\mathrm{\mid },t\mathrm{\ne }s\},$

so cylinders are clopen. Empty cylinders are permitted. Neither this topology nor the winning-strategy definition asserts nonemptiness of $[T]$ in ZF for arbitrary $E$.