The $Σ$_1 Provability Logic of HA
In this paper we introduce a modal theory $H_σ$, which is sound and complete for arithmetical $Σ$_1 substitutions in ${\bf HA}$, in other words, we will show that $H_σ$ is the $Σ$_1-provability logic of ${\bf HA}$. Moreover we will show that $H_σ$ is decidable. As a by-product of these results, we show that ${\bf HA} + \Box\bot$ has de Jongh property.
math.LO↗