Von semantischen Spielen zu Kalkülen, und retour

Dieses Projekt befindet sich an der Schnittstelle zwischen den Forschungsgebieten Logik und Spieltheorie. Die Logik beschäftigt sich unter anderem mit dem Verhältnis zwischen der syntaktischen Form einer Aussage und den semantischen Strukturen, wie etwa Graphen, Datenbanken etc., in denen die Aussage zutrifft. Man kann hierbei einerseits danach fragen, ob eine Aussage in einer bestimmten Struktur zutrifft man spricht dann von der Wahrheit der Aussage oder, anderseits, ob sie in einer ganzen Klasse von möglichen Strukturen zutrifft dann spricht man von der logischen Gültigkeit der Aussage. Interessanterweise lassen sich beide Konzepte oft mittels formaler Zweipersonenspiele charakterisieren. Diese Spiele heißen semantische Spiele bzw. Beweisbarkeitsspiele. Ein wichtiges Konzept in beiden Spielen (und in der Spieltheorie im Allgemeinen) ist das einer Gewinnstrategie. Damit meint man eine Strategie, mit der wir in einem Spiel gegen jeden Gegner gewinnen können, ganz egal welche Züge er oder sie wählt. Zu einer gegebenen Aussage und Struktur gibt es nun in semantischen Spielen genau dann eine Gewinnstrategie, wenn die Aussage in der Struktur wahr ist. In Beweisbarkeitsspielen hingegen gibt es zu einer gegebenen Aussage genau dann eine Gewinnstrategie, wenn die Aussage logisch gültig ist. Intuitiv sollte es möglich sein von einem semantischen Spiel zu einem Beweisbarkeitsspiel überzugehen, indem man von der konkret gewählten Struktur abstrahiert. In der Tat ist dies in zumindest einem Fall (für die mehrwertige Lukasiewicz-Logik) bereits gelungen. Dort hatte das so erhaltene Beweisbarkeitsspiel noch eine weitere nützliche Eigenschaft: Es ließ sich direkt in einen analytischen Kalkül übersetzen. Ein solcher analytischer Kalkül ist ein vielseitid verwendbares Werkzeug zur formalen Herleitung logisch gültiger Aussagen. Das Ziel des vorliegenden Projektes ist es nun dieses Ergebnis zu verallgemeinern und auf systematische Art semantische Spiele in Beweisbarkeitsspiele zu übersetzen. In einem weiteren Schritt sollen aus den so erhaltenen Beweisbarkeitsspielen analytische Kalküle entstehen. Weiters wollen wir auch den umgekehrten Weg beschreiten und analytische Kalküle erst in Beweisbarkeitsspiele übersetzen, um anschließend aus diesen Beweisbarkeitsspielen semantische Spiele zu gewinnen. Unser Ansatz unterscheidet sich von früheren Arbeiten darin, dass wir nicht spezielle Fälle von Spielen oder Kalkülen betrachten wollen, sondern eine viel allgemeinere Übersetzung ins Auge fassen, welche sich auf ganze Klassen von Kalkülen und Spielen anwenden lässt.

Dieses Projekt war an der Schnittstelle zwischen Logik und Spieltheorie angesiedelt. Die Logik beschäftigt sich unter anderem mit dem Verhältnis zwischen der syntaktischen Form einer Aussage und den semantischen Strukturen (Interpretationen, Modellen) in denen die Aussage zutrifft. Man kann hierbei einerseits danach fragen, ob eine Aussage in einer bestimmten Struktur zutrifft - man spricht dann von der Wahrheit der Aussage - oder, anderseits, ob sie in einer ganzen Klasse von möglichen Strukturen zutrifft - dann spricht man von der logischen Gültigkeit der Aussage. Interessanterweise lassen sich beide Konzepte oft mittels formaler Zweipersonenspiele charakterisieren. Diese Spiele heißen semantische Spiele bzw. Beweisbarkeitsspiele. Ein wichtiges Konzept in beiden Spielen (und in der Spieltheorie im Allgemeinen) ist das einer Gewinnstrategie. Damit meint man eine Strategie, mit der wir in einem Spiel gegen jeden Gegner gewinnen können, ganz egal welche Züge er oder sie wählt. Zu einer gegebenen Aussage und Struktur gibt es nun in semantischen Spielen genau dann eine Gewinnstrategie, wenn die Aussage in der Struktur wahr ist. In Beweisbarkeitsspielen hingegen gibt es zu einer gegebenen Aussage genau dann eine Gewinnstrategie, wenn die Aussage logisch gültig ist. Intuitiv sollte es möglich sein von einem semantischen Spiel zu einem Beweisbarkeitsspiel überzugehen, indem man von der konkret gewählten Struktur abstrahiert. In der Tat ist dies in zumindest einem Fall (für die mehrwertige Lukasiewicz-Logik) bereits vor Projektbeginn gelungen. Dort hatte das so erhaltene Beweisbarkeitsspiel noch eine weitere nützliche Eigenschaft: Es ließ sich direkt in einen analytischen Kalkül übersetzen. Ein solcher analytischer Kalkül ist ein vielseitig verwendbares Werkzeug zur formalen Herleitung logisch gültiger Aussagen. Das Ziel des vorliegenden Projektes war es dieses Ergebnis zu verallgemeinern und auf systematische Art semantische Spiele in Beweisbarkeitsspiele und weiter in analytische Kalküle zu übersetzen. Um dieses Ziel zu erreichen, haben wir die beschriebene Methodik auf verschiedene Typen von Logik angewendet. Auf diese Weise konnten wir ein sogenanntes Wahrheitsvergleichsspiel für die Gödel-Logik, eine wichtige Fuzzy-Logik, in ein Beweisspiel transferieren, das wiederum in einen analytischen Kalkül eines speziellen Formats mit Vergleichsformelpaaren als Basisobjekten umgewandelt werden kann. Eine weitere Verallgemeinerung dieser Art betrifft die hybride Modallogik, die eine ganzen Familie von Logiken umfasst, die es ermöglichen, verschiedene mögliche Zustände explizit zu benennen und darauf zu verweisen. Wir haben unseren spiel-basierten Ansatz auch erfolgreich auf Logiken angewendet, die formales Schließen über Gruppenpolarisierung in sozialen Netzwerken unterstützen, und haben so entsprechende semantische Spiele, Beweisbarkeitsspiele sowie analytische Kalküle entwickelt. Des Weiteren haben wir die Methodik angepasst und verfeinert, um einen allgemeinen Rahmen bereitzustellen, der auf eine Vielzahl von Logiken anwendbar ist, um so semantische Spiele zunächst in Beweisbarkeitsspiele und schließlich diese Spiele in analytische Beweissysteme umzuwandeln.