可证性逻辑的ω-规则及其模型
摘要：关于证明逻辑$mathbf{GL}$的一个证明系统$mathsf{NGL}$的讨论，其中包含一个$omega$规则。我们展示了三种可传递Kripke框架的类别，即强验证$omega$规则的类别，弱验证$omega$规则的类别，以及由L"{o}b公式定义的类别，这些类别互不相同，但都能表征$mathbf{GL}$。这给出了一个证明系统$P$和Kripke框架类别$C$的例子，其中$P$相对于$C$是sound的，但不能通过$P$中的推导高度的简单归纳来证明sound性。我们还以代数的方式展示了$mathsf{NGL}$的Kripke完备性。作为推论，我们展示了由方程$Box xleqBoxBox x$和$igwedge\_{ninomega}Diamond^{n}1=0$定义的模态代数类别不是一个variety。
作者：Katsumi Sasaki and Yoshihito Tanaka
论文ID：2002.04782
分类：Logic
分类简称：math.LO
提交时间：2023-05-24