4
$\begingroup$

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.

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

2 Answers 2

Reset to default
6
$\begingroup$

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.

Improve this answer
$\endgroup$
15
  • $\begingroup$ 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. $\endgroup$
    – Carl Mummert
    Commented Apr 10, 2012 at 12:33
  • $\begingroup$ 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. $\endgroup$
    – Carl Mummert
    Commented Apr 10, 2012 at 12:45
  • $\begingroup$ 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 ... $\endgroup$
    – Emil Jeřábek
    Commented Apr 10, 2012 at 12:52
  • 1
    $\begingroup$ ... 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. $\endgroup$
    – Emil Jeřábek
    Commented Apr 10, 2012 at 12:56
  • 1
    $\begingroup$ @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. $\endgroup$
    – Andrej Bauer
    Commented Apr 11, 2012 at 4:42
6
$\begingroup$

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.

Improve this answer
$\endgroup$
8
  • $\begingroup$ 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$. $\endgroup$
    – David Roberts ♦
    Commented Apr 11, 2012 at 7:45
  • $\begingroup$ You can apply the results just to $\mathrm{Set}$ if you wish. That is a special case. $\endgroup$
    – Andrej Bauer
    Commented Apr 11, 2012 at 8:26
  • 2
    $\begingroup$ 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. $\endgroup$
    – Ulrik Buchholtz
    Commented Apr 18, 2012 at 19:34
  • 1
    $\begingroup$ @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? $\endgroup$
    – Andrej Bauer
    Commented Apr 18, 2012 at 20:12
  • 2
    $\begingroup$ @Andrej: yes, you make sense, and I guess my objection is more terminological: I would take first-order PA to satisfy an induction schema for first-order formulas only, whereas the version here (in Lambek and Scott) is schematic in all (ambiently definable) predicates on N. If you have a PA object N in a topos that only satisfies induction for first-order formulas, then it could be non-standard, but in the topos logic you could then separate out the standard part and make a NNO. $\endgroup$
    – Ulrik Buchholtz
    Commented Apr 21, 2012 at 16:48

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .