Categorical Numbers

Sorry for the delay in the category theory articles. I've been busy with work, and haven't had time to do the research to be able to properly write up the last major topic that I plan to cover in cat theory. While doing my research on closed cartesian categories and lambda calculus, I came across this little tidbit that I hadn't seen before, and I thought it would be worth taking a brief diversion to look at.

Category theory is sufficiently powerful that you can build all of mathematics from it. This is something that we've known for a long time. But it's not really the easiest thing to demonstrate.

But then, I came across this lovely little article on wikipedia. It turns out that you can [build the natural numbers entirely in terms of categories][wikipedia] in a beautifully simple way.

Before we dive into categorical numbers, let's take a moment to remember what we really mean by natural numbers.

Peano Arithmetic
------------------

The meanings of natural numbers are normally defined in terms of what we call *Peano arithmetic*. Peano arithmetic defines the natural numbers, **N** in terms of five fundamental axioms:

1. 0 ∈ **N** (0 is a natural number.)
2. ∀ a ∈ **N** ∃ a'=s(n), a' ∈ **N**. (Every natural number a has a successor, s(a))
3. ¬ ∃ a ∈ **N** : s(a)=0. (No natural number has 0 as its successor.)
4. ∀ a,b ∈ **N**: s(a)=s(b) ⇒ a=b. (Each number has a unique successor.)
5. (P(0) ∧ ∀ a : P(a) ⇒ P(s(a))) ⇒ ∀ b ∈ **N** : P(b). (If a property P is true for 0; and it can be shown that for any number a, if it's true for a, then it's true for b, then that means that it's true for all natural numbers. This is the *axiom of induction*.)

To get to arithmetic, we need to add two operations: addition and multiplication.

We can define addition recursively quite easily:

1. ∀ x ∈ **N**: x+0 = x
2. ∀ x,y ∈ **N**: s(x)+y=x+s(y)

And once we have addition, we can do multiplication:

1. ∀ x ∈ **N**: x \* 0 = 0 ∧ 0 \* x = 0
2. ∀ x ∈ **N**: 1 \* x = x
3. ∀ x,y ∈ **N**: s(x)\*y = (x\*y) + y

To sum up: Peano arithmetic is based on a definition of the natural numbers in terms of five fundamental properties, called the Peano axioms, built on "0", a successor function, and induction. If we have those five properties, we can define addition and multiplication; and given those, we have the ability to build up arbitrary functions, sets, and the other fundamentals of mathematics in terms of the natural numbers.

Peano Naturals and Categories
---------------------------------

The peano axioms can be captured in a category diagram for a relatively simple object called a *natural number object (NNO)*. A natural number object can exist in many categories: basically any category with a terminal object *can* have NNOs. Any closed cartesian category *does* have an NNO.

There are two alternate constructions; a general construct that works for all NNO-containing categories; and a more specific one for closed cartesian categories. (You can show that they are ultimately the same in a CCC.)

I actually think that the general one is easier to understand, so that's what I'll describe. This is basically a construction that captures the ideas of successor and recursion.

Given a category C with a terminal object **1**. A *natural number object* is an object *N* with two arrows z : 1 → *N*, and s : *N* → *N*, where z and s have the following property.

(∀ a ∈ Obj(C), (q : 1 → a, f : a → a) ∈ Arrows(C)) : u º z = q ∧ u º s = f º u.

That statement means the same thing as saying that the following diagram commutes:

Let's just walk through that a bit. Think of the object **N** as a set. "s" is successor. So S is an arrow from *N* to *N* that maps each number to its successor. *N* is "rooted" by the terminal object; that gives it its basic structure. The "z" arrow from the terminal object maps to the zero value in *N*. So we've got an arrow that selects zero; and we've got an arrow that defines the successor.

Think of "q" as a predicate, and "u" as a statement that a value in *N* satisfies the predicate.

So u º z, that is the path from 1 to a by stepping through z and u is a statement that the predicate "q" is true for z (zero); because composing u (the number I'm composed with satisfies q) and z (the number zero) gives us "q" (zero satifies q).

Now the induction rule part. *N* maps to *N* by s - that's saying that s is an arrow from a number in *N* to its successor. If you have an arrow composition that says "q is true for n", then f can be composed onto that giving you "q is true for n + 1".

If for all q, u is unique - that is, there is only *one* mapping where induction works; then you've got a categorical structure that satisfies the Peano axioms.

[wikipedia]: http://en.wikipedia.org/wiki/Natural_number_object