 Finally, one can of course study predicate provability logic. The language is that of predicate logic without function symbols, together with the operator \(\Box\). Here, the situation becomes much more complex than in the case of propositional provability logic. To begin with, the straightforward quantified version of GL does not have the fixed-point property, is not complete with respect to any class of Kripke frames, and is not arithmetically complete with respect to Peano Arithmetic (Montagna, 1984). The question then arises: Is there any nicely axiomatized predicate provability logic that is adequate, proving exactly the valid principles of provability? The answer is unfortunately a resounding no: Vardanyan (1986) has proved on the basis of ideas by Artemov (1985a) that the set of sentences of predicate provability logic all of whose realizations are provable in PA is not even recursively enumerable but \(\Pi^0_2\)-complete, so it has no reasonable axiomatization. Visser and De Jonge (2006) showed that there is no escape from Vardanyan’s theorem by proving a generalization: For a wide range of arithmetical theories \(T\), the set of sentences of predicate provability logic all of whose realizations are provable in \(T\) turns out to be \(\Pi^0_2\)-complete as well. 