Ehrenfeucht-Fraïssé-Spiele

Ehrenfeucht-Fraïssé-Spiele (EF-Spiele) sind eine Beweistechnik der Modelltheorie. Durch EF-Spiele lässt sich die Äquivalenz zweier Strukturen zeigen bzw. widerlegen. Strukturen dienen in der beschreibenden Komplexitätstheorie meist als Formalismus zur Beschreibung von Objekten wie Wörtern oder Graphen. Ehrenfeucht-Fraïssé-Spiele liefern so ein Hilfsmittel zum Beweisen von unteren Schranken, also zum Beweis, dass sich eine gegebene Klasse von Strukturen nicht durch eine bestimmte Logik ausdrücken lässt.

Entwickelt wurden sie von Andrzej Ehrenfeucht auf Grundlage der theoretischen Arbeit des Mathematikers Roland Fraïssé.

Ein EF-Spiel wird von zwei Spielern gespielt, gewöhnlich bezeichnet mit Spoiler und Duplicator (nach Joel Spencer) oder Samson und Delilah (nach Neil Immerman).^[1]

• Sei ${\displaystyle {\mathcal {A}}}$ eine Struktur. Dann bezeichne ${\displaystyle |{\mathcal {A}}|}$ das entsprechende Universum (Grundmenge, Trägermenge).
• ${\displaystyle {\mathsf {STRUKT}}[\sigma ]}$ bezeichne die Menge aller endlichen Strukturen der Signatur ${\displaystyle \sigma }$.

Ehrenfeucht-Fraïssé-Spiele in ihrer herkömmlichen Form haben einen engen Bezug zu Logiken erster Stufe. Diese Grundform ist wie folgt definiert.

Seien

${\displaystyle {\mathcal {A}},{\mathcal {B}}}$ zwei Strukturen der gleichen Signatur,

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

Ein n-Runden-Spiel wird auf den Interpretationen ${\displaystyle ({\mathcal {A}},\mathbf {a'} ),({\mathcal {B}},\mathbf {b'} )}$ definiert:

Das EF-Spiel ${\displaystyle G_{n}(({\mathcal {A}},\mathbf {a'} ),({\mathcal {B}},\mathbf {b'} ))}$ hat n Runden, die Ausgangsmenge ist ${\displaystyle \{(a'_{0},b'_{0}),\ \ldots \ ,(a'_{k-1},b'_{k-1})\}\subseteq |{\mathcal {A}}|\times |{\mathcal {B}}|}$;

• in jeder Runde i (i<n) wählt zunächst Samson ein beliebiges ${\displaystyle a_{i}\in |{\mathcal {A}}|}$ oder ein ${\displaystyle b_{i}\in |{\mathcal {B}}|}$, welches noch nicht zuvor gewählt wurde
• falls Samson ein Element aus ${\displaystyle |{\mathcal {A}}|}$ gewählt hat, wählt daraufhin Delilah auf dieselbe Weise ein beliebiges ${\displaystyle b_{i}\in |{\mathcal {B}}|}$, sonst ein ${\displaystyle a_{i}\in |{\mathcal {A}}|}$
• das resultierende Tupel ${\displaystyle (a_{i},b_{i})}$ wird zur Ausgangsmenge hinzugefügt.

Nach n Runden resultiert eine Menge von 2-Tupeln ${\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}}|}$.

• Falls durch diese Menge ein partieller Isomorphismus ${\displaystyle \varphi :|{\mathcal {A}}|\rightarrow |{\mathcal {B}}|}$ definiert wird, hat Delilah gewonnen, ansonsten hat Samson gewonnen.

Per Definition gewinnt Delilah das Spiel ${\displaystyle G_{n}(({\mathcal {A}},\mathbf {a'} ),({\mathcal {B}},\mathbf {b'} ))}$, falls sie eine zwingende Gewinnstrategie hat.

Oft gilt ${\displaystyle k=0}$; man schreibt ${\displaystyle G_{n}({\mathcal {A}},{\mathcal {B}})}$ und die Ausgangsmenge ist leer.

Zwei Strukturen ${\displaystyle {\mathcal {A}},{\mathcal {B}}}$ sind ${\displaystyle n}$-äquivalent, ${\displaystyle {\mathcal {A}}\equiv _{n}{\mathcal {B}}\Leftarrow }$ Delilah gewinnt ${\displaystyle G_{n}({\mathcal {A}},{\mathcal {B}})}$. Falls die Signatur der Strukturen endlich ist, gilt auch die Umkehrung.

Dabei nennt man zwei Strukturen ${\displaystyle {\mathcal {A}}}$ und ${\displaystyle {\mathcal {B}}}$ ${\displaystyle n}$-äquivalent, in Zeichen ${\displaystyle {\mathcal {A}}\equiv _{n}{\mathcal {B}}}$, wenn ${\displaystyle {\mathcal {A}}}$ und ${\displaystyle {\mathcal {B}}}$ dieselben Sätze der Prädikatenlogik erster Stufe erfüllen, deren Verschachtelungstiefe von All- und Existenzquantoren höchstens ${\displaystyle n}$ ist.

Delilah gewinnt ${\displaystyle G_{n}({\mathcal {A}},{\mathcal {B}})}$ für alle ${\displaystyle n\,\iff \,\forall n\in \mathbb {N} :{\mathcal {A}}\equiv _{n}{\mathcal {B}}\,:\iff \,{\mathcal {A}}}$ und ${\displaystyle {\mathcal {B}}}$ sind elementar äquivalent.

