I'm studying from Kechris' "Classical Descriptive Set Theory" and I'm trying to solve exercise 20.3, which asks to show that the Gale-Stewart theorem is equivalent to the axiom of choice AC in ZF. I'm of course interested only in the implication Gale Thm $\Rightarrow AC$. I recall the theorem:
Let $T$ be a non-empty pruned tree on a set $U$. Let $W\subseteq[T]$ be open or closed in $[T]$. Then $G(T,W)$ is determined.
I recall also a formal statement of AC :
$\forall X[\emptyset \not\in X \Longrightarrow \exists f:X \rightarrow \bigcup X \quad \forall A \in X (f(A) \in A)]$
I think I solved it, but I'm now sure and I doubt it was the smartest way to do it. So, following the previous notation, what I did is taking the set $U = X \cup \bigcup X$ and defining a tree $T \subseteq U^{<\mathbb{N}}$ with the condition:
- $(a_0) \in T \iff a_0 \neq \emptyset$
- $(a_0,a_1) \in T \iff a_1 \in a_0$
- $(a_0,a_1,\dots,a_n) \in T \iff a_n = a_1$
and then taking $W = \emptyset$. The hypotheses of Gale-Stewart thm are satisfied, so we have a winning strategy $\sigma: T \rightarrow U$ for player II. In fact, player I cannot have a winning strategy. Let's suppose otherwise, let's call $\sigma_1$ a winning strategy for I, then we'd have that, given a constant strategy for II $\sigma_2: T \mapsto c \in \sigma_1(\emptyset)$, the play $\sigma_1 \otimes \sigma_2 \in \emptyset$, which is absurd.
Then a choice function would be: $$A \in X, f(A) = \sigma((A))$$ What do you think?
EDIT: isn't Dependent Choice necessary to extract a play given two strategies like I did when proving that I cannot have a winning strategy? EDIT 2: now it should not need DC
You need to argue that the winning strategy cannot be for Player I. This much is easy, of course, but needs to be mentioned.
Other than this, the proof is fine.
Response to the Edit. The proof is better, yes. And $\sf DC$ is not needed here, since your tree has height $3$.
This proof is almost the same as the proof that $p\Vdash\exists x\varphi(x)$ implies $\exists\dot x\, p\Vdash\varphi(\dot x)$, in the context of forcing.