Strictly Positive Fragments of the Provability Logic of Heyting Arithmetic

Abstract

We determine the strictly positive fragment ${\mathsf{QPL}}^{+}(\mathsf{HA})$ of the quantified provability logic $\mathsf{QPL}(\mathsf{HA})$ of Heyting Arithmetic. We show that ${\mathsf{QPL}}^{+}(\mathsf{HA})$ is decidable and that it coincides with ${\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. On our way to proving these results, we carve out the strictly positive fragment ${\mathsf{PL}}^{+}(\mathsf{HA})$ of the provability logic $\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 2022 result by Mojtahedi, where an axiomatization for $\mathsf{PL}(\mathsf{HA})$ is provided. This axiomatization, although decidable, is of considerable complexity.