论文标题
通过可及性规则的一阶模态逻辑的嵌套序列
Nested Sequents for First-Order Modal Logics via Reachability Rules
论文作者
论文摘要
我们介绍了第一个无剪切的嵌套序列系统，用于一阶模态逻辑，该系统可以接受增加，减少，恒定和空的域以及所谓的一般路径条件和序列性。我们通过两个设备获得此类系统：“可及性规则”和“结构改进”。关于以前的设备，我们将可及性规则作为特殊的逻辑规则引入参数，该规则用正式的语法（即半thue系统的类型）参数，该规则是通过传播公式和/或检查是否沿嵌套顺序中的某些路径进行操作的，该路径是否沿着某些路径存在，其中路径是由字符串编码为通过参数化的语法来构成字符串的。关于后一种设备，结构改进是一种相对较新的方法，用于通过消除结构/关系规则，引入可及性规则，然后进行著名翻译，从标记系统中提取嵌套序列系统（最终是从语义中获得的）。因此，我们演示了如何将此方法扩展到一阶模态逻辑的设置，并揭示应用此方法自然产生的可及性规则。
We introduce the first cut-free nested sequent systems for first-order modal logics that admit increasing, decreasing, constant, and empty domains along with so-called general path conditions and seriality. We obtain such systems by means of two devices: 'reachability rules' and 'structural refinement'. Regarding the former device, we introduce reachability rules as special logical rules parameterized with formal grammars (viz. types of semi-Thue systems) that operate by propagating formulae and/or checking if data exists along certain paths within a nested sequent, where paths are encoded as strings generated by a parameterizing grammar. Regarding the latter device, structural refinement is a relatively new methodology used to extract nested sequent systems from labeled systems (which are ultimately obtained from a semantics) by means of eliminating structural/relational rules, introducing reachability rules, and then carrying out a notational translation. We therefore demonstrate how this method can be extended to the setting of first-order modal logics, and expose how reachability rules naturally arise from applying this method.
