12
$\begingroup$

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.

$\endgroup$
10
  • $\begingroup$ This is not how EF games are defined for ordinals $\gamma \geq \omega$. The plays of an EF game are always finite. At each move, Spoiler picks an ordinal smaller than the previous one he played, or smaller than $\gamma$ if this is the first move. The game ends when Spoiler picks the ordinal 0, which is bound to happen in finitely many steps. $\endgroup$ Aug 12, 2011 at 21:13
  • $\begingroup$ Also, Duplicator wins $G_\omega(\mathfrak{A},\mathfrak{B})$ if and only if $\mathfrak{A}$ and $\mathfrak{B}$ are elementarily equivalent. When $\mathfrak{A}$ and $\mathfrak{B}$ are finite or countable and Duplicator wins the $G_\gamma(\mathfrak{A},\mathfrak{B})$ game for every ordinal $\gamma$, then $\mathfrak{A}$ and $\mathfrak{B}$ are isomorphic. $\endgroup$ Aug 12, 2011 at 21:15
  • $\begingroup$ François, I just copied the definition from pp. 95 to 96 of Hodges's treatise on model theory. Theorem 3.2.3 there states that, in the finite or countable case, Duplicator wins $G_\omega(\mathfrak{A}, \mathfrak{B})$ iff $\mathfrak{A}$ and $\mathfrak{B}$ are isomorphic. Perhaps you're thinking of what on p. 102 Hodges calls "unnested" EF games. Corrollary 3.3.3 states that $\mathfrak{A}$ and $\mathfrak{B}$ are elementarily equivalent iff Duplicator wins every such game of finite length. This fits with your second comment. $\endgroup$
    – Cole Leahy
    Aug 12, 2011 at 22:06
  • $\begingroup$ I would believe it if you told me that unnested EF games are more useful than the ones I described. Do you care to elaborate? $\endgroup$
    – Cole Leahy
    Aug 12, 2011 at 22:06
  • 1
    $\begingroup$ I figured out the history here. On the one hand, the EF games I just described were introduced by Barwise. On the other hand, Karp studied the game $G_\omega(\mathfrak{A},\mathfrak{B})$ as you describe it. (Longer games have been studied by various later authors.) It appears that both variants have been called EF games... $\endgroup$ Aug 12, 2011 at 22:07

3 Answers 3

5
$\begingroup$

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 cannot be captured in FOL.

$\endgroup$
1
  • $\begingroup$ Nice to see you, Jesse! $\endgroup$
    – Cole Leahy
    Jan 16, 2013 at 17:30
5
$\begingroup$

For reference, Jouko Väänänen -of Dependence Logic fame (wikipedia) gives a thorough treatment of EF games in Cambridge publication (2011) of Models and Games. He discusses Scott Watershed ordinal in Dynamic EF game as well as considers Transfinite Dynamic EF and EF game of generalized monotone quantifier Q. (The book contains about 500 exercises.)

Edit: A possible area of interest may be uses of EF in hypergames.

$\endgroup$
1
$\begingroup$

Software can exploit Ehrenfeucht Fraisse Games to view a database schema as a Property Graph Schema (graph database) or an Entity Relationship Diagram (relational database).

Logical points of structure in a common metamodel expressed as theorems under a theory of finite model theory can be viewed/interpreted in multiple ways, exploiting Ehrenfeucht Fraisse Games.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.