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

Hoelzel, Matthias; Grädel, Erich; Hella, Lauri

doi:HT020455198

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

Hoelzel, Matthias^RWTH*

2019 & 2020

Verantwortlichkeitsangabevorgelegt von Matthias Hoelzel, M.Sc.

ImpressumAachen 2019

Umfang1 Online-Ressource (ii, 103 Seiten) : Illustrationen, Diagramme

Dissertation, RWTH Aachen University, 2019

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University 2020

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Grädel, Erich (Thesis advisor)^RWTH* ; Hella, Lauri (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2019-12-10

Online
DOI: 10.18154/RWTH-2020-05121
URL: https://publications.rwth-aachen.de/record/789282/files/789282.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
closure properties (frei) ; existential second-order logic (frei) ; greatest fixed-point logics (frei) ; logics with team semantics (frei) ; model-checking games (frei)

Thematische Einordnung (Klassifikation)
DDC: 510

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.

In this thesis different fragments of logics with team semantics and of existential second-order logic will be studied. The fragments we are interested in are the union closed fragments of these logics, inclusion logic of restricted arity and variants of logics with team semantics using dependency concepts which can distinguish elements only up to a given equivalence. Logics with team semantics are extensions of first-order logic that allow to express concepts like (in)dependence in the form of atomic statements. To this end formulae are not evaluated against a single assignment but against so-called teams which are sets of such assignments. There is a strong connection between these logics and ESO, the existential fragment of second-order logic, which is reflected in the possibility to express formulae of logics with team semantics as equivalent ESO-sentences with an additional predicate for the team and vice versa. Dependence logic goes back to Väänänen and has the same expressive power as the fragment of ESO in which the team predicate occurs only negatively. Independence logic, introduced by Grädel und Väänänen, has, as Galliani has proved, the full expressive power of ESO and is equivalent to inclusion-exclusion logic, in whose formulae so-called in- resp.~exclusion atoms can be used. If one allows only in- or only exclusion atoms, one speaks of the in- or exclusion logic. The latter corresponds exactly to dependence logic, while Galliani and Hella have shown that the inclusion logic corresponds to the greatest fixed-point logic GFP. Even though formulae of inclusion logic are closed under unions, not every union closed formulae is expressible in inclusion logic. This leads to the question how such formulae can be characterised. In this thesis, it will be proved that union closed ESO-sentences can be characterised syntactically by myopic ESO-sentences. Towards this end, we will define and study novel inclusion-exclusion games that are precisely the model-checking games of ESO. Using these games it is also possible to identify a corresponding syntactical fragment of inclusion-exclusion logic. Furthermore, these games give rise to the definition of an atom that, when added to first-order logic, also precisely captures the union-closed fragment. Another, so far open, problem that this thesis deals with is the question of Rönnholm, which fragment of GFP corresponds to the inclusion logic of restricted arity. In this thesis such a fragment is going to be introduced and effective translations between it and the restricted inclusion logic and vice versa are provided. Finally, we study variants of logics with dependency concepts, which can distinguish elements only up to a given equivalence. We juxtapose these new logics with equivalent fragments of ESO and study their expressive powers on different classes of structures.

OpenAccess:
PDF
(additional files)