It is <a href="http://mathoverflow.net/questions/23788/reducing-aca-proof-to-first-order-pa">well-known</a> that $\mathsf{ACA}_0$ is a conservative extension of PA. I assume this theorem gets a lot of attention because $\mathsf{Z}_2$ is _not_ conservative over PA. Thus there ought to be first-order formulas of number theory that are not provable in PA, but are provable in $\mathsf{Z}_2$. Meanwhile, the only difference between $\mathsf{Z}_2$ and $\mathsf{ACA}_0$ is that $\mathsf{Z}_2$ allows you to assume the existence of sets of numbers defined by impredicative properties, that is, properties that are described by predicates containing set quantifiers.

So my question has two parts:

1. Show me a first-order sentence that can be proven in $\mathsf{Z}_2$ but not in $\mathsf{ACA}_0$ or PA. (I _do_ understand how to turn "the consistency of PA" into a first-order sentence because that's explained in every book about Gödel's Incompleteness Theorem. I also understand why it is not provable in PA, for the same reason. So feel free to say "the consistency of PA" if that is in fact the answer.)
2. What impredicative set (or sets) must be assumed to exist in $\mathsf{Z}_2$ to allow the proof of the first-order sentence given above?

For the record, I'm not particularly interested in:

1. A detailed breakdown of all the subsystems of $\mathsf{Z}_2$. I don't especially care whether you need $\mathsf{ATR}_0$ or $\Pi_1^1\hbox{-}\mathsf{CA}_0$ to prove the example. I just want to know what you can get by using _any_ set quantifiers in a formula appearing in an induction or set comprehension axiom.
2. The consistency of various axiom systems. I brought up "the consistency of PA" because I know that it's an example of a sentence that can be written using first-order symbols, can't be proven in PA, but can be proven some other way. (I had hoped $\mathsf{Z}_2$ could do it, and was apparently correct.) But Goodstein's theorem is as good of an example as Con(PA) so far as I'm concerned.

My objective is to understand how those set quantifiers make it possible to prove otherwise-unprovable things. I'm still burning through a lot of material on well-ordering, since that seems to be key here.