谓词模态逻辑的不动点性质

众所周知，可证性命题模态逻辑 $\mathbf{GL}$ 满足 de Jongh-Sambin 不动点性质。另一方面，Montagna 证明了谓词模态系统 $\mathbf{QGL}$（即 $\mathbf{GL}$ 的自然变体）丧失了不动点性质。在本文中，我们讨论谓词模态逻辑中不动点性质的若干版本。首先，我们证明包括 $\mathbf{NQGL}$ 在内的 $\mathbf{QGL}$ 的若干扩张不具有不动点性质。其次，我们证明逻辑 $\mathbf{QK} + \Box^{n+1} \bot$ 的不动点定理。作为推论，我们得到传递且有限高度的 Kripke 框架类 $\mathsf{FH}$ 局部满足不动点性质。我们还展示了 $\mathbf{NQGL}$ 的 Craig 插值性质的失效。最后，我们给出公式在 $\mathbf{QGL}$ 中具有不动点的一个充分条件。