Kripke semantics for provability logic GLP

A well-known polymodal provability logic 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 is that it is incomplete w.r.t. any class of Kripke frames. In this paper we provide a complete Kripke semantics for . First, we isolate a certain subsystem of that is sound and complete w.r.t. a nice class of finite frames. Second, appropriate models for are defined as the limits of chains of finite expansions of models for . 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.