Nested Sequents for First-Order Modal Logics via Reachability Rules

TL;DR

This paper develops novel nested sequent systems for first-order modal logics with various domain conditions, using reachability rules parameterized by formal grammars and structural refinement to derive these systems from semantics.

Contribution

It introduces the first cut-free nested sequent systems for first-order modal logics with general domain conditions, utilizing reachability rules and structural refinement techniques.

Findings

First nested sequent systems for first-order modal logics are established.

Reachability rules are parameterized by formal grammars for path checking.

Structural refinement effectively derives sequent systems from semantic models.

Abstract

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.