Strictly Positive Fragments of the Provability Logic of Heyting Arithmetic

Abstract

We determine the strictly positive fragment QPL+(HA) of the quantified provability logic QPL(HA) of Heyting Arithmetic. We show that QPL+(HA) is decidable and that it coincides with QPL+(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 PL+(HA) of the provability logic PL(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, where an axiomatization for PL(HA) is provided. This axiomatization, although decidable, is of considerable complexity.

Keywords

Provability logic, strictly positive logic, quantified modal logic, feasible fragments, Heyting Arithmetic

Citation

de Almeida Borges, A. & Joosten, J. J. (2024). Strictly positive fragments of the provability logic of Heyting Arithmetic. Studia Logica. URL: https://link.springer.com/content/pdf/10.1007/s11225-024-10152-y.pdf

@Article{AlmeidaBorges_Joosten2023_QRC1HA,
  author = "{de Almeida Borges}, Ana and Joosten, Joost J.",
  title = "Strictly Positive Fragments of the Provability Logic of {H}eyting {A}rithmetic",
  year = "2024",
  journal = "Studia Logica",
  url = "https://link.springer.com/content/pdf/10.1007/s11225-024-10152-y.pdf",
  keywords = "Provability logic, strictly positive logic, quantified modal logic, feasible fragments, Heyting Arithmetic",
  abstract = "We determine the strictly positive fragment QPL+(HA) of the quantified provability logic QPL(HA) of Heyting Arithmetic. We show that QPL+(HA) is decidable and that it coincides with QPL+(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 PL+(HA) of the provability logic PL(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, where an axiomatization for PL(HA) is provided. This axiomatization, although decidable, is of considerable complexity."
}