or a member of . Duplicator picks an element or in the model from which Spoiler did not pick. Spoiler and Duplicator continue to pick members of and for more steps. 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 finite 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 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 [sic] and Abelard (and often denoted by and ) after Heloise and Abelard, a naming scheme introduced by Wilfrid Hodges in his book Model Theory, or alternatively Eve and Adam. Further reading Chapter 1 of Poizat's model theory text contains an introduction to the Ehrenfeucht–Fraïssé game, and so do Chapters 6, 7, and 13 of Rosenstein's book on linear orders. A simple example of the Ehrenfeucht–Fraïssé game is given in one of Ivars Peterson's MathTrek columns. Phokion Kolaitis' slides and Neil Immerman's book chapter on Ehrenfeucht–Fraïssé games discuss applications in computer science, the methodology for proving inexpressibility results, and several simple inexpressibility proofs using this methodology. Ehrenfeucht–Fraïssé games are the basis for the operation of derivative on modeloids. Modeloids are certain equivalence relations and the derivative provides for a generalization of standard model theory. References External links Six Lectures on Ehrenfeucht-Fraïssé games at MATH EXPLORERS' CLUB, Cornell