A cut-free proof system for a predicate extension of the logic of provability

Yoshihito Tanaka


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

AMS subject classification: 03F05, 03F45

Słowa kluczowe: Provability logic, predicate logic, cut-free system

[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.

Czasopismo ukazuje się w sposób ciągły on-line.
Pierwotną formą czasopisma jest wersja elektroniczna.