Yikes! My apologies; I'm new to reverse mathematics. Should I edit the question to remove the offending word or will that create more confusion than it resolves?

Excellent! I think Goodstein's Theorem is a nicer example of what I'm looking for than Con(PA), primarily because it's simpler. From here I have to understand three things: How to encode the claim that $\epsilon_0$ is well-founded into the language of $\mathsf{Z}_2$, how to prove that claim, and then how to translate that claim into a first-order sentence (which will probably be Goodstein's theorem; I assume technical reasons make it impossible to encode the well-foundedness of $\epsilon_0$ directly in first-order terms). I may be able to do these without assistance; I'm still reading.

I've updated the question per this discussion. Furthermore, in response to: "So if your question is 'Why does Z2 prove Con(PA)?', then what you should want to see is an instance of Z2 proving induction along very long well-orderings." I would say, "Yes, this is exactly what I'm looking for, but I would still be interested if we can prove something simpler than Con(PA), as long as it can be translated into a first-order formula."

My apologies; the consistency of PA is a red herring. I'll settle for any first-order sentence that makes use of the special features of $\mathbf{Z}_2$. (I don't particularly care how much impredicativity gets used, either; it doesn't matter whether the formula is $\Pi_1^1$ or $\Pi_0^{200}$.) Also, per an update you just made: I was taught that "impredicativity" is the use of set quantifiers in the definition of a set. But what I'm looking for right now is an understanding of how second-order induction gives you access to proofs that first-order induction doesn't.

Ah, OK. Repeating this back to make sure I have it right: The only reason we need impredicative sets in the proof of Con(PA) is so that we can use them with the induction axiom, which in $\mathsf{Z}_2$ is written in terms of sets. You're saying that we can bypass the set definition as long as we're able to perform induction on that second-order formula directly. Could you link to any references on ACA? I can't find it in the Simpson book (Subsystems of Second Order Arithmetic).

Great, OK. What I understand right now: We first use $\mathsf{Z}_2$ (or even $\mathsf{ATR}_0$) to define an impredicative set. Once we have it, we find an inductive proof that all numbers are in this set. Which means that every number has whatever property defined that set. This property can't be first-order since its formula still contains set quantifiers, but "à la" Gentzen, we can somehow eliminate those, yielding a theorem containing only first-order symbols but requiring second-order logic to prove. I promise not to leave before accepting an answer, but I need an evening to digest this.