Ehrenfeucht–Fraïssé game explained

In the mathematical discipline of model theory, the Ehrenfeucht–Fraïssé game (also called back-and-forth games)is a technique based on game semantics 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.

Ehrenfeucht–Fraïssé-like games can also be defined for other logics, such as fixpoint logics[1] 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 – Spoiler and Duplicator. Duplicator wants to show that the two structures are elementarily equivalent (satisfy the same first-order sentences), whereas Spoiler wants to show that they are different. The game is played in rounds. A round proceeds as follows: Spoiler chooses any element from one of the structures, and Duplicator chooses an element from the other structure. In simplified terms, the Duplicator's task is to always pick an element "similar" to the one that the Spoiler has chosen, whereas the Spoiler's task is to choose an element for which no "similar" element exists in the other structure. Duplicator wins if there exists an isomorphism between the eventual substructures chosen from the two different structures; otherwise, Spoiler wins.

The game lasts for a fixed number of steps

\gamma

(which is an ordinal – usually a finite number or

\omega

).

Definition

Suppose that we are given two structures

ak{A}

and

ak{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

Gn(ak{A},ak{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

ak{A}

or a member

b1

of

ak{B}

.
  1. If Spoiler picked a member of

ak{A}

, Duplicator picks a member

b1

of

ak{B}

; otherwise, Duplicator picks a member

a1

of

ak{A}

.
  1. Spoiler picks either a member

a2

of

ak{A}

or a member

b2

of

ak{B}

.
  1. Duplicator picks an element

a2

or

b2

in the model from which Spoiler did not pick.
  1. Spoiler and Duplicator continue to pick members of

ak{A}

and

ak{B}

for

n-2

more steps.
  1. At the conclusion of the game, we have chosen distinct elements

a1,...,an

of

ak{A}

and

b1,...,bn

of

ak{B}

. We therefore have two structures on the set

\{1,...,n\}

, one induced from

ak{A}

via the map sending

i

to

ai

, and the other induced from

ak{B}

via the map sending

i

to

bi

. Duplicator wins if these structures are the same; Spoiler wins if they are not.

For each n we define a relation

ak{A} \overset{n}{\sim} ak{B}

if Duplicator wins the n-move game

Gn(ak{A},ak{B})

. 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

ak{A}\simak{B}

.

Equivalence and inexpressibility

It is easy to prove that if Duplicator wins this game for all finite n, that is,

ak{A}\simak{B}

, then

ak{A}

and

ak{B}

are elementarily equivalent. If the set of relation symbols being considered is finite, the converse is also true.

If a property

Q

is true of

ak{A}

but not true of

ak{B}

, but

ak{A}

and

ak{B}

can be shown equivalent by providing a winning strategy for Duplicator, then this shows that

Q

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;[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

\exists

and

\forall

) 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[6] contains an introduction to the Ehrenfeucht–Fraïssé game, and so do Chapters 6, 7, and 13 of Rosenstein's book on linear orders.[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.

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

  1. Book: Bosse, Uwe . Computer Science Logic: 6th Workshop, CSL'92, San Miniato, Italy, September 28 - October 2, 1992. Selected Papers . 702 . Lecture Notes in Computer Science . Egon . Börger . . 1993 . 0808.03024 . 3-540-56992-8 . 100–114 . An Ehrenfeucht–Fraïssé game for fixpoint logic and stratified fixpoint logic . https://link.springer.com/content/pdf/10.1007/3-540-56992-8_8.pdf. 10.1007/3-540-56992-8_8 .
  2. Sur une nouvelle classification des systèmes de relations, Roland Fraïssé, Comptes Rendus 230 (1950), 1022 - 1024.
  3. 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.
  4. http://matwbn.icm.edu.pl/ksiazki/fm/fm49/fm4919.pdf An application of games to the completeness problem for formalized theories
  5. http://plato.stanford.edu/entries/logic-games/ Stanford Encyclopedia of Philosophy, entry on Logic and Games.
  6. A Course in Model Theory, Bruno Poizat, tr. Moses Klein, New York: Springer-Verlag, 2000.
  7. Linear Orderings, Joseph G. Rosenstein, New York: Academic Press, 1982.
  8. https://www.sciencenews.org/article/subtle-logic-winning-game Example of the Ehrenfeucht-Fraïssé game.
  9. http://www.cs.ucsc.edu/~kolaitis/talks/essllif.ps Course on combinatorial games in finite model theory by Phokion Kolaitis (.ps file)
  10. Book: Neil Immerman. Descriptive Complexity. Descriptive Complexity. Chapter 6: Ehrenfeucht–Fraïssé Games. https://books.google.com/books?id=kWSZ0OWnupkC&pg=PA91. 1999. Springer. 978-0-387-98600-5. 91–112.

External links

This article is licensed under the GNU Free Documentation License. It uses material from the Wikipedia article "Ehrenfeucht–Fraïssé game".

Except where otherwise indicated, Everything.Explained.Today is © Copyright 2009-2024, A B Cryer, All Rights Reserved. Cookie policy.