Ein Zwei-Spieler-Kombinationsspiel auf einem Paar relationaler Strukturen, bei dem ein Spieler (Spoiler) versucht, einen Unterschied zu zeigen, und der andere (Duplicator) versucht, eine partielle Isomorphie zu erhalten; existiert für den Duplicator eine Gewinnstrategie in k Runden, so charakterisiert das die Ununterscheidbarkeit durch erste-Ordnung-Formeln mit Quantorrang ≤ k.

Prinzip

Syntaktische Ununterscheidbarkeit (Formeln mit beschränktem Quantorrang) in ein operatives Verfahren übersetzen: Jeder Quantor entspricht einer Wahl eines Elements in einer der Strukturen, und passende Antworten erhalten die Hin- und Rück-Beziehung, die partielle Isomorphismen realisiert.

Demonstration

Vergleiche zwei endliche Graphen G und H: Um zu zeigen, dass sie alle FO-Sätze mit Quantorrang ≤ 2 gemeinsam erfüllen, konstruiere eine Duplicator-Strategie für zwei Runden, die stets das vom Spoiler gewählte Vertex auf ein Vertex mit denselben Adjazenzbeziehungen zu den bereits gewählten Vertexen abbildet; eine solche Strategie impliziert, dass kein FO-Satz mit Rang ≤ 2 sie trennt.

Fehlanwendung

Zu folgern, dass ein Duplicator-Sieg für ein festes k die Strukturen elementar äquivalent macht — dafür müsste der Duplicator für alle endlichen k gewinnen, nicht nur für ein einzelnes k.

Konsequenz

Bietet ein konkretes Werkzeug, um Nichtdefinierbarkeits- oder Ununterscheidbarkeitsresultate zu zeigen, die Ausdrucksstärke von FO-Fragmenten zu begrenzen und untere Schranken durch Spoiler-Strategien herzuleiten.

Umkehrung

Umgekehrt als Back-and-Forth-Konstruktion betrachtet: Anstatt des Spiels interpretiert man die Existenz von Duplicator-Strategien für alle k als koinduktives Kriterium für elementare Äquivalenz; das Rollenwechseln betont unterscheidende Eigenschaften statt Ununterscheidbarkeit.

Abgrenzung

Gilt für relationale erste-Ordnung-Logik und ihre Fragmente beschränkten Quantorrangs; erfasst nicht unmittelbar Erweiterungen wie Fixpunktlogiken, höhere Logiken oder Logiken mit Kardinalitätsquantoren ohne Modifikation.

Semantische Spannung

Steht in Spannung zu Bisimulationsmethoden: Beide erfassen Ununterscheidbarkeit, jedoch für unterschiedliche syntaktische Fragmente (Ehrenfeucht–Fraïssé für FO-Quantorrang, Bisimulation für modale/garded Fragmente); Vermischung führt oft zu Fehlinterpretationen.

Synthese

Das Ehrenfeucht–Fraïssé-Spiel operationalisiert den Strukturvergleich, indem es Quantorwechsel in eine konkrete Folge von Zügen übersetzt: Eine Duplicator-Gewinnstrategie bis zu k Runden ist das kombinatorische Zeugnis dafür, dass keine FO-Formel mit Quantorrang ≤ k die Strukturen unterscheidet.