Strictly Positive Fragments of the Provability Logic of Heyting Arithmetic

We determine the strictly positive fragment ${\mathsf{Q}\mathsf{P}\mathsf{L}}^{+}(\mathsf{H}\mathsf{A})$ of the quantified provability logic $\mathsf{Q}\mathsf{P}\mathsf{L}(\mathsf{H}\mathsf{A})$ of Heyting Arithmetic. We show that ${\mathsf{Q}\mathsf{P}\mathsf{L}}^{+}(\mathsf{H}\mathsf{A})$ is decidable and that it coincides with ${\mathsf{Q}\mathsf{P}\mathsf{L}}^{+}(\mathsf{P}\mathsf{A})$, which is the strictly positive fragment of the quantified provability logic of of Peano Arithmetic. This positively resolves a previous conjecture of the authors. On our way to proving these results, we carve out the strictly positive fragment ${\mathsf{P}\mathsf{L}}^{+}(\mathsf{H}\mathsf{A})$ of the provability logic $\mathsf{P}\mathsf{L}(\mathsf{H}\mathsf{A})$ 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 2022 result by Mojtahedi, where an axiomatization for $\mathsf{P}\mathsf{L}(\mathsf{H}\mathsf{A})$ is provided. This axiomatization, although decidable, is of considerable complexity.