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 eine Struktur. Dann bezeichne das entsprechende Universum (Grundmenge, Trägermenge).
  • bezeichne die Menge aller endlichen Strukturen der Signatur .

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

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.

Satz

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

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

Beweisen von unteren Schranken

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

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]

Definition

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

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

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

Satz

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

Siehe auch

Referenzen

  1. Stanford Encyclopedia of Philosophy, Logic and Games.
  2. Neil Immerman: Descriptive Complexity. Springer, 1999, ISBN 978-0-387-98600-5.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. The authors of the article are listed here. Additional terms may apply for the media files, click on images to show image meta data.