Z_2 versus second-order PA

Question

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

Answer 1

$Z_2$ as it is usually viewed is a first-order theory with two sorts, and as such is not categorical. The difference (apart from terminological issues) is entirely in the semantics that are used. In "full" second-order semantics, the set variables quantify over all subsets of the domain, while in first-order "Henkin" semantics each model has a domain for number variables and a second domain for set quantifiers to range over.

There are two things that you might mean by $PA_2$ (I realized this after writing the answer, so I have expanded it). The first option is to have $PA_2$ include the entire second-order induction scheme; let's call that $PA^s_2$. $PA^s_2$ and $ACA$ are indeed equiconsistent. Every model of $ACA$ is already a model of $PA^s_2$, and every model of $PA^2_2$ extends to a model of $ACA$ by just throwing in the definable sets. In fact, this extends any model of $PA^s_2$ to a model of $Z_2$, so these theories are equiconsistent. There is an issue that this could mean "equiconsistent in full second order semantics" or "equiconsistent in first-order semantics", but either way they are pairwise equiconsistent as long as the same semantics is used for both theories.

The other option is that $PA_2$ might just have the single second-order induction axiom $$ (\forall x)[0 \in X \land (\forall n)[n \in X \to n+1\in X] \to (\forall n) n \in X]. $$ Let's call that version $PA^i_2$. Now the semantics matters. In full second-order semantics, any model of $PA^i_2$ is a model of $PA^s_2$, so it extends to a model of $Z_2$. In first-order semantics, $PA^i_2$ is very weak, because without any comprehension axioms the single second-order induction axiom is not very strong in first-order semantics. $PA^i_2$ is (syntactically) a subtheory of $\mathsf{RCA}_0$, one of the weak systems of arithmetic considered in reverse mathematics, and so $PA^i_2$ has a much lower consistency strength than $Z_2$ in the first-order setting.

Answer 2

Regarding the first question: The second order theory $PA_2$ is usually defined relative to an ambient universe $V$ of Zermelo-Fraenkel set theory, and as such it only has one model up to isomorphism. In other words, $PA_2$ is a categorical theory from the point of view of any model $V$ of $ZF$ since all of its models are isomorphic to $(\Bbb{N},\mathcal{P}(\omega))$, where $\Bbb{N}$ is the standard model of $PA$ and $\mathcal{P}(\omega)$ is the collection of all subsets of natural numbers (from the point of view of $V$).

On the other hand, $Z_2$ is a first-order approximation of $PA_2$, and by some standard theorems of model theory, it has many $2^\kappa$ nonisomorphic models of cardinality $\kappa$ for each infinite cardinal $\kappa$. In particular, there are continuum-many nonisomorphic countable models of $Z_2$. Each such countable model of $Z_2$ is of the form $(\Bbb{M},\mathcal{F})$, where $\Bbb{M}$ is a standard or nonstandard model of $PA$, and $\mathcal{F}$ is a countable family of subsets of the universe of discourse $M$ of $\Bbb{M}$

Regarding the second question: $ACA$ is much stronger than first order Peano Arithmetic $PA$ since it proves Con($PA$) (the formal consistency of $PA$) and much more (itertions of consistency statements) .

However, $ACA$ is, in turn, much weaker than $Z_2$ since already the fragment known as $\Pi^1_1$-$CA$ of $Z_2$ can prove Con($ACA$).

One way to see this is based on an old result (noticed by a number of people, including Takeuti and Feferman) that $ACA$ is equiconsistent with an extension $PA(T)$ of $PA$ with a distinguished predicate $T$ that codes up the full truth predicate for the ambient model of arithmetic. Note that $PA(T)$ includes induction in the extended language of arithmetic augmented by the predicate $T$.

P.S. The subsystem $ATR_0$ of $\Pi^1_1$-$CA$ already proves Con($ACA$).