Ehrenfeucht–Fraïssé games and elementary equivalence: is it possible to remove the relations-only constraint? How do you generalize Ehrenfeucht–Fraïssé games beyond relational theories, assuming that the signature is finite?
The Wikipedia definition of an Ehrenfeucht–Fraïssé game restricts attention to relational signatures.
In David Marker's A Shorter Model Theory, some additional constraints are given. Namely, given a finite relational language $L$ and models $M$ and $N$, $M$ is elementarily equivalent to $N$ if and only if the $n$-move EF game is a win for Duplicator for all $n$. (Paraphrased from Theorem 2.4.6 on page 53).
I'm curious if there's a generalization of this result that drops the "relations only" constraint, but keeps the finite language constraint.
For each turn pair $t_i$, Spoiler picks an element of $A$ or an element of $B$ and then  Duplicator picks an element of the other structure.
The turn pairs can be thought of as producing $A'$ and $B'$, where the domain of each is limited to items picked during the game. If the shared signature of $A$ and $B$ has no function or relation symbols, restricting the domains of $A$ and $B$ like this works, since there's no danger of $A'$ or $B'$ failing to be closed under the interpretation of constant or relation symbols.

One strategy that seems somewhat straightforward is paraphrasing away constants and variables in order to produce a new signature and a new theory.
Replace each constant $c$ with a unary predicate $P(x)$ and add the sentence $\exists! x \mathop. P(x)$ to the theory.
Replace each $n$-ary function $f$ with an $(n+1)$-ary predicate $P(x_1, \cdots, x_n)$ and all the sentence $\forall x_1 \cdots \forall x_n \mathop. \exists! x_{n+1} \mathop. P(x_1, \cdots, x_n, x_{n+1})$.
However, I'm not sure that this strategy preserves the intended victory conditions for the Ehrenfeucht–Fraïssé game.
 A: Yes and no.
Yes - it is possible to save the EF game theorem
No - it doesn't immediately works and requires some modifications

First let's redefine the game: instead of looking on the 2 sequences $a=(a_0,a_1,...,a_{n-1})$ and $b=(b_0,b_1,...,b_{n-1})$, we will look at the closure of those 2 sequences, and similarly instead of looking for (partial) embedding $h:a\to b$, we will look at a (partial) embedding between the 2 substructures such that $h(a_i)=b_i$

Let $N=(|N|, s, 0)$ be the standard model of arithmetic, and let $M=(|M|, S, 0)$ be such that $N\prec M$, $|N|\subset |M|$, $0^N=0^M$(we will just use $0$) and $s(x)=S(x)$ for all $x$ in $|N|$.
Now let $h:N\to M$ be embedding, if $c\in|M|$ is non standard, then $c\notin f''|N|$(*)

Claim: $N\equiv M$ but in the generalized version of EF game, the spoiler always has winning strategy, regardless of the length of the game

Proof: let the spoiler choose a non standard element of $|M|$, then the duplicator must choose an element from $|N|$, let the rest of the game continue (it doesn't matter what each of the player choose from now on)
Let $A$, $B$ be the closure of the sequences of element the player chose from $N$ and $M$ respectively, notice that $A=N$ (as every element of $|N|$ can be constructed using a finite formula with 0 parameters using only $0$ and $s$)
If the duplicator won, then there is a partial embedding $h:N\to B$ such that $h(x_0)$ is non standard, but by (*) we can't have a non standard element in the range of $h$.

Before explaining how to save the EF game theorem, let's notice what went wrong.
In the usual version, if the duplicator wins on $n$ steps game, then (and only then) the 2 structure are elementary equivalent for statements with $n$ quantifiers.
When we add a function symbol, to represent it as a relation symbol we are adding quantifiers.
More specifically, if $M$ is a model with language that contains function symbols, and $M'$ is the model $M$ after replacing each function symbol with relations symbol+the axioms of the relation symbols being functional, then if $\phi$ is an $M-$formula, then the equivalent $M'-$formual, $\phi'$ will have more quantifiers (usually).
So we can save our theorem now:
Instead of counting quantifiers, count $m(\phi)$ where, $m$ on a variable is $0$, $m$ on a constant is $1$, $m(\lnot\phi)=m(\phi), m(\phi\lor \psi)=\max(\phi,\psi),m(\exists x\phi)=m(\phi)+1$, and lastly, if $c_0$ to $c_{n-1}$ are terms then:
$$m(f(c_0,...,c_{n-1}))=1+m(c_0)+...+m(c_1), m(c_0=c_1)=\max(m(c_0)+m(c_1)-1, 0)$$.
This function $m$ adds to our usual counting the "price of unnesting" each formula

I believe the modified version of the game is due to Hodges
