ARITHMETICAL INTERPRETATIONS AND KRIPKE FRAMES OF PREDICATE MODAL LOGIC OF PROVABILITY

Solovay 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 A -theory T extending I Σ1, and (3) Th(QGL) â Fr(QGL) â© PL(T) for any recursively enumerable 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).