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.

翻译：我们引入并研究了一类称为“直觉性语法逻辑（IGLs）”的广泛直觉性多模态逻辑的单结论嵌套矢列演算。这些逻辑作为经典语法逻辑的直觉性对应物，涵盖了标准直觉性模态与时态逻辑，包括扩展了T、B、4、5和D公理组合的IK和IKt。我们分析了这些演算的基本可逆性与可容许性性质，并引入了一种名为“移位规则”的新型结构规则，该规则将源自模态框架条件的标准结构规则统一为单一规则。这一规则使得对所有IGLs统一的切割可容许性的纯语法证明成为可能，并由此推出嵌套矢列演算的完备性。最后，我们定义了一个负翻译，它构成了经典语法逻辑（CGLs）到IGLs的忠实嵌入，并通过CGLs的多结论嵌套矢列证明与IGLs的单结论嵌套矢列证明之间的证明变换加以体现。这一归约将CGLs的一般有效性判定问题约简为IGLs的一般有效性判定问题。针对逻辑类C的一般有效性判定问题询问：给定C中的逻辑L与公式A，A在L中是否有效？由于已知CGLs的这一问题是不可判定的，我们的归约表明IGLs的这一问题同样是不可判定的。