Document type
ArticleVersion
Published versionPublication date
Publication license
Please use this identifier to cite or link to this item: https://hdl.handle.net/2445/228610
Strictly Positive Fragments of the Provability Logic of Heyting Arithmetic
Journal Title
Director/Tutor
Additional contribution
Journal ISSN
Volume Title
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 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.
Related resource
Subject
Subject (English)
Citation
Collections
Citation
ALMEIDA BORGES, Ana de and JOOSTEN, Joost J. Strictly Positive Fragments of the Provability Logic of Heyting Arithmetic. Studia Logica. 2024. ISSN 0039-3215. [consulted: 9 of October of 2026]. Available at: https://hdl.handle.net/2445/228610