nForum - Search Results Feed (Tag: natural) 2022-01-17T11:43:33-05:00 https://nforum.ncatlab.org/ Lussumo Vanilla & Feed Publisher Strong induction principle for NNO https://nforum.ncatlab.org/discussion/12029/ 2020-12-09T06:50:21-05:00 2020-12-13T13:59:17-05:00 YimingXu https://nforum.ncatlab.org/account/2504/ It is well-known that we can do proof by induction in a topos using the natural number object, I am interested in proving the strong induction principle, and I am attempting to translate this proof ...

It is well-known that we can do proof by induction in a topos using the natural number object, I am interested in proving the strong induction principle, and I am attempting to translate this proof here https://math.ou.edu/~nbrady/teaching/f14-2513/LeastPrinciple.pdf ( (I) $\to$ (SI) ) into an abstract version, so it works for the natural number object in a category satisfies ETCS (In particular, the topos satisfies well-foundedness, and every subobject has complement, therefore, this is a Boolean topos).

The $\le$ relation is given as the pullback of $o: 1\to N$, as the element $0$ of natural number, along the map truncated subtraction $-: N\times N \to N$, as in Sketch of an elephant by Johnstone (page 114, A2.5).

I think the statement of strong induction to prove is as the following.

For a subobject $p: P \to N$, if for an arbitary element $n: 1 \to N$ of the NNO, “all member $n_0: 1\to N$ such that $- \circ \langle n_0, n\rangle = o$ factorises through $P$” implies “$s \circ n: 1 \to N \to N$ factors through P”, then $P\cong N$.

I am not sure what to do with the $Q$ though, and I am not sure if constructing such a $Q$ need the comprehension axiom for ETCS, and hence have trouble translating the proof in the link to also work for NNO. I think if we translate the proof, then we should reduce the task of $P\cong N$ into the task of proving $Q \cong N$. I am now asking about how to construct such a $Q$, which corresponds to the predicate $Q$ in the link. Any help, please?

p.s. The problem that I am actually interested in is proving the well-foundedness of natural number object (explicitly, every non-empty set has a minimal element), but the “material set theoretic proof” using strong induction. Therefore I think I should get strong induction principle for NNO. It will also be great if we can directly prove the well-ordered principle for NNO. (Have searched online for well-orderedness and strong induction for NNO, but nothing helpful is found. Is there any material to read about them?)

]]>
Relating two functors via one "intermediary" functor. https://nforum.ncatlab.org/discussion/7888/ 2017-07-05T11:47:18-04:00 2017-07-05T11:56:32-04:00 Peter Heinig https://nforum.ncatlab.org/account/1588/ (reconsidered; no time at the moment to bring post into satisfactory form)

(reconsidered; no time at the moment to bring post into satisfactory form)

]]>
equivariant_related_illustration20170619 https://nforum.ncatlab.org/discussion/7857/ 2017-06-19T05:29:57-04:00 2017-06-19T05:29:57-04:00 Peter Heinig https://nforum.ncatlab.org/account/1588/ Created equivariant_related_illustration20170619, for future use.

Created equivariant_related_illustration20170619, for future use.

]]>
A proof that the induction principle holds in a suitable type theory https://nforum.ncatlab.org/discussion/7751/ 2017-05-10T12:11:05-04:00 2017-05-15T15:56:36-04:00 JamesSmith https://nforum.ncatlab.org/account/1586/ Hi, I am trying to answer my own question here… Is it possible to derive the axiom of induction from a model of the natural numbers? …and came across this page on nLab: natural numbers ...

Hi,

I am trying to answer my own question here…

Is it possible to derive the axiom of induction from a model of the natural numbers?

natural numbers type

This seems to have what I need, but the going is hard. I wonder if anyone can help.

I am stuck, for example, on what exactly $rec_p^n(...)$ is, and what a fibration is. The text says ’the above fibration’ but there is no fibration above so far as I can see, only what I’m guessing is a related display map. The page on fibrations is duanting and didn’t, at a quick glance, seem to give me the necessary relevant information.

All help appreciated!

Kind regards,

James

]]>