Ehrenfeucht Fraisse Spiele EF Spiele sind eine Beweistechnik der Modelltheorie Durch EF Spiele lasst sich die Aquivalenz zweier Strukturen zeigen bzw widerlegen Strukturen dienen in der beschreibenden Komplexitatstheorie meist als Formalismus zur Beschreibung von Objekten wie Wortern oder Graphen Ehrenfeucht Fraisse 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 ausdrucken lasst Entwickelt wurden sie von Andrzej Ehrenfeucht auf Grundlage der theoretischen Arbeit des Mathematikers Roland Fraisse Ein EF Spiel wird von zwei Spielern gespielt gewohnlich bezeichnet mit Spoiler und Duplicator nach Joel Spencer oder Samson und Delilah nach Neil Immerman 1 Inhaltsverzeichnis 1 Bezeichnungen 2 Das n Runden EF Spiel 2 1 Definition 2 2 Eigenschaften von EF Spielen 2 2 1 Satz 2 2 2 Korollar 2 3 Beweisen von unteren Schranken 3 EF Spiele fur die Pradikatenlogik zweiter Stufe 3 1 SO Spiele 3 1 1 Definition 3 2 Ajtai Fagin Spiele 3 2 1 Definition 3 2 2 Satz 4 Siehe auch 5 EinzelnachweiseBezeichnungen BearbeitenSei A displaystyle mathcal A nbsp eine Struktur Dann bezeichne A displaystyle mathcal A nbsp das entsprechende Universum Grundmenge Tragermenge S T R U K T s displaystyle mathsf STRUKT sigma nbsp bezeichne die Menge aller endlichen Strukturen der Signatur s displaystyle sigma nbsp Das n Runden EF Spiel BearbeitenEhrenfeucht Fraisse Spiele in ihrer herkommlichen Form haben einen engen Bezug zu Logiken erster Stufe Diese Grundform ist wie folgt definiert Definition Bearbeiten Seien A B displaystyle mathcal A mathcal B nbsp zwei Strukturen der gleichen Signatur a A k b B k k n N displaystyle mathbf a in mathcal A k mathbf b in mathcal B k k n in mathbb N nbsp Ein n Runden Spiel wird auf den Interpretationen A a B b displaystyle mathcal A mathbf a mathcal B mathbf b nbsp definiert Das EF Spiel G n A a B b displaystyle G n mathcal A mathbf a mathcal B mathbf b nbsp hat n Runden die Ausgangsmenge ist a 0 b 0 a k 1 b k 1 A B displaystyle a 0 b 0 ldots a k 1 b k 1 subseteq mathcal A times mathcal B nbsp in jeder Runde i i lt n wahlt zunachst Samson ein beliebiges a i A displaystyle a i in mathcal A nbsp oder ein b i B displaystyle b i in mathcal B nbsp welches noch nicht zuvor gewahlt wurde falls Samson ein Element aus A displaystyle mathcal A nbsp gewahlt hat wahlt daraufhin Delilah auf dieselbe Weise ein beliebiges b i B displaystyle b i in mathcal B nbsp sonst ein a i A displaystyle a i in mathcal A nbsp das resultierende Tupel a i b i displaystyle a i b i nbsp wird zur Ausgangsmenge hinzugefugt Nach n Runden resultiert eine Menge von 2 Tupeln a 0 b 0 a n 1 b n 1 a 0 b 0 a k 1 b k 1 A B 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 nbsp Falls durch diese Menge ein partieller Isomorphismus f A B displaystyle varphi mathcal A rightarrow mathcal B nbsp definiert wird hat Delilah gewonnen ansonsten hat Samson gewonnen Per Definition gewinnt Delilah das Spiel G n A a B b displaystyle G n mathcal A mathbf a mathcal B mathbf b nbsp falls sie eine zwingende Gewinnstrategie hat Oft gilt k 0 displaystyle k 0 nbsp man schreibt G n A B displaystyle G n mathcal A mathcal B nbsp und die Ausgangsmenge ist leer Eigenschaften von EF Spielen Bearbeiten Satz Bearbeiten Zwei Strukturen A B displaystyle mathcal A mathcal B nbsp sind n displaystyle n nbsp aquivalent A n B displaystyle mathcal A equiv n mathcal B Leftarrow nbsp Delilah gewinnt G n A B displaystyle G n mathcal A mathcal B nbsp Falls die Signatur der Strukturen endlich ist gilt auch die Umkehrung Dabei nennt man zwei Strukturen A displaystyle mathcal A nbsp und B displaystyle mathcal B nbsp n displaystyle n nbsp aquivalent in Zeichen A n B displaystyle mathcal A equiv n mathcal B nbsp wenn A displaystyle mathcal A nbsp und B displaystyle mathcal B nbsp dieselben Satze der Pradikatenlogik erster Stufe erfullen deren Verschachtelungstiefe von All und Existenzquantoren hochstens n displaystyle n nbsp ist Korollar Bearbeiten Delilah gewinnt G n A B displaystyle G n mathcal A mathcal B nbsp fur alle n n N A n B A displaystyle n iff forall n in mathbb N mathcal A equiv n mathcal B iff mathcal A nbsp und B displaystyle mathcal B nbsp sind elementar aquivalent Beweisen von unteren Schranken Bearbeiten Um zu beweisen dass eine Menge I S T R U K T s displaystyle I subset mathsf STRUKT left sigma right nbsp nicht durch F O displaystyle FO nbsp s displaystyle left sigma right nbsp Formeln definiert werden kann genugt es zu zeigen dass es fur jedes n N displaystyle mathbb N nbsp zwei Strukturen A I displaystyle mathcal A in I nbsp und B S T R U K T s I displaystyle mathcal B in mathsf STRUKT sigma setminus I nbsp gibt so dass Delilah eine Gewinnstrategie fur G n A B displaystyle G n mathcal A mathcal B nbsp hat EF Spiele fur die Pradikatenlogik zweiter Stufe BearbeitenEhrenfeucht Fraisse Spiele konnen relativ problemlos auf Logiken zweiter Stufe erweitert werden Das Beweisen von Gewinnstrategien wird hierbei jedoch deutlich schwieriger Eine eingeschrankte Variante sind Spiele fur die existentielle Pradikatenlogik zweiter Stufe S O E S O S O displaystyle SO exists ESO SO exists nbsp spielt durch die Charakterisierung der Komplexitatsklasse NP eine wichtige Rolle in der beschreibenden Komplexitatstheorie siehe dazu auch Satz von Fagin Beschrankt man die S O displaystyle SO exists nbsp Logik weiter auf monadische Pradikate M S O displaystyle MSO exists nbsp so ist diese Version der EF Spiele aquivalent zu den Ajtai Fagin Spielen 2 SO Spiele Bearbeiten Definition Bearbeiten Seien A B displaystyle mathcal A mathcal B nbsp zwei Strukturen der gleichen Signatur c n N s N c displaystyle c n in mathbb N mathbf s in mathbb N c nbsp die Eingaben fur ein S O displaystyle SO exists nbsp Spiel Samson wahlt die c displaystyle c nbsp Pradikate P i A displaystyle P i mathcal A nbsp der Stelligkeit s i displaystyle s i nbsp uber A displaystyle mathcal A nbsp Delilah wahlt daraufhin die c displaystyle c nbsp Pradikate P i B displaystyle P i mathcal B nbsp der Stelligkeit s i displaystyle s i nbsp uber B displaystyle mathcal B nbsp Auf der beiden erweiterten Strukturen wird schliesslich das Ehrenfeucht Fraisse Spiel G n A P A B P B displaystyle G n mathcal A mathbf P mathcal A mathcal B mathbf P mathcal B nbsp gespielt Bei M S O displaystyle MSO exists nbsp Spielen Beschrankung auf monadische Pradikate gilt s i 1 displaystyle s i 1 nbsp fur alle i displaystyle i nbsp Ajtai Fagin Spiele Bearbeiten Ajtai Fagin Spiele sind in dem Sinne aquivalent zu den MSO Spielen als dass Delilah das Ajtai Fagin Spiel auf einer Menge I displaystyle I subset nbsp S T R U K T s displaystyle mathsf STRUKT left sigma right nbsp genau dann gewinnt wenn es fur jedes c displaystyle c nbsp und jedes n displaystyle n nbsp zwei Strukturen A I displaystyle mathcal A in I nbsp und B S T R U K T s I displaystyle mathcal B in mathsf STRUKT sigma setminus I nbsp gibt so dass sie das entsprechende M S O displaystyle MSO exists nbsp Spiel gewinnt Ajtai Fagin Spiele sind jedoch formal leichter handhabbar als M S O displaystyle MSO exists nbsp Spiele Definition Bearbeiten Ein Ajtai Fagin Spiel wird auf einer Menge von Strukturen I S T R U K T s displaystyle I subset mathsf STRUKT left sigma right nbsp gespielt Zuerst wahlt Samson zwei Zahlen c n N displaystyle c n in mathbb N nbsp Delilah wahlt daraufhin eine Struktur A I displaystyle mathcal A in I nbsp Samson wahlt die monadischen Pradikate P 1 A P c A displaystyle P 1 mathcal A ldots P c mathcal A nbsp uber A displaystyle mathcal A nbsp Delilah wahlt nun eine weitere Struktur B S T R U K T s I displaystyle mathcal B in mathsf STRUKT sigma setminus I nbsp sowie die monadischen Pradikate P 1 B P c B displaystyle P 1 mathcal B ldots P c mathcal B nbsp uber B displaystyle mathcal B nbsp Nun wird auf den beiden erweiterten Strukturen das Ehrenfeucht Fraisse Spiel G n A P A B P B displaystyle G n mathcal A mathbf P mathcal A mathcal B mathbf P mathcal B nbsp gespieltSatz Bearbeiten Sei I S T R U K T s displaystyle I subset mathsf STRUKT left sigma right nbsp Dann gewinnt Delilah das Ajtai Fagin Spiel auf I displaystyle I nbsp genau dann wenn I displaystyle I nbsp nicht durch M S O s displaystyle MSO exists left sigma right nbsp Logik definierbar ist Siehe auch BearbeitenElementare Aquivalenz Satz von FraisseEinzelnachweise Bearbeiten Stanford Encyclopedia of Philosophy Logic and Games Neil Immerman Descriptive Complexity Springer 1999 ISBN 978 0 387 98600 5 Abgerufen von https de wikipedia org w index php title Ehrenfeucht Fraisse Spiele amp oldid 227385597
