Mojtaba Mojtahedi
University of Tehran & IPM

Let $$\mathcal{PL}({\sf T},{\sf T}')$$ and $$\mathcal{PL}_{_{\Sigma_1}}({\sf T},{\sf T}')$$ respectively indicate the provability logic and $$\Sigma_1$$-provability logic of $${\sf T}$$ relative in $${\sf T}'.$$ In this paper we characterize the following relative provability logics: $$\mathcal{PL}_{_{\Sigma_1}}({\sf HA},\mathbb{N})$$, $$\mathcal{PL}_{_{\Sigma_1}}({\sf HA},{\sf PA})$$, $$\mathcal{PL}_{_{\Sigma_1}}({\sf HA}^*,\mathbb{N})$$, $$\mathcal{PL}_{_{\Sigma_1}}({\sf HA}^*,{\sf PA})$$, $$\mathcal{PL}({\sf PA},{\sf HA})$$, $$\mathcal{PL}_{_{\Sigma_1}}({\sf PA},{\sf HA})$$, $$\mathcal{PL}({\sf PA}^*,{\sf HA})$$, $$\mathcal{PL}_{_{\Sigma_1}}({\sf PA}^*,{\sf HA})$$, $$\mathcal{PL}({\sf PA}^*,{\sf PA})$$, $$\mathcal{PL}_{_{\Sigma_1}}({\sf PA}^*,{\sf PA})$$, $$\mathcal{PL}({\sf PA}^*,\mathbb{N})$$, $$\mathcal{PL}_{_{\Sigma_1}}({\sf PA}^*,\mathbb{N})$$. It turns out that all of these provability logics are decidable.

The notion of reduction for provability logics was first informally considered in a joint paper with Mohammad Ardeshir in 2015. In this paper, we formalize a generalization of this notion and provide several reductions of provability logics. The interesting fact is that $$\mathcal{PL}_{_{\Sigma_1}}({\sf HA},\mathbb{N})$$ is the hardest provability logic: the arithmetical completenesses of all provability logics listed above, as well as well-known provability logics like $$\mathcal{PL}({\sf PA},{\sf PA})$$, $$\mathcal{PL}({\sf PA},\mathbb{N})$$, $$\mathcal{PL}_{_{\Sigma_1}}({\sf PA},{\sf PA})$$, $$\mathcal{PL}_{_{\Sigma_1}}({\sf PA},\mathbb{N})$$ and $$\mathcal{PL}_{_{\Sigma_1}}({\sf HA},{\sf HA})$$, are all propositionally reducible to the arithmetical completeness of $$\mathcal{PL}_{_{\Sigma_1}}({\sf HA},\mathbb{N})$$.