2023/12/22 by Ana de Almeida Borges, Joost J. Joosten, Borges, Ana de Almeida +1
Computer Science · #Advanced Algebra and Logic #FOS: Mathematics #Logic (math.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2312.14727
openalex publication_date 2023/12/22 · openalex created_date 2023/12/26 · openalex updated_date 2026/07/28
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 2022 result by Mojtahedi, where an axiomatization for PL(HA) is provided. This axiomatization, although decidable, is of considerable complexity.