Ehrenfeucht–Fraïssé game


In the mathematical discipline of model theory, the Ehrenfeucht–Fraïssé game
is a technique for determining whether two structures
are elementarily equivalent. The main application of Ehrenfeucht–Fraïssé games is in proving the inexpressibility of certain properties in first-order logic. Indeed, Ehrenfeucht–Fraïssé games provide a complete methodology for proving inexpressibility results for first-order logic. In this role, these games are of particular importance in finite model theory and its applications in computer science, since Ehrenfeucht–Fraïssé games are one of the few techniques from model theory that remain valid in the context of finite models. Other widely used techniques for proving inexpressibility results, such as the compactness theorem, do not work in finite models.
Ehrenfeucht–Fraïssé-like games can also be defined for other logics, such as fixpoint logics and pebble games for finite variable logics; extensions are powerful enough to characterise definability in existential second-order logic.

Main idea

The main idea behind the game is that we have two structures, and two players. One of the players wants to show that the two structures are different, whereas the other player wants to show that they are elementarily equivalent. The game is played in turns and rounds. A round proceeds as follows: the first player first chooses any element from one of the structures, and the second player chooses an element from the other structure. The duplicator's task is to always pick an element that is "similar" to the one the spoiler chose. The duplicator wins if and only if there exists an isomorphism between the eventual substructures chosen in the two different structures.
The game lasts for a fixed number of steps .

Definition

Suppose that we are given two structures
and, each with no function symbols and the same set of relation symbols,
and a fixed natural number n. We can then define the Ehrenfeucht–Fraïssé
game to be a game between two players, Spoiler and Duplicator,
played as follows:
  1. The first player, Spoiler, picks either a member of or a member of.
  2. If Spoiler picked a member of, Duplicator picks a member of ; otherwise, Duplicator picks a member of.
  3. Spoiler picks either a member of or a member of.
  4. Duplicator picks an element or in the model from which Spoiler did not pick.
  5. Spoiler and Duplicator continue to pick members of and for more steps.
  6. At the conclusion of the game, we have chosen distinct elements of and of. We therefore have two structures on the set, one induced from via the map sending to, and the other induced from via the map sending to. Duplicator wins if these structures are the same; Spoiler wins if they are not.
For each n we define a relation if Duplicator wins the n-move game. These are all equivalence relations on the class of structures with the given relation symbols. The intersection of all these relations is again an equivalence relation.

Equivalence and inexpressibility

It is easy to prove that if Duplicator wins this game for all n, that is,, then and are elementarily equivalent. If the set of relation symbols being considered is finite, the converse is also true.
If a property is true of but not true of, but and can be shown equivalent by providing a winning strategy for Duplicator, then this also shows that is inexpressible in the logic captured by this game.

History

The back-and-forth method used in the Ehrenfeucht–Fraïssé game to verify elementary equivalence was given by Roland Fraïssé
in his thesis;
it was formulated as a game by Andrzej Ehrenfeucht. The names Spoiler and Duplicator are due to Joel Spencer. Other usual names are Eloise and Abelard after Heloise and Abelard, a naming scheme introduced by Wilfrid Hodges in his book Model Theory, or alternatively Eve and Adam.