Start a new discussion

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeJan 12th 2010

started an Examples-section at natural numbers object

btw, the natural numbers objects of a topos is unique, up to isomorphism, right? if so, we should say that

• CommentRowNumber2.
• CommentAuthorMike Shulman
• CommentTimeJan 12th 2010

Yes, of course, since it has a universal property.

• CommentRowNumber3.
• CommentAuthorUrs
• CommentTimeApr 27th 2012

I have expanded a little at Transfer of NNOs along inverse images.

• CommentRowNumber4.
• CommentAuthorTodd_Trimble
• CommentTimeAug 14th 2013

I added an explicit definition of parametrized NNO to natural numbers object.

I have a question: there is mention in that article of a categories with finite products and a parametrized NNO, and the initial such structure $F$, and it is written that the canonical maps

$\hom_F(N^k, N) \to \hom_{Set}(\mathbb{N}^k, \mathbb{N})$

surject onto the primitive recursive maps. Why couldn’t “surject” be replaced by “biject”?

• CommentRowNumber5.
• CommentAuthorZhen Lin
• CommentTimeAug 14th 2013

Perhaps it’s a question of extensionality? The morphisms $N^k \to N$ are surely constructed by syntactic means, and it’s conceivable that two such morphisms describe the same primitive recursive function in the standard model of arithmetic while not being provably equal (in whatever system of arithmetic corresponds to $F$).

• CommentRowNumber6.
• CommentAuthorTodd_Trimble
• CommentTimeAug 14th 2013

Maybe, but I’d really like to see a specific example of that.

• CommentRowNumber7.
• CommentAuthorZhen Lin
• CommentTimeAug 14th 2013

Hmmm. Well, consider the primitive recursive “function” $G$ defined by $G(n) = 1$ if $n$ codes the proof of a contradiction in Peano arithmetic, and $G(n) = 0$ otherwise. (This is primitive recursive because no unbounded searches are required to verify the validity of a proof.) In the standard model of arithmetic, $G$ is the constant $0$ function, but we could equally consider the elementary topos corresponding to a model of $ZFC + \neg Con(PA)$, in which $G$ is not the constant $0$ function. Thus $G$ and the constant $0$ function must be distinct in the category $F$.

• CommentRowNumber8.
• CommentAuthorTodd_Trimble
• CommentTimeAug 14th 2013

Ah yes, that certainly seems to work. Nice!

• CommentRowNumber9.
• CommentAuthorTodd_Trimble
• CommentTimeAug 14th 2013
• (edited Aug 14th 2013)

But wait: ZFC proves that PA is consistent (since one can establish ordinal induction up to $\epsilon_0$ in ZFC).

Edit: Well, I think the conclusion must still hold anyway: in the initial structure, it cannot be established that $G = 0$, since that would amount to provability of that statement within primitive recursive arithmetic. So $G$ and $0$ are distinct there.

• CommentRowNumber10.
• CommentAuthorZhen Lin
• CommentTimeAug 14th 2013

Oops, quite right. I suppose $ZFC + \neg Con(ZFC)$, with the “function” that verifies proofs of inconsistency of ZFC, is what I meant.

• CommentRowNumber11.
• CommentAuthorDavidRoberts
• CommentTimeDec 28th 2015

Why is it that a parameterized NNO is the same as being preserved by all the functors to the coKelisli categories for the comonad $A\times -$? I’m trying to see how this works as I’d like to think of an NNO as being an initial algebra for a polynomial endofunctor (arising from 1←1→1+1→1) and these two pictures aren’t meshing.

• CommentRowNumber12.
• CommentAuthorziggurism
• CommentTimeMay 21st 2020

please doublecheck my correction. but it seems like the second pair is backwards. if we identify (\pi_1 \circ a, \pi_2 \circ b) and (\pi_2 \circ a, \pi_1 \circ b), that means we’re declaring i-l = j-k for i+j = k+l, whereas we actually want i-l = k-j. So we want to identify (\pi_1 \circ b, \pi_2 \circ a)

• CommentRowNumber13.
• CommentAuthorTodd_Trimble
• CommentTimeMay 21st 2020

Yes, you seem to be correct. Good catch.

• CommentRowNumber14.
• CommentAuthorUrs
• CommentTimeJun 27th 2020