Consider the theory $\mathrm{PA}+\mathrm{BHO}$ consisting of first-order Peano arithmetic ($\mathrm{PA}$) enriched by an axiom scheme which allows well-founded induction up to any ordinal less than [a standard recursive presentation of] the Bachmann-Howard ordinal. More precisely, let $\prec$ be the explicit well-ordering on $\mathbb{N}$ which results from, say, [this description](https://en.wikipedia.org/wiki/Ordinal_collapsing_function#An_example_leading_up_to_the_Bachmann%E2%80%93Howard_ordinal) and which has order type of the Bachmann-Howard ordinal, and add to Peano's axioms an axiom scheme ($\mathrm{BHO}$) which for every formula $\phi$ and every $n$ asserts that


$(\forall m\prec n((\forall p\prec m(\phi(p)))\Rightarrow\phi(m)))\Rightarrow\forall m\prec n(\phi(m))$


These are supposed to be theorems of Kripke-Platek set theory ($\mathrm{KP}$), whose proof ordinal is the B-H ordinal, so—unless I badly messed things up—all theorems of $\mathrm{PA}+\mathrm{BHO}$ are arithmetical consequences of $\mathrm{KP}$. My question is whether the converse holds: *can every arithmetical theorem of $\mathrm{KP}$ be proved in $\mathrm{PA}+\mathrm{BHO}$?* If not, what would a counterexample be?


The naïve idea I have is to somehow define the constructible hierarchy (up to and excluding the Bachmann-Howard ordinal), or α-recursion, in $\mathrm{PA}+\mathrm{BHO}$ but I can't imagine how it would work without some kind of second-order language. I'm not asking for details, just a general idea of how things might work (if they do).


More generally, a broader question should be something like: in what respect can "artificially" increasing the proof ordinal of some theory give it the same arithmetical strength as some stronger theory with that proof ordinal. So if there's some way to modify my question to give this, I'd like to know.



Arithmetic strength of Peano + the Howard ordinal
The answer is *yes*, using the ordinal analysis of KP. See Pohlers' *A Short Course in Ordinal Analysis* for why the usual ordinal analyses are *profound*, that is, they imply conservativity of the analyzed theory over PA + TI($\prec\_i$) for arithmetical sentences. Here TI($\prec\_i$) is the scheme of transfinite induction along all *proper* initial segments of the primitive recursive well-ordering $\prec$ that measures the proof-theoretic ordinal of the theory.


