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可定义的命题模态逻辑在可变域、递增域、递减域和常域下的扩展。每个演算被证明具有良好的结构性质：弱化和收缩是高度保持可容许的，切割是（语法上）可容许的。每个演算被证明等价于相应的公理化系统，因此是可靠且完全的。最后，论证了当存在谓词可在语言中表达时，这些演算是内部的——即每个矢列具有公式解释。