AXIOMATIZATION OF PROVABLE n -PROVABILITY
Е. А. Колмаков, Lev D. Beklemishev · Journal of Symbolic Logic · 2019
Abstract A formula φ is called n-provable in a formal arithmetical theory S if φ is provable in S together with all true arithmetical ${{\rm{\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 φ 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.