Kripke semantics for provability logic GLP. (English) Zbl 1223.03046
Summary: The well-known polymodal provability logic \(\mathbf {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 \(\mathbf {GLP}\) is that it is incomplete w.r.t. any class of Kripke frames. In this paper we provide a complete Kripke semantics for \(\mathbf {GLP}\). First, we isolate a certain subsystem \(\mathbf {J}\) of \(\mathbf {GLP}\) that is sound and complete w.r.t. a nice class of finite frames. Second, appropriate models for \(\mathbf {GLP}\) are defined as the limits of chains of finite expansions of models for \(\mathbf {J}\). The techniques involve 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.
MSC:
| 03F45 | Provability logics and related algebras (e.g., diagonalizable algebras) |
| 03B45 | Modal logic (including the logic of norms) |
References:
| [1] | Beklemishev, L.; Joosten, J.; Vervoort, M., A finitary treatment of the closed fragment of Japaridze’s provability logic, Journal of Logic and Computation, 15, 4, 447-463 (2005) · Zbl 1080.03038 |
| [2] | Beklemishev, L. D., Provability algebras and proof-theoretic ordinals, I, Annals of Pure and Applied Logic, 128, 103-123 (2004) · Zbl 1048.03045 |
| [3] | Beklemishev, L. D., Reflection principles and provability algebras in formal arithmetic, Uspekhi Matematicheskikh Nauk, 60, 2, 3-78 (2005), (in Russian) English translation in: Russian Mathematical Surveys, 60(2): 197-268, 2005 · Zbl 1097.03054 |
| [4] | L.D. Beklemishev, On the Craig interpolation and the fixed point property for GLP. Logic Group Preprint Series 262, University of Utrecht, December 2007. http://preprints.phil.uu.nl/lgps/; L.D. Beklemishev, On the Craig interpolation and the fixed point property for GLP. Logic Group Preprint Series 262, University of Utrecht, December 2007. http://preprints.phil.uu.nl/lgps/ |
| [5] | Blackburn, P.; de Rijke, M.; Venema, Y., Modal Logic (2001), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0988.03006 |
| [6] | Boolos, G., The Logic of Provability (1993), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0891.03004 |
| [7] | Chagrov, A.; Zakharyaschev, M., Modal Logic (1997), Clarendon Press: Clarendon Press Oxford · Zbl 0871.03007 |
| [8] | Goldblatt, R. I., Metamathematics of modal logic, Part I, Reports on Mathematical Logic, 6, 41-78 (1976) · Zbl 0356.02016 |
| [9] | Goldblatt, R. I., Metamathematics of modal logic, Part II, Reports on Mathematical Logic, 7, 21-52 (1976) · Zbl 0356.02017 |
| [10] | T. Icard, III, Models of the polymodal provability logic. M.Sc. Thesis, ILLC, University of Amsterdam, http://www.illc.uva.nl/Publications/ResearchReports/MoL-2008-06.text.pdf, 2008; T. Icard, III, Models of the polymodal provability logic. M.Sc. Thesis, ILLC, University of Amsterdam, http://www.illc.uva.nl/Publications/ResearchReports/MoL-2008-06.text.pdf, 2008 |
| [11] | K.N. Ignatiev, The closed fragment of Dzhaparidze’s polymodal logic and the logic of \(\Sigma_1\)-conservativity, in: ITLI Prepublication Series X-92-02, University of Amsterdam, 1992; K.N. Ignatiev, The closed fragment of Dzhaparidze’s polymodal logic and the logic of \(\Sigma_1\)-conservativity, in: ITLI Prepublication Series X-92-02, University of Amsterdam, 1992 |
| [12] | Ignatiev, K. N., On strong provability predicates and the associated modal logics, The Journal of Symbolic Logic, 58, 249-290 (1993) · Zbl 0795.03082 |
| [13] | G.K. Japaridze, The modal logical means of investigation of provability. Thesis in Philosophy, Moscow, 1986 (in Russian); G.K. Japaridze, The modal logical means of investigation of provability. Thesis in Philosophy, Moscow, 1986 (in Russian) |
| [14] | G.K. Japaridze, The polymodal logic of provability, in: Intensional Logics and Logical Structure of Theories: Material from the fourth Soviet-Finnish Symposium on Logic, Telavi, May 20-24, 1985, Metsniereba, Tbilisi, 1988. pp. 16-48 (in Russian); G.K. Japaridze, The polymodal logic of provability, in: Intensional Logics and Logical Structure of Theories: Material from the fourth Soviet-Finnish Symposium on Logic, Telavi, May 20-24, 1985, Metsniereba, Tbilisi, 1988. pp. 16-48 (in Russian) · Zbl 0725.03038 |
| [15] | Shapirovsky, I., PSPACE-decidability of Japaridze’s polymodal logic, (Areces, C.; Goldblatt, R., Advances in Modal Logic, vol. 7 (2008), King’s College Publications), 289-304 · Zbl 1244.03073 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
