These days, Peano Arithmetic ($PA$) refers to the first-order version of the axioms, where induction is only over formulas referring to natural number variables. Peano's original version of the induction axiom was actually second-order, allowing reference to sets-of-natural-numbers variables. This latter version corresponds to what a category theorist (like me) would call a natural number object. Call this 'second-order $PA$' or $PA_2$.

However, we also have second-order arithmetic $Z_2$ (wikipedia), which up to some redundant axioms, looks like $PA_2$ plus a comprehension axiom schema ([details](<http://en.wikipedia.org/wiki/Second-order_arithmetic#Induction_and_comprehension_schema) of the schema). We know that $PA_2$ has a unique model up to isomorphism, and so does $Z_2$. My first question is then

What, if anything, separates a model of $PA_2$ from a model of $Z_2$?

I imagine that there are sets of naturals in $Z_2$ that cannot be proved to exist in $PA2$, but where is the boundary?

From the Wikipedia page I see that $ACA_0$, a subsystem of $Z_2$ with restricted induction, is a conservative extension of $PA$ (and equiconsistent with $PA$), and I infer that $ACA$, the same subsystem plus unrestricted induction, would be a conservative extension of $PA_2$.

Is this true? Is $ACA$ equiconsistent with $PA_2$?

One reason I am interested in this is that McLarty has proved that the machinery of derived functor cohomology, in the setting appropriate for arithmetic geometry, is do-able in $Z_2$ (more precisely, derived functor cohomology over a Noetherian scheme, with coefficients in an arbitrary sheaf of modules on the Zariski site, only requires a system equiconsistent with second-order arithmetic). If one can get from working in $Z_2$ down to $ACA$, then these tools of algebraic geometry are available as soon as one accepts the existence of natural number objects (and, presumably, classical logic).

These days, Peano Arithmetic ($PA$) refers to the first-order version of the axioms, where induction is only over formulas referring to natural number variables. Peano's original version of the induction axiom was actually second-order, allowing reference to sets-of-natural-numbers variables. This latter version corresponds to what a category theorist (like me) would call a natural number object. Call this 'second-order $PA$' or $PA_2$.

However, we also have second-order arithmetic $Z_2$ (wikipedia), which up to some redundant axioms, looks like $PA_2$ plus a comprehension axiom schema (details of the schema). We know that $PA_2$ has a unique model up to isomorphism, and so does $Z_2$. My first question is then

What, if anything, separates a model of $PA_2$ from a model of $Z_2$?

I imagine that there are sets of naturals in $Z_2$ that cannot be proved to exist in $PA2$, but where is the boundary?

From the Wikipedia page I see that $ACA_0$, a subsystem of $Z_2$ with restricted induction, is a conservative extension of $PA$ (and equiconsistent with $PA$), and I infer that $ACA$, the same subsystem plus unrestricted induction, would be a conservative extension of $PA_2$.

Is this true? Is $ACA$ equiconsistent with $PA_2$?

One reason I am interested in this is that McLarty has proved that the machinery of derived functor cohomology, in the setting appropriate for arithmetic geometry, is do-able in $Z_2$ (more precisely, derived functor cohomology over a Noetherian scheme, with coefficients in an arbitrary sheaf of modules on the Zariski site, only requires a system equiconsistent with second-order arithmetic). If one can get from working in $Z_2$ down to $ACA$, then these tools of algebraic geometry are available as soon as one accepts the existence of natural number objects (and, presumably, classical logic).

These days, Peano Arithmetic ($PA$) refers to the first-order version of the axioms, where induction is only over formulas referring to natural number variables. Peano's original version of the induction axiom was actually second-order, allowing reference to sets-of-natural-numbers variables. This latter version corresponds to what a category theorist (like me) would call a natural number object. Call this 'second-order $PA$' or $PA2$.

However, we also have second-order arithmetic $Z_2$ (wikipedia), which up to some redundant axioms, looks like $PA2$ plus a comprehension axiom schema ([details](<http://en.wikipedia.org/wiki/Second-order_arithmetic#Induction_and_comprehension_schema) of the schema). We know that $PA2$ has a unique model up to isomorphism, and so does $Z_2$. My first question is then

What, if anything, separates a model of $PA2$ from a model of $Z_2$?

I imagine that there are sets of naturals in $Z_2$ that cannot be proved to exist in $PA2$, but where is the boundary?

From the Wikipedia page I see that $ACA_0$, a subsystem of $Z_2$ with restricted induction, is a conservative extension of $PA$ (and equiconsistent with $PA$), and I infer that $ACA$, the same subsystem plus unrestricted induction, would be a conservative extension of $PA2$.

Is this true? Is $ACA$ equiconsistent with $PA2$?

One reason I am interested in this is that McLarty has proved that the machinery of derived functor cohomology, in the setting appropriate for arithmetic geometry, is do-able in $Z_2$ (more precisely, derived functor cohomology over a Noetherian scheme, with coefficients in an arbitrary sheaf of modules on the Zariski site, only requires a system equiconsistent with second-order arithmetic). If one can get from working in $Z_2$ down to $ACA$, then these tools of algebraic geometry are available as soon as one accepts the existence of natural number objects (and, presumably, classical logic).

These days, Peano Arithmetic ($PA$) refers to the first-order version of the axioms, where induction is only over formulas referring to natural number variables. Peano's original version of the induction axiom was actually second-order, allowing reference to sets-of-natural-numbers variables. This latter version corresponds to what a category theorist (like me) would call a natural number object. Call this 'second-order $PA$' or $PA_2$.

However, we also have second-order arithmetic $Z_2$ (wikipedia), which up to some redundant axioms, looks like $PA_2$ plus a comprehension axiom schema ([details](<http://en.wikipedia.org/wiki/Second-order_arithmetic#Induction_and_comprehension_schema) of the schema). We know that $PA_2$ has a unique model up to isomorphism, and so does $Z_2$. My first question is then

What, if anything, separates a model of $PA_2$ from a model of $Z_2$?

I imagine that there are sets of naturals in $Z_2$ that cannot be proved to exist in $PA2$, but where is the boundary?

From the Wikipedia page I see that $ACA_0$, a subsystem of $Z_2$ with restricted induction, is a conservative extension of $PA$ (and equiconsistent with $PA$), and I infer that $ACA$, the same subsystem plus unrestricted induction, would be a conservative extension of $PA_2$.

Is this true? Is $ACA$ equiconsistent with $PA_2$?

One reason I am interested in this is that McLarty has proved that the machinery of derived functor cohomology, in the setting appropriate for arithmetic geometry, is do-able in $Z_2$ (more precisely, derived functor cohomology over a Noetherian scheme, with coefficients in an arbitrary sheaf of modules on the Zariski site, only requires a system equiconsistent with second-order arithmetic). If one can get from working in $Z_2$ down to $ACA$, then these tools of algebraic geometry are available as soon as one accepts the existence of natural number objects (and, presumably, classical logic).