Эренфейхт-Фрайссе ойыны: Модельдердің эквиваленттілігін анықтау және логикалық емес қасиеттерді дәлелдеу

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 and pebble games for finite variable logics; extensions are powerful enough to characterise definability in existential second order logic.

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 (which is an ordinal – usually a finite number or ).

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.