Short Proofs for Slow Consistency

Abstract

Let $\mathrm{Con}(\mathbf{T})\upharpoonright x$ denote the finite consistency statement "there are no proofs of contradiction in $\mathbf{T}$ with $\le x$ symbols". For a large class of natural theories $\mathbf{T}$, Pudlák has shown that the lengths of the shortest proofs of $\mathrm{Con}(\mathbf{T})\upharpoonright n$ in the theory $\mathbf{T}$ itself are bounded by a polynomial in $n$. At the same time he conjectures that $\mathbf{T}$ does not have polynomial proofs of the finite consistency statements $\mathrm{Con}(\mathbf{T}+\mathrm{Con}(\mathbf{T}))\upharpoonright n$. In contrast we show that Peano arithmetic ($\mathbf{PA}$) has polynomial proofs of $\mathrm{Con}(\mathbf{PA}+{\mathrm{Con}}^{\ast }(\mathbf{PA}))\upharpoonright n$, where ${\mathrm{Con}}^{\ast }(\mathbf{PA})$ is the slow consistency statement for Peano arithmetic, introduced by S.-D. Friedman, Rathjen and Weiermann. We also obtain a new proof of the result that the usual consistency statement $\mathrm{Con}(\mathbf{PA})$ is equivalent to ${\epsilon }_0$ iterations of slow consistency. Our argument is proof-theoretic, while previous investigations of slow consistency relied on non-standard models of arithmetic.

References in corpus (3)

• Slow and Ordinary Provability for Peano Arithmetic
• Proof Lengths for Instances of the Paris-Harrington Principle
• Slow Reflection