In the mathematical discipline of model theory, the Ehrenfeucht–Fraïssé game (also called back-and-forth games) 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 (specifically Computer Aided Verification and database theory), 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.
Contents
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 (defined below). 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 (satisfy the same first-order sentences). The game is played in turns and rounds; A round proceeds as follows: First the first player (Spoiler) chooses any element from one of the structures, and the other player chooses an element from the other structure. The other player's task is to always pick an element that is "similar" to the one that Spoiler chose. The second player (Duplicator) wins if there exists an isomorphism between the elements chosen in the two different structures.
The game lasts for a fixed amount of steps (
Definition
Suppose that we are given two structures
- The first player, Spoiler, picks either a member
a 1 A or a memberb 1 B . - If Spoiler picked a member of
A , Duplicator picks a memberb 1 B ; otherwise, Duplicator picks a membera 1 A . - Spoiler picks either a member
a 2 A or a memberb 2 B . - Duplicator picks an element
a 2 b 2 - Spoiler and Duplicator continue to pick members of
A andB forn − 2 more steps. - At the conclusion of the game, we have chosen distinct elements
a 1 , … , a n A andb 1 , … , b n B . We therefore have two structures on the set{ 1 , … , n } , one induced fromA via the map sendingi toa i B via the map sendingi tob i
For each n we define a relation
It is easy to prove that if Duplicator wins this game for all n, that is,
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 [sic] and Abelard (and often denoted by