Intuitionistic grammar logics fuse constructive and multi-modal reasoning while permitting the use of converse modalities, serving as a generalization of standard intuitionistic modal logics. In this paper, we provide definitions of these logics as well as establish a suitable proof theory thereof. In particular, we show how to apply the structural refinement methodology to extract cut-free nested sequent calculi for intuitionistic grammar logics from their semantics. This method proceeds by first transforming the semantics of these logics into sound and complete labeled sequent systems, which we prove have favorable proof-theoretic properties such as syntactic cut-elimination. We then transform these labeled systems into nested sequent systems via the introduction of propagation rules and the elimination of structural rules. Our derived proof systems are then put to use, whereby we prove the conservativity of intuitionistic grammar logics over their modal counterparts, establish the general undecidability of these logics, and recognize a decidable subclass, referred to as "simple" intuitionistic grammar logics.
翻译:抽象的语法逻辑结合了建设性和多模式的推理,同时允许使用相反的模式,作为标准的直觉模式逻辑的概括性。在本文中,我们提供了这些逻辑的定义,并建立了适当的证据理论。特别是,我们展示了如何应用结构完善方法,从语义学语法逻辑中提取直觉学语法逻辑的切除式巢状序列计算法。这种方法首先将这些逻辑的语义转换为健全和完整的标记序列系统,我们证明这些逻辑具有超常的校准理论特性,例如合成切除法。我们随后通过引入传播规则和消除结构规则,将这些标记的系统转换为嵌入序列系统。然后,我们衍生的举证系统被投入使用,从而证明直觉语法语法逻辑相对于其语法逻辑的保守性,确立这些逻辑的一般不可减损性,并承认被称为“简单”直观语法逻辑的可分解子类。