Reasoning about dependence and independence : teams and multiteams

Wilke, Richard Marlon; Grädel, Erich; Lakemeyer, Gerhard; Väänänen, Jouko

doi:HT021288607

Reasoning about dependence and independence : teams and multiteams

Wilke, Richard Marlon^RWTH*

2021 & 2022

Verantwortlichkeitsangabevorgelegt von Richard Marlon Wilke, M.Sc.

ImpressumAachen : RWTH Aachen University 2021

Umfang1 Online-Ressource : Illustrationen

Dissertation, RWTH Aachen University, 2021

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University 2022

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Grädel, Erich (Thesis advisor)^RWTH* ; Lakemeyer, Gerhard (Thesis advisor) ; Väänänen, Jouko (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2021-07-23

Online
DOI: 10.18154/RWTH-2022-02743
URL: https://publications.rwth-aachen.de/record/842872/files/842872.pdf

Einrichtungen

Projekte

GRK 2236 - UNRAVEL - UNcertainty and Randomness in Algorithms, VErification, and Logic (282652900) (282652900)

Inhaltliche Beschreibung (Schlagwörter)
dependence (frei) ; existential second-order logic (frei) ; independence (frei) ; multiteam semantics (frei) ; team semantics (frei)

Thematische Einordnung (Klassifikation)
DDC: 510

Kurzfassung
Team-Semantik ist die mathematische Grundlage moderner Logiken für Abhängigkeit und Unabhängigkeit. Ihr Kernmerkmal ist, dass Formeln über einer Menge von Zuweisungen ausgewertet werden, die als Team bezeichnet wird. Dieser Ansatz geht auf Hodges (1997) zurück, der ihn verwendet hat, um eine kompositionelle Semantik der Independence Friendly Logic anzugeben. Aufbauend auf dieser Idee schlug Väänänen (2007) vor, dass Abhängigkeiten zwischen Variablen als atomare Aussagen anstelle von Annotationen von Quantoren behandelt werden sollen. Da die Team-Semantik auf Mengen basiert, kann sie ausschließlich über das Vorhandensein oder Fehlen von Daten sprechen. Multiteam-Semantik berücksichtigt die Multiplizitäten der Daten und basiert auf Multimengen von Zuweisungen, genannt Multiteams. In dieser Dissertation entwickeln und untersuchen wir systematisch Logiken mit Multiteam-Semantik. Die Definition der Multiteam-Semantik wird durch bestimmte Postulate begründet, die natürliche Eigenschaften widerspiegeln, die eine Logik mit Multiteam-Semantik erfüllen sollte. Des Weiteren entspricht die natürliche Erweiterung der spieltheoretischen Semantik (GTS) von Logiken mit Team-Semantik um Multiplizitäten der GTS unserer Semantik. Wir erforschen ein breites Spektrum von Logiken mit Multiteam-Semantik hinsichtlich ihrer Eigenschaften und Ausdrucksstärke. Ein paar der erzielten Ergebnisse ähneln dem, was aus der Team-Semantik bekannt ist, erfordern aber neue Techniken. Die Formalismen weisen auch interessante Unterschiede auf. Beispielsweise ist die Inklusions-Exklusions Logik in der Team-Semantik äquivalent zur Unabhängigkeitslogik und hat damit die volle Ausdrucksstärke der existentiellen Logik zweiter Stufe. In der Multiteam-Semantik hingegen kann Unabhängigkeit nicht durch eine beliebige Kombination von nach unten abgeschlossenen und unter Vereinigung abgeschlossenen Atomen ausgedrückt werden. Darüber hinaus vergleichen wir die Multiteam-Semantik mit der Team-Semantik und einer Variante der existentiellen Logik zweiter Stufe. Ferner werden Modellprüfungsspiele für Logiken mit Multiteam-Semantik entwickelt. Ein weiterer Beitrag dieser Dissertation betrifft die Charakterisierung der unter Vereinigung abgeschlossenen Fragmente von Logiken mit Team-Semantik und existentieller Logik zweiter Stufe. Dies beantwortet offene Fragen von Galliani und Hella (2013). Insbesondere entwickeln wir neuartige Modellprüfungsspiele für die Team-Semantik, genannt inclusion-exclusion games, und verwenden diese, um ein Atom zu definieren, dessen Abschluss unter den logischen Junktoren und Quantoren erster Stufe alle unter Vereinigung abgeschlossenen Eigenschaften von Teams, die in der existentiellen Logik zweiter Stufe definierbar sind, erfasst. Der letzte Beitrag dieser Dissertation behandelt Logiken mit inquisitiver Semantik, welche, wie von Ciardelli (2016) beobachtet wurde, auffallende Parallelen zu Logiken mit Team-Semantik haben. Wir führen eine inquisitive monadische Logik zweiter Stufe (InqMSO) ein und geben eine präzise Charakterisierung von Ciardellis inquisitiver Logik erster Stufe (InqBQ) als ein Fragment von InqMSO an.

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.

OpenAccess:
PDF
(additional files)