Abstract

For the Heyting Arithmetic HA, $HA^{\text{*}} $ is defined [14, 15] as the theory $\left\{ {A|HA \vdash A^\square } \right\}$, where $A^\square $ is called the box translation of A. We characterize the ${\text{\Sigma }}_1 $-provability logic of $HA^{\text{*}} $ as a modal theory $iH_\sigma ^{\text{*}} $.