[proofplan] We replace the closed payoff set $A$ by its tree $T$ of finite approximations. Positions from which player I cannot force the play to remain inside $T$ are assigned ordinal ranks by recursion, with the recursion depending on whose turn it is. If the empty position is ranked, player II follows a strategy that strictly decreases the rank whenever she moves, forcing the play eventually to leave $T$. If the empty position is unranked, player I always chooses an unranked successor; this produces an infinite branch through $T$, and closedness gives that the resulting play belongs to $A$. [/proofplan]

[step:Encode the closed payoff set by its tree of finite approximations]Let $\mathbb{N}^{<\mathbb{N}}$ denote the set of finite sequences of natural numbers. For $s \in \mathbb{N}^{<\mathbb{N}}$, let $|s| \in \mathbb{N} \cup \{0\}$ denote its length, and for $n \in \mathbb{N}$ let $s^\frown n \in \mathbb{N}^{<\mathbb{N}}$ denote the sequence obtained by appending $n$ to $s$. Define the tree of finite approximations to $A$ by \begin{align*} T := \{s \in \mathbb{N}^{<\mathbb{N}} : \text{there exists } x \in A \text{ such that } x_i = s_i \text{ for every } 0 \le i < |s|\}. \end{align*} Thus $T$ is downward closed: if $s \in T$ and $t$ is an initial segment of $s$, then $t \in T$. Let $[T] \subseteq \mathbb{N}^{\mathbb{N}}$ denote the set of infinite branches through $T$: \begin{align*} [T] := \{x \in \mathbb{N}^{\mathbb{N}} : (x_0,\dots,x_{m-1}) \in T \text{ for every } m \in \mathbb{N} \cup \{0\}\}. \end{align*} We claim that $[T] = A$. The inclusion $A \subseteq [T]$ follows directly from the definition of $T$. Conversely, let $x \in [T]$. For each $m \in \mathbb{N}$, the basic cylinder \begin{align*} N_m(x) := \{y \in \mathbb{N}^{\mathbb{N}} : y_i = x_i \text{ for every } 0 \le i < m\} \end{align*} meets $A$, because $(x_0,\dots,x_{m-1}) \in T$. Hence every basic neighbourhood of $x$ meets $A$, so $x \in \overline{A}$. Since $A$ is closed, $\overline{A} = A$, and therefore $x \in A$. This proves $[T] = A$.[/step]

[guided]The point of passing from $A$ to $T$ is that membership in $T$ records finite compatibility with the [closed set](/page/Closed%20Set) $A$. A finite position $s$ belongs to $T$ exactly when the current partial play can still be extended to some element of $A$. Formally, $\mathbb{N}^{<\mathbb{N}}$ is the set of all finite sequences of natural numbers. If $s \in \mathbb{N}^{<\mathbb{N}}$, then $|s|$ is its length, and $s^\frown n$ is the one-step extension obtained by appending $n \in \mathbb{N}$. We define \begin{align*} T := \{s \in \mathbb{N}^{<\mathbb{N}} : \text{there exists } x \in A \text{ such that } x_i = s_i \text{ for every } 0 \le i < |s|\}. \end{align*} This is a tree because initial segments preserve extendability: if $s$ is extended by some $x \in A$, then every initial segment of $s$ is also extended by that same $x$. The infinite branches through $T$ are \begin{align*} [T] := \{x \in \mathbb{N}^{\mathbb{N}} : (x_0,\dots,x_{m-1}) \in T \text{ for every } m \in \mathbb{N} \cup \{0\}\}. \end{align*} We prove that $[T] = A$. If $x \in A$, then every finite initial segment of $x$ is extended by $x$ itself, so every initial segment lies in $T$; hence $x \in [T]$. For the reverse inclusion, take $x \in [T]$. For each $m \in \mathbb{N}$, define the basic cylinder neighbourhood of $x$ determined by its first $m$ coordinates: \begin{align*} N_m(x) := \{y \in \mathbb{N}^{\mathbb{N}} : y_i = x_i \text{ for every } 0 \le i < m\}. \end{align*} Because $x \in [T]$, the finite sequence $(x_0,\dots,x_{m-1})$ lies in $T$. By the definition of $T$, there is some element of $A$ extending this finite sequence, so $N_m(x) \cap A \ne \varnothing$. The cylinders $N_m(x)$ form a neighbourhood basis at $x$ in the [product topology](/page/Product%20Topology) on $\mathbb{N}^{\mathbb{N}}$, so every neighbourhood of $x$ meets $A$. Therefore $x \in \overline{A}$. Since $A$ is closed, $\overline{A} = A$, and $x \in A$. Thus $[T] = A$.[/guided]

