论文标题
通过结构改进的直觉语法逻辑的嵌套序列
Nested Sequents for Intuitionistic Grammar Logics via Structural Refinement
论文作者
论文摘要
直觉语法逻辑融合了建设性和多模式推理，同时允许使用匡威模态，并作为标准直觉模态逻辑的概括。在本文中，我们提供了这些逻辑的定义，并建立了其合适的证明理论。特别是，我们展示了如何应用结构改进方法来从其语义中提取直觉语法逻辑的无切割嵌套序列。该方法通过首先将这些逻辑的语义转换为声音和完整标记的序列系统来进行，我们证明这具有有利的证明理论属性，例如句法切割 - 淘汰。然后，我们通过引入传播规则和消除结构规则将这些标记的系统转换为嵌套的序列系统。然后使用我们的派生证明系统，在此过程中，我们证明了直觉语法逻辑在其模态对应物上的保守性，建立了这些逻辑的一般不可证明性，并识别可决定的子类，被称为“简单”直觉语法逻辑。
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.
