Nested Sequents for First-Order Modal Logics via Reachability Rules
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.
Cite
@article{arxiv.2210.00789,
title = {Nested Sequents for First-Order Modal Logics via Reachability Rules},
author = {Tim S. Lyon},
journal= {arXiv preprint arXiv:2210.00789},
year = {2023}
}