Skip to main content
added 1165 characters in body
Source Link
Noah Schweber
  • 20.5k
  • 10
  • 110
  • 331

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

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


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

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

fixed typos in formula
Source Link
François G. Dorais
  • 44.4k
  • 6
  • 150
  • 233

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 $\phi$ is a well-ordering of $\mathbb{R}$, and $\forall x<_W y(\psi(x))\implies \psi(y)$, then $\forall x\psi(x)$."}$$$$ \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.)


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

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 $\phi$ is a well-ordering of $\mathbb{R}$, 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.)


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

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


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

Source Link
Noah Schweber
  • 20.5k
  • 10
  • 110
  • 331

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 $\phi$ is a well-ordering of $\mathbb{R}$, 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.)


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