Nested Sequents for Intuitionistic Multi-Modal Logics: Modularity, Cut-Elimination, and Undecidability

TL;DR

This paper develops nested sequent calculi for intuitionistic multi-modal logics, introduces a unifying structural rule, and demonstrates the undecidability of validity problems through a reduction from classical grammar logics.

Contribution

It presents a uniform syntactic proof of cut-admissibility for IGLs, introduces the shift rule, and establishes the undecidability of validity for these logics via a faithful embedding.

Findings

Unified the shift rule for modal frame conditions.

Proved cut-admissibility and completeness of the nested calculi.

Showed validity problem undecidability for IGLs via reduction from CGLs.

Abstract

We introduce and study single-conclusioned nested sequent calculi for a broad class of intuitionistic multi-modal logics known as "intuitionistic grammar logics (IGLs)." These logics serve as the intuitionistic counterparts of classical grammar logics, and subsume standard intuitionistic modal and tense logics, including IK and IKt extended with combinations of the T, B, 4, 5, and D axioms. We analyze fundamental invertibility and admissibility properties of our calculi and introduce a novel structural rule, called the "shift rule," which unifies standard structural rules arising from modal frame conditions into a single rule. This rule enables a purely syntactic proof of cut-admissibility that is uniform over all IGLs, and yields completeness of our nested calculi as a corollary. Finally, we define a negative translation that constitutes a faithful embedding of classical grammar logics (CGLs) into IGLs, witnessed by proof transformations between multi-conclusioned and single-conclusioned nested sequent proofs for CGLs and IGLs, respectively. This reduces the general validity problem for CGLs to that of IGLs. The general validity problem over a class C of logics asks: given a logic L in C and a formula A, is A valid in L? As this problem is known to be undecidable for CGLs, our reduction implies its undecidability for IGLs as well.