[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$.
[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]
[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.
[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]
[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]