The $\Sigma$_1 Provability Logic of HA

Abstract

In this paper we introduce a modal theory $H_{\sigma }$, which is sound and complete for arithmetical $\Sigma$_1 substitutions in $\mathbf{HA}$, in other words, we will show that $H_{\sigma }$ is the $\Sigma$_1-provability logic of $\mathbf{HA}$. Moreover we will show that $H_{\sigma }$ is decidable. As a by-product of these results, we show that $\mathbf{HA}+\square \perp$ has de Jongh property.