A cut-free proof system for a predicate extension of the logic of provability
cytuj
pobierz pliki
RIS BIB ENDNOTEChoose format
RIS BIB ENDNOTEA cut-free proof system for a predicate extension of the logic of provability
Publication date: 06.09.2018
Reports on Mathematical Logic, 2018, Number 53, pp. 97 - 109
https://doi.org/10.4467/20842589RM.18.006.8839Authors
A cut-free proof system for a predicate extension of the logic of provability
In this paper, we introduce a proof system NQGL for a Kripke complete predicate extension of the logic GL of provability. While GL is defined by K and the Lӧb formula □(□p ⊃p) ⊃□p, NQGL does not have the L¨ob formula as its axiom, but has a non-compact rule, that is, a derivation rule with countably many premises, instead. We show that NQGL enjoys cut admissibility and is complete with respect to the class of Kripke frames such that for each world, the supremum of the length of the paths from the world is finite.
Received 21 February 2018
[1] S. Artemov and G. Dzhaparidze, Finite Kripke models and predicate logics of provability, The Journal of Symbolic Logic 55 (1990), 1090–1098.
[2] A. Avron, On modal systems having arithmetical interpretations, The Journal of Symbolic Logic 49 (1984), 935–942.
[3] G. Boolos, The logic of provability, Cambridge University Press, 1993.
[4] R. Goldblatt, Mathematics of Modality, vol. 43 of CSLI Lecture Notes, CSLI Publications, Stanford, 1993.
[5] J.Y. Halpern and Y. Moses, A guide to completeness and complexity for modal logics of knowledge and beliefs, Artificial Intelligence 54 (1992), 319–379.
[6] T. Kurahashi, Arithmetical interpretations and Kripke frames of predicate modal logic of provability, The Review of Symbolic Logic 6 (2013), 129–146.
[7] D. Leivant, On the proof theory of modal logic for arithmetic provability, The Journal of Symbolic Logic 46 (1981), 531–538.
[8] F. Montagna, The predicate modal logic of provability, Notre Dame Journal of Formal Logic 25 (1984), 179–189.
[9] Y. Schwarz and G. Tourlakis, On the proof-theory of a first-order extension of GL, Logic and Logical Philosophy 23 (2014), 329–363.
[10] K. Segerberg, A model existence theorem in infinitary propositional modal logic, Journal of Philosophical Logic 23 (1994), 337–367.
[11] Y. Tanaka, Model existence in non-compact modal logic, Studia Logica 67 (2001), 61–73.
[12] Y. Tanaka, Some proof systems for predicate common knowledge logic, Reports on Mathematical Logic 37 (2003), 79–100.
[13] S. Valentini, The modal logic of provability, Journal of Philosophical Logic 12 (1983), 471–476.
[14] F. Wolter, First order common knowledge logics, Studia Logica 65 (2000), 249–271.
[15] R.E. Yavorsky, On arithmetical completeness of first order logics of provability, In: F. Wolter, H. Wansin and M. Zakharyaschev, editors, vol. 3 of Advances in Modal Logic, CSLI Publications, 2001, pp. 1–16.
Information: Reports on Mathematical Logic, 2018, Number 53, pp. 97 - 109
Article type: Original article
Titles:
A cut-free proof system for a predicate extension of the logic of provability
A cut-free proof system for a predicate extension of the logic of provability
Kyushu Sangyo University 2-3-1 Matsukadai, Higashi-ku, Fukuoka 813-8503, Japan
Published at: 06.09.2018
Article status: Open
Licence: CC BY-NC-ND
Percentage share of authors:
Article corrections:
-Publication languages:
EnglishView count: 1517
Number of downloads: 1046