The ${\Sigma }_1$-Provability Logic of HA*

Mohammad Ardeshir, Mojtaba Mojtahedi

For the Heyting Arithmetic HA, HA* is defined as the theory $\{A\mid \mathsf{HA}⊢A^{\square }\}$, where $A^{\square }$ is called the box translation of $A$. We characterize the ${\Sigma }_1$-pr…