Axiomatizing provable $n$-provability

TL;DR

This paper characterizes theories based on $n$-provability using iterated local reflection principles, revealing their axiomatizability, proof-theoretic strength, and proof speed-up phenomena.

Contribution

It provides a natural axiomatization of $n$-provability theories via iterated local reflection, connecting proof-theoretic strength with reflection principles.

Findings

Theories of $n$-provability can be axiomatized by iterated local reflection.

The set of provably 1-provable sentences in PA is axiomatized by $oldsymbol{ ext{ε}}_0$ iterations of reflection.

Proofs of $n$-provability can be significantly shorter than those from reflection principles.

Abstract

A formula $\phi$ is called \emph{$n$-provable} in a formal arithmetical theory $S$ if $\phi$ is provable in $S$ together with all true arithmetical $\Pi_{n}$-sentences taken as additional axioms. While in general the set of all $n$-provable formulas, for a fixed $n>0$, is not recursively enumerable, the set of formulas $\phi$ whose $n$-provability is provable in a given r.e.\ metatheory $T$ is r.e. This set is deductively closed and will be, in general, an extension of $S$. We prove that these theories can be naturally axiomatized in terms of progressions of iterated local reflection principles. In particular, the set of provably 1-provable sentences of Peano arithmetic PA can be axiomatized by $\varepsilon_0$ times iterated local reflection schema over PA. Our characterizations yield additional information on the proof-theoretic strength of these theories (w.r.t. various measures of it) and on their axiomatizability. We also study the question of speed-up of proofs and show that in some cases a proof of $n$-provability of a sentence can be much shorter than its proof from iterated reflection principles.