Hard Provability Logics

Abstract

Let $\mathcal{P}\mathcal{L}(\mathsf{T},{\mathsf{T}}^{\prime })$ and ${\mathcal{P}\mathcal{L}}_{{\Sigma }_1}(\mathsf{T},{\mathsf{T}}^{\prime })$ respectively indicates the provability logic and ${\Sigma }_1$-provability logic of $\mathsf{T}$ relative in ${\mathsf{T}}^{\prime }$. In this paper we characterize the following relative provability logics: ${\mathcal{P}\mathcal{L}}_{{\Sigma }_1}(\mathsf{HA},\mathbb{N})$, ${\mathcal{P}\mathcal{L}}_{{\Sigma }_1}(\mathsf{HA},\mathsf{PA})$, ${\mathcal{P}\mathcal{L}}_{{\Sigma }_1}({\mathsf{HA}}^{\ast },\mathbb{N})$, ${\mathcal{P}\mathcal{L}}_{{\Sigma }_1}({\mathsf{HA}}^{\ast },\mathsf{PA})$, $\mathcal{P}\mathcal{L}(\mathsf{PA},\mathsf{HA})$, ${\mathcal{P}\mathcal{L}}_{{\Sigma }_1}(\mathsf{PA},\mathsf{HA})$, $\mathcal{P}\mathcal{L}({\mathsf{PA}}^{\ast },\mathsf{HA})$, ${\mathcal{P}\mathcal{L}}_{{\Sigma }_1}({\mathsf{PA}}^{\ast },\mathsf{HA})$, $\mathcal{P}\mathcal{L}({\mathsf{PA}}^{\ast },\mathsf{PA})$, ${\mathcal{P}\mathcal{L}}_{{\Sigma }_1}({\mathsf{PA}}^{\ast },\mathsf{PA})$, $\mathcal{P}\mathcal{L}({\mathsf{PA}}^{\ast },\mathbb{N})$, ${\mathcal{P}\mathcal{L}}_{{\Sigma }_1}({\mathsf{PA}}^{\ast },\mathbb{N})$ (see Table \ref{Table-Theories}). It turns out that all of these provability logics are decidable. The notion of {\em reduction} for provability logics, first informally considered in \cite{reduction}. In this paper, we formalize a generalization of this notion (\Cref{Definition-Reduction-PL}) and provide several reductions of provability logics (See diagram \ref{Diagram-full}). The interesting fact is that ${\mathcal{P}\mathcal{L}}_{{\Sigma }_1}(\mathsf{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{P}\mathcal{L}(\mathsf{PA},\mathsf{PA})$, $\mathcal{P}\mathcal{L}(\mathsf{PA},\mathbb{N})$, ${\mathcal{P}\mathcal{L}}_{{\Sigma }_1}(\mathsf{PA},\mathsf{PA})$, ${\mathcal{P}\mathcal{L}}_{{\Sigma }_1}(\mathsf{PA},\mathbb{N})$ and ${\mathcal{P}\mathcal{L}}_{{\Sigma }_1}(\mathsf{HA},\mathsf{HA})$ are all propositionally reducible to the arithmetical completeness of ${\mathcal{P}\mathcal{L}}_{{\Sigma }_1}(\mathsf{HA},\mathbb{N})$.