In model theory , the **Ehrenfeucht-Fraisse Game** is a technique of determining whether two models are elementarily equivalent . The recursive definition of the relation $\mathfrak{A}\equiv_n\mathfrak{B}$ on models $\mathfrak{A},\mathfrak{B}$ of the same language $\mathscr{L}$ can be reformulated as a game played by two players - on Wikipedia, these players are called "Spoiler" and "Duplicator". The game is played as follows:

1. Spoiler goes first, choosing a member of $a_1\in A$ or $b_1\in B$.

2. If Spoiler picked an element $a_1\in A$, then Duplicator picks an element $b_1\in B$, whereas if Spoiler picked a member $b_1$ of $B$, then Duplicator picks an $a_1\in A$.

3. Steps $(1)$ and $(2)$ are repeated $n-1$ more times, so that Spoiler and Duplicator together pick elements $a_2,...,a_n$ and $b_2,...,a_n$.

4. At the end of the game, after all of these elements have been chosen, let $\mathfrak{A}'$ be the submodel of $(\mathfrak{A},a_1,...,a_n)$ generated by ${a_1,...,a_n}$, and let $\mathfrak{B}'$ be the submodel of $(\mathfrak{B},b_1,...,b_n)$ generated by ${b_1,...,b_n}$. Spoiler wins if $\mathfrak{A}'\not\cong\mathfrak{B}'$, and Duplicator wins if $\mathfrak{A}'\cong\mathfrak{B}'$.

If Duplicator has a winning strategy, then $\mathfrak{A}\equiv_n\mathfrak{B}$, which follows from the recursive definition of $\equiv_n$. Additionally, if Duplicator has a winning strategy for all values of $n$, then $\mathfrak{A}\equiv \mathfrak{B}$, and the two models are elementarily equivalent. (The converse is not necessarily true unless $\mathfrak{A},\mathfrak{B}$ have no function symbols and only finitely many relation symbols.)

As an example, we can prove the following result using EF games:

Theorem 1.If $A$ and $B$ are sets linearly ordered by $\leq$, and $A\times\mathbb Z$ and $B\times\mathbb Z$ are ordered lexicographically, then

Proof.Consider an Ehrenfeucht-Fraisse game on these two models, and let Duplicator's strategy for a game consisting of $n$ steps be given as follows:

- Duplicator's first choice may be made arbitrarily, regardless of Spoiler's choice.
- On move $1<m$, if Spoiler chooses an element that is exactly $k$ steps to the left or to the right of an element that has already been chosen, with $k < 2^{m-n}$, then let Duplicator choose the element in the other set which is exactly $k$ steps respectively to the left or to the right of the corresponding constant.
- Otherwise, on move $1<m<n$, if Spoiler chooses an element that is at least $2^{m-n}$ steps to the left or to the right of each element that has already been chosen, let Duplicator choose according to the following cases:
- If Spoiler's choice $a_h$ is between $a_i$ and $a_j$, then Duplicator may choose some $b_h$ between $b_i$ and $b_j$ that is at least $2^{m-n-1}$ steps separated from both of them, since $b_i$ and $b_j$ are separated by at least $2^{m-n}$ steps.
- Similarly, if Spoiler's choice $b_h$ is between $b_i$ and $b_j$, then Duplicator may choose some $a_h$ between $a_i$ and $a_j$ that is at least $2^{m-n-1}$ steps separated from both of them.
- If Spoiler's choice $a_h$ is less than the smallest previously chosen element $a_i$, then Duplicator may choose $b_h$ exactly $2^{m-n}$ steps to the left of $b_i$.
- Similarly, if Spoiler's choice $b_h$ is less than the smallest previously chosen element $b_i$, then Duplicator may choose $a_h$ exactly $2^{m-n}$ steps to the left of $a_i$.
Note that it makes sense to talk of "steps" in the ordered sets $A\times \mathbb Z$ and $B\times \mathbb Z$ because they are discrete, meaning that each of their elements has an immediate successor and predecessor. For clarity, the phrase "$a_i < a_j$ have $k$ steps between them" means that there are exactly $k-1$ elements that are greater than $a_i$ and less than $a_j$.

We may show inductively that, after $m$ moves, for any $a_i < a_j$ with fewer than $2^{m-n}$ steps between them, the elements $b_i < b_j$ have exactly the same number of steps between them. Similarly, if $b_i < b_j$ have fewer than $2^{m-n}$ steps between them, then $a_i < a_j$ have exactly the same number of steps between them. This ensures that it is always possible for Duplicator to choose an element of the other set that has the same position as Spoiler's choice relative to the previous choices, and it maintains enough "wiggle room" to last until the end of the game. $\blacksquare$

We can use a similar strategy to show that, for instance, as in the exercise listed here .