- Ehrenfeucht–Fraïssé game
In the mathematical discipline of
model theory , the Ehrenfeucht-Fraïssé game is a technique for determining whether two structures areelementarily 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 infinite model theory and its applications in computer science (specificallyComputer Aided Verification anddatabase theory ), since Ehrenfeucht-Fraïssé games are one of the such few techniques from model theory that remain valid in the context of finite models. (Other widely used techniques for proving inexpressibility results, such as thecompactness theorem , are not valid in the finite.)Ehrenfeucht-Fraïssé like games can also be defined for other logics, e.g.
pebble games for finite variable logics and fixpoint logics.Definition
Suppose that we are given two structures mathfrak{A} and mathfrak{B}, 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 G_n(mathfrak{A},mathfrak{B}) to be a game between two players, Spoiler and Duplicator, played as follows:
# The first player, Spoiler, picks either a member a_1 of mathfrak{A} or a member b_1 of mathfrak{B}.
# If Spoiler picked a member of mathfrak{A}, Duplicator picks a member b_1 of mathfrak{B}; otherwise, Spoiler picked a member of mathfrak{B}, and Duplicator picks a member a_1 of mathfrak{A}.
# Spoiler picks either a member a_2 e a_1 of mathfrak{A} or a member b_2 e b_1 of mathfrak{B}.
# Duplicator picks whichever of a_2 or b_2 Spoiler did not pick.
# Spoiler and Duplicator continue to pick members of mathfrak{A} and mathfrak{B} for n-2 more steps.
# At the conclusion of the game, we have chosen distinct elements a_1, dots, a_n of mathfrak{A} and b_1, dots, b_n of mathfrak{B}. We therefore have two structures on the set 1, dots,n}, one induced from mathfrak{A} via the map sending i to a_i, and the other induced from mathfrak{B} via the map sending i to b_i. Duplicator wins if these structures are the same; Spoiler wins if they are not.It is easy to prove that if Duplicator wins this game for all "n", thenmathfrak{A} and mathfrak{B} are elementarilyequivalent. If the set of relation symbols being considered is finite,the converse is also true.
History
The
back-and-forth method used in the Ehrenfeucht-Fraïsségame to verify elementary equivalence was given byRoland Fraïssé in his thesis ["Sur une nouvelle classification des systèmes de relations", Roland Fraïssé, "Comptes Rendus" 230 (1950), 1022–1024.] , ["Sur quelques classifications des systèmes de relations", Roland Fraïssé, thesis, Paris, 1953;published in "Publications Scientifiques de l'Université d'Alger", series A 1 (1954), 35–182.] ;it was formulated as a game byAndrzej Ehrenfeucht . [An application of gamesto the completeness problem for formalized theories, A. Ehrenfeucht, "Fundamenta Mathematicae" 49 (1961), 129–141.] The names Spoiler and Duplicator are due toJoel Spencer . [ [http://plato.stanford.edu/entries/logic-games/ Stanford Encyclopedia of Philosophy, entry on Logic and Games.] ]Further reading
Chapter 1 of Poizat's model theory text ["A Course in Model Theory", Bruno Poizat, tr. Moses Klein, New York: Springer-Verlag, 2000.] contains an introduction to the Ehrenfeucht-Fraïssé game, and so do Chapters 6, 7, and 13 of Rosenstein's book on linear orders. ["Linear Orderings", Joseph G. Rosenstein, New York: Academic Press, 1982.] A simple example of the Ehrenfeucht-Fraïssé game is given in [ [http://www.maa.org/mathland/mathtrek_3_19_01.html Example of the Ehrenfeucht-Fraïssé game.] ] .
Phokion Kolaitis' slides on Ehrenfeucht-Fraïssé games discuss applications in computer science, the methodology theorem for proving inexpressibility results, and several simple inexpressibility proofs using this methodology [ [http://www.cs.ucsc.edu/~kolaitis/talks/essllif.ps Course on combinatorial games in finite model theory by Phokion Kolaitis (.ps file)] ] .
References
Wikimedia Foundation. 2010.