# name
Strictly Positive Fragments of the Provability Logic of Heyting Arithmetic

# metadata.dc.description.abstract[].value
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 described in [14]. 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 [43], where an axiomatization for PL(HA) is provided. This axiomatization, although decidable, is of considerable complexity.

# metadata.dc.rights[].value
cc by (c) Almeida Borges, Ana de et al., 2024

# metadata.dc.source[].value
Articles publicats en revistes (Filosofia)

# metadata.dc.title[].value
Strictly Positive Fragments of the Provability Logic of Heyting Arithmetic