On Prenex Fragment of Provability Logic with Quantifiers on Proofs

We consider a fragment of provability logic with quantifiers on proofs that consists of formulas with no occurrences of quantifiers in the scope of the proof predicate. By definition, a logic ql is the set of formulas that are true in the standard model of arithmetic under every interpretation based on the standard Gödel proof predicate. We describe Kripke-style semantics for the logic ql and prove the corresponding completeness theorem. For the case of injective arithmetical interpretations, the decidability is proved.