Ehrenfeucht Fraïssé Games

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 ). ${\displaystyle {\mathcal {A}}}$ ${\displaystyle |{\mathcal {A}}|}$
• ${\displaystyle STRUKT[\sigma ]}$denote the set of all finite structures of the signature . ${\displaystyle \sigma }$

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

${\displaystyle {\mathcal {A}},{\mathcal {B}}}$ two structures of the same signature,

${\displaystyle \mathbf {a'} \in |{\mathcal {A}}|^{k},\mathbf {b'} \in |{\mathcal {B}}|^{k},\ \ k,n\in \mathbb {N} }$.

An n-round game is defined on the interpretations : ${\displaystyle ({\mathcal {A}},\mathbf {a'} ),({\mathcal {B}},\mathbf {b'} )}$

The EF game has n rounds, the starting set is ; ${\displaystyle G_{n}(({\mathcal {A}},\mathbf {a'} ),({\mathcal {B}},\mathbf {b'} ))}$ ${\displaystyle \{(a'_{0},b'_{0}),\ \ldots \ ,(a'_{k-1},b'_{k-1})\}\subseteq |{\mathcal {A}}|\times |{\mathcal {B}}|}$

• in each round i (i <n) , Samson first chooses any or one that has not been chosen before ${\displaystyle a_{i}\in |{\mathcal {A}}|}$ ${\displaystyle b_{i}\in |{\mathcal {B}}|}$
• if Samson has chosen an element , Delilah then chooses any in the same way , otherwise one ${\displaystyle |{\mathcal {A}}|}$ ${\displaystyle b_{i}\in |{\mathcal {B}}|}$ ${\displaystyle a_{i}\in |{\mathcal {A}}|}$
• the resulting tuple is added to the initial set. ${\displaystyle (a_{i},b_{i})}$

After n rounds a set of 2-tuples results . ${\displaystyle \{(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}}|}$

• If this set defines a partial isomorphism , Delilah wins, otherwise Samson wins. ${\displaystyle \varphi :|{\mathcal {A}}|\rightarrow |{\mathcal {B}}|}$

By definition , Delilah wins the game if she has a compelling winning strategy . ${\displaystyle G_{n}(({\mathcal {A}},\mathbf {a'} ),({\mathcal {B}},\mathbf {b'} ))}$

Often applies ; you write and the initial set is empty. ${\displaystyle k=0}$ ${\displaystyle G_{n}({\mathcal {A}},{\mathcal {B}})}$

Features of EF games

sentence

Two structures are equivalent, Delilah wins . If the signature of the structures is finite, the converse also applies. ${\displaystyle {\mathcal {A}},{\mathcal {B}}}$ ${\displaystyle n}$ ${\displaystyle {\mathcal {A}}\equiv _{n}{\mathcal {B}}\Leftarrow }$ ${\displaystyle G_{n}({\mathcal {A}},{\mathcal {B}})}$

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 . ${\displaystyle {\mathcal {A}}}$ ${\displaystyle {\mathcal {B}}}$ ${\displaystyle n}$ ${\displaystyle {\mathcal {A}}\equiv _{n}{\mathcal {B}}}$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle {\mathcal {B}}}$ ${\displaystyle n}$

Corollary

Delilah wins for everyone and are elementarily equivalent . ${\displaystyle G_{n}({\mathcal {A}},{\mathcal {B}})}$ ${\displaystyle n\,\iff \,\forall n\in \mathbb {N} :{\mathcal {A}}\equiv _{n}{\mathcal {B}}\,:\iff \,{\mathcal {A}}}$ ${\displaystyle {\mathcal {B}}}$

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 STRUKT\left[\sigma \right]}$ ${\displaystyle FO}$ ${\displaystyle \left[\sigma \right]}$ ${\displaystyle \mathbb {N} }$ ${\displaystyle {\mathcal {A}}\in I}$ ${\displaystyle {\mathcal {B}}\in STRUKT[\sigma ]\setminus I}$ ${\displaystyle G_{n}({\mathcal {A}},{\mathcal {B}})}$

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 }$

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 }$ ${\displaystyle (MSO\exists )}$

SO∃ games

definition

Be

${\displaystyle {\mathcal {A}},{\mathcal {B}}}$ two structures of the same signature

${\displaystyle c,n\in \mathbb {N} ,\ \mathbf {s} \in \mathbb {N} ^{c}}$

the inputs for a game. ${\displaystyle SO\exists }$

• Samson selects the predicates of arity over ${\displaystyle c}$ ${\displaystyle P_{i}^{\mathcal {A}}}$ ${\displaystyle s_{i}}$ ${\displaystyle |{\mathcal {A}}|}$
• Delilah then over- selects the predicates of arity ${\displaystyle c}$ ${\displaystyle P_{i}^{\mathcal {B}}}$ ${\displaystyle s_{i}}$ ${\displaystyle |{\mathcal {B}}|}$
• The Ehrenfeucht-Fraïssé game is finally played on the two expanded structures . ${\displaystyle G_{n}(({\mathcal {A}},\mathbf {P} ^{\mathcal {A}}),({\mathcal {B}},\mathbf {P} ^{\mathcal {B}}))}$

For games (limited to monadic predicates) applies to all . ${\displaystyle MSO\exists }$ ${\displaystyle s_{i}=1}$ ${\displaystyle i}$

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 }$ ${\displaystyle STRUKT\left[\sigma \right]}$ ${\displaystyle c}$ ${\displaystyle n}$ ${\displaystyle {\mathcal {A}}\in I}$ ${\displaystyle {\mathcal {B}}\in STRUKT[\sigma ]\setminus I}$ ${\displaystyle MSO\exists }$ ${\displaystyle MSO\exists }$

definition

An Ajtai Fagin game is played on a set of structures : ${\displaystyle I\subset STRUKT\left[\sigma \right]}$

• First, Samson chooses two numbers ${\displaystyle c,n\in \mathbb {N} }$
• Delilah then chooses a structure ${\displaystyle {\mathcal {A}}\in I}$
• Samson selects the monadic predicates over ${\displaystyle P_{1}^{\mathcal {A}},\ \ldots \ ,P_{c}^{\mathcal {A}}}$ ${\displaystyle |{\mathcal {A}}|}$
• Delilah now another structure selects and monadic predicates over ${\displaystyle {\mathcal {B}}\in STRUKT[\sigma ]\setminus I}$ ${\displaystyle P_{1}^{\mathcal {B}},\ \ldots \ ,P_{c}^{\mathcal {B}}}$ ${\displaystyle |{\mathcal {B}}|}$
• Now the Ehrenfeucht Fraïssé game is played on the two expanded structures ${\displaystyle G_{n}(({\mathcal {A}},\mathbf {P} ^{\mathcal {A}}),({\mathcal {B}},\mathbf {P} ^{\mathcal {B}}))}$

sentence

Be . Then Delilah wins the Ajtai-Fagin game if and only if it cannot be defined by logic. ${\displaystyle I\subset STRUKT\left[\sigma \right]}$ ${\displaystyle I}$ ${\displaystyle I}$ ${\displaystyle MSO\exists \left[\sigma \right]}$

See also

• Elementary equivalence
• Fraïssé's theorem

credentials

1. ^ Stanford Encyclopedia of Philosophy, Logic and Games.
2. ^ Neil Immerman: Descriptive Complexity. Springer, 1999, ISBN 978-0-387-98600-5 .