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 de ned by K and the Lob formula 2(2p  p)  2p, NQGL does not have the Lob 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 nite.

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

S. Artemov and G. Dzhaparidze, Finite Kripke models and predicate logics of provability, The Journal of Symbolic Logic 55 (1990), 1090-1098.

A. Avron, On modal systems having arithmetical interpretations, The Journal of Symbolic Logic 49 (1984), 935-942.

G. Boolos, The logic of provability, Cambridge University Press, 1993.

R. Goldblatt, Mathematics of Modality, volume 43 of CSLI Lecture Notes, CSLI Publications, 1993.

J. Y. Halpern and Y. Moses, A guide to completeness and complexity for modal logics of knowledge and beliefs, Arti cial Intelligence 54 (1992), 319-379.

T. Kurahashi, Arithmetical interpretations and Kripke frames of predicate modal logic of provability, The Review of Symbolic Logic 6 (2013), 129-146.

D. Leivant, On the proof theory of modal logic for arithmetic provability, The Journal of Symbolic Logic 46 (1981), 531-538.

F. Montagna, The predicate modal logic of provability, Notre Dame Journal of Formal Logic 25 (1984), 179-189.

Y. Schwarz and G. Tourlakis, On the proof-theory of a rst-order extension of GL,Logic and Logical Philosophy 23 (2014), 329-363.

K. Segerberg, A model existence theorem in in nitary propositional modal logic, Journal of Philosophical Logic 23 (1994), 337-367.

Y. Tanaka, Model existence in non-compact modal logic, Studia Logica 67 (2001), 61-73.

Y. Tanaka, Some proof systems for predicate common knowledge logic, Reports on Mathematical Logic 37 (2003), 79-100.

S. Valentini, The modal logic of provability, Journal of Philosophical Logic 12 (1983), 471-476.

F. Wolter, First order common knowledge logics, Studia Logica 65 (2000), 249-271.

R. E. Yavorsky, On arithmetical completeness of rst order logics of provability, In F. Wolter, H. Wansin, and M. Zakharyaschev, editors, Advances in Modal Logic, volume 3, CSLI Publications, 2001, pp. 1-16.

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