Eine Semantik für logische Sprachen, die die Wahrheit einer Formel in einem Modell als Existenz einer Gewinnstrategie in einem zugehörigen Auswertungsspiel zwischen zwei Spielern (Verifier und Falsifier) interpretiert; logische Junktoren und Quantoren werden in Spielregeln übersetzt, die Züge und Gewinnbedingungen festlegen.

Prinzip

Wahrheit wird operativ durch Existenz von Gewinnstrategien definiert: Existenzquantoren entsprechen Verifier-Zügen zur Wahl von Zeugen, Allquantoren den Wahlen des Falsifier, Konjunktionen bedeuten, dass der Falsifier eine Konjunktion wählt, Disjunktionen geben dem Verifier die Wahl, Negation kehrt die Rollen um.

Demonstration

Die Formel ∃x∀y R(x,y) in einer Struktur M auswerten: Im Auswertungsspiel wählt der Verifier ein Element a für x; der Falsifier wählt ein b für y; der Verifier gewinnt genau dann, wenn R(a,b) gilt. Die Existenz einer Verifier-Strategie, die gegen alle Falsifier-Antworten gewinnt, ist äquivalent zu M ⊨ ∃x∀y R(x,y).

Fehlanwendung

Gewinnstrategien als formale Beweise der Wahrheit gleichzusetzen, ohne zwischen uniformen Strategien und nicht-uniformen existentiellen Zeugen zu unterscheiden, oder naive Spielregeln auf Logiken anzuwenden, deren Junktoren keine lokale Zuginterpretation haben (z. B. bestimmte probabilistische oder graduierte Modalitäten), ohne das Spiel anzupassen.

Konsequenz

Lieferte ein anschauliches, oft konstruktives Verständnis von Wahrheit, klärt die Abhängigkeit von Wahlentscheidungen, ermöglicht die Analyse von Informationsgehalt und Strategien (z. B. unabhängige Logiken) und verbindet semantische Konzepte mit algorithmischen Suchproblemen.

Umkehrung

Im Kontrast zur tarskischen kompositionellen Semantik: Anstatt Wahrheitswerte durch strukturelle Induktion zuzuweisen, reduziert die spieltheoretische Semantik Wahrheit auf die Existenz von Gewinnstrategien — die Umkehrung des Blickwinkels macht den Unterschied zwischen operationaler und denotationeller Sicht deutlich.

Abgrenzung

Funktioniert direkt für Logiken, deren Junktoren und Quantoren sich in lokale Zugregeln übersetzen lassen; Erweiterungen (z. B. Fixpunktlogiken, probabilistische oder ressourcenbeschränkte Logiken) benötigen angepasste Spiele oder erweiterte Strategiebegriffe, um die intendierte Semantik zu erfassen.

Semantische Spannung

Spannungen bestehen zu proof-theoretischen Auffassungen (Wahrheit als Beweisbarkeit) und zu rein modeltheoretischen Sichtweisen, besonders hinsichtlich Uniformität und Konstruktivität von Zeugen: GTS betont Strategien, andere Sichtweisen betonen Bewertungen oder Herleitungen.

Synthese

Die spieltheoretische Semantik versteht Wahrheit als Ergebnis eines informationsstrukturierten Wettstreits: Durch Festlegen lokaler Zugregeln für syntaktische Konstrukte entstehen Spiele, deren Gewinnstrategien die semantischen Wahrheitsbedingungen exakt kodieren.