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