What metatheory proves $\mathsf{ACA}_0$ conservative over PA? Simpson's book shows  $\mathsf{ACA}_0$ is conservative over $\mathsf{PA}$ in the natural way by model theory using definable subsets.  Of course, $\mathsf{ACA}_0$ being conservative over PA is interesting even apart from consistency strength.  So one might not be explicit about the metatheory.  And I am sure it is not a strong one.  
But I am curious to know the exact logic of this argument.  
 A: The conservativity of $\mathrm{ACA}_0$ over $\mathrm{PA}$ is provable in $I\Delta_0+\mathit{SUPEXP}$ by a cut elimination argument. It is not provable in $I\Delta_0+\mathit{EXP}$, since $\mathrm{ACA}_0$ has superexponential speedup over $\mathrm{PA}$ (a result attributed to Solovay, Pudlák, and Friedman).
EDIT: Let me briefly sketch a proof of the speedup theorem here.
Theorem:


*

*$I\Delta_0+\mathit{EXP}\nvdash\mathrm{Con}_\mathrm{PA}\to\mathrm{Con}_{\mathrm{ACA}_0}$.

*For any $k$, there are true $\Sigma^0_1$-sentences $\phi$ such that $l_\mathrm{PA}(\phi)\ge2_k^{l_{\mathrm{ACA}_0}(\phi)}$, where $l_T(\phi)$ denotes the smallest Gödel number of a $T$-proof of $\phi$, and $2_k^x$ is the $k$-times iterated exponential of $x$. Consequently, the ($\Sigma^0_1$-)conservativity of $\mathrm{ACA}_0$ over $\mathrm{PA}$ is not provable in $I\Delta_0+\mathit{EXP}+\mathrm{Th}_{\Sigma^0_2}(\mathbb N)$.
Proof:
For 1, a variant of Parikh’s theorem shows that if $I\Delta_0+\mathit{EXP}\vdash\mathrm{Con}_\mathrm{PA}\to\mathrm{Con}_{\mathrm{ACA}_0}$, there is a constant $k$ such that
$$\tag{$*$}I\Delta_0\vdash p\le\log^{(k)}(x)\land\mathrm{Proof}_{\mathrm{ACA}_0}(p,\ulcorner\bot\urcorner)\to\exists q\le x\,\mathrm{Proof}_{\mathrm{PA}}(q,\ulcorner\bot\urcorner).$$
Working in $\mathrm{ACA}_0$, one can define a cut $I(n)$ consisting of those $n$ such that there exists a truth-predicate for $\Sigma^0_n$-sentences satisfying Tarski’s definition (the inductive clauses can be described by an arithmetical formula, hence $I$ is $\Sigma^1_1$-definable). Using the method of shortening of cuts, let $J(n)$ be a cut $\mathrm{ACA}_0$-provably closed under $\omega_k$ and included in $I$. We have
$$\mathrm{ACA}_0\vdash(I\Delta_0+\Omega_k+\mathrm{Con}_\mathrm{PA})^J.$$
Let $K(n)\iff J(2_k^n)$. Then $K$ is a cut closed under multiplication, and we have
$$\mathrm{ACA}_0\vdash(I\Delta_0+\mathrm{Con}_{\mathrm{ACA}_0})^K$$
using $(*)$, which contradicts a suitable version of Gödel’s incompleteness theorem.
For 2, let $\psi$ be the $\Pi^0_1$-sentence
$$\forall s\in\Sigma^0_1\forall x,p\,\bigl(p\le\log^{(k)}(x)\land\mathrm{Proof}_{\mathrm{ACA}_0}(p,s)\to\exists q\le x\,\mathrm{Proof}_{\mathrm{PA}}(q,s)\bigr)$$
expressing that $\mathrm{ACA}_0$ has no speedup faster than $2_k^x$ over $\mathrm{PA}$ (for $\Sigma^0_1$-sentences). By the same argument as in 1, we show
$$\mathrm{ACA}_0+\psi\vdash(I\Delta_0+\mathrm{Con}_{\mathrm{ACA}_0+\psi})^K,$$
hence $\mathrm{ACA}_0\vdash\neg\psi$ by Gödel’s theorem. In particular, $\psi$ is false, hence $\mathrm{ACA}_0$ has speedup faster than $2_k^x$ over $\mathrm{PA}$ for some $\Sigma^0_1$-sentences $\phi$.
One can construct an explicit such sentence, as well as avoid the appeal to the $\Sigma^0_1$-soundness of $\mathrm{ACA}_0$ at the end of the proof, by defining
$$\vdash\phi\leftrightarrow\exists x,p\,\bigl(p\le\log^{(k)}(x)\land\mathrm{Proof}_{\mathrm{ACA}_0}(p,\ulcorner\phi\urcorner)\land\forall q\le x\,\neg\mathrm{Proof}_{\mathrm{PA}}(q,\ulcorner\phi\urcorner)\bigr)$$
using self-reference, and working with $\psi=\neg\phi$.
Notice that there is nothing particularly specific to $\mathrm{PA}$ in the proof. In general, if $T$ is a consistent sequential theory in a finite language, axiomatized by finitely many axioms and axiom schemata (allowing for all formulas with parameters, such as the induction schema of $\mathrm{PA}$), and $T^+$ is its “second-order” conservative extension with first-order comprehension axioms, and the schemata of $T$ replaced with the corresponding $\Pi^1_1$-sentences, then the speedup theorem holds with $T$ and $T^+$ in place of $\mathrm{PA}$ and $\mathrm{ACA}_0$. Particular examples of such theories are $\mathrm{ZF(C)}$ and $\mathrm{GB(C)}$.
