Show that Z2 is not conservative over PA

Question

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.

Answer 1

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$. Z₂ can prove that $\varepsilon_0$ is wellfounded and even the predicative system ATR₀ can prove that every ordinal up to the Feferman-Schütte ordinal $\Gamma_0$ is wellfounded.

Answer 2

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.

Answer 3

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)$.)