What is the quantifier complexity of the function sending an ordinal to the power set iterated that many times? One use of the Axiom Schema of Replacement in ZFC is that it allows one to prove that for a set $X$ and a limit ordinal $\alpha$, the transfinitely iterated powerset $P^\alpha(X)$ exists (for a successor ordinal $\beta+1$, one only needs $P^\beta(X)$ to exist beforehand). Sometimes people consider restricted versions of Replacement with restricted complexity on the description of the function to which it is being applied. I was wondering what the quantifier complexity of the statement that Replacement is then applied to in order to get $P^\alpha(X)$. This would then put a floor on how low complexity Replacement instances can be before iterated powerset no longer becomes available.
 A: It looks $\Sigma_2$ to me: we have $y=\mathcal{P}^\alpha(x)$ iff there is a certain sequence of length $\alpha+1$ with first term $x$, last term $y$ and satisfying a certain $\Pi_1$ property (namely that limit terms are the unions of prior terms and successor terms are the powersets of their predecessor terms). So $\mathsf{KP+\Sigma_2Rep+Pow}$ proves the existence of ordinal iterates of the powerset operation.
This isn't as fine-grained as one might hope, though - $\Sigma_2$-$\mathsf{Rep}$ lets us do a lot more than just iterate the particular $\Pi_1$ powerset function, and so seems like overkill. If memory serves, a theory of intermediate strength which shows up a lot here is $\mathsf{KP^{Pow}}$ (maybe $\mathsf{KP^\mathcal{P}}$?). This is the analogue of $\mathsf{KP}$ in the language $\{\in,\mathcal{P}\}$: basically, the powerset operation is taken as primitive here, and we are given $\Delta_1$ separation and $\Sigma_1$ replacement for formulas involving it. This is intermediate between $\mathsf{KP}$ and $\mathsf{KP+\Sigma_2Rep+Pow}$ and, I believe, incomparable with $\mathsf{KP+\Sigma_2Rep}$.
