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?
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.