The $\Sigma$_1 Provability Logic of HA

TL;DR

This paper introduces a modal logic $H_{\sigma}$ that precisely captures the $\Sigma_1$-provability in Heyting Arithmetic (HA), proving its soundness, completeness, and decidability, and establishing the de Jongh property for HA with inconsistency.

Contribution

The paper defines the $H_{\sigma}$ modal theory as the $\Sigma_1$-provability logic of HA and proves its soundness, completeness, and decidability, advancing the understanding of HA's provability logic.

Findings

$H_{\sigma}$ is sound and complete for $\Sigma_1$ substitutions in HA.

$H_{\sigma}$ is a decidable modal theory.

HA + $\Box\bot$ has the de Jongh property.

Abstract

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