Show that Z2 is not conservative over PA

It is well-known 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.

Concerning the answer I accepted: While I appreciate everyone's contributions, Goodstein's theorem seems to be the winner. Goodstein's theorem can be written using only first-order symbols because of a well-known trick to convert statements about sequences (e.g. Goodstein sequences) into first-order sentences. But the theorem's proof depends on a coded version of the well-foundedness of $\varepsilon_0$, which can't be proven in PA. I'm still a bit hazy on which set exactly needs to exist, but everyone who replied agrees that the point of defining the set is to support induction. The actual set we need to be able to construct is either a representation of a well-ordering of the (coded) ordinals, per Noah's answer, or something related that is needed for the transfinite induction over all the ordinals in $\varepsilon_0$. This set presumably can't be defined without set quantifiers (which is why you can't do this proof in PA), but then as soon as we get it we use it in the induction axiom as a parameter to prove our actual result.

-
I think the confusion is the concern with "impredicativity." The reason why $\mathsf{ATR}_0$ and $\mathsf{ACA}_0+\mathsf{I}\Sigma^1_1$ were brought up is that these are predicative systems. –  François G. Dorais Jan 26 at 1:25
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? –  A.C. Jan 26 at 1:40
@François: I firmly disagree that either $ATR_0$ or $ACA_0 + I\Sigma^1_1$ is predicative. –  Nik Weaver Jan 26 at 3:48
@NikWeaver: Yes, I'm aware of your disagreement and I agree with you that "predicative" is almost systematically misused. I tend to agree with your objection regarding $\Sigma^1_1$ induction. It's also unfair to call $\mathsf{ATR}_0$ predicative since it fits the Friedman-Simpson predicative reductionist philosophy rather than the actual predicative philosophy. –  François G. Dorais Jan 26 at 4:12

The consistency of PA is an example another example is Goodstein's Theorem. The idea is that PA cannot prove that the ordinal $\varepsilon_0$ is wellfounded. Gentzen has shown that one can prove the consistency of PA by induction up to $\varepsilon_0$ and the usual proof of Goodstein's theorem is by induction up to $\varepsilon_0$. Z2 can prove that $\varepsilon_0$ is wellfounded and even the predicative system ATR0 can prove that every ordinal up to the Feferman-Schütte ordinal $\Gamma_0$ is wellfounded.

-
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. –  A.C. Jan 26 at 1:24
@A.C. Every ordinal below $\varepsilon_0$ has a unique hereditary base $\omega$ representation and the ordering of two such ordinals can be determined recursively from these finite representations (coded using numbers in the usual manner). Longer wellorderings such as $\Gamma_0$ have similar, but more complicated, computable systems of notations. –  François G. Dorais Jan 26 at 1:29
What Francois described is how to talk about ordinals directly in the language of $PA$, which is what you really want. However, let me point out that talking about well-orderings in $Z_2$ is substantially easier; in particular, the statement "$R(x, y)$ is a well-ordering" no longer has to be expressed as an induction scheme, but is just a single $\Pi^1_1$ sentence. –  Noah S Jan 26 at 3:41

Yes, the sentence Con(PA) expressing the consistency of PA is one of the statements that is provable in $\mathsf{Z}_2$ and not in $\mathsf{ACA}_0$.

On the other hand, it is not the case that any impredicative sets must be added to make Con(PA) become provable. It is enough to just add the full second-order induction scheme, which yields the stronger theory $\mathsf{ACA}$. Every $\omega$-model of $\mathsf{ACA}_0$ is, of course, an $\omega$-model of $\mathsf{ACA}$, which I would interpret as saying that no additional sets are needed, impredicative or not.

In general there is an interplay between the set existence axioms and the induction axioms. For example, the stronger second-order system $\mathsf{ATR}_0$ does prove the consistency of PA, without assuming the whole second-order induction scheme. The difference is that $\mathsf{ATR}_0$ is able to form a single satisfaction predicate for sentences of first-order PA, and then use that as a parameter to prove that every statement provable in PA is satisfied by $\mathbb{N}$. On the other hand, the consistency proof of PA in $\mathsf{ACA}$ avoids forming that satisfaction predicate, but uses strong instances of the induction scheme to work with approximations that it can produce of the full satsifcation predicate.

-
In fact Con(PA) is provable in systems quite weaker than $\mathsf{ATR}_0$; once you have the satisfaction predicate for first-order sentences, the rest can be done in $\mathsf{ACA}_0$. –  Carl Mummert Jan 25 at 22:00
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). –  A.C. Jan 25 at 23:04
Very nice. Do you know how much induction you really need to prove Con(PA)? Is $\Sigma^1_1$-induction enough? –  François G. Dorais Jan 25 at 23:42
@François: yes, it is enough in addition to $\mathsf{ACA}_0$. All you need is "for all $n$ there is a truth set for $\Sigma^0_n$ formulas without set parameters", i.e. a fragment of $\mathsf{ACA}_0'$. The claim is that this proves that $\mathbb{N}$ satisfies PA, and then Con(PA) follows from the completeness theorem and $0\not=1$. The proof is by cases; only induction is interesting; given a coded formula $\phi(n)$ for an instance of induction in PA, we may form the truth set for $\phi$ by assumption, and then use normal set induction to verify that $\mathbb{N}$ satisfies that instance. –  Carl Mummert Jan 26 at 0:29
@A.C. try Takeuti's book Proof Theory (second edition). He refers to $\mathsf{ACA}$ as $\mathbf{S}^2$. The system Carl has talked about ($\mathsf{ACA}_0 + \Sigma^1_1\text{-}\mathsf{IND}$) is referred to as $\mathbf{S}^1$. –  Benedict Eastaugh Jan 26 at 1:12

