Axiomatizing modal inclusion logic and its variants

TL;DR

This paper develops a complete axiomatization for modal inclusion logic and its variants, establishing foundational proof systems and normal form theorems for these expressive modal logics.

Contribution

It provides the first complete axiomatizations for modal inclusion logic and two of its extensions, enhancing understanding of their proof-theoretic properties.

Findings

Complete axiomatization of modal inclusion logic established

Normal form and expressive completeness theorems refined

Axiomatizations extended to logic variants with might operators

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.