[step:Assign ranks to positions from which player I cannot force staying inside the tree] Let $\mathrm{Ord}$ denote the class of ordinals. We define a class $R \subseteq \mathbb{N}^{<\mathbb{N}}$ of ranked positions, a rank map $\rho: R \to \mathrm{Ord}$, and, for ranked odd positions in $T$, a selected move function $m$ by transfinite recursion on ordinal stages. At stage $0$, rank every position outside the tree: \begin{align*} R_0 := \mathbb{N}^{<\mathbb{N}} \setminus T. \end{align*} For each $s \in R_0$, define $\rho(s) := 0$. Suppose $\alpha$ is an ordinal and the sets $R_\beta$ and the values of $\rho$ have been defined for all $\beta < \alpha$. Let \begin{align*} R_{<\alpha} := \bigcup_{\beta < \alpha} R_\beta. \end{align*} At stage $\alpha$, add exactly the following previously unranked positions in $T$. If $|s|$ is even, add $s$ when every one-step extension $s^\frown n$ already lies in $R_{<\alpha}$. For such an $s$, define \begin{align*} \rho(s) := \sup_{n \in \mathbb{N}}(\rho(s^\frown n)+1). \end{align*} This is an ordinal because it is the supremum of a set of ordinals indexed by $\mathbb{N}$. If $|s|$ is odd, add $s$ when at least one one-step extension $s^\frown n$ already lies in $R_{<\alpha}$. For such an $s$, let $m(s)$ be the least natural number $n$ such that $s^\frown n \in R_{<\alpha}$, and define \begin{align*} \rho(s) := \rho(s^\frown m(s))+1. \end{align*} Finally set \begin{align*} R := \bigcup_{\alpha \in \mathrm{Ord}} R_\alpha. \end{align*} Since $\mathbb{N}^{<\mathbb{N}}$ is a set, this stage construction stabilizes after at most $|\mathbb{N}^{<\mathbb{N}}|^+$ many stages: if a new position were added at cofinally many later stages, those stages would inject into the set $\mathbb{N}^{<\mathbb{N}}$. Hence the displayed recursion defines a well-determined class of ranked positions and an ordinal-valued rank map on it. Equivalently, $R$ is the least class satisfying the even and odd closure clauses above, with $\rho(s)$ assigned at the first stage at which $s$ enters. By construction, whenever $s \in R \cap T$ and $|s|$ is odd, the extension $s^\frown m(s)$ is ranked and satisfies \begin{align*} \rho(s^\frown m(s)) < \rho(s). \end{align*} Whenever $s \in R \cap T$ and $|s|$ is even, every extension $s^\frown n$ is ranked and satisfies \begin{align*} \rho(s^\frown n) < \rho(s). \end{align*} [/step]

[step:Use a ranked initial position to build a winning strategy for player II] Assume first that the empty sequence $\varnothing$ belongs to $R$. We define a strategy $\tau$ for player II as follows. At a finite position $s \in \mathbb{N}^{<\mathbb{N}}$ with $|s|$ odd, if $s \in R \cap T$, set \begin{align*} \tau(s) := m(s). \end{align*} If $s \notin R \cap T$, define $\tau(s)$ arbitrarily, for instance $\tau(s) := 0$. We prove that $\tau$ is winning for player II. Let $x \in \mathbb{N}^{\mathbb{N}}$ be any play compatible with $\tau$, and for each $k \in \mathbb{N} \cup \{0\}$ define the finite position \begin{align*} s_k := (x_0,\dots,x_{k-1}). \end{align*} Suppose, toward a contradiction, that $s_k \in T$ for every $k$. Since $s_0 = \varnothing \in R$, induction on $k$ shows that $s_k \in R$ for every $k$. Indeed, if $s_k \in R \cap T$ and $k$ is even, then player I chooses some $x_k \in \mathbb{N}$, and the even-rank clause gives $s_{k+1} = s_k^\frown x_k \in R$. If $s_k \in R \cap T$ and $k$ is odd, then compatibility with $\tau$ gives $x_k = m(s_k)$, so $s_{k+1} = s_k^\frown m(s_k) \in R$. Moreover, in both cases the ranks strictly decrease: \begin{align*} \rho(s_{k+1}) < \rho(s_k). \end{align*} Thus the sequence \begin{align*} \rho(s_0), \rho(s_1), \rho(s_2), \dots \end{align*} is an infinite strictly descending sequence of ordinals, impossible by well-foundedness of the ordinals. Hence some $s_k$ is not in $T$. Then $x \notin [T]$, and since $[T] = A$, we have $x \notin A$. Therefore player II wins every play compatible with $\tau$, so $\tau$ is a winning strategy. [/step]

