# In a topos with a NNO, how does one define the subobject "$<$'' of $\mathbf N\times\mathbf N$?

The first problem in Chapter VI of Sheaves in Geometry and Logic: A First Introduction to Topos Theory by Mac Lane and Moerdijk has two parts. The first part (which I have already done) can be found in this stackexchange post, and asks the reader to show that, in a topos, each arrow $$\mathbf N \times X \xrightarrow{f} Y$$ is given uniquely by some $$X \xrightarrow{g} Y$$ and another $$X \times Y \xrightarrow{h} Y$$ when the following diagram commutes.

$$\begin{array}{rclcl} 1 \times X & \xrightarrow{0_N \times 1_X} & \mathbf N \times X & \xrightarrow{s \times 1_X} & \mathbf N\times X \newline \pi_2 \downarrow & & \downarrow (f, \pi_2) & & \downarrow f \newline X & \xrightarrow{(g, 1_X)} & Y\times X & \xrightarrow{h} & Y \end{array}$$ In the above diagram, $$\pi_j$$ is the $$j$$th projection, and $$1 \xrightarrow{0_N} \mathbf N \xrightarrow{s} \mathbf N$$ is a NNO. The second asks for several definitions that make use of recursion in a parameter: Addition, multiplication, and the subobject < of $$\mathbf N \times \mathbf N$$. Mac & Moe call this "recursion in a parameter".

Now, I have definitions for addition and multiplication worked out, but I can't seem to find the correct $$g$$ and $$h$$ for the subobject <. What I would like is a hint, not a solution, as to where to look.

A few thoughts on the matter: I imagine that I want $$X = \mathbf N$$ and $$Y = \Omega$$, where $$\Omega$$ is the subobject classifier, so that $$\mathbf N \times \mathbf N \xrightarrow{f} \Omega$$ is the classifying map for $$< \subseteq \mathbf N \times \mathbf N$$. My first attempt was to take $$g(n)$$ to be the formula "$$0 < n$$" ($$g$$ is the characteristic map of the pullback of $$s$$ along $$1_\mathbf N$$), and $$h = \pi_1$$. Here I was trying to model the example, "$$2 < 5$$ because $$1 < 4$$ because $$0 < 3$$," but that isn't how things turned out. Instead, in $$\mathbf{Sets}$$, this would give \begin{align} f (1, 1) &= f \circ (s \times 1_N) (0, 1)\newline &= f (0, 1), \end{align} which is not what I want. I also tried to prove a different theorem than the one in the first part, to make this idea work, in which the "$$s \times 1_X$$" is replaced by "$$s \times s$$" in the diagram, but this also came with issues.

The definition of $$<$$ in terms of addition, as in the last paragraph of Derek Elkins's answer, seems to be a favorite of many topos theorists. My own preference is to define $$x by induction on $$y$$. (Formally, that means defining the curried version $$\mathbb N\to\Omega^{\mathbb N}:y\mapsto(x\mapsto [x of the predicate $$<:\mathbb N^2\to\Omega$$.) The inductive clauses are $$[x<0] = \bot$$ and $$[x

• This construction (or equally the construction in the Derek Elkins answer) also makes it clear that ${<} : \mathbb{N}^2 \to \Omega$ factors through $2$, i.e. $m < n$ is a (uniformly) decidable proposition for all $m, n \in \mathbb{N}$. Oct 11 '20 at 21:44

Think about how you would compute this given just structural recursion on the naturals. You'd likely have a definition like: \begin{align}f(0,n)&=n\neq 0\\f(m+1,0)&=\bot\\f(m+1,n+1)&=f(m,n)\end{align} This corresponds to a nested induction. We can make it fit the format better via: \begin{align}f(0)(n)&=n\neq 0\\f(m+1)(n)&=g(n)\\ g(0)&=\bot\\g(n+1)&=f(m)(n)\end{align} This presents $$f$$ as $$f:\mathbb N\to\Omega^\mathbb N$$. However, $$g$$'s definition depends on $$f$$ and these are mutually recursive, so how can we deal with that. Easy, abstract. \begin{align}f(0)(n)&=n\neq 0\\f(m+1)(n)&=g(n,f(m))\\ g(0,h)&=\bot\\g(n+1,h)&=h(n)\end{align} You can now define $$g$$ independently, and then define $$f$$ in terms of $$g$$. I'll leave it to you to formulate this in the language of an elementary topos.

As an alternative, we often define $$m\leq n$$ as $$m\leq n \iff \exists k:\mathbb N.m+k=n$$. We can easily define $$<$$ in terms of $$\leq$$. Given that you've already defined addition, this too can be articulated in the language of an elementary topos. In this case, it won't (directly) require the universal property of an NNO. It indirectly requires via the definition of addition, of course.

• A year of contemplation, and I can confidently say that, as much as this answer was what I was looking for at the time, Andreas Blass' answer is just so elegant... Feb 26 '20 at 15:43