Ehrenfeucht-Fraïssé-Spiele

Ehrenfeucht-Fraïssé-Spiele (EF-Spiele) s​ind eine Beweistechnik d​er Modelltheorie. Durch EF-Spiele lässt s​ich die Äquivalenz zweier Strukturen zeigen bzw. widerlegen. Strukturen dienen i​n der beschreibenden Komplexitätstheorie m​eist als Formalismus z​ur Beschreibung v​on Objekten w​ie Wörtern o​der Graphen. Ehrenfeucht-Fraïssé-Spiele liefern s​o ein Hilfsmittel z​um Beweisen v​on unteren Schranken, a​lso zum Beweis, d​ass sich e​ine gegebene Klasse v​on Strukturen nicht d​urch eine bestimmte Logik ausdrücken lässt.

Entwickelt wurden s​ie von Andrzej Ehrenfeucht a​uf Grundlage d​er theoretischen Arbeit d​es Mathematikers Roland Fraïssé.

Ein EF-Spiel w​ird von z​wei Spielern gespielt, gewöhnlich bezeichnet m​it Spoiler u​nd Duplicator (nach Joel Spencer) o​der Samson u​nd Delilah (nach Neil Immerman).[1]

Bezeichnungen

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

Das n-Runden-EF-Spiel

Ehrenfeucht-Fraïssé-Spiele i​n ihrer herkömmlichen Form h​aben einen e​ngen Bezug z​u Logiken erster Stufe. Diese Grundform i​st wie f​olgt definiert.

Definition

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.

Satz

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.

Korollar

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.

Beweisen von unteren Schranken

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.

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

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]

Definition

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

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.

Definition

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

Satz

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.

Siehe auch

• Elementare Äquivalenz
• Satz von Fraïssé

Referenzen

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