An \omega-rule for the logic of provability and its models

arXiv2002.04782MaRDI QIDQ6334635FDOQ6334635

Authors: Katsumi Sasaki, Yoshihito Tanaka 

Publication date: 11 February 2020

Abstract: In this paper, we discuss a proof system $mathsfNGL$ for the logic $mathbfGL$ of provability, which is equipped with an $omega$-rule. We show the three classes of transitive Kripke frames, the class which strongly validates the $omega$-rule, the class which weakly validates the $omega$-rule, and the class which is defined by the L"{o}b formula, are mutually different, while all of them characterize $mathbfGL$. 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 $mathsfNGL$ in an algebraic manner. As a corollary, we show that the class of modal algebras which is defined by equations $BoxxleqBoxBoxx$ and $$ is not a variety.

Mathematics Subject Classification ID

Provability logics and related algebras (e.g., diagonalizable algebras) (03F45) Boolean algebras with additional operations (diagonalizable algebras, etc.) (06E25)

This page was built for publication: An $\omega$-rule for the logic of provability and its models

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6334635)