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.
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.
Shouldn't that be s(x)*y = (x*y)+y?
Otherwise, great post as always.
Good catch, thanks.
Do the Peano axioms as shown have the properties for only the natural number (0, 1, 2, ...). Could we have these axioms for some other set of numbers. We could start with 0 and let the successor function define as adding 0.5 Then s(0) = 0.5 this would map to the symbol '1' s(s(0)) would be 1.0 and this would map to the symbol '2' and so on. I think that some other axioms would be needed to define the natural numbers and only them.
David: The successor function isn't defined as "Add 1 to the number". This would imply that we're using numbers (and addition!) to define numbers!
Rather, we define a function called successor. That's it. The other axioms define something about it. The result returned by successor is also a number, all numbers have a unique successor, and no number has 0 as a successor. That is the sum total of our knowledge about successor. However, using that, we come up with entities (which we call numbers) which just happen to have the exact same properties as our natural numbers!
Note that - The Peano axioms define things that just happen to act the way that natural numbers do. That's why we use it. We didn't create natural numbers using these axioms, they came along later and duplicate the properties that we had already assigned.
Once again, Xanthir beats me to the answer :-).
He's absolutely right. What the peano axioms do is define a sequence of "objects", each of which has exactly one "successor", etc. If you look at, for example, the definition of addition, it never says "add one" to anything; it's defined in terms of *successor*. Peano arithmetic can be used not just for the natural numbers, but for *any* fully ordered countable set with an initial value - that is, for any set that meets the Peano axioms.
So you *can* use the Peano axioms to talk about the numbers 0, 0.5, 1, 1.5, etc. - they're a set of values that satisfy the Peano axioms. They work find. You can also use the peano axioms to talk about various kinds of character strings, or set constructions, or lambda calculus church numerals, or...
You described rule 4 as "(Each number has a unique successor.)", but that is reversed. It actually means "Each successor is the output from only one number", the classic mono condition. It's the rule that guarantees we don't end up in a cycle where, for example, s(s(s(s(0)))) = s(s(0)). Rule 2 requires the successor relation to be a function, that guarantees every number has a unique successor.
Just now catching this, but shouldn't axiom 2 read:
2. â a â N â a'=s(a), a' â N
2. â a â N â a'=s(n), a' â N
I.e., where'd that lower case 'n' come from?
Axiom 5 states:
(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.)
Shouldn't "it's true for b" be "it's true for s(a)"?
One thing I absolutely love about the Internet is that I can throw out a random comment and, occasionally, provoke an informative reply from someone much more knowledgeable than I am. Case in point: the connection between surreal numbers and Cartesian closed categories.