8
$\begingroup$

Nelson's predicative arithmetic (survey article) is a very weak system of arithmetic extending Robinson's $Q$ (Wikipedia).

We can have natural number objects in a topos, or even a merely finitely complete category, which essentially model the Peano axioms, so it is natural to wonder if we have objects which in some sense are internal versions of weaker arithmetics.

In particular, even though this question would be interesting for $Q$, Nelson's arithmetic is interesting in that one has the collection of natural numbers, but one can only prove that an initial segment forms a commutative ring closed under successor, rather than the collection of all the natural numbers (I'm fudging on some metamathematical details here). Also, one cannot define a total exponentiation function on any initial segment.

So is there a way to talk about Nelson Natural Number Objects in a category? (i.e. NNNOs - which could be a rich source of spell-checking confusion :) Assume as much structure on said category as necessary.

Improve this question
$\endgroup$
3
  • 2
    $\begingroup$ I don't have time to write a proper answer, but basically yes. By going from intuitionistic to linear lambda calculus (CCCs to monoidal closed cats), fewer recursive functions are definable. This gives implicit characterizations of complexity classes, and by using these calculi as realizers, you can give realizability models of things like Nelson arithmetic. Be warned that these logics are often quite strange, since contraction fails (as $A \to A \otimes A$ isn't definable in general). E.g., see Terui's Light Affine Set Theory. The general area is called "implicit complexity". $\endgroup$
    – Neel Krishnaswami
    Jul 28, 2011 at 7:47
  • 2
    $\begingroup$ The category can't be too rich, or else you will get something like $\lambda$-calculus on top of $\mathscr{Q}$, which will increase the power of the calculus. $\endgroup$
    – Andrej Bauer
    Jan 25, 2013 at 12:07
  • $\begingroup$ @Andrej, I would expect natural examples to not be cartesian closed, so no λ-calculus. $\endgroup$
    – David Roberts ♦
    Jan 27, 2013 at 3:01

1 Answer 1

Reset to default
1
$\begingroup$

I think the answer is no, because being an natural number object is a universal property and being a model of Nelson arithmetic is not.

As long as a category is Heyting (is a regular category where the inverse image maps between subobject lattices have right adjoints) it is possible to talk about models of any first order theory inside the category. There is a problem though: often the models of a first order theory are not unique up to (unique) isomorphism in Heyting categories. So being the model of a first order theory in a Heyting category isn't often a universal property.

A natural number object is not essentially a model of Peano arithmetic, as Peano arithmetic has many non standard models. I would say that it is essentially a model of second order arithmetic, although this doesn't directly make sense in other categories than toposes.

Nelson arithmetic is weaker than Peano arithmetic, and therefore has the same non standard models, if not many more. One could say that there are usually are many non isomorphic Nelson natural number objects. But I don't think this is what you mean.

After Francois' comment, I might have a better idea of what you are looking for. I suppose you want something like a natural number object, that happens to force Nelson's arithmetic in the internal language.

The definition of natural number object makes sense in arbitrary monoidal categories, if formulated properly. In these contexts we still have all primitive recursive functions, though; they don't have the restrictions in complexity that the survey article on Nelson's arithmetic mentions. So removing structure from the ambient category is insufficient.

Linear logics are capable of controlling complexity, and I would look for an answer there. The idea is that the ambient category has an endofunctor $!$, and that recursion does not give you morphisms from the natural number object $N$, but from $!N$ instead. You can now control the debt of recursion in functions $N\to N$ by controlling which morphisms $!N\to N$ factor though a canonical morphism $!N\to N$. I have tried to find a related universal property a couple of months back, but have been unsuccessful.

Improve this answer
$\endgroup$
4
  • 2
    $\begingroup$ This is the wrong point of view. Every topos with a nno has a unique nno, but not all toposes have the same nno. The nnos that occur in this way are known - mathoverflow.net/questions/93631/nno-first-order-pa David is asking whethere there is a class of categories and "nnnos" that correspond to Nelson's theory. $\endgroup$
    – François G. Dorais
    Jan 25, 2013 at 18:06
  • $\begingroup$ An NNO corresponds to Peano's original formulation, which is second-order, but is not the same thing as second-order arithmetic $Z_2$. (I don't think I knew this when I asked this question.) Perhaps we could have some sort of comonad which encodes the modalities summable and multiplicable, not necessarily $!$. $\endgroup$
    – David Roberts ♦
    Jan 27, 2013 at 2:08
  • 2
    $\begingroup$ When linear logic was introduced by Girard, $!$ was a comonad. In order to get control over complexity, however, you have to let go of $!\alpha\to !!\alpha$, I think. $\endgroup$
    – Wouter Stekelenburg
    Jan 27, 2013 at 9:06
  • $\begingroup$ Hmm, ok. I'll have a look at it. Thanks! $\endgroup$
    – David Roberts ♦
    Jan 28, 2013 at 23:03

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.