可证性逻辑的 ω-规则及其模型

本文讨论可证性逻辑 $\mathbf{GL}$ 的一个配备 $\omega$-规则的证明系统 $\mathsf{NGL}$。我们证明三类传递 Kripke 框架——强验证 $\omega$-规则的类、弱验证 $\omega$-规则的类，以及由 Löb 公式定义的类——互不相同，而它们都刻画 $\mathbf{GL}$。这给出了一个证明系统 $P$ 与 Kripke 框架类 $C$ 的实例，使得 $P$ 关于 $C$ 是可靠的，但该可靠性不能通过对 $P$ 中推导高度作简单归纳来证明。我们还以代数方式证明了 $\mathsf{NGL}$ 的 Kripke 完备性。作为推论，我们证明了由方程 $\Box x\leq\Box\Box x$ 与 $\bigwedge_{n\in\omega}\Diamond^{n}1=0$ 定义的模态代数类不是一个簇。