Nested Sequents for Quantified Modal Logics

TL;DR

This paper develops nested sequent calculi for various quantified modal logics, establishing their structural properties, soundness, completeness, and internal interpretability under certain conditions.

Contribution

It introduces and proves properties of nested sequent calculi for a range of quantified modal logics with different domain conditions, ensuring their structural soundness and completeness.

Findings

Calculi have height-preserving admissibility of weakening and contraction.

Cut rule is syntactically admissible in all calculi.

Calculi are equivalent to their axiomatic systems, ensuring soundness and completeness.

Abstract

This paper studies nested sequents for quantified modal logics. In particular, it considers extensions of the propositional modal logics definable by the axioms D, T, B, 4, and 5 with varying, increasing, decreasing, and constant domains. Each calculus is proved to have good structural properties: weakening and contraction are height-preserving admissible and cut is (syntactically) admissible. Each calculus is shown to be equivalent to the corresponding axiomatic system and, thus, to be sound and complete. Finally, it is argued that the calculi are internal -- i.e., each sequent has a formula interpretation -- whenever the existence predicate is expressible in the language.