THE ${\text{\Sigma }}_1 $-PROVABILITY LOGIC OF $HA^{\text{*}} $
Mohammad Ardeshir, Mojtaba Mojtahedi · Journal of Symbolic Logic · 2019
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 (Definition 2.4). We characterize the ${\text{\Sigma }}_1 $ -provability logic of $HA^{\text{*}} $ as a modal theory $iH_\sigma ^{\text{*}} $ (Definition 3.17).