Ehrenfeucht Fraïssé games ( EF games ) are a proof technique of model theory . EF games can be used to show or refute the equivalence of two structures . Structures used in the descriptive complexity theory mostly as a formalism to describe objects such as words or graphs . Ehrenfeucht-Fraïssé games provide a tool for proving lower bounds , i.e. for proving that a given class of structures cannot be expressed by a certain logic .
They were developed by Andrzej Ehrenfeucht on the basis of the theoretical work of the mathematician Roland Fraïssé .
An EF game is played by two players, usually called Spoiler and Duplicator (after Joel Spencer ) or Samson and Delilah (after Neil Immerman ).
Designations
- Be a structure. Then denote the corresponding universe ( basic set , carrier set ).
![{\ mathcal {A}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/280ae03440942ab348c2ca9b8db6b56ffa9618f8)
![| \ mathcal {A} |](https://wikimedia.org/api/rest_v1/media/math/render/svg/d037d9457c3f17ab973b83a8b217ec106558530f)
-
denote the set of all finite structures of the signature .![\ sigma](https://wikimedia.org/api/rest_v1/media/math/render/svg/59f59b7c3e6fdb1d0365a494b81fb9a696138c36)
The n- round EF game
Ehrenfeucht Fraïssé games in their conventional form are closely related to first-level logic . This basic form is defined as follows.
definition
Be
-
two structures of the same signature,
-
.
An n-round game is defined on the interpretations :
![(\ mathcal {A}, \ mathbf {a '}), (\ mathcal {B}, \ mathbf {b'})](https://wikimedia.org/api/rest_v1/media/math/render/svg/20c07b4afc7d66de3fe9393a37f3a97b989f6ae3)
- The EF game has n rounds, the starting set is ;
![G_n ((\ mathcal {A}, \ mathbf {a '}), (\ mathcal {B}, \ mathbf {b'}))](https://wikimedia.org/api/rest_v1/media/math/render/svg/24a7ddb5792c8c1435a9c512f90238045f430f48)
![\ {(a'_0, b'_0), \ \ ldots \, (a '_ {k-1}, b' _ {k-1}) \} \ subseteq | \ mathcal {A} | \ times | \ mathcal {B} |](https://wikimedia.org/api/rest_v1/media/math/render/svg/032bf4439e9b4a0aba20526f1c58e43619053236)
- in each round i (i <n) , Samson first chooses any or one that has not been chosen before
![a_i \ in | \ mathcal {A} |](https://wikimedia.org/api/rest_v1/media/math/render/svg/266a985c95c32f97f2a0bb5944fb2494182bf99b)
![b_i \ in | \ mathcal {B} |](https://wikimedia.org/api/rest_v1/media/math/render/svg/5ae75e5db46b741052fefbd8526908d7f345d894)
- if Samson has chosen an element , Delilah then chooses any in the same way , otherwise one
![| \ mathcal {A} |](https://wikimedia.org/api/rest_v1/media/math/render/svg/d037d9457c3f17ab973b83a8b217ec106558530f)
![b_i \ in | \ mathcal {B} |](https://wikimedia.org/api/rest_v1/media/math/render/svg/5ae75e5db46b741052fefbd8526908d7f345d894)
- the resulting tuple is added to the initial set.
![(a_i, b_i)](https://wikimedia.org/api/rest_v1/media/math/render/svg/8ca50fe7f8ba26cc2b9dbde9500a51e660e10a92)
- After n rounds a set of 2-tuples results .
![\ {(a_0, b_0), \ \ ldots \, (a_ {n-1}, b_ {n-1}), (a'_0, b'_0), \ \ ldots \, (a '_ {k -1}, b '_ {k-1}) \} \ subseteq | \ mathcal {A} | \ times | \ mathcal {B} |](https://wikimedia.org/api/rest_v1/media/math/render/svg/ecb6d2bad998cdde35ebb6858c90cd9165d27ead)
- If this set defines a partial isomorphism , Delilah wins, otherwise Samson wins.
![\ varphi: | \ mathcal {A} | \ rightarrow | \ mathcal {B} |](https://wikimedia.org/api/rest_v1/media/math/render/svg/10ed82002e53ec61dc384dfd8001c9bc12705d55)
- By definition , Delilah wins the game if she has a compelling winning strategy .
![G_n ((\ mathcal {A}, \ mathbf {a '}), (\ mathcal {B}, \ mathbf {b'}))](https://wikimedia.org/api/rest_v1/media/math/render/svg/24a7ddb5792c8c1435a9c512f90238045f430f48)
Often applies ; you write and the initial set is empty.
![k = 0](https://wikimedia.org/api/rest_v1/media/math/render/svg/6307c8a99dad7d0bcb712352ae0a748bd99a038b)
![G_n (\ mathcal {A}, \ mathcal {B})](https://wikimedia.org/api/rest_v1/media/math/render/svg/25db409fcd3a07ba9a993fd29cc6c8fb5fa6930a)
Features of EF games
sentence
Two structures are equivalent, Delilah wins . If the signature of the structures is finite, the converse also applies.
![\ mathcal {A}, \ mathcal {B}](https://wikimedia.org/api/rest_v1/media/math/render/svg/41879b46fbc115435588ce159332fd2a7f85b41d)
![n](https://wikimedia.org/api/rest_v1/media/math/render/svg/a601995d55609f2d9f5e233e36fbe9ea26011b3b)
![G_n (\ mathcal {A}, \ mathcal {B})](https://wikimedia.org/api/rest_v1/media/math/render/svg/25db409fcd3a07ba9a993fd29cc6c8fb5fa6930a)
Two structures are called and equivalent, in signs , if and fulfill the same sentences of the first-order predicate logic, whose depth of nesting of universal and existential quantifiers is at most .
![{\ mathcal {A}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/280ae03440942ab348c2ca9b8db6b56ffa9618f8)
![n](https://wikimedia.org/api/rest_v1/media/math/render/svg/a601995d55609f2d9f5e233e36fbe9ea26011b3b)
![\ mathcal {A} \ equiv_n \ mathcal {B}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d6bd8c4aa44a14294070ee9ad1137542f291e422)
![{\ mathcal {A}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/280ae03440942ab348c2ca9b8db6b56ffa9618f8)
![{\ mathcal {B}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e5622de88a69f68340f8dcb43d0b8bd443ba9e13)
![n](https://wikimedia.org/api/rest_v1/media/math/render/svg/a601995d55609f2d9f5e233e36fbe9ea26011b3b)
Corollary
Delilah wins for everyone and are elementarily equivalent .
![G_n (\ mathcal {A}, \ mathcal {B})](https://wikimedia.org/api/rest_v1/media/math/render/svg/25db409fcd3a07ba9a993fd29cc6c8fb5fa6930a)
![n \, \ iff \, \ forall n \ in \ mathbb {N}: \ mathcal {A} \ equiv_n \ mathcal {B} \,: \ iff \, \ mathcal {A}](https://wikimedia.org/api/rest_v1/media/math/render/svg/29deae1ec92c17f39fb75f58493f6f9b8eb1b926)
![{\ mathcal {B}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e5622de88a69f68340f8dcb43d0b8bd443ba9e13)
Prove lower bounds
To prove that a set cannot be defined by -formulas, it suffices to show that for every n ∈ there are two structures and such that Delilah has a winning strategy for .
![{\ displaystyle I \ subset STRUCTURE \ left [\ sigma \ right]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6778ef5bf0b9a1854c5a7bd75db928ed74cf069c)
![FO](https://wikimedia.org/api/rest_v1/media/math/render/svg/5412cf4b0373a810c14d9731f15e14296dd2cc28)
![{\ displaystyle \ left [\ sigma \ right]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6b574013e364a1a2f4e7f4f3e4dfbcb31d6b6fae)
![\ mathbb {N}](https://wikimedia.org/api/rest_v1/media/math/render/svg/fdf9a96b565ea202d0f4322e9195613fb26a9bed)
![\ mathcal {A} \ in I.](https://wikimedia.org/api/rest_v1/media/math/render/svg/33c5aae8ab9f1d350cfc4af9080b503aa14d4052)
![\ mathcal {B} \ in STRUCTURE [\ sigma] \ setminus I](https://wikimedia.org/api/rest_v1/media/math/render/svg/350ead05f384f0ededd9050e3cf8847e7f365456)
![G_n (\ mathcal {A}, \ mathcal {B})](https://wikimedia.org/api/rest_v1/media/math/render/svg/25db409fcd3a07ba9a993fd29cc6c8fb5fa6930a)
EF games for second order predicate logic
Ehrenfeucht Fraïssé games can be extended to second level logic relatively easily . However, proving winning strategies becomes much more difficult. A restricted variant are games for the existential predicate logic of the second level plays an important role in the
descriptive complexity theory through the characterization of the complexity class NP , see also Fagin's theorem .
![{\ displaystyle (SO \ exists, ESO) .SO \ exists}](https://wikimedia.org/api/rest_v1/media/math/render/svg/59014801126a0e054a82b2b9c42d287f43ddf0ef)
If the logic is further restricted to monadic predicates , this version of the EF games is equivalent to the Ajtai-Fagin games.
![{\ displaystyle SO \ exists}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4376f6ce7a6754fcbc0507a2d0cb049cf0494f41)
![{\ displaystyle (MSO \ exists)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/377f16614f54bbdba6e1c252ab2db374931bb8ef)
SO∃ games
definition
Be
-
two structures of the same signature
![c, n \ in \ mathbb {N}, \ \ mathbf {s} \ in \ mathbb {N} ^ c](https://wikimedia.org/api/rest_v1/media/math/render/svg/8f9633416d70708c4f25a22ec58ab87f77656caf)
the inputs for a game.
![{\ displaystyle SO \ exists}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4376f6ce7a6754fcbc0507a2d0cb049cf0494f41)
-
Samson selects the predicates of arity over
![c](https://wikimedia.org/api/rest_v1/media/math/render/svg/86a67b81c2de995bd608d5b2df50cd8cd7d92455)
![s_ {i}](https://wikimedia.org/api/rest_v1/media/math/render/svg/cfda82668232cbdc0874ed28ab8b6079420d1ffe)
-
Delilah then over- selects the predicates of arity
![c](https://wikimedia.org/api/rest_v1/media/math/render/svg/86a67b81c2de995bd608d5b2df50cd8cd7d92455)
![P_i ^ \ mathcal {B}](https://wikimedia.org/api/rest_v1/media/math/render/svg/93e3ce04701d83f3ea0e163929cddb2ccc475269)
![s_ {i}](https://wikimedia.org/api/rest_v1/media/math/render/svg/cfda82668232cbdc0874ed28ab8b6079420d1ffe)
- The Ehrenfeucht-Fraïssé game is finally played on the two expanded structures .
![G_n ((\ mathcal {A}, \ mathbf {P} ^ \ mathcal {A}), (\ mathcal {B}, \ mathbf {P} ^ \ mathcal {B}))](https://wikimedia.org/api/rest_v1/media/math/render/svg/4fc81e5c34574b0a970faacae42e88625fb78e10)
For games (limited to monadic predicates) applies to all .
![{\ displaystyle MSO \ exists}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4d33a8b30fb8346b35a100d161dfc7af324fa8bc)
![s_i = 1](https://wikimedia.org/api/rest_v1/media/math/render/svg/8757dc8386d9685bf56c6f638c028507ce3845aa)
![i](https://wikimedia.org/api/rest_v1/media/math/render/svg/add78d8608ad86e54951b8c8bd6c8d8416533d20)
Ajtai Fagin games
Ajtai - Fagin games are equivalent in the sense of the MSO∃ games than that Delilah the Ajtai-Fagin game on a setif and only wins if it for eachand everytwo structuresandare, making them the appropriate- Game wins. Ajtai-Fagin games are formally easier to handle thangames.
![{\ displaystyle I \ subset}](https://wikimedia.org/api/rest_v1/media/math/render/svg/979b7eaef75d92f0e17f18446aa17a2cbdc611f8)
![{\ displaystyle STRUCTURE \ left [\ sigma \ right]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6c32c0d06359b5660a9b160bb2bb5b230bd6ff1a)
![c](https://wikimedia.org/api/rest_v1/media/math/render/svg/86a67b81c2de995bd608d5b2df50cd8cd7d92455)
![n](https://wikimedia.org/api/rest_v1/media/math/render/svg/a601995d55609f2d9f5e233e36fbe9ea26011b3b)
![\ mathcal {A} \ in I.](https://wikimedia.org/api/rest_v1/media/math/render/svg/33c5aae8ab9f1d350cfc4af9080b503aa14d4052)
![\ mathcal {B} \ in STRUCTURE [\ sigma] \ setminus I](https://wikimedia.org/api/rest_v1/media/math/render/svg/350ead05f384f0ededd9050e3cf8847e7f365456)
![{\ displaystyle MSO \ exists}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4d33a8b30fb8346b35a100d161dfc7af324fa8bc)
![{\ displaystyle MSO \ exists}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4d33a8b30fb8346b35a100d161dfc7af324fa8bc)
definition
An Ajtai Fagin game is played on a set of structures :
![{\ displaystyle I \ subset STRUCTURE \ left [\ sigma \ right]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6778ef5bf0b9a1854c5a7bd75db928ed74cf069c)
- First, Samson chooses two numbers
-
Delilah then chooses a structure
-
Samson selects the monadic predicates over
![P_1 ^ \ mathcal {A}, \ \ ldots \, P_c ^ \ mathcal {A}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0941df5fa90678c90581e2279370296428b434ab)
-
Delilah now another structure selects and monadic predicates over
![\ mathcal {B} \ in STRUCTURE [\ sigma] \ setminus I](https://wikimedia.org/api/rest_v1/media/math/render/svg/350ead05f384f0ededd9050e3cf8847e7f365456)
![P_1 ^ \ mathcal {B}, \ \ ldots \, P_c ^ \ mathcal {B}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7c21923744a19915022c728d5b887d21a1f50728)
- Now the Ehrenfeucht Fraïssé game is played on the two expanded structures
![G_n ((\ mathcal {A}, \ mathbf {P} ^ \ mathcal {A}), (\ mathcal {B}, \ mathbf {P} ^ \ mathcal {B}))](https://wikimedia.org/api/rest_v1/media/math/render/svg/4fc81e5c34574b0a970faacae42e88625fb78e10)
sentence
Be . Then Delilah wins the Ajtai-Fagin game if and only if it cannot be defined by logic.
![{\ displaystyle I \ subset STRUCTURE \ left [\ sigma \ right]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6778ef5bf0b9a1854c5a7bd75db928ed74cf069c)
![I.](https://wikimedia.org/api/rest_v1/media/math/render/svg/535ea7fc4134a31cbe2251d9d3511374bc41be9f)
![I.](https://wikimedia.org/api/rest_v1/media/math/render/svg/535ea7fc4134a31cbe2251d9d3511374bc41be9f)
![{\ displaystyle MSO \ exists \ left [\ sigma \ right]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/45aa602370992ad9a29da40cafb83758846d5151)
See also
credentials
-
^ Stanford Encyclopedia of Philosophy, Logic and Games.
-
^ Neil Immerman: Descriptive Complexity. Springer, 1999, ISBN 978-0-387-98600-5 .