Nested Sequents for Horn-Characterizable Quantified Modal Logics with Equality via Reachability Rules

We introduce cut-free nested sequent systems for a broad class of quantified modal logics (QMLs). The QMLs we consider are semantically defined using relational models that assign both an inner and outer domain to each world. This rich model structure enables the specification of various QMLs by enforcing different frame conditions, including increasing, decreasing, constant, and empty domains, as well as general path conditions and seriality. We extend the usual notion of nested sequent to include signatures, i.e., multisets of terms, which let us naturally define rules capturing the aforementioned domain conditions. A distinctive feature of our nested sequent systems is the use of reachability rules--inference rules parameterized by formal grammars (viz., semi-Thue systems). These rules operate by propagating or consuming formulae or terms along certain paths within a nested sequent, where paths are encoded as strings generated by a parameterizing grammar. This paper is the first to provide sound and complete nested systems for QMLs semantically characterized by models using both inner and outer domains. We analyze the proof-theoretic properties of these systems, identify a number of admissible structural rules, establish the invertibility of all rules, and prove a non-trivial syntactic cut-elimination theorem. We also observe that the standard universal quantifier rule used in nested systems subsumes the Extended Barcan Rule, which forces nested systems to capture QMLs with constant outer domains.