Can the Axiom of Determinacy be stated in 1st order logic? Statement of AD: Fix a subset $A \subseteq \mathbb{N}^\mathbb{N}$. Define the two-player game $G_A$ as follows. On the first turn, Player 1 chooses some $n_0 \in \mathbb{N}$, then Player 2 chooses some $m_0 \in \mathbb{N}$. On the second turn, Player 1 chooses some $n_1 \in \mathbb{N}$, then Player 2 chooses some $m_1\in \mathbb{N}$. This carries on forever, and in the end a sequence $n_0m_0n_1m_1... \in \mathbb{N}^\mathbb{N}$ has been constructed. Player 1 wins if this sequence is an element of $A$, and Player 2 wins otherwise. AD states that for any $A$, one of the players will always have a winning strategy to the game $G_A$.
I was thinking of how to translate this into 1st order logic. At first I thought
"Player 1 has a winning strategy" = $\exists n_0n_1...\in \mathbb{N}^\mathbb{N}$ such that $\forall m_0m_1...\in \mathbb{N}^\mathbb{N}, n_0m_0n_1m_1... \in A$,
but I realize this translation actually does not work. Is there a way to put this into 1st order logic without ending up with an infinitely long sentence?
 A: The basic idea is that the play of the game needs to be described in a recursive way  This of course requires a bit of set theory to be able to do, but not much.
Firstly, note that a winning strategy is a function $\sigma$ from finite sequences of $\mathbb{N}$ to $\mathbb{N}$ itself, meaning $\sigma:\mathbb{N}^{<\mathbb{N}}\rightarrow\mathbb{N}$.  What this means is that if player II plays $m=\langle m_i:i\in\mathbb{N}\rangle$ then the play of the game should be given by $m$ and $\sigma$ as follows:
$$\begin{matrix}\text{I:} & \sigma(\emptyset) && \sigma(\langle m_0\rangle) && \sigma(\langle m_0, m_1\rangle) && \sigma(\langle m_0,m_1,m_2\rangle) && \cdots
\\
\text{II:}&&m_0&&m_1&&m_2&&\cdots\end{matrix}$$
So the play of the game is the real $\langle \sigma(\emptyset),m_0,\sigma(\langle m_0\rangle),m_1,\sigma(\langle m_0,m_1\rangle),\cdots\rangle$.  In first order logic, we can then say the play of the game given by $\sigma$ and $m$ is $x\in\mathbb{N}^{\mathbb{N}}$ defined by the formula $\mathrm{Outcome}_\mathrm{I}(\sigma,m,x)$ below
$$\forall n\in\mathbb{N}\ \left(\begin{matrix}\text{if }n=2k+1\text{ is odd, then }x(n)=m(k)\\ \text{if }n=2k\text{ is even, then }x(n)=\sigma(m\upharpoonright  k)\end{matrix}\right)\text{.}$$
We can similarly define $\mathrm{Outcome}_{\mathrm{II}}(\sigma,m,x)$ when II is using the strategy $\sigma$ and I plays $m$ (just swap the even and odd cases above).  Anyway, player I having a winning strategy in $G_A$ can now be stated by
$$\exists \sigma\in\mathbb{N}^{(\mathbb{N}^{<\mathbb{N}})}\ \forall m\in\mathbb{N}^{\mathbb{N}}\ \exists x\in\mathbb{N}^\mathbb{N}\ (\mathrm{Outcome}_{\mathrm{I}}(\sigma,m,x)\text{ and }x\in A)$$
and so $\mathsf{AD}$ can be stated by
$$\forall A\in\mathcal{P}(\mathbb{N})\ \exists\sigma\in\mathbb{N}^{(\mathbb{N}^{<\mathbb{N}})}\ \begin{pmatrix} \forall m\in\mathbb{N}^{\mathbb{N}}\ \exists x\in\mathbb{N}^\mathbb{N}\ (\mathrm{Outcome}_{\mathrm{I}}(\sigma,m,x)\text{ and }x\in A)\\
\text{or } \forall m\in\mathbb{N}^{\mathbb{N}}\ \exists x\in\mathbb{N}^\mathbb{N}\ (\mathrm{Outcome}_{\mathrm{II}}(\sigma,m,x)\text{ and }x\not\in A)\end{pmatrix}\text{.}$$
Of course, all of this requires also a definition of $\mathbb{N}$ which requires a bit of set theory as well, but given its use in your question, I assume you're okay with that.

On a related note to your infinitely long formulas, there is an interpretation of the axiom of determinacy along these lines: player I having a winning strategy in the game $G_A$ is the same as saying
$$\exists s_1\ \forall m_1\ \exists s_2\ \forall m_2\ \cdots\ (\langle s_1, m_1,\cdots\rangle\in A)\text{.}$$
Player II having a winning strategy is the same as saying
$$\forall s_1\ \exists m_1\ \forall s_2\ \exists m_2\ \cdots\ (\langle s_1, m_1,\cdots\rangle\not\in A)\text{.}$$
So the usual first-order logic rule of $\neg\forall\neg$ being $\exists$ and vice versa applied "infinitely many times" motivates the statement
$$ \neg \exists s_1\ \forall m_1\ \exists s_2\ \forall m_2\ \cdots\ (\langle s_1, m_1,\cdots\rangle\in A) \quad \text{iff}\quad \forall s_1\ \exists m_1\ \forall s_2\ \exists m_2\ \cdots\ (\langle s_1, m_1,\cdots\rangle\not\in A)\text{,}$$
and this statement is equivalent to the axiom of determinacy.
