Kripke semantics for provability logic GLP

Abstract

A well-known polymodal provability logic GLP is complete w.r.t. the arithmetical semantics where modalities correspond to reflection principles of restricted logical complexity in arithmetic [9, 5, 8]. This system plays an important role in some recent applications of provability algebras in proof theory [2, 3]. 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.