An \(\omega \)-Rule for the Logic of Provability and Its Models

In this paper, we discuss semantical properties of the logic \(\textbf{GL}\) $\mathbf{GL}$ of provability. The logic \(\textbf{GL}\) $\mathbf{GL}$ is a normal modal logic which is axiomatized by the the Löb formula \( \Box (\Box p\supset p)\supset \Box p \) $\square (\square p\supset p)\supset \square p$ , but it is known that \(\textbf{GL}\) $\mathbf{GL}$ can also be axiomatized by an axiom \(\Box p\supset \Box \Box p\) $\square p\supset \square \square p$ and an \(\omega \) $\omega$ -rule \((\Diamond ^{*})\) $({◊}^{\ast })$ which takes countably many premises \(\phi \supset \Diamond ^{n}\top \) $\varphi \supset {◊}^n\top$ \((n\in \omega )\) $(n\in \omega )$ and returns a conclusion \(\phi \supset \bot \) $\varphi \supset \perp$ . We show that the class of transitive Kripke frames which validates \((\Diamond ^{*})\) $({◊}^{\ast })$ and the class of transitive Kripke frames which strongly validates \((\Diamond ^{*})\) $({◊}^{\ast })$ are equal, and that the following three classes of transitive Kripke frames, the class which validates \((\Diamond ^{*})\) $({◊}^{\ast })$ , the class which weakly validates \((\Diamond ^{*})\) $({◊}^{\ast })$ , and the class which is defined by the Löb formula, are mutually different, while all of them characterize \(\textbf{GL}\) $\mathbf{GL}$ . This gives an example of a proof system P and a class C of Kripke frames such that P is sound and complete 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 the proof system with \((\Diamond ^{*})\) $({◊}^{\ast })$ in an algebraic manner. As a corollary, we show that the class of modal algebras which is defined by equations \(\Box x\le \Box \Box x\) $\square x\le \square \square x$ and \(\bigwedge _{n\in \omega }\Diamond ^{n}1=0\) ${\bigwedge }_{n\in \omega }{◊}^{n}1=0$ is not a variety.