Fragments of existential second-order logic and logics with team semantics

Hoelzel, Matthias; Grädel, Erich (Thesis advisor); Hella, Lauri (Thesis advisor)

Aachen (2019, 2020)
Doktorarbeit

Dissertation, RWTH Aachen University, 2019

Kurzfassung

In dieser Arbeit werden verschiedene Fragmente von Logiken mit Teamsemantik und der existenziellen Logik zweiter Stufe untersucht. Die Fragmente, an denen wir interessiert sind, sind die unter Vereinigungen abgeschlossenen Fragmente dieser Logiken, Inklusionslogik mit eingeschränkter Stelligkeit sowie Varianten von Logiken mit Teamsemantik mit Abhängigkeitskonzepten, welche Elemente nur bis auf eine gegebene Äquivalenz unterscheiden können. Logiken mit Teamsemantik sind Erweiterungen der Prädikatenlogik, welche es erlauben Konzepte wie (Un-)Abhängigkeiten in Form von atomaren Aussagen auszudrücken. Dazu werden Formeln nicht mithilfe einer einzigen Variablenbelegung, sondern mit sogenannten Teams, Mengen von solchen Belegungen, ausgewertet. Es gibt eine starke Verbindung zwischen diesen Logiken und ESO, dem existenziellen Fragment der Logik zweiter Stufe, was sich in der Möglichkeit widerspiegelt, Formeln aus Logiken mit Teamsemantik als äquivalente ESO-Sätze mit einem zusätzlichen Prädikat für das Team und umgekehrt auszudrücken. Die Abhängigkeitslogik geht zurück auf Väänänen, und hat die gleiche Ausdrucksstärke wie das Fragment von ESO, in dem das Teamprädikat nur negativ verwendet wird. Die von Grädel und Väänänen, eingeführte Unabhängigkeitslogik hat die volle Ausdrucksstärke von ESO und ist, wie Galliani bewiesen hat, äquivalent zur Inklusion-Exklusionslogik, in deren Formeln sogenannte In- bzw.~Exklusionsatome verwendet werden können. Erlaubt man nur In- bzw.~nur Exklusionsatome, so spricht man von der In- bzw.~Exklusionslogik. Letztere entspricht genau der Abhängigkeitslogik, während Galliani und Hella gezeigt haben, dass die Inklusionslogik der größten Fixpunktlogik GFP entspricht. Zwar sind Formeln der Inklusionslogik abgeschlossen unter Vereinigungen, aber nicht jede unter Vereinigungen abgeschlossene Formel ist in der Inklusionslogik ausdrückbar. Dies führt zu der Frage, wie man solche Formeln charakterisieren kann. In dieser Arbeit wird bewiesen, dass unter Vereinigungen abgeschlossene ESO-Sätze syntaktisch durch die myopischen ESO-Sätze charakterisiert werden können. Dafür werden neuartige Inklusion-Exklusionsspiele definiert und untersucht, welche genau die Modellauswertungsspiele von ESO sind. Mithilfe dieser Spiele ist es auch möglich, ein entsprechendes syntaktisches Fragment von der Inklusions-Exklusionslogik zu identifizieren. Darüber hinaus ermöglichen es diese Spiele ein Atom zu definieren, welches, hinzugefügt zur Prädikatenlogik, ebenfalls dieses Fragment beschreibt. Ein weiteres bislang offenes Problem, mit dem sich diese Arbeit befasst, ist die Frage von Rönnholm, welches Fragment von GFP der Inklusionslogik mit eingeschränkter Stelligkeit gegenüber zu stellen ist. In dieser Arbeit wird ein solches Fragment vorgestellt und effektive Übersetzungen zu und von diesem Fragment werden angegeben. Schließlich betrachten wir Varianten von teamsemantischen Atomen, in denen Elemente nur noch bis auf eine gegebene Äquivalenz betrachtet werden können. Diesen neuen Logiken stellen wir äquivalente Fragmente von ESO gegenüber und untersuchen dessen Ausdrucksstärke auf unterschiedlichen Strukturklassen.

Einrichtungen

• Fachgruppe Mathematik [110000]
• Lehr- und Forschungsgebiet Mathematische Grundlagen der Informatik (Logik und Komplexität) [117220]