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})\).