The $\Sigma_1$-Provability Logic of HA*

TL;DR

This paper characterizes the $oldsymbol{ ext{Σ}_1}$-provability logic of the theory HA* derived from Heyting Arithmetic, using a specific modal theory ${ ext{iH}}_oldsymbol{ extsigma}^*$, advancing understanding of intuitionistic provability.

Contribution

The paper provides a complete modal logic characterization of the $ ext{Σ}_1$-provability logic of HA*, a new theory based on Heyting Arithmetic and box translation.

Findings

Identifies the modal theory ${ ext{iH}}_ extsigma^*$ as the $ ext{Σ}_1$-provability logic of HA*

Establishes a formal correspondence between HA* and the modal logic ${ ext{iH}}_ extsigma^*$

Advances the understanding of provability logic in intuitionistic arithmetic contexts.

Abstract

For the Heyting Arithmetic HA, HA* is defined as the theory $\{A\mid {\sf HA}\vdash A^{\Box}\}$, where $A^{\Box}$ is called the box translation of $A$. We characterize the $\Sigma_1$-provability logic of HA* as a modal theory ${\sf iH}_\sigma^*$.