Most of us meet the natural numbers as a set, or as an inductive type, induced by zero, and the successor map. Lawvere [1] gave a categorical definition that needs neither elements nor syntax for induction. In a category with a terminal object $\top$, a natural numbers object (NNO) is an object $N$ equipped with
- a zero $z : \top \to N$, and
- a successor $s : N \to N$,
that is initial among such structures: for every object $A$ carrying a point $q : \top \to A$ and an endomap $f : A \to A$, there is a unique $u : N \to A$ with
$$ u ∘ z = q \qquad\text{and}\qquad u ∘ s = f ∘ u. $$
Read those two equations as a recursive program: $u(0) = q$ and $u (n{+}1) = f(u,n)$. The universal property is the principle of definition by (structural) recursion — and its uniqueness half is the principle of proof by induction.
What is remarkable is that this element-free object faithfully mimics the familiar naturals: in the category of sets it is the standard naturals, and in a general category it underwrites the same recursive definitions and the same inductive arguments. But it is far from obvious how to recover the familiar properties — even pedestrian arithmetic identities — from this abstraction, where a proof may no longer inspect a number or split into cases, but is only ever a chain of equations between arrows.
This post dwells on that gap, which turned out to be a rabbit hole (for me) and occupied me for much longer than I expected. The destination is a single, innocuous implication about truncated subtraction $\mathbin{\dot-}$ (read $n \mathbin{\dot-} m$ as $n - m$ clamped at $0$):
$$ n \mathbin{\dot-} m = k + 1 \quad\Longrightarrow\quad n = m + (k + 1).$$
— I need it for something else; I may explain one day.
This must be self-evident: a positive difference means $n$ overshoots $m$, so $n$ equals $m$ plus the size of the overshoot. Formalized point-free, in a generic category, it is anything but. What follows is a tour of a surprisingly long path from the bare (parametrized) NNO axioms to that one line. Can it be shorter? I do not know.
The whole route is illustrated by a formalization in the Agda proof assistant [5] using a setoid-based deep embedding of category theory into dependent type theory.
Formalizing the Naturals
agda-categories [2] is a large development of category theory in Agda, and an NNO drops into it almost verbatim. Here is the core record, lightly trimmed:
record IsNNO (N : Obj) : Set (o ⊔ ℓ ⊔ e) where
field
z : ⊤ ⇒ N
s : N ⇒ N
universal : ∀ {A} → ⊤ ⇒ A → A ⇒ A → N ⇒ A
z-commute : ∀ {A} {q : ⊤ ⇒ A} {f : A ⇒ A} → q ≈ universal q f ∘ z
s-commute : ∀ {A} {q : ⊤ ⇒ A} {f : A ⇒ A} → f ∘ universal q f ≈ universal q f ∘ s
unique : ∀ {A} {q : ⊤ ⇒ A} {f : A ⇒ A} {u : N ⇒ A} → q ≈ u ∘ z → f ∘ u ≈ u ∘ s → u ≈ universal q f
universal q f is the recursor; z-commute/s-commute are its two defining equations; unique is induction. The whole thing lives in an arbitrary category C — it is point-free. There are no elements n : N to pattern-match on; everything we say about numbers will be an equation between arrows.
There is a catch though: the bare recursor produces maps out of N: universal q f : N ⇒ A, seeded by a global point q : ⊤ ⇒ A. This for one thing is not enough to define binary functions, such as addition and subtraction sum, sub : N × N ⇒ N. To define them one needs to recurse in one argument while the other rides along as a parameter. A global seed ⊤ ⇒ A has nowhere to put that parameter.
This is standardly remedied by currying: a map A × N ⇒ X is the same thing as N ⇒ Xᴬ, so you recurse over N into the exponential Xᴬ and uncurry at the end. But that move requires the exponential Xᴬ to exist, which is the case if the category is Cartesian closed. I am not assuming that. My ambient category has finite products and nothing more.
So the parameter must be built into the universal property from the start. That is the parametrized NNO, and it is actually the one we take as a basis:
record IsParametrizedNNO (N : Obj) : Set (o ⊔ ℓ ⊔ e) where
field
z : ⊤ ⇒ N
s : N ⇒ N
universal : ∀ {A X} → A ⇒ X → X ⇒ X → A × N ⇒ X
commute₁ : ∀ {A X} {f : A ⇒ X} {g : X ⇒ X}
→ f ≈ universal f g ∘ ⟨ id , z ∘ ! ⟩
commute₂ : ∀ {A X} {f : A ⇒ X} {g : X ⇒ X}
→ g ∘ universal f g ≈ universal f g ∘ (id ×₁ s)
unique : ∀ {A X} {f : A ⇒ X} {g : X ⇒ X} {u : A × N ⇒ X}
→ f ≈ u ∘ ⟨ id , z ∘ ! ⟩ → g ∘ u ≈ u ∘ (id ×₁ s)
→ u ≈ universal f g
Now universal f g : A × N ⇒ X takes a seed f : A ⇒ X that may depend on the parameter A, and commute₁/commute₂ read as recursion with that parameter in scope:
$$ u(x, 0) = f(x), \qquad u(x, n{+}1) = g(u(x, n)). $$
This scheme is a special case of primitive recursion, which is in fact derivable from it in full generality. Namely,
primitive recursion defines u from f as before and g of a more general form:
$$ u(x, 0) = f(x), \qquad u(x,\ n{+}1) = g(u(x, n),\ x,\ n). $$
We thus iterate not on the bare value but on a triple carrying the value together with the parameter and the current index: seed it at (f x, x, 0), let each step apply g to the value and bump the index while leaving the parameter alone, then project the value back out at the end:
module _ {X C : Obj} (zero : X ⇒ C) (succ : C × X × N ⇒ C) where
prec : X × N ⇒ C
prec = π₁ ∘ universal ⟨ zero , ⟨ id , z ∘ ! ⟩ ⟩ ⟨ succ , (id ×₁ s) ∘ π₂ ⟩
Here ⟨ id , z ∘ ! ⟩ plants the index at $0$, (id ×₁ s) ∘ π₂ is what increments it, and π₁ reads off the value; the two equations above then hold as the lemmas prec-zero and prec-succ.
Every parametrized NNO is an NNO, but the converse holds only in presence of (certain) exponentials [4].
Basic Definitions and Properties
With prec in hand, truncated subtraction and addition are two-liners. Writing s⁻¹ for the truncated predecessor:
sum : N × N ⇒ N -- n + 0 = n, n + (m+1) = (n + m) + 1
sum = prec id (s ∘ π₁)
sub : N × N ⇒ N -- n ∸ 0 = n, n ∸ (m+1) = (n ∸ m) ∸ 1
sub = prec id (s⁻¹ ∘ π₁)
and max, min are easily expressible:
max = sum ∘ ⟨ sub , π₂ ⟩ -- max(n,m) = (n ∸ m) + m
min = sub ∘ ⟨ π₁ , sub ⟩ -- min(n,m) = n ∸ (n ∸ m)
Defining the arithmetic, then, is easy and pleasant. The natural next question: can we prove, point-free, the facts every schoolchild knows? Commutativity and associativity of $+$; that max and min commute; that $(n+m) \mathbin{\dot-} m = n$. Each is an equation between arrows, so each ought to be provable — and many are, with varying effort:
sum-comm : sum ∘ swap ≈ sum -- n + m = m + n
sum-assoc : sum ∘ (sum ×₁ id) ≈ sum ∘ ⟨ π₁ ∘ π₁ , sum ∘ (π₂ ×₁ id) ⟩ -- (n + m) + k = n + (m + k)
sub-sum : sub ∘ ⟨ sum , π₂ ⟩ ≈ π₁ -- (n + m) ∸ m = n
sub-Δ : sub ∘ Δ ≈ z ∘ ! -- n ∸ n = 0
And then there is the one I expected to dispatch in an afternoon – call it the positive difference lemma:
-- if n ∸ m = k+1, then n = (k + m) + 1
sub>0 : sub ∘ ⟨ n , m ⟩ ≈ s ∘ k → n ≈ s ∘ sum ∘ ⟨ k , m ⟩
On paper this is nothing. If $n \mathbin{\dot-} m$ is a successor $k+1$, then $n$ genuinely exceeds $m$, so $n = (n \mathbin{\dot-} m) + m = (k+1) + m$. One line. The rest of this post is a winding story of deriving it painstakingly from the definition of a parametrized NNO.
Why “Obvious” Is a Lie
Part of the trouble is that the positive difference lemma is a conditional statement: an implication that assumes $n \mathbin{\dot-} m = k+1$ and concludes $n = m + (k+1)$. With some creativity, conditional statements can still be reduced to unconditional identities. One good example is the cancellativity of addition:
cancel : sum ∘ ⟨ n , k ⟩ ≈ sum ∘ ⟨ m , k ⟩ → n ≈ m
That is: $n + k = m + k$ implies $n = m$. The unconditional equation behind it — the one that yields it at once — is sub-sum, $(n+m) \mathbin{\dot-} m = n$. Proving such unconditional identities, however, is still generally tricky. The recipe behind every easy one so far (except for deriving it from other equations by plain equational reasoning) is to single out a pivotal variable, induct over it through the recursion principle, and carry the rest along as parameters: sum-comm, sub-sum, sub-Δ are all proven this way — precisely the recipe the parametrized NNO naively supports.
Fiddling long enough with the positive difference lemma reveals one equation, mentioned above, which turns out to be unavoidable — commutativity of maximum, $\max(n,m) = \max(m,n)$, i.e.
$$ n + (m \mathbin{\dot-} n) = m + (n \mathbin{\dot-} m). $$
Naive attempts to prove it by induction over $n$ or over $m$ fail hopelessly. However, the equation turns out to be so special that Goodstein’s entire 1954 paper [3] revolves around it: it is credited there as a key equation, instrumental for building a logic-free system of recursive arithmetic — in a way justifying that the definition of (parametrized) natural numbers through a universal property, as above, is indeed the right one.
Goodstein’s Trick
Note the identity
$$ \max(n,m) = \sum_{i \ge 0} \operatorname{sgn}\big((n \mathbin{\dot-} i) + (m \mathbin{\dot-} i)\big), $$
where the signum $\operatorname{sgn}$ ($\operatorname{sgn} 0 = 0$, $\operatorname{sgn}(n+1) = 1$) is easily definable.
The summand is $1$ exactly when $i < \max(n,m)$ (at least one of $n \mathbin{\dot-} i$, $m \mathbin{\dot-} i$ is positive precisely when $i$ is below the larger of the two), and $0$ otherwise — so the sum is $\max(n,m)$. The summand $(n \mathbin{\dot-} i) + (m \mathbin{\dot-} i)$ is now visibly symmetric in $n$ and $m$, which makes the resulting formula a provably commutative definition of max without ever comparing $n$ and $m$. That is the essence of Goodstein’s trick.
We thus implement recursively:
-- goodstein((n,m), k) = Σ_{i<k} sgn((n ∸ i) + (m ∸ i))
goodstein : (N × N) × N ⇒ N
goodstein = prec (z ∘ !) (sum ∘ (id ×₁ sgn ∘ sum ∘ subs))
Here subs is the pair of differences against the current index, subs((n,m),k) = (n ∸ k, m ∸ k).
Now, what ties goodstein back to max is one provable recurrence:
-- max(n ∸ 1, m ∸ 1) + sgn(n + m) = max(n, m)
max-succ : sum ∘ ⟨ max ∘ (s⁻¹ ×₁ s⁻¹) , sgn ∘ sum ⟩ ≈ max
It says that lowering both arguments by one drops $\max$ by exactly $\operatorname{sgn}(n+m)$. Using that, we can show that the sum $\max(n \mathbin{\dot-} k, m \mathbin{\dot-} k) + \mathrm{goodstein}((n,m),k)$ remains the same if $k$ is increased by one, and at $k = 0$ it equals $\max(n,m)$. By induction on $k$, therefore
$$ \max(n \mathbin{\dot-} k,\ m \mathbin{\dot-} k)\ +\ \mathrm{goodstein}((n,m),k)\ =\ \max(n,m). $$
The same consideration can be repeated with $n$ and $m$ exchanged, and using the
fact that goodstein is stable under permutation of its first two arguments, we obtain
$$ \max(m \mathbin{\dot-} k,\ n \mathbin{\dot-} k)\ +\ \mathrm{goodstein}((n,m),k)\ =\ \max(m,n). $$
Now, set $k = m$ in both equations. Then $m \mathbin{\dot-} m = 0$, so $\max(n \mathbin{\dot-} m, 0) = \max(0, n \mathbin{\dot-} m) = n \mathbin{\dot-} m$. Both left-hand sides end up being equal, giving us the desired commutativity of $\max$:
$$ \max(n,m)\ =\ (n \mathbin{\dot-} m) + \mathrm{goodstein}((n,m),m)\ =\ \max(m,n). $$
Lots of auxiliary machinery is omitted (such as proving $\max(n,0) = n$ and the like), but it is relatively easy, albeit tedious, to prove.
Positive Difference Lemma
The hard part is seemingly behind us. Recall the goal: if $n \mathbin{\dot-} m = k+1$, then $n = m + (k+1)$.
With max-comm available the argument is — again seemingly — short. The hypothesis says the difference $n \mathbin{\dot-} m$ is positive, so $n$ is the larger of the two numbers, and the larger of two numbers is their maximum. Point-free, in three moves:
- $n = 0 + n = (m \mathbin{\dot-} n) + n = \max(m, n)$ — provided $m \mathbin{\dot-} n = 0$;
- $\max(m, n) = \max(n, m)$, by
max-comm; - $\max(n, m) = (n \mathbin{\dot-} m) + m = (k+1) + m = (k + m) + 1$, using the hypothesis $n \mathbin{\dot-} m = k+1$.
So two ingredients carry it: commutativity of max, and the proviso in the first move — that a positive difference one way forces a zero difference the other way:
-- n ∸ m > 0 ⟹ m ∸ n = 0
n∸m>0→m∸n=0 : sub ∘ ⟨ n , m ⟩ ≈ s ∘ k → sub ∘ ⟨ m , n ⟩ ≈ z ∘ !
Written out, sub>0 is exactly that chain of three:
sub>0 eq = begin
n ≈⟨ sum-zˡ ⟨
sum ∘ ⟨ z ∘ ! , n ⟩ ≈⟨ pushʳ (unique (pullˡ project₁ ○ eq') (pullˡ project₂ ○ project₂)) ⟩
max ∘ ⟨ m , n ⟩ ≈⟨ pushˡ max-comm ○ ∘-resp-≈ʳ swap∘⟨⟩ ⟩
max ∘ ⟨ n , m ⟩ ≈⟨ pushʳ (unique (pullˡ project₁ ○ eq) (pullˡ project₂ ○ project₂)) ⟨
sum ∘ ⟨ s ∘ k , m ⟩ ≈⟨ pushʳ (sym first∘⟨⟩) ○ pushˡ sum-sˡ ⟩
s ∘ sum ∘ ⟨ k , m ⟩ ∎
where
eq' : sub ∘ ⟨ m , n ⟩ ≈ z ∘ !
eq' = n∸m>0→m∸n=0 eq
The justification terms within ≈⟨ ⟩ are constructed from equational proof manipulation primitives of agda-categories.
The Missing Bits
With max-comm established, one might expect the positive difference lemma to follow quickly. But it still does not. max-comm is heavily used in what follows, but it is not sufficient on its own: a substantial amount of further work is still needed to close the remaining gaps.
The proviso, n∸m>0→m∸n=0, rests on two facts:
-- n ∸ m = (n ∸ m) ∸ (m ∸ n)
sub-sub-comm : sub ≈ sub ∘ ⟨ sub , sub ∘ swap ⟩
-- n ∸ (k+1) = n ⟹ n = 0
n∸sk≈n : sub ∘ ⟨ n , s ∘ k ⟩ ≈ n → n ≈ z ∘ !
sub-sub-comm says that subtracting the other difference changes nothing. n∸sk≈n says a number that survives subtracting a successor unchanged must be zero. Putting them together: assume $n \mathbin{\dot-} m = k+1$. By sub-sub-comm with $n$ and $m$ swapped, $(m \mathbin{\dot-} n) \mathbin{\dot-} (n \mathbin{\dot-} m) = m \mathbin{\dot-} n$; since $n \mathbin{\dot-} m = k+1$, that reads $(m \mathbin{\dot-} n) \mathbin{\dot-} (k+1) = m \mathbin{\dot-} n$. So n∸sk≈n forces $m \mathbin{\dot-} n = 0$.
That is the logical skeleton. Both supporting facts, however, require further work. Here is a sketch of the dependency spine, checked against the proofs:
sub>0 -- n ∸ m = k+1 ⟹ n = (k+m)+1
├─ max-comm -- commutativity of max
│ ├─ goodstein -- Goodstein's helper
│ ├─ max-succ -- max(n ∸ 1, m ∸ 1) + sgn(n + m) = max(n, m)
│ └─ max-subs-xyy / -yxy -- max(x ∸ y, y ∸ y) = max(y ∸ y, x ∸ y) = x ∸ y
└─ n∸m>0→m∸n=0 -- n ∸ m > 0 ⟹ m ∸ n = 0
├─ sub-sub-comm -- n ∸ m = (n ∸ m) ∸ (m ∸ n)
│ ├─ sub-min -- a ∸ b = a ∸ min(a, b)
│ └─ min-subs -- min(n ∸ m, m ∸ n) = 0
│ ├─ min-transl -- min(n, m) + k = min(n + k, m + k)
│ │ └─ sub-transl -- (n + k) ∸ (m + k) = n ∸ m
│ └─ min-comm -- min(n, m) = min(m, n)
└─ n∸sk≈n -- n ∸ (k+1) = n ⟹ n = 0
├─ n∸k≈n -- n ∸ (k+1) = n ⟹ n ∸ j = n (for any j)
│ └─ n∸sk≈n∸k -- n ∸ (k+1) = n ⟹ n ∸ (j+1) = n ∸ j (for any j)
│ └─ n∸1≈n -- n ∸ (k+1) = n ⟹ n ∸ 1 = n
│ └─ 1∸n≈1 -- n ∸ (k+1) = n ⟹ 1 ∸ n = 1
│ └─ sk∸n≈sk -- n ∸ (k+1) = n ⟹ (k+1) ∸ n = k+1
└─ sub-Δ -- n ∸ n = 0
sub-sub-comm leans on sub-min and the disjointness lemma min-subs, which in turn need translation-invariance (sub-transl, min-transl) and commutativity of min; and min-comm is max-comm carried through cancellation.
n∸sk≈n is proved through a chain of intermediate equations, each holding under the hypothesis $n \mathbin{\dot-} (k+1) = n$: from $(k+1) \mathbin{\dot-} n = k+1$ (sk∸n≈sk), to $1 \mathbin{\dot-} n = 1$ (1∸n≈1), to $n \mathbin{\dot-} 1 = n$ (n∸1≈n), to $n \mathbin{\dot-} (j+1) = n \mathbin{\dot-} j$ for every $j$ (n∸sk≈n∸k), and by induction to $n \mathbin{\dot-} j = n$ for every $j$ (n∸k≈n). Setting $j = n$ and comparing with $n \mathbin{\dot-} n = 0$ (sub-Δ) gives $n = 0$.
max-comm is used at several points: directly in sub>0, in min-comm, and in the sk∸n≈sk and n∸1≈n steps under n∸sk≈n.
What can we conclude from this? In a way, it all worked out as expected. The definition we started with — thanks to Lawvere — turned out to be enough, even though we made no extra assumptions about the ambient category, assumptions that would certainly have made the task simpler, or even trivial. There is something almost magical in how natural numbers and primitive recursion stay so robust that the ambient category need not ever interfere with the arguments built on them (what Goodstein called “logic-free”). And yet, to achieve this, the path from the axioms to a simple, natural statement can become remarkably non-linear, passing through numerous waypoints that are hard to foresee.
References
[1] Lawvere, F. W. (1964). “An elementary theory of the category of sets.” Proceedings of the National Academy of Sciences 52(6), 1506–1511.
[2] Hu, J. Z. S. and Carette, J. (2021). “Formalizing Category Theory in Agda.” CPP 2021. Library: https://github.com/agda/agda-categories.
[3] Goodstein, R. L. (1954). “Logic-free formalisations of recursive arithmetic.” Mathematica Scandinavica 2, 246–260.
[4] nLab authors. “Natural numbers object — with parameters.” https://ncatlab.org/nlab/show/natural+numbers+object#withparams.
[5] https://gist.github.com/sergey-goncharov/ea2ff922e1dade03aac538cbdd412d8e.