  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.
