Predicate counterparts of modal logics of provability: High undecidability and Kripke incompleteness

In this paper, the predicate counterparts, defined both axiomatically and semantically by means of Kripke frames, of the modal propositional logics GL, Grz, wGrz and their extensions are considered. It is proved that the set of semantical consequences on Kripke frames of every logic between QwGrz and QGL.3 or between QwGrz and QGrz.3 is Pi(l )(l)-hard even in languages with three (sometimes, two) individual variables, two (sometimes, one) unary predicate letters, and a single proposition letter. As a corollary, it is proved that infinite families of modal predicate axiomatic systems, based on the classical first-order logic and the modal propositional logics GL, Grz, wGrz are not Kripke complete. Both Pi(l )(l)-hardness and Kripke incompleteness results of the paper do not depend on whether the logics contain the Barcan formula.