The Σ1-provability logic of HA

In this paper we introduce a modal theory iHσ which is sound and complete for arithmetical Σ1-interpretations in HA, in other words, we will show that iHσ is the Σ1-provability logic of HA. Moreover we will show that iHσ is decidable. As a by-product of these results, we show that HA+□⊥ has de Jongh property.