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.

翻译：暂无翻译