You've already answered question (1); possibly a more satisfying response, however, is that $Z_2$ proves more induction than $ACA_0$ does. This isn't substantively different, but it might feel more satisfying. For starters, note that the induction already allowed by $ACA_0$ (and much less) allows for set parameters; this means that "the only difference" as you say between $Z_2$ and $PA$ is absolutely gigantic. For example, $Z_2$ proves $\Sigma^1_{2014}$-induction, that is, for each $\Sigma^1_{2014}$ formula $\phi$ defining a binary relation on $\mathbb{N}$ and each formula $\psi$, $Z_2$ proves the statement $$\text{"If \lt_W is a well-ordering of \mathbb{N}, and \forall x<_W y(\psi(x))\implies \psi(y), then \forall x\psi(x)."}$$ The proof of this in $Z_2$ uses set comprehension to generate a set $X$ such that $\Sigma^0_1$ induction with $X$ as a parameter is enough to prove the theorem; you should work out the details of this proof. In particular, I think it will elucidate just how much power is present in set existence axioms. Now these higher induction statements aren't first-order, but a la Gentzen higher-order induction winds up having lower-order consequences; in particular, this is why $Z_2$ proves the consistency of $ACA_0$, as well as much stronger systems.

As to (2), if the question is "What impredicative sets exist, given $Z_2$?" the answer is "Lots." For example, the set of (natural numbers coding) computable well-orderings of $\mathbb{N}$ is guaranteed to exist by $Z_2$ - actually, just $\Pi^1_1-CA_0$, a very small fragment of $Z_2$ - and is impredicative by every definition of "impredicative" I'm aware of.

Alternatively, since $WKL_0$ already can prove that consistency = satisfiability, each of the theories $\Pi^1_n-CA_0$ has a (countable coded) model in any model of $Z_2$. These models will necessarily be impredicative because of the previous paragraph, but maybe they form a more satisfying example of "impredicative stuff $Z_2$ gives you."

(If, on the other hand, the question is "How much impredicativity is needed to prove $Con(ACA_0)$?", then see Carl's answer.)

EDIT: Possibly more relevant to your question is the notion of "predicative ordinal." Essentially, an ordinal is "predicative" if it can be proved to be well-founded in a predicative manner. We might say that a theory is "predicatively consistent" if its consistency follows from "$\alpha$ is well-ordered" (again, together with the base theory above) for some predicative ordinal $\alpha$. The predicative ordinals are usually taken to be those $<\Gamma_0$, which incidentally is the proof-theoretic ordinal of $ATR_0$; so arguably "impredicativity" is only necessary for consistency proofs at the level of $ATR_0$ and above. Note, however, that even $\Gamma_0$ is a computable ordinal, meaning that there is a relation on $\mathbb{N}$ of order type $\Gamma_0$ which is computable; the relevant sense of impredicativity here is with respect to methods of proof, not methods of set construction (although this distinction is kind of nonsense in practice, since proving well-foundedness of orderings of $\mathbb{N}$ basically reduces to developing nice construction methods for building those orderings; I'm just trying to get rid of a potential confusion here).

The gulf between $Z_2$ and $ACA_0$ (or first-order consequences of $PA$) is truly vast. I suspect that you'll get a more satisfying understanding if you look at a much smaller gulf, say the first-order sentences provable in $ATR_0$ but not $PA$. (Such as, of course, $Con(PA)$.)

-
I just realized that in my answer when I say "a la Gentzen" I assume familiarity with Gentzen's work. Francois' answer has an explanation of what I mean by that. –  Noah S Jan 25 at 22:03
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. –  A.C. Jan 25 at 22:50
I think there's still a confusion: "a la Gentzen" is just a reference to the fact that, for all natural theories (including $PA$), a very small finitary theory together with "enough" induction proves that theory's consistency. Now, what "enough" means here varies from theory to theory, and is known as the "proof-theoretic ordinal" of a theory. For example, the proof-theoretic ordinal of $PA$ is $\epsilon_0$, which means that "$\epsilon_0$ is well-founded" (together with a very weak - much weaker than $RCA_0$ - base theory) proves $Con(PA)$. (cont'd) –  Noah S Jan 26 at 0:33
(By the way, $\epsilon_0$ is the least fixed point of the map $\alpha\mapsto \omega^\alpha$, usually suggestively written as $\epsilon_0:= \omega^{\omega^{\omega^{.^{.^.}}}}$.) So the way that $Z_2$ proves $Con(PA)$ is by proving induction along very long well-orderings. So if your question is "Why does $Z_2$ prove $Con(PA)$?", then what you should want to see is an instance of $Z_2$ proving induction along very long well-orderings. (cont'd) –  Noah S Jan 26 at 0:40
(Specifically, I'm confused by the linking of consistency proofs with impredicativity, which seems to me like it might be a red herring in this context.) –  Noah S Jan 26 at 0:49