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.
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|$(*)
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