Review of Symbolic Logic 6 (1):1-18 (2013)
AbstractSolovay proved the arithmetical completeness theorem for the system GL of propositional modal logic of provability. Montagna proved that this completeness does not hold for a natural extension QGL of GL to the predicate modal logic. Let Th(QGL) be the set of all theorems of QGL, Fr(QGL) be the set of all formulas valid in all transitive and conversely well-founded Kripke frames, and let PL(T) be the set of all predicate modal formulas provable in Tfor any arithmetical interpretation. Montagna’s results are described as Th(QGL) ⊊ (Fr(QGL), PL(PA) ⊈ Fr(QGL), and Th(QGL) ⊊ PL(PA). In this paper, we prove the following three theorems: (1) Fr(QGL) ⊈ PL(T) for any Σ1-sound recursively enumerable extension T of I Σ1, (2) PL(T) ⊈ Fr(QGL) for any recursively enumerable S1755020312000275_inline1 A -theory T extending I Σ1, and (3) Th(QGL) ⊊ Fr(QGL) ∩ PL(T) for any recursively enumerable S1755020312000275_inline2 A -theory T extending I Σ2. To prove these theorems, we use iterated consistency assertions and nonstandard models of arithmetic, and we improve Artemov’s lemma which is used to prove Vardanyan’s theorem on the Π0 2-completeness of PL(T)
Similar books and articles
Added to PP
Historical graph of downloads
Citations of this work
On Predicate Provability Logics and Binumerations of Fragments of Peano Arithmetic.Taishi Kurahashi - 2013 - Archive for Mathematical Logic 52 (7-8):871-880.
On Inclusions Between Quantified Provability Logics.Taishi Kurahashi - 2022 - Studia Logica 110 (1):165-188.
References found in this work
Transfinite Recursive Progressions of Axiomatic Theories.Solomon Feferman - 1962 - Journal of Symbolic Logic 27 (3):259-316.
Induction Rules, Reflection Principles, and Provably Recursive Functions.Lev D. Beklemishev - 1997 - Annals of Pure and Applied Logic 85 (3):193-242.
The Predicate Modal Logic of Provability.Franco Montagna - 1984 - Notre Dame Journal of Formal Logic 25 (2):179-189.
Provability: The Emergence of a Mathematical Modality.George Boolos & Giovanni Sambin - 1991 - Studia Logica 50 (1):1 - 23.