On the Provability Logic of HA

TL;DR

This paper axiomatizes the provability logic of Heyting Arithmetic (HA), proves its decidability, and introduces provability models combining Kripke semantics with propositional provability for extended modal logics.

Contribution

It provides the first axiomatization and decidability proof for the provability logic of HA, and introduces provability models as a new semantic framework.

Findings

Axiomatization of HA's provability logic

Decidability of the provability logic of HA

Introduction of provability models combining Kripke semantics with propositional provability

Abstract

We axiomatize the provability logic of $\HA$ and prove its decidability. Furthermore, we axiomatize the preservativity and relative admissibility relations for several modal logics extending iK4. A principal technical tool is the introduction of a new type of semantics, termed \emph{provability models}, for modal logics extending iGL. This semantics combines elements of standard Kripke semantics with provability in propositional modal logics.