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) .

Das n-Runden-EF-Spiel

Ehrenfeucht-Fraïssé-Spiele in ihrer herkömmlichen Form eignen sich zum Beweis verschiedener Eigenschaften von Logiken erster Stufe. Diese Grundform ist wie folgt definiert.

Definition

Seien

• ${\mathcal {A}},{\mathcal {B}}$ zwei Strukturen der gleichen Signatur, dabei bezeichnen $|{\mathcal {A}}|,\ |{\mathcal {B}}|$ das jeweilige Universum (Grundmenge)
• $\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 $({\mathcal {A}},\mathbf {a'} ),({\mathcal {B}},\mathbf {b'} )$ definiert:

Das EF-Spiel $G_{n}(({\mathcal {A}},\mathbf {a'} ),({\mathcal {B}},\mathbf {b'} ))$ hat n Runden, die Ausgangsmenge ist $\{(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 $a_{i}\in |{\mathcal {A}}|$ oder ein $b_{i}\in |{\mathcal {B}}|$, welches noch nicht zuvor gewählt wurde
• falls Samson ein Element aus $|{\mathcal {A}}|$ gewählt hat, wählt daraufhin Delilah auf die selbe Weise ein beliebiges $b_{i}\in |{\mathcal {B}}|$, sonst ein $a_{i}\in |{\mathcal {A}}|$
• das resultierende Tupel $(a_{i},b_{i})$ wird zur Ausgangsmenge hizugefügt

Nach n Runden resultiert eine Menge von 2-Tupeln $\{(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 $\varphi :|{\mathcal {A}}|\rightarrow |{\mathcal {B}}|$ definiert wird, hat Delilah gewonnen, ansonsten hat Samson gewonnen

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

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

Eigenschaften von EF-Spielen

Satz

Zwei Strukturen ${\mathcal {A}},{\mathcal {B}}$ sind n-äquivalent, ${\mathcal {A}}\equiv _{n}{\mathcal {B}}\iff$ Delilah gewinnt $G_{n}({\mathcal {A}},{\mathcal {B}})$.

Korollar

$\forall n\in \mathbb {N} :{\mathcal {A}}\equiv _{n}{\mathcal {B}}\iff {\mathcal {A}}$ und ${\mathcal {B}}$ sind elementar äquivalent.

Beweisen von unteren Schranken

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

EF-Spiele für die Prädikatenlogik zweiter Stufe

EF-Spiele können relativ problemlos auf Logiken zweiter Stufe erweitert werden. Das Beweisen von Gewinnstrategien wird hierbei aber deutlich schwieriger. Eine eingeschränkte Variante sind Spiele für die existentielle Prädikatenlogik zweiter Stufe (SO∃, ESO). SO∃ spielt durch die Charakterisierung der Komplexitätsklasse NP eine wichtige Rolle in der beschreibenden Komplexitätstheorie.

Beschränkt man die SO∃-Logik weiter auf monadische Prädikate, so ist diese Version der EF-Spiele äquivalent zu den Ajtai-Fagin-Spielen .

Ajtai-Fagin-Spiele

Ajtai-Fagin-Spiele sind bei Beschränkung auf monadische Prädikate in dem Sinne äquivalent zu den SO∃-Spielen, als dass Delilah das Ajtai-Fagin-Spiel auf einer Menge I ⊆ STRUKT[σ] gewinnt, genau dann, wenn es für jedes c und jedes n zwei Strukturen ${\mathcal {A}}\in I$ und ${\mathcal {B}}\in STRUKT[\sigma ]\setminus I$ gibt, so dass sie das entsprechende SO∃-Spiel gewinnt. Ajtai-Fagin-Spiele sind jedoch formal leichter handhabbar als SO∃-Spiele.

Definition

Ein Ajtai-Fagin-Spiel wird auf einer Menge von Strukturen I ⊆ STRUKT[σ] gespielt:

• Zuerst wählt Samson zwei Zahlen $c,n\in \mathbb {N}$
• Delilah wählt daraufhin eine Struktur Fehler beim Parsen (Konvertierungsfehler. Der Server („/media/api/rest_“) hat berichtet: „Cannot get mml. TeX parse error: Undefined control sequence \emph“): {\displaystyle {\mathcal {A}}\in {\emph {I}}}
• Samson wählt die monadischen Prädikate $P_{1}^{\mathcal {A}},\ \ldots \ ,P_{c}^{\mathcal {A}}$ auf $|{\mathcal {A}}|$
• Delilah wählt nun eine weitere Struktur Fehler beim Parsen (Konvertierungsfehler. Der Server („/media/api/rest_“) hat berichtet: „Cannot get mml. TeX parse error: Undefined control sequence \emph“): {\displaystyle {\mathcal {B}}\in STRUKT[\sigma ]\setminus {\emph {I}}} sowie die monadischen Prädikate $P_{1}^{\mathcal {B}},\ \ldots \ ,P_{c}^{\mathcal {B}}$ auf $|{\mathcal {B}}|$
• Nun wird auf den beiden erweiterten Strukturen das Ehrenfeucht-Fraïssé-Spiel $G_{n}(({\mathcal {A}},\mathbf {P} ^{\mathcal {A}}),({\mathcal {B}},\mathbf {P} ^{\mathcal {B}}))$ gespielt