Kripke semantics for provability logic GLP

AbstractA well-known polymodal provability logic GLP due to Japaridze is complete w.r.t. the arithmetical semantics where modalities correspond to reflection principles of restricted logical complexity in arithmetic. This system plays an important role in some recent applications of provability algebras in proof theory. However, an obstacle in the study of GLP is that it is incomplete w.r.t. any class of Kripke frames. In this paper we provide a complete Kripke semantics for GLP. First, we isolate a certain subsystem J of GLP that is sound and complete w.r.t. a nice class of finite frames. Second, appropriate models for GLP are defined as the limits of chains of finite expansions of models for J. The techniques involves unions of n-elementary chains and inverse limits of Kripke models. All the results are obtained by purely modal-logical methods formalizable in elementary arithmetic