What does the Ehrenfeucht-Fraïssé game on structures with infinitely many relations tell us? EF-games are typically presented for structures with finitely many relations, and if you want to extend them to structures with functions, you can relationalize the functions. This seems to be to avoid having infinitely many inequivalent atomic formulas, so as to be able to use the Fraïssé-Hintikka theorem (see https://ncatlab.org/nlab/show/Ehrenfeucht-Fra%C3%AFss%C3%A9+games )
If you allow infinitely many relations in your language, it still makes sense to talk about EF-games, with the same condition for duplicator losing: there being some atomic formula among the matched elements differing between the structures.
My question is: are there characterizations of when two structures with infinitely many relations are distinguishable by these sorts of EF-games?
Playing around with $\mathbb{N}$ and $\mathbb{N}$-disjoint-union-$\mathbb{Z}$ equipped with a constant 0 and relationalized versions of all finite iterates of the successor operation ($S^0, S^1, \ldots$), it seems like Spoiler has a winning strategy that exploits the fact that in the first structure, $\forall x: \bigvee_{n \in \mathbb{N}} x = S^n(0)$. However, these structures are elementarily equivalent to each other (since $(\mathbb{N},S)$ and $(\mathbb{N} + \mathbb{Z},S)$ are elementarily equivalent).
My guess then is that two structures with infinitely many relations are distinguishable by these extended EF-games in n turns iff there is a formula with quantifier depth n distinguishing them in first-order-logic extended by infinite conjunction and infinite disjunction of atomic formulas.
 A: Duplicator wins in E-F game for structures $A,B$ in position given by tuples $\vec{a}\in A$, $\vec{b}\in B$ and $2n$ turns left $\iff$ the same $L_{\infty,\omega}$ formulas of the quantifier rank $n$ hold on $\vec{a}$ and $\vec{b}$.
Here formula is of the quantifier rank $\le \alpha$ iff it is an infinitary Boolean combination of atomic formulas and formulas of the form $\exists x\;\varphi$, where $\varphi$ is of the quantifier rank $<\alpha$.
$\Rightarrow$ is proved by straightforward induction on $n$.
To prove $\Leftarrow$ note that the Lindenbaum-Tarski algebra $\mathbf{Q}^m_\alpha$ of $L_{\infty,\omega}$ formulas (of our fixed signature) of the quantifier rank $\le \alpha$ depending on variables $x_1,\ldots,x_m$ is a complete atomic Boolean algebra (L-T algebra is the Boolean algebra of equivalence classes of formulas under provable equivalence). Let the $\alpha$-type of an $m$-tuple $\vec{a}\in A$ be the unique $\mathbf{Q}_\alpha^m$ atom that (as a formula of $m$-variables) holds on $\vec{a}$. Now by straightforward induction on $n$ we prove the implication:
$\vec{a}\in A$ and $\vec{b}\in B$ have the same $n$-types $\Rightarrow$ Duplicator wins in E-F game for structures $A,B$ in position given by $m$-tuples $\vec{a}\in A$, $\vec{b}\in B$ with $2n$ turns left.
P.S. Note that in the case of finite signatures each atom in $\mathbf{Q}_n^m$ is represented by some finite formula and hence we recover the result about the equivalent characterization of Duplicator winning a $2n$-turns long E-F games as equivalence of the corresponding structures on sentences of the quantifier depth $n$.
