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