  This paper presents the logic QRC$_1$, which is a strictly positive fragment
of quantified modal logic. The intended reading of the diamond modality is that
of consistency of a formal theory. Predicate symbols are interpreted as
parametrized axiomatizations. We prove arithmetical soundness of the logic
QRC$_1$ with respect to this arithmetical interpretation.
  Quantified provability logic is known to be undecidable. However, the
undecidability proof cannot be performed in our signature and arithmetical
reading. We conjecture the logic QRC$_1$ to be arithmetically complete. This
paper takes the first steps towards arithmetical completeness by providing
relational semantics for QRC$_1$ with a corresponding completeness proof. We
also show the finite model property, which implies decidability.
