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)
Dissertation / PhD Thesis

Dissertation, RWTH Aachen University, 2019

Abstract

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.