Axiomatizing modal inclusion logic and its variants

TL;DR

The paper tackles the problem of axiomatizing modal inclusion logic and two expressively equivalent extensions, ${\mathcal{ML}}(\subseteq)$, ${\mathcal{ML}}(\trianglepb)$, and ${\mathcal{ML}}(\trianglepbdot)$, within the framework of modal team semantics. It develops normal-form characterizations via Hintikka-style formulas and proves expressive completeness for the union-closed, empty-team, and bounded-bisimulation-invariant class ${\mathbb{U}}$, while establishing uniform interpolation and compactness as corollaries. A natural-deduction framework is introduced for each logic, with completeness shown by translating formulas to their normal forms; the systems for the inclusion-atom logic and the two might-operator variants are shown to be sound and complete. The results demonstrate that the three logics share the same expressive power and provide practical proof systems, contributing a foundational basis for reasoning about dependencies, possibilities, and information states in team semantics.

Abstract

We provide a complete axiomatization of modal inclusion logic - team-based modal logic extended with inclusion atoms. We review and refine an expressive completeness and normal form theorem for the logic, define a natural deduction proof system, and use the normal form to prove completeness of the axiomatization. Complete axiomatizations are also provided for two other extensions of modal logic with the same expressive power as modal inclusion logic: one augmented with a might operator and the other with a single-world variant of the might operator.

Theorems & Definitions (65)

• Definition 2.1
• Definition 2.2
• Proposition 2.3
• Proposition 2.4
• proof
• Corollary 2.5
• Example 2.6
• Lemma 2.7: yang2022
• Lemma 2.9
• proof