On the Provability Logic of HA
Logic
2026-01-05 v4
Abstract
We axiomatize the provability logic of 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.
Keywords
Cite
@article{arxiv.2206.00445,
title = {On the Provability Logic of HA},
author = {Mojtaba Mojtahedi},
journal= {arXiv preprint arXiv:2206.00445},
year = {2026}
}