Adding bounded quantifiers increases complexity in $L$

I'm reading Devlin's Constructability to learn about $L$. Following the proof that $L_\alpha$ has a $\Sigma_1$ skolem function for limit $\alpha>\omega$ (II.6.5), the author notes

Notice that in general, the above procedure will not produce a $\Sigma_n$ skolem function if $n>1$ ... (The procedure works in the case $n=1$ because a bounded universal quantifier prefixing a $\Sigma_0$ formula results in another $\Sigma_0$ formula, whereas if $n>1$, a bounded universal quantifier prefixing a $\Sigma_{n-1}$ formula gives a $\Pi_n$ formula.)

This is surprising to me. If you add a bounded quantifier to a formula in the external language of set theory, and you work over a sufficiently strong base theory, you can show that your bounded quantifier didn't increase the complexity. However when you work in the internalised language, this can fail over $L_\alpha$. Is this just because the $L_\alpha$s won't, in general, be models of the sufficiently strong base theory required to do the operations for eliminating the bounded quantifier?

• That's right. The proof that bounded quantifiers can be absorbed uses the replacement axiom. So it may fails when replacement fails, like it will in many $L_\alpha$'s (and $V_\alpha$'s too).
– user104955
Apr 24, 2015 at 21:18
• Applying the rules on en.m.wikipedia.org/wiki/Prenex_normal_form#Implication for creating logically equivalent formulae, we can show $\forall(x\in y)\exists z\phi$ (i.e. $\forall x(x\in y\rightarrow\exists z\phi)$) is logically equivalent to some $\forall x\exists z\psi$ where $\psi$ has the same complexity as $\phi$, but this doesn't seem to need replacement. Is there a sneaky application of replacement here?
– C7X
Mar 20, 2022 at 2:09