Kripke semantics for provability logic GLP

11 years 5 months ago
Kripke semantics for provability logic GLP
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. This paper is devoted to a modal-logical study of polymodal provability logic GLP introduced by Giorgi Japarid...
Lev D. Beklemishev
Added 08 Dec 2010
Updated 08 Dec 2010
Type Journal
Year 2010
Where APAL
Authors Lev D. Beklemishev
Comments (0)