Abstract

Predicate modal formulas are considered as schemata of arithmetical formulas, where is interpreted as the standard formula of provability in a fixed sufficiently rich theory T in the language of arithmetic. QL T(T) and QL T are the sets of schemata of T-provable and true formulas, correspondingly. Solovay's well-known result — construction an arithmetical counterinterpretation by Kripke countermodel — is generalized on the predicate modal language; axiomatizations of the restrictions of QL T(T) and QL T by formulas, which contain no variables different from x, are given by means of decidable prepositional bimodal systems; under the assumption that T is 1-complete, there is established the enumerability of the restrictions of QL T(T) and QL T by: 1) formulas in which the domains of different occurrences of don't intersect and 2) formulas of the form n A.