Nested Sequents for First-Order Modal Logics via Reachability Rules

10/03/2022
by   Tim S. Lyon, et al.
0

We introduce (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 two devices: 'reachability rules' and 'structural refinement.' Regarding the former device, we introduce reachability rules as special logical rules parameterized with formal grammars (viz. 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.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset