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?