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]

Bezeichnungen

Bearbeiten
  • Sei   eine Struktur. Dann bezeichne   das entsprechende Universum (Grundmenge, Trägermenge).
  •   bezeichne die Menge aller endlichen Strukturen der Signatur  .

Das n-Runden-EF-Spiel

Bearbeiten

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

Definition

Bearbeiten

Seien

  zwei Strukturen der gleichen Signatur,
 .

Ein n-Runden-Spiel wird auf den Interpretationen   definiert:

Das EF-Spiel   hat n Runden, die Ausgangsmenge ist  ;
  • in jeder Runde i (i<n) wählt zunächst Samson ein beliebiges   oder ein  , welches noch nicht zuvor gewählt wurde
  • falls Samson ein Element aus   gewählt hat, wählt daraufhin Delilah auf dieselbe Weise ein beliebiges  , sonst ein  
  • das resultierende Tupel   wird zur Ausgangsmenge hinzugefügt.
Nach n Runden resultiert eine Menge von 2-Tupeln  .
  • Falls durch diese Menge ein partieller Isomorphismus   definiert wird, hat Delilah gewonnen, ansonsten hat Samson gewonnen.
Per Definition gewinnt Delilah das Spiel  , falls sie eine zwingende Gewinnstrategie hat.

Oft gilt  ; man schreibt   und die Ausgangsmenge ist leer.

Eigenschaften von EF-Spielen

Bearbeiten

Zwei Strukturen   sind  -äquivalent,   Delilah gewinnt  . Falls die Signatur der Strukturen endlich ist, gilt auch die Umkehrung.

Dabei nennt man zwei Strukturen   und    -äquivalent, in Zeichen  , wenn   und   dieselben Sätze der Prädikatenlogik erster Stufe erfüllen, deren Verschachtelungstiefe von All- und Existenzquantoren höchstens   ist.

Korollar

Bearbeiten

Delilah gewinnt   für alle   und   sind elementar äquivalent.

Beweisen von unteren Schranken

Bearbeiten

Um zu beweisen, dass eine Menge   nicht durch   -Formeln definiert werden kann, genügt es zu zeigen, dass es für jedes n ∈   zwei Strukturen   und   gibt, so dass Delilah eine Gewinnstrategie für   hat.

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

Bearbeiten

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   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  -Logik weiter auf monadische Prädikate  , so ist diese Version der EF-Spiele äquivalent zu den Ajtai-Fagin-Spielen.[2]

SO∃-Spiele

Bearbeiten

Definition

Bearbeiten

Seien

  zwei Strukturen der gleichen Signatur
 

die Eingaben für ein  -Spiel.

  • Samson wählt die   Prädikate   der Stelligkeit   über  
  • Delilah wählt daraufhin die   Prädikate   der Stelligkeit   über  
  • Auf der beiden erweiterten Strukturen wird schließlich das Ehrenfeucht-Fraïssé-Spiel   gespielt.

Bei  -Spielen (Beschränkung auf monadische Prädikate) gilt   für alle  .

Ajtai-Fagin-Spiele

Bearbeiten

Ajtai-Fagin-Spiele sind in dem Sinne äquivalent zu den MSO∃-Spielen, als dass Delilah das Ajtai-Fagin-Spiel auf einer Menge    genau dann gewinnt, wenn es für jedes   und jedes   zwei Strukturen   und   gibt, so dass sie das entsprechende  -Spiel gewinnt. Ajtai-Fagin-Spiele sind jedoch formal leichter handhabbar als  -Spiele.

Definition

Bearbeiten

Ein Ajtai-Fagin-Spiel wird auf einer Menge von Strukturen   gespielt:

  • Zuerst wählt Samson zwei Zahlen  
  • Delilah wählt daraufhin eine Struktur  
  • Samson wählt die monadischen Prädikate   über  
  • Delilah wählt nun eine weitere Struktur   sowie die monadischen Prädikate   über  
  • Nun wird auf den beiden erweiterten Strukturen das Ehrenfeucht-Fraïssé-Spiel   gespielt

Sei  . Dann gewinnt Delilah das Ajtai-Fagin-Spiel auf   genau dann, wenn   nicht durch  -Logik definierbar ist.

Siehe auch

Bearbeiten

Einzelnachweise

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