Ehrenfeucht–Fraïssé game

From Wikipedia, the free encyclopedia

In the mathematical discipline of model theory, the Ehrenfeucht-Fraïssé game is a technique for determining whether two structures are elementarily equivalent.

Contents

[edit] 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:

  1. The first player, Spoiler, picks either a member a1 of \mathfrak{A} or a member b1 of \mathfrak{B}.
  2. If Spoiler picked a member of \mathfrak{A}, Duplicator picks a member b1 of \mathfrak{B}; otherwise, Spoiler picked a member of \mathfrak{B}, and Duplicator picks a member a1 of \mathfrak{A}.
  3. Spoiler picks either a member a_2\ne a_1 of \mathfrak{A} or a member b_2\ne b_1 of \mathfrak{B}.
  4. Duplicator picks whichever of a2 or b2 Spoiler did not pick.
  5. Spoiler and Duplicator continue to pick members of \mathfrak{A} and \mathfrak{B} for n − 2 more steps.
  6. 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 ai, and the other induced from \mathfrak{B} via the map sending i to bi. 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, then \mathfrak{A} and \mathfrak{B} are elementarily equivalent. If the set of relation symbols being considered is finite, the converse is also true.

[edit] 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[1],[2]; it was formulated as a game by Andrzej Ehrenfeucht.[3] The names Spoiler and Duplicator are due to Joel Spencer.[4]

[edit] Further reading

Chapter 1 of Poizat's model theory text[5] contains an introduction to the Ehrenfeucht-Fraïssé game, and so do Chapters 6, 7, and 13 of Rosenstein's book on linear orders.[6] A simple example of the Ehrenfeucht-Fraïssé game is given in [7].

[edit] References

  1. ^ Sur une nouvelle classification des systèmes de relations, Roland Fraïssé, Comptes Rendus 230 (1950), 1022–1024.
  2. ^ 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.
  3. ^ An application of games to the completeness problem for formalized theories, A. Ehrenfeucht, Fundamenta Mathematicae 49 (1961), 129–141.
  4. ^ Stanford Encyclopedia of Philosophy, entry on Logic and Games.
  5. ^ A Course in Model Theory, Bruno Poizat, tr. Moses Klein, New York: Springer-Verlag, 2000.
  6. ^ Linear Orderings, Joseph G. Rosenstein, New York: Academic Press, 1982.
  7. ^ Example of the Ehrenfeucht-Fraïssé game.
Languages