一阶模态逻辑的有束片段：(不)可判定性

量化模态逻辑提供了一种自然的逻辑语言，用于对模态态度进行推理，同时保留量化的丰富性以指代域上的谓词。但在多数模型类上，该逻辑的大多数片段是不可判定的。多年来，仅少数片段（如单子片段）被证明是可判定的。本文受早期关于知何/知为何/知何事认知逻辑研究的启发，研究将量词与模态词捆绑在一起的片段。与量化模态逻辑一贯的情况一样，域在各世界间是否保持不变会产生显著差异。特别地，我们证明在常域解释下，即便仅使用一元谓词，∀□ 束也是不可判定的，而 ∃□ 束是可判定的。另一方面，在递增域解释下，我们使用无限制谓词的 ∀□ 与 ∃□ 束均得到可判定性。在这些情形下，我们还获得了运行于 PSPACE 的基于表证的程序。我们进一步表明，∃□ 束无法区分常域与递增域解释。