On the Provability Logic of Constructive Arithmetic: The Σ_1-provability logics of fragments of Heyting Arithmetic
Borja Sierra Miranda

Abstract:
We study provability logic in the context of intuitionistic arithmetics. In particular, we focus on the Σ1-provability logics of subtheories of Heyting Arithmetic HA. In order to do so, we analyze the tools developed by Visser and Zoethout and a method for constructing so-called slow provability predicates introduced by Visser. We also study a theory distinct from HA, iIΣ_1^+ , for which we can calculate its Σ_1-provability logic.