Nested Sequents for Quasi-transitive Modal Logics

TL;DR

This paper develops a constructive cut-elimination procedure and modular proof systems for quasi-transitive modal logics using nested sequents, enhancing the theoretical foundations of these logics.

Contribution

It introduces a new constructive cut-elimination method and modular formulations specifically for quasi-transitive modal logics within the nested sequent framework.

Findings

Successful cut-elimination procedure for quasi-transitive modal logics

Modular proof systems for these logics

Enhanced understanding of nested sequent calculus applications

Abstract

Previous works by Gor\'e, 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.