Axiomatizing Provable n-Provability

Abstract

The set of all formulas whose n-provability in a given arithmetical theory S is provable in another arithmetical theory T is a recursively enumerable extension of S. We prove that such extensions can be naturally axiomatized in terms of transfinite progressions of iterated local reflection schemata over S. Specifically, the set of all provably 1-provable sentences in Peano arithmetic PA can be axiomatized by an ε₀-times iterated local reflection schema over PA. The resulting characterizations provide additional information on the proof-theoretic strength of these theories and on the complexity of their axiomatization.