Slow and Ordinary Provability for Peano Arithmetic

Abstract

The notion of slow provability for Peano Arithmetic ($\mathsf{PA}$) was introduced by S.D. Friedman, M. Rathjen, and A. Weiermann. They studied the slow consistency statement $\mathrm{Con}_{\mathsf{s}}$ that asserts that a contradiction is not slow provable in $\mathsf{PA}$. They showed that the logical strength of $\mathsf{PA}+\mathrm{Con}_{\mathsf{s}}$ lies strictly between that of $\mathsf{PA}$ and $\mathsf{PA}$ together with its ordinary consistency: $\mathsf{PA}\subsetneq \mathsf{PA}+\mathrm{Con}_{\mathsf{s}}\subsetneq \mathsf{PA}+\mathrm{Con}$. This paper is a further investigation into slow provability and its interplay with ordinary provability in $\mathsf{PA}$. We study three variants of slow provability. The associated consistency statement of each of these yields a theory that lies strictly between $\mathsf{PA}$ and $\mathsf{PA}+\mathrm{Con}$ in terms of logical strength. We investigate Turing-Feferman progressions based on these variants of slow provability. We show that for our three notions, the Turing-Feferman progression reaches $\mathsf{PA}+\mathrm{Con}$ in a different numbers of steps, namely $\varepsilon_0$, $\omega$, and $2$. For each of the three slow provability predicates, we also determine its joint provability logic with ordinary $\mathsf{PA}$-provability.