Quelltext der Seite Ehrenfeucht-Fraïssé-Spiele

'''Ehrenfeucht-Fraïssé-Spiele''' ('''EF-Spiele''') sind eine Beweistechnik der [[Modelltheorie]]. Durch EF-Spiele lässt sich die Äquivalenz zweier [[Struktur (erste Stufe)|Strukturen]] zeigen bzw. widerlegen. ''Strukturen'' dienen in der [[Beschreibende Komplexitätstheorie|beschreibenden Komplexitätstheorie]] meist als Formalismus zur Beschreibung von Objekten wie [[Wort (Theoretische Informatik)|Wörtern]] oder [[Graph (Graphentheorie)|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 [[Prädikatenlogik|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]]).<ref>[https://plato.stanford.edu/entries/logic-games/ Stanford Encyclopedia of Philosophy, Logic and Games.]</ref>

== Bezeichnungen ==
* Sei <math>\mathcal{A}</math> eine Struktur. Dann bezeichne <math>|\mathcal{A}|</math> das entsprechende Universum ([[Grundmenge]], [[Trägermenge]]).
* <math>\mathsf{STRUKT}[\sigma]</math> bezeichne die Menge aller endlichen Strukturen der [[Signatur (Modelltheorie)|Signatur]] <math>\sigma</math>.

== Das ''n''-Runden-EF-Spiel ==
Ehrenfeucht-Fraïssé-Spiele in ihrer herkömmlichen Form haben einen engen Bezug zu [[Prädikatenlogik erster Stufe|Logiken erster Stufe]]. Diese Grundform ist wie folgt definiert.

=== Definition ===
Seien
: <math>\mathcal{A}, \mathcal{B}</math> zwei Strukturen der gleichen Signatur,
: <math>\mathbf{a'} \in |\mathcal{A}|^k, \mathbf{b'} \in |\mathcal{B}|^k,\ \ k, n \in \mathbb{N}</math>.

Ein ''n-Runden-Spiel'' wird auf den [[Interpretation (Logik)|Interpretationen]] <math>(\mathcal{A},\mathbf{a'}),(\mathcal{B},\mathbf{b'})</math> definiert:

:Das EF-Spiel <math>G_n((\mathcal{A},\mathbf{a'}),(\mathcal{B},\mathbf{b'}))</math> hat ''n'' Runden, die Ausgangsmenge ist <math>\{(a'_0,b'_0),\ \ldots\ ,(a'_{k-1},b'_{k-1})\}\subseteq |\mathcal{A}|\times|\mathcal{B}|</math>;

:* in jeder Runde ''i (i<n)'' wählt zunächst ''Samson'' ein beliebiges <math>a_i \in |\mathcal{A}|</math> oder ein <math>b_i \in |\mathcal{B}|</math>, welches noch nicht zuvor gewählt wurde
:* falls ''Samson'' ein Element aus <math>|\mathcal{A}|</math> gewählt hat, wählt daraufhin ''Delilah'' auf dieselbe Weise ein beliebiges <math>b_i \in |\mathcal{B}|</math>, sonst ein <math>a_i \in |\mathcal{A}|</math>
:* das resultierende Tupel <math>(a_i,b_i)</math> wird zur Ausgangsmenge hinzugefügt.

:Nach ''n'' Runden resultiert eine Menge von 2-Tupeln <math>\{(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}|</math>.
:*Falls durch diese Menge ein [[Partielle Funktion|partieller]] [[Isomorphismus]] <math>\varphi: |\mathcal{A}|\rightarrow|\mathcal{B}|</math> definiert wird, hat ''Delilah'' gewonnen, ansonsten hat ''Samson'' gewonnen.

:Per Definition ''gewinnt Delilah das Spiel'' <math>G_n((\mathcal{A},\mathbf{a'}),(\mathcal{B},\mathbf{b'}))</math>, falls sie eine zwingende [[Gewinnstrategie]] hat.

Oft gilt <math>k=0</math>; man schreibt <math>G_n(\mathcal{A},\mathcal{B})</math> und die Ausgangsmenge ist leer.

=== Eigenschaften von EF-Spielen ===
==== Satz ====
Zwei Strukturen <math>\mathcal{A}, \mathcal{B}</math> sind <math>n</math>-äquivalent, <math>\mathcal{A}\equiv_n\mathcal{B} \Leftarrow</math> ''Delilah'' gewinnt <math>G_n(\mathcal{A},\mathcal{B})</math>. Falls die Signatur der Strukturen endlich ist, gilt auch die Umkehrung.

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

==== Korollar ====
Delilah gewinnt <math>G_n(\mathcal{A}, \mathcal{B})</math> für alle <math>n \,\iff\, \forall n \in\mathbb{N}: \mathcal{A}\equiv_n\mathcal{B} \,:\iff\, \mathcal{A}</math> und <math>\mathcal{B}</math> sind [[Elementare Äquivalenz|elementar äquivalent]].

=== Beweisen von unteren Schranken ===
Um zu beweisen, dass eine Menge <math>I\subset \mathsf{STRUKT}\left[\sigma\right]</math> nicht durch [[Prädikatenlogik erster Stufe|<math>FO</math>]]<math>\left[\sigma\right]</math>-Formeln definiert werden kann, genügt es zu zeigen, dass es für jedes ''n''&nbsp;∈&nbsp;<math>\mathbb{N}</math> zwei Strukturen <math>\mathcal{A} \in I</math> und <math>\mathcal{B} \in \mathsf{STRUKT}[\sigma]\setminus I</math> gibt, so dass ''Delilah'' eine Gewinnstrategie für <math>G_n(\mathcal{A},\mathcal{B})</math> hat.

== EF-Spiele für die Prädikatenlogik zweiter Stufe ==
Ehrenfeucht-Fraïssé-Spiele können relativ problemlos auf [[Prädikatenlogik zweiter Stufe|Logiken zweiter Stufe]] erweitert werden. Das Beweisen von [[Gewinnstrategie]]n wird hierbei jedoch deutlich schwieriger. Eine eingeschränkte Variante sind Spiele für die existentielle Prädikatenlogik zweiter Stufe <math>(SO\exist, ESO). SO\exist</math> spielt durch die Charakterisierung der [[Komplexitätsklasse NP]] eine wichtige Rolle in der
[[Beschreibende Komplexitätstheorie|beschreibenden Komplexitätstheorie]], siehe dazu auch [[Satz von Fagin]].

Beschränkt man die <math>SO\exist</math>-Logik weiter auf [[Monadische Prädikatenlogik zweiter Stufe|''monadische'' Prädikate <math>(MSO\exist)</math>]], so ist diese Version der EF-Spiele äquivalent zu den Ajtai-Fagin-Spielen.<ref>Neil Immerman: ''Descriptive Complexity.'' Springer, 1999, ISBN 978-0-387-98600-5.</ref>

=== SO&exist;-Spiele ===

==== Definition ====
Seien
: <math>\mathcal{A}, \mathcal{B}</math> zwei Strukturen der gleichen Signatur
: <math>c, n \in \mathbb{N},\ \mathbf{s} \in \mathbb{N}^c</math>
die Eingaben für ein <math>SO\exist</math>-Spiel.
* ''Samson'' wählt die <math>c</math> Prädikate <math>P_i^\mathcal{A}</math> der [[Stelligkeit]] <math>s_i</math> über <math>|\mathcal{A}|</math>
* ''Delilah'' wählt daraufhin die <math>c</math> Prädikate <math>P_i^\mathcal{B}</math> der Stelligkeit <math>s_i</math> über <math>|\mathcal{B}|</math>
* Auf der beiden erweiterten Strukturen wird schließlich das Ehrenfeucht-Fraïssé-Spiel <math>G_n((\mathcal{A},\mathbf{P}^\mathcal{A}),(\mathcal{B},\mathbf{P}^\mathcal{B}))</math> gespielt.

Bei <math>MSO\exist</math>-Spielen (Beschränkung auf monadische Prädikate) gilt <math>s_i = 1</math> für alle <math>i</math>.

=== Ajtai-Fagin-Spiele ===
''[[Miklós Ajtai|Ajtai]]-[[Ronald Fagin|Fagin]]-Spiele'' sind in dem Sinne äquivalent zu den MSO∃-Spielen, als dass ''Delilah'' das Ajtai-Fagin-Spiel auf einer Menge <math>I\subset</math>[[#Bezeichnungen|<math>\mathsf{STRUKT}\left[\sigma\right]</math>]] genau dann gewinnt, wenn es für jedes <math>c</math> und jedes <math>n</math> zwei Strukturen <math>\mathcal{A} \in I</math> und <math>\mathcal{B} \in \mathsf{STRUKT}[\sigma]\setminus I</math> gibt, so dass sie das entsprechende <math>MSO\exist</math>-Spiel gewinnt. Ajtai-Fagin-Spiele sind jedoch formal leichter handhabbar als <math>MSO\exist</math>-Spiele.

==== Definition ====
Ein Ajtai-Fagin-Spiel wird auf einer Menge von Strukturen <math>I\subset \mathsf{STRUKT}\left[\sigma\right]</math> gespielt:
* Zuerst wählt ''Samson'' zwei Zahlen <math>c, n \in \mathbb{N}</math>
* ''Delilah'' wählt daraufhin eine Struktur <math>\mathcal{A} \in I</math>
* ''Samson'' wählt die monadischen Prädikate <math>P_1^\mathcal{A},\ \ldots\ ,P_c^\mathcal{A}</math> über <math>|\mathcal{A}|</math>
* ''Delilah'' wählt nun eine weitere Struktur <math>\mathcal{B} \in \mathsf{STRUKT}[\sigma]\setminus I</math> sowie die monadischen Prädikate <math>P_1^\mathcal{B},\ \ldots\ ,P_c^\mathcal{B}</math> über <math>|\mathcal{B}|</math>
* Nun wird auf den beiden erweiterten Strukturen das Ehrenfeucht-Fraïssé-Spiel <math>G_n((\mathcal{A},\mathbf{P}^\mathcal{A}),(\mathcal{B},\mathbf{P}^\mathcal{B}))</math> gespielt

==== Satz ====
Sei <math>I\subset \mathsf{STRUKT}\left[\sigma\right]</math>.
Dann gewinnt ''Delilah'' das Ajtai-Fagin-Spiel auf <math>I</math> genau dann, wenn  <math>I</math> nicht durch <math>MSO\exist\left[\sigma\right]</math>-Logik definierbar ist.

== Siehe auch ==
* [[Elementare Äquivalenz]]
* [[Satz von Fraïssé]]

== Einzelnachweise ==
<references />

[[Kategorie:Modelltheorie]]
[[Kategorie:Spieltheorie]]
[[Kategorie:Theoretische Informatik]]