Nested Sequents for Quasi-transitive Modal Logics
Sonia Marin, Paaras Padhiar
TL;DR
The paper addresses how to design proof-theoretic systems for modal logics extended with path axioms using nested sequents, focusing on a quasi-transitive fragment where $l=0$ and $\\mathsf{4}^{n}: \\Diamond^n A \\supset \\Diamond A$. It develops a constructive cut-elimination procedure for these nested-sequent systems and proposes a modular formulation that allows mixing axioms as separate rule sets without cross-dependency. The results clarify the correspondence between path axioms and frame conditions and provide a flexible, compositional approach to proof systems beyond standard $\\mathsf{K}$. This has practical impact for automated reasoning about modal logics with constrained transitivity properties, enabling modular, cut-free proof search in the quasi-transitive fragment.
Abstract
Previous works by Goré, Postniece and Tiu have provided sound and cut-free complete proof systems for modal logics extended with path axioms using the formalism of nested sequent. Our aim is to provide (i) a constructive cut-elimination procedure and (ii) alternative modular formulations for these systems. We present our methodology to achieve these two goals on a subclass of path axioms, namely quasi-transitivity axioms.