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

• Autorzy: Tanaka Y.

Identyfikatory

DOI

10.4467/20842589RM.18.006.8839

• Języki publikacji: EN

Abstrakty

EN

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¨ob 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.

Słowa kluczowe

EN

provability logic; predicate logic; cut-free system

• Wydawca: Wydawnictwo Uniwersytetu Jagiellońskiego
• Czasopismo: Reports on Mathematical Logic
• Rocznik: 2018
• Tom: Vol. 53
• Strony: 97--109
• Opis fizyczny: Bibliogr. 15 poz.

Twórcy

autor

Tanaka Y.

• Kyushu Sangyo University 2-3-1 Matsukadai, Higashi-ku Fukuoka 813-8503, Japan

Bibliografia

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

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2018).