Reasoning about dependence and independence : teams and multiteams

Wilke, Richard Marlon; Grädel, Erich (Thesis advisor); Lakemeyer, Gerhard (Thesis advisor); Väänänen, Jouko (Thesis advisor)

Aachen : RWTH Aachen University (2021, 2022)
Dissertation / PhD Thesis

Dissertation, RWTH Aachen University, 2021

Abstract

Team semantics is the mathematical basis of modern logics for reasoning about dependence and independence. Its core feature is that formulae are evaluated against a set of assignments, called a team. This approach dates back to Hodges (1997) who used it to provide a compositional semantics for independence friendly logic. Building on this idea, Väänänen (2007) suggested that dependencies between variables should be treated as atomic propositions instead of annotations of quantifiers. However, being based on sets, team semantics can only be used to reason about the presence or absence of data. Multiteam semantics instead takes multiplicities of data into account and is based on multisets of assignments, called multiteams. In this thesis we systematically develop and study logics with multiteam semantics. The specific definitions of the multiteam semantics of logical operators are justified by postulates which reflect natural properties that a logic with multiteam semantics should satisfy. Furthermore, the natural extension of the game theoretic semantics (GTS) of logics with team semantics to the multiteam setting is equivalent to the GTS of our semantics. A wide spectrum of logics with multiteam semantics is explored with regard to their properties and expressive power. Some of these results resemble what is known from team semantics but require new techniques. On the other side, there are also interesting differences. For instance, inclusion-exclusion logic in team semantics is expressively equivalent to independence logic, and thus has the full power of existential second-order logic. In multiteam semantics, however, independence cannot be expressed by any combination of downwards closed and union closed atoms. Further, we establish connections between logics with multiteam semantics, logics with team semantics and variants of existential second-order logic. Moreover, we investigate model-checking games for logics with multiteam semantics. A further contribution of this thesis concerns characterisations of the union closed fragments of logics with team semantics and existential second-order logic, resolving problems posed by Galliani and Hella (2013). In particular, we develop novel model-checking games for team semantics, called inclusion-exclusion games, and use these to construct a specific dependency atom, whose first-order closure captures all union closed properties of teams that are definable in existential second-order logic. The final contribution of this thesis concerns logics with inquisitive semantics which, as observed by Ciardelli (2016), have striking analogies with logics with team semantics. We introduce an inquisitive monadic second-order logic (InqMSO) and give a precise characterisation of Ciardelli’s inquisitive first-order logic (InqBQ) as a fragment of InqMSO.

Institutions

• UnRAVeL Research Training Group [080060]
• Department of Mathematics [110000]
• Mathematical Fundamentals of Computer Science (Logic and Complexity) Teaching and Research Area [117220]