Predicate provability logic with non-modalized quantifiers

Abstract

Predicate modal formulas with non-modalized quantifiers (call them Q′-formulas) are considered as schemata of arithmetical formulas, where □ is interpreted as the provability predicate of some fixed correct extension T of arithmetic. A method of constructing 1) non-provable in T and 2) false arithmetical examples for Q′-formulas by Kripke-like countermodels of certain type is given. Assuming the means of T to be strong enough to solve the (undecidable) problem of derivability in Q′GL, the Q′-fragment of the predicate version of the logic GL, we prove the recursive enumerability of the sets of Q′-formulas all arithmetical examples of which are: 1) T-provable, 2) true. In. particular, the first one is shown to be exactly Q′GL and the second one to be exactly the Q′-fragment of the predicate version of Solovay's logic S.