Um zu beweisen, dass eine Menge ${\displaystyle I\subset {\mathsf {STRUKT}}\left[\sigma \right]}$ nicht durch ${\displaystyle FO}$${\displaystyle \left[\sigma \right]}$-Formeln definiert werden kann, genügt es zu zeigen, dass es für jedes n ∈ ${\displaystyle \mathbb {N} }$ zwei Strukturen ${\displaystyle {\mathcal {A}}\in I}$ und ${\displaystyle {\mathcal {B}}\in {\mathsf {STRUKT}}[\sigma ]\setminus I}$ gibt, so dass Delilah eine Gewinnstrategie für ${\displaystyle G_{n}({\mathcal {A}},{\mathcal {B}})}$ hat.

Ehrenfeucht-Fraïssé-Spiele können relativ problemlos auf Logiken zweiter Stufe erweitert werden. Das Beweisen von Gewinnstrategien wird hierbei jedoch deutlich schwieriger. Eine eingeschränkte Variante sind Spiele für die existentielle Prädikatenlogik zweiter Stufe ${\displaystyle (SO\exists ,ESO).SO\exists }$ spielt durch die Charakterisierung der Komplexitätsklasse NP eine wichtige Rolle in der beschreibenden Komplexitätstheorie, siehe dazu auch Satz von Fagin.

Beschränkt man die ${\displaystyle SO\exists }$-Logik weiter auf monadische Prädikate ${\displaystyle (MSO\exists )}$, so ist diese Version der EF-Spiele äquivalent zu den Ajtai-Fagin-Spielen.^[2]

Seien

${\displaystyle {\mathcal {A}},{\mathcal {B}}}$ zwei Strukturen der gleichen Signatur

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

die Eingaben für ein ${\displaystyle SO\exists }$-Spiel.

• Samson wählt die ${\displaystyle c}$ Prädikate ${\displaystyle P_{i}^{\mathcal {A}}}$ der Stelligkeit ${\displaystyle s_{i}}$ über ${\displaystyle |{\mathcal {A}}|}$
• Delilah wählt daraufhin die ${\displaystyle c}$ Prädikate ${\displaystyle P_{i}^{\mathcal {B}}}$ der Stelligkeit ${\displaystyle s_{i}}$ über ${\displaystyle |{\mathcal {B}}|}$
• Auf der beiden erweiterten Strukturen wird schließlich das Ehrenfeucht-Fraïssé-Spiel ${\displaystyle G_{n}(({\mathcal {A}},\mathbf {P} ^{\mathcal {A}}),({\mathcal {B}},\mathbf {P} ^{\mathcal {B}}))}$ gespielt.

Bei ${\displaystyle MSO\exists }$-Spielen (Beschränkung auf monadische Prädikate) gilt ${\displaystyle s_{i}=1}$ für alle ${\displaystyle i}$.

Ajtai-Fagin-Spiele sind in dem Sinne äquivalent zu den MSO∃-Spielen, als dass Delilah das Ajtai-Fagin-Spiel auf einer Menge ${\displaystyle I\subset }$${\displaystyle {\mathsf {STRUKT}}\left[\sigma \right]}$ genau dann gewinnt, wenn es für jedes ${\displaystyle c}$ und jedes ${\displaystyle n}$ zwei Strukturen ${\displaystyle {\mathcal {A}}\in I}$ und ${\displaystyle {\mathcal {B}}\in {\mathsf {STRUKT}}[\sigma ]\setminus I}$ gibt, so dass sie das entsprechende ${\displaystyle MSO\exists }$-Spiel gewinnt. Ajtai-Fagin-Spiele sind jedoch formal leichter handhabbar als ${\displaystyle MSO\exists }$-Spiele.

Ein Ajtai-Fagin-Spiel wird auf einer Menge von Strukturen ${\displaystyle I\subset {\mathsf {STRUKT}}\left[\sigma \right]}$ gespielt:

• Zuerst wählt Samson zwei Zahlen ${\displaystyle c,n\in \mathbb {N} }$
• Delilah wählt daraufhin eine Struktur ${\displaystyle {\mathcal {A}}\in I}$
• Samson wählt die monadischen Prädikate ${\displaystyle P_{1}^{\mathcal {A}},\ \ldots \ ,P_{c}^{\mathcal {A}}}$ über ${\displaystyle |{\mathcal {A}}|}$
• Delilah wählt nun eine weitere Struktur ${\displaystyle {\mathcal {B}}\in {\mathsf {STRUKT}}[\sigma ]\setminus I}$ sowie die monadischen Prädikate ${\displaystyle P_{1}^{\mathcal {B}},\ \ldots \ ,P_{c}^{\mathcal {B}}}$ über ${\displaystyle |{\mathcal {B}}|}$
• Nun wird auf den beiden erweiterten Strukturen das Ehrenfeucht-Fraïssé-Spiel ${\displaystyle G_{n}(({\mathcal {A}},\mathbf {P} ^{\mathcal {A}}),({\mathcal {B}},\mathbf {P} ^{\mathcal {B}}))}$ gespielt

Sei ${\displaystyle I\subset {\mathsf {STRUKT}}\left[\sigma \right]}$. Dann gewinnt Delilah das Ajtai-Fagin-Spiel auf ${\displaystyle I}$ genau dann, wenn ${\displaystyle I}$ nicht durch ${\displaystyle MSO\exists \left[\sigma \right]}$-Logik definierbar ist.

• Elementare Äquivalenz
• Satz von Fraïssé

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