Axiomatizing Provable n-Provability
Е. А. Колмаков, Lev D. Beklemishev · Doklady Mathematics · 2018
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 ε 0 -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.