Strictly Positive Fragments of the Provability Logic of Heyting Arithmetic

We determine the strictly positive fragment \(\textsf{QPL}^+(\textsf{HA})\) ${\mathsf{QPL}}^{+}(\mathsf{HA})$ of the quantified provability logic \(\textsf{QPL}(\textsf{HA})\) $\mathsf{QPL}(\mathsf{HA})$ of Heyting Arithmetic. We show that \(\textsf{QPL}^+(\textsf{HA})\) ${\mathsf{QPL}}^{+}(\mathsf{HA})$ is decidable and that it coincides with \(\textsf{QPL}^+(\textsf{PA})\) ${\mathsf{QPL}}^{+}(\mathsf{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})\) ${\mathsf{PL}}^{+}(\mathsf{HA})$ of the provability logic \(\textsf{PL}(\textsf{HA})\) $\mathsf{PL}(\mathsf{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})\) $\mathsf{PL}(\mathsf{HA})$ is provided. This axiomatization, although decidable, is of considerable complexity.