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.

翻译：我们首次提出适用于递增、递减、常域和空域以及所谓一般路径条件和序列性的无切割嵌套矢列系统。这些系统通过两种机制实现：'可达性规则'与'结构精化'。就前者而言，我们引入以形式文法（即半图厄系统类型）参数化的特殊逻辑规则作为可达性规则，这些规则通过在嵌套矢列中沿特定路径传播公式和/或检查数据是否存在来运作，其中路径被编码为由参数化文法生成的字符串。就后者而言，结构精化是一种相对较新的方法，通过消除结构/关系规则、引入可达性规则并执行符号翻译，从标记系统（最终从语义获得）中提取嵌套矢列系统。我们因此展示了如何将该方法扩展至一阶模态逻辑的设定，并揭示了可达性规则如何自然产生于该方法的应用过程。