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.

翻译：本文研究量化模态逻辑的嵌套矢列。具体而言，本文考虑了由公理D、T、B、4和5可定义的命题模态逻辑的扩展，这些扩展分别涉及变化域、递增域、递减域和恒定域。每个演算都被证明具有良好的结构性质：弱化和收缩是高度保持可容许的，并且切割是（语法上）可容许的。本文还表明每个演算都等价于相应的公理系统，从而证明了其可靠性与完备性。最后，本文论证了当存在谓词可在语言中表达时，这些演算是内部的——即每个矢列都具有公式解释。