Strong induction for natural number object

categorical-logiccategory-theorytopos-theory

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!

Best Answer

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$.
Related Question