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}⊊\mathsf{PA}+{\mathrm{Con}}_{\mathsf{s}}⊊\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 ${\epsilon }_0$, $\omega$, and $2$. For each of the three slow provability predicates, we also determine its joint provability logic with ordinary $\mathsf{PA}$-provability.

46 pages

Cited by in corpus (3)

• Proof Lengths for Instances of the Paris-Harrington Principle
• Short Proofs for Slow Consistency
• The Absorption Law, or How to Kreisel a Hilbert-Bernays-Löb