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

TL;DR

This paper develops cut-free nested sequent systems for a wide range of quantified modal logics with complex domain conditions, using reachability rules parameterized by formal grammars.

Contribution

It introduces the first sound and complete nested sequent systems for QMLs with models having inner and outer domains, employing reachability rules and signatures.

Findings

Proved soundness and completeness of the systems.

Established invertibility of all inference rules.

Proved a non-trivial cut-elimination theorem.

Abstract

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.