Decidable and enumerable predicate logics of provability

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 ₁-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 ⁿ A.