Around provability logic (Q1035652)

In this paper, the author presents some results on algebraic and modal analysis of polynomial distortions of the standard provability predicate in Peano Arithmetic. The basic modal system for the distortions is shown to be K4.Grz, on which (the modal versions of) notions such as demonstrability predicate, Gödel's Second Incompleteness (g), and weak Löb axiom (wL) are characterized by certain specializations respectively. Among other interesting observations, the well-known modal system GL is shown to be axiomatized as K4.Grz+(g)+(wL), while the two axioms are, on K4.Grz, independent from each other. The paper includes also a description of the dual category of K4.Grz-algebras and a short review of relational and topological semantics for these modal systems.