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.
The main idea behind the game is that we have two structures, and two players – Spoiler and Duplicator.
to be a game between two players, Spoiler and Duplicator, played as follows: For each n we define a relation
It is easy to prove that if Duplicator wins this game for all finite n, that is,
If the set of relation symbols being considered is finite, the converse is also true.
can be shown equivalent by providing a winning strategy for Duplicator, then this shows that
[further explanation needed] 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;[2][3] it was formulated as a game by Andrzej Ehrenfeucht.
[4] The names Spoiler and Duplicator are due to Joel Spencer.
[5] Other usual names are Eloise [sic] and Abelard (and often denoted by
) after Heloise and Abelard, a naming scheme introduced by Wilfrid Hodges in his book Model Theory, or alternatively Eve and Adam.
[7] A simple example of the Ehrenfeucht–Fraïssé game is given in one of Ivars Peterson's MathTrek columns.
[8] Phokion Kolaitis' slides[9] and Neil Immerman's book chapter[10] on Ehrenfeucht–Fraïssé games discuss applications in computer science, the methodology for proving inexpressibility results, and several simple inexpressibility proofs using this methodology.
Modeloids are certain equivalence relations and the derivative provides for a generalization of standard model theory.