# NNO = (first order) PA

Recall the definition of a Natural Numbers Object in a topos, and the first order axioms for Peano Arithmetic. I am more familiar with the first definition than the second, so I cannot tell from the (obviously infallible) Wikipedia page whether first order PA is equivalent to 'second order' PA -- PA with the induction axiom scheme replaced by a similar one involving inductive subsets $A \subset \mathbb{N}$.

The equivalence between 'second order' PA and a NNO in $Set$ in one direction (NNO $\Rightarrow$ PA) is easy, and the other (PA $\Rightarrow$ NNO) is in MacLane's book Mathematics, form and function which I haven't seen (bonus question: another reference for the proof would be nice).

But I would like to see a proof of NNO = (first order) PA, if possible.

My motivation is to consider possibly weaker forms of arithmetic, and it is how to deal with (versions of) the induction axiom schema as usually presented from a logic point of view on which I would like a bit of background.

Edit: As Andreas points out, I really should be asking about models of PA and NNOs.

-
As it stands, the question asks about equivalence between a structure (an NNO) and a theory (PA). Please clarify what you mean by that. –  Andreas Blass Apr 10 '12 at 15:26
Mac Lane's book is available for download here: libgen.info/view.php?id=268190 –  Dmitri Pavlov Apr 10 '12 at 20:10
@Andreas - you're absolutely right. I'm editing the question to make it better-formed. –  David Roberts Apr 11 '12 at 0:03

J. Lambek and P. J. Scott: Introduction to higher-order categorical logic, Cambridge University Press, 1986, Part II, Section 4, Theorem 4.1 shows that a nno satisfies the first-order Peano rules (which are listed on page 135 under 3.7, 3.8., 3.9), while Part II, Section 12, Proposition 12.4 shows that Peano rules give a nno for the syntactic topos. By the universal property of the syntactic topos it then follows that in any topos which validates Peano rules has a nno.

The whole business with classical vs. non-classical logic is a red herring. You may throw excluded middle in if that is your wish.

-
Hmm, very interesting. I knew the internal logic of the topos would have to make an entrance at some point, because we can't always work in $Set$. –  David Roberts Apr 11 '12 at 7:45
You can apply the results just to $\mathrm{Set}$ if you wish. That is a special case. –  Andrej Bauer Apr 11 '12 at 8:26
So I presume (because I can't read all the details in Lambek-Scott via Google Books) that one could have a model of the Peano axioms in a topos, but the NNO is not necessarily isomorphic to it? –  David Roberts Apr 12 '12 at 5:54
Andrej, aren't these results about higher-order type theories with power types and full comprehension? They say that a topos with NNO is equivalent to a model of higher-order type theory with full comprehension, in the sense that you can go back and forth (using internal language and syntactic category). Since full comprehension is always assumed, this says little about first-order PA. –  Ulrik Buchholtz Apr 18 '12 at 19:34
@Ulrik: I am not sure I understand your objection. The question asked for a proof that in a topos the nno satisfies the Peano axioms, and that an object in a topos satisfying the Peano axioms is a NNO. Surely then, in proving these things we can work with anything that the topos provides. The "first-order" in the question does not refer to the ambient logic (which you correctly observe to be higher-order), but to the first-order Peano axioms (as opposed to some higher-order version), in particular induction is stated as a schema. Do I make sense? –  Andrej Bauer Apr 18 '12 at 20:12

A NNO is unique up to isomorphism (likewise, a model of second-order arithmetic is unique). In contrast, every first-order theory with at least one infinite model has a proper class of nonisomorphic models of arbitrary large cardinalities, due to Löwenheim–Skolem theorem. Thus, NNO cannot be equivalent to PA, or any other first-order arithmetic for that matter.

-
There is something more subtle here. Category theory, after all, is a first-order theory, and so while within each topos with a NNO the NNO is unique, of course this doesn't mean the NNOs between different categories must be isomorphic (for example, consider the NNOs in SET in a countable $\omega$-model of ZFC and a countable non-$\omega$-model of ZFC). I think the interesting question is: given some "standard" axiomatization $TN$ for a topos with a NNO, let $ATN$ be the set of sentences of arithmetic provable from $TN$. How does $ATN$ compare with $PA$? N.B. this is a syntactic question. –  Carl Mummert Apr 10 '12 at 12:33
In other words, a question I don't know the answer to, because of a lack of familiarity with topos theory, is whether a 'standard' axiomatization of $ATN$ proves the entire theory $Z_2$ of classical second-order arithmetic. I suspect the answer is "yes" from things I have heard, at least if we are talking about toposes with classical internal logic, but in any case I think that this syntactic question gets to the heart of the matter. –  Carl Mummert Apr 10 '12 at 12:45
But this does not seem to be the question the OP is interested in, as he equates NNO with second-order arithmetic (the real categorical one, not two-sorted first-order arithmetic like $Z_2$), and the only way to make sense of that he means models of the arithmetical theory inside the topos. Your question is interesting, but a different one. As for an answer, first, a trivial topos is a topos with a NNO, hence ATN does not even prove $0\ne1$. Ignoring that, the elementary theory of the category of sets (topos with NNO, well-pointed, all epis split) is supposed to have the same strength as ... –  Emil Jeřábek Apr 10 '12 at 12:52
... Zermelo's set theory with separation restricted to $\Delta_0$-formulas. I believe this theory should prove that Z_2 holds in the standard model, since all relevant quantifiers are bounded to $\omega$ or $\mathcal P(\omega)$. The theory should prove much more arithmetic than that (due to its richer language), and in particular, I guess it proves the consistency of $Z_2$. I have no idea what happens when you drop the well-pointedness axiom and the axiom of choice. –  Emil Jeřábek Apr 10 '12 at 12:56
@David Roberts: I am very suspicious of your claims to Carl. Are you quite sure that $\mathrm{Sub}(N)$ is Boolean in a sheaf topos? Wouldn't that imply that $\mathrm{Sub}(1)$ is Boolean? Also, why is the constant $\mathbb{N}$-valued sheaf the nno in a sheaf topos? I thought you had to sheafify it, so you typically get something like the sheaf of locally constant $\mathbb{N}$-valued maps. –  Andrej Bauer Apr 11 '12 at 4:42