[step:Use an unranked initial position to build a winning strategy for player I]Assume now that the empty sequence $\varnothing$ does not belong to $R$. We define a strategy $\sigma$ for player I. At a finite position $s \in \mathbb{N}^{<\mathbb{N}}$ with $|s|$ even, if $s \notin R$, then the even-rank clause implies that not every extension $s^\frown n$ is ranked. Choose $n(s) \in \mathbb{N}$ such that \begin{align*} s^\frown n(s) \notin R, \end{align*} and set \begin{align*} \sigma(s) := n(s). \end{align*} If $s \in R$, define $\sigma(s)$ arbitrarily, for instance $\sigma(s) := 0$. We prove that $\sigma$ is winning for player I. Let $x \in \mathbb{N}^{\mathbb{N}}$ be any play compatible with $\sigma$, and define \begin{align*} s_k := (x_0,\dots,x_{k-1}) \end{align*} for each $k \in \mathbb{N} \cup \{0\}$. We show by induction on $k$ that $s_k \notin R$ for every $k$. The base case is the present assumption $s_0 = \varnothing \notin R$. If $s_k \notin R$ and $k$ is even, then player I follows $\sigma$, so \begin{align*} s_{k+1} = s_k^\frown n(s_k) \notin R. \end{align*} If $s_k \notin R$ and $k$ is odd, then player II chooses some $x_k \in \mathbb{N}$. If $s_{k+1} = s_k^\frown x_k$ were in $R$, then the odd-rank clause would imply $s_k \in R$, contradicting the induction hypothesis. Hence $s_{k+1} \notin R$. Because every position outside $T$ belongs to $R$, the fact that $s_k \notin R$ implies $s_k \in T$ for every $k$. Therefore $x \in [T]$. Since $[T] = A$, we have $x \in A$. Hence player I wins every play compatible with $\sigma$, so $\sigma$ is a winning strategy.[/step]

[guided]Here the unranked case is the positive case for player I. Intuitively, a position is unranked precisely when player I can keep the play inside the tree $T$ no matter how player II responds. Assume $\varnothing \notin R$. We define player I's strategy $\sigma$ only at positions of even length, because those are exactly the positions where player I moves. Let $s \in \mathbb{N}^{<\mathbb{N}}$ with $|s|$ even. If $s \notin R$, then the even-rank clause says that $s$ would be ranked if all extensions $s^\frown n$ were ranked. Since $s$ is not ranked, at least one extension is not ranked. Choose such an extension index and call it $n(s)$: \begin{align*} s^\frown n(s) \notin R. \end{align*} Define \begin{align*} \sigma(s) := n(s). \end{align*} If $s \in R$, the value of $\sigma(s)$ is irrelevant for the argument, so we may set $\sigma(s) := 0$. Now let $x \in \mathbb{N}^{\mathbb{N}}$ be any play compatible with $\sigma$. For each $k \in \mathbb{N} \cup \{0\}$, define the position after $k$ moves by \begin{align*} s_k := (x_0,\dots,x_{k-1}). \end{align*} We prove that every $s_k$ is unranked. The base case is $s_0 = \varnothing \notin R$. Suppose $s_k \notin R$. If $k$ is even, then player I moves from $s_k$ and follows $\sigma$. Therefore \begin{align*} s_{k+1} = s_k^\frown \sigma(s_k) = s_k^\frown n(s_k). \end{align*} By the definition of $n(s_k)$, this extension is unranked: \begin{align*} s_{k+1} \notin R. \end{align*} If $k$ is odd, then player II moves. Player II may choose any natural number $x_k$. We must show that the resulting extension remains unranked. Suppose instead that \begin{align*} s_{k+1} = s_k^\frown x_k \in R. \end{align*} Since $|s_k|$ is odd, the odd-rank clause says that a position of odd length is ranked as soon as it has at least one ranked extension. The ranked extension $s_{k+1}$ would therefore force $s_k \in R$, contradicting the induction hypothesis $s_k \notin R$. Hence $s_{k+1} \notin R$. Thus $s_k \notin R$ for every $k$. Since every position outside $T$ was assigned rank $0$, no unranked position can lie outside $T$. Therefore \begin{align*} s_k \in T \end{align*} for every $k$. This means exactly that the resulting infinite sequence $x$ is a branch through $T$, so $x \in [T]$. From the first step we proved $[T] = A$, using closedness of $A$. Hence $x \in A$, so player I wins this play. Since the play was arbitrary among those compatible with $\sigma$, $\sigma$ is a winning strategy for player I.[/guided]

[step:Conclude that one of the two players has a winning strategy] Exactly one of the alternatives $\varnothing \in R$ and $\varnothing \notin R$ holds. If $\varnothing \in R$, the strategy $\tau$ constructed above is winning for player II. If $\varnothing \notin R$, the strategy $\sigma$ constructed above is winning for player I. Therefore the Gale-Stewart game $G(A)$ is determined. [/step]