From Lawvere's paper about ETCS we know that we can do induction for natural number object. My aim is to prove the strong induction principle for an NNO in a topos by translating this argument https://math.ou.edu/~nbrady/teaching/f14-2513/LeastPrinciple.pdf ((I) $\to$ (SI)) into an abstract version, so it works in any category satisfies ETCS. In particular, the axioms of ETCS make sure that we have a Boolean topos.

I think the statement of strong induction to prove in ETCS 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$ where $p$ is an isomorphism.

Here $N$ is the NNO, $s: N \to N$ is the successor map the $\le$ relation on NNO 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 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 (which is not in Lawvere's original paper). Hence I 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?

If anything I said is wrong, or if there is a better approach, thanks a lot for pointing out!

  • $\begingroup$ The condition '$-\circ\langle n_0,n\rangle=o$' to state $n_0\le n$ was hard to comprehend. And the conclusion should be that specifically $p$ is an isomorphism. $\endgroup$ – Berci Dec 9 '20 at 16:26
  • $\begingroup$ @Berci $-\circ \langle n_0,n\rangle = o$ just states that $n_0 - n = 0$ (as $-$ is truncated subtraction, that produces an element of natural number, if $n_0 - n$ is negative when we do subtraction on integers, it will still give $0$.) Therefore this condition is just that $n_0 \le n$. And thank you! It should be $p$ is an isomorphism. $\endgroup$ – Y.X. Dec 10 '20 at 0:49

The construction you want definitely works in any elementary topos (with an NNO), even those which are not Boolean, and in fact it will also work in any arithmetic universe ("predicative toposes, toposes without power objects").

I'm in a hurry, there are surely more elegant ways to construct $Q$, but here is one:

  1. Construct $List(P)$, the object of (finite) lists of values from $P$.
  2. Construct the map $N \to List(N)$ thought as mapping $n$ to $[0,1,\ldots,n-1]$.
  3. Intersect $List(P)$ with the image of that map (as subobjects of $List(N)$).
  4. The image of the resulting object under the map $length : List(N) \to N$ is the desired object $Q$.
  • $\begingroup$ Thank you! This method is interesting. I know the concept of "list object", but could you please tell me if there is an explicit construction of such an object in a topos? $\endgroup$ – Y.X. Dec 22 '20 at 13:32
  • 1
    $\begingroup$ There is. Again, without claim for maximum elegance, you could construct $List(A)$ as a suitable subobject of the internal hom $[N,1+A]$, where $1$ is the terminal object and $+$ means coproduct. The object $[N,1+A]$ itself is the object of infinite lists with holes. Alternatively, you could construct $List(A)$ as a suitable subobject of $P(N \times A)$ (any list can be regarded as a set of index-value-pairs). $\endgroup$ – Ingo Blechschmidt Dec 25 '20 at 14:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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