1 results
AXIOMATIZATION OF PROVABLE n-PROVABILITY
-
- Journal:
- The Journal of Symbolic Logic / Volume 84 / Issue 2 / June 2019
- Published online by Cambridge University Press:
- 08 February 2019, pp. 849-869
- Print publication:
- June 2019
-
- Article
- Export citation
-
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.
