论文标题
$ω$ rule用于可预订性的逻辑及其模型
An $ω$-rule for the logic of provability and its models
论文作者
论文摘要
在本文中，我们讨论了一个证明系统$ \ mathsf {ngl} $ for provibaly的逻辑$ \ mathbf {gl} $，该$配备了$ω$ -rule。我们显示了三类的及时旋转kripke框架，即强烈验证$ω$ -RULE的类，该类别弱验证了$ω$ -rule的类，以及由Löb公式定义的类，相互不同，而所有这些类别都是$ \ Mathbf {gl} $。这给出了一个证明系统$ p $和$ c $的kripke框架的示例，以便相对于$ c $，$ p $是合理的，但是声音性能无法通过简单的感应来证明$ p $。我们还以代数方式显示了$ \ mathsf {ngl} $的Kripke完整性。作为推论，我们表明，由等式定义的模态代数类别$ \ box x \ leq \ box \ box x $和$ \ bigWedge_ {n \inΩ} \ diamond^{n} 1 = 0 $不是品种。
In this paper, we discuss a proof system $\mathsf{NGL}$ for the logic $\mathbf{GL}$ of provability, which is equipped with an $ω$-rule. We show the three classes of transitive Kripke frames, the class which strongly validates the $ω$-rule, the class which weakly validates the $ω$-rule, and the class which is defined by the Löb formula, are mutually different, while all of them characterize $\mathbf{GL}$. This gives an example of a proof system $P$ and a class $C$ of Kripke frames such that $P$ is sound with respect to $C$ but the soundness cannot be proved by simple induction on the height of the derivations in $P$. We also show Kripke completeness of $\mathsf{NGL}$ in an algebraic manner. As a corollary, we show that the class of modal algebras which is defined by equations $\Box x\leq\Box\Box x$ and $\bigwedge_{n\inω}\Diamond^{n}1=0$ is not a variety.
