Let $\mathfrak{A} = \langle A, \dots \rangle$ and $\mathfrak{B} = \langle B, \dots \rangle$ be structures for a signature $\mathscr{L}$. For each ordinal $\gamma$ we define a game of perfect information between two players, Spoiler and Duplicator:



> 
> For each $\xi < \gamma$ Spoiler picks an element from $A$ or $B$, and Duplicator responds with an element from the other set. Together they determine a pair $(a\_{\xi}, b\_{\xi})$ in $A \times B$. After $\gamma$ rounds, Duplicator wins if there is an isomorphism, carrying each $a\_{\xi}$ to $b\_{\xi}$, from the substructure of $\mathfrak{A}$ generated by the $a\_{\xi}$ sequence to the substructure of $\mathfrak{B}$ generated by the $b\_{\xi}$ sequence. Else Spoiler wins.
> 
> 
> 


This is the *Ehrenfeucht-Fraïssé game* $G\_{\gamma}(\mathfrak{A},\mathfrak{B})$ of length $\gamma$ on $(\mathfrak{A}, \mathfrak{B})$. Note, as François did in the comments, that in some contexts this term designates a different game.


If $\mathfrak{A}$ and $\mathfrak{B}$ are isomorphic, then clearly Duplicator can win the game for any $\gamma$. Moreover, if $\mathfrak{A}$ and $\mathfrak{B}$ are finite or countable, then they are isomorphic iff Duplicator has a winning strategy for $G\_{\omega}(\mathfrak{A},\mathfrak{B})$. Such games may therefore be used toward establishing isomorphisms.


Ehrenfeucht-Fraïssé games can also show that a structural property isn't expressible in a first order language. Given a class $K$ of finite structures for a relational signature $\mathscr{L}$, to show that there is no first order $\mathscr{L}$ theory $\Gamma$ whose class of finite models is precisely $K$, it suffices to show that for each $n$ there are $\mathscr{L}$ structures $\mathfrak{A}\_n \in K$ and $\mathfrak{B}\_n \in \neg K$ such that Duplicator can win $G\_n(\mathfrak{A}\_n,\mathfrak{B}\_n)$. This is because if Duplicator can win, then $\mathfrak{A}\_n$ and $\mathfrak{B}\_n$ verify the same sentences of quantifier rank $\leq n$. (I forget whether this works when $\mathscr{L}$ has function symbols.)


What are some lesser known uses for these games, or for minor variations on them? I have a special interest in models of set theory.



What are some other uses for Ehrenfeucht-Fraïssé games?
These games have many uses. I think they're a lot of fun, but proofs that Duplicator has a winning strategy tend to get tedious quickly. Several applications are given (either in the body of the text or as exercises) in *Elements of Finite Model Theory* by Libkin. One application of E-F games that I like: to show that in first-order logic with equality and a single unary relation symbol *R* there is no sentence such that for all structures *A* the sentence holds in *A* iff the cardinality of the interpretation of *R* in *A* is even. Lots of other "cardinality properties" can be similarly shown with E-F games to be undefinable in FOL, such as FOL's inability to capture that the cardinality of the interpretation of two unary relations *R* and *S* are equal (in the finite case, without regard for the infinite case). In my Ph.D. dissertation I applied E-F games to a fun little example in the same spirit: given a first-order signature with three unary relation symbols *V*, *E*, and *F*, one cannot give a formula that captures the class of structures *A* for which *V^A - E^A + F^A* = 2. That is to say, in a suitable sense [Euler's polyhedron formula](http://en.wikipedia.org/wiki/Euler%27s_polyhedron_formula#Polyhedra) cannot be captured in FOL.


