We investigate several consequences of inclusion relations between quantified provability logics. Moreover, we give a necessary and sufficient condition for the inclusion relation between quantified provability logics with respect to \ arithmetical interpretations.

We determine the strictly positive fragment \(\textsf{QPL}^+(\textsf{HA})\) of the quantified provability logic \(\textsf{QPL}(\textsf{HA})\) of Heyting Arithmetic. We show that \(\textsf{QPL}^+(\textsf{HA})\) is decidable and that it coincides with \(\textsf{QPL}^+(\textsf{PA})\), which is the strictly positive fragment of the quantified provability logic of of Peano Arithmetic. This positively resolves a previous conjecture of the authors described in [ 14 ]. On our way to proving these results, we carve out the strictly positive fragment \(\textsf{PL}^+(\textsf{HA})\) of the provability logic \(\textsf{PL}(\textsf{HA})\) of Heyting Arithmetic, provide (...) a simple axiomatization, and prove it to be sound and complete for two types of arithmetical interpretations. The simple fragments presented in this paper should be contrasted with a recent result by Mojtahedi [ 43 ], where an axiomatization for \(\textsf{PL}(\textsf{HA})\) is provided. This axiomatization, although decidable, is of considerable complexity. (shrink)