Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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
Yes, of course, since it has a universal property.
I have expanded a little at Transfer of NNOs along inverse images.
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”?
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$).
Maybe, but I’d really like to see a specific example of that.
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$.
Ah yes, that certainly seems to work. Nice!
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.
Oops, quite right. I suppose $ZFC + \neg Con(ZFC)$, with the “function” that verifies proofs of inconsistency of ZFC, is what I meant.
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.
1 to 11 of 11