Return to 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.

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.

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.

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.

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?

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.