## Axiomatic $~\mathbb{N}$

We all feel pretty comfortable with the natural numbers but how would you explain to a computer? In Lean, `Nat`

is the type of the natural numbers. It looks like

The basic building blocks for `Nat`

are a particular term, `zero`

, and function `succ : Nat → Nat`

.

The keyword `inductive`

tells Lean to make all possible expressions using just these two pieces. How does that work?

Well, to use `succ`

, we need something plug in. We have `zero`

. We can make a new term `succ zero`

. With a new term, we can apply `succ`

again to get `succ (succ zero)`

. Now, we can apply `succ`

again, etc…

Thus, from the two pieces, `zero`

and `succ`

, we get a list of terms

We would usually denote these as \(0, 1, 2, 3,\ldots\) The term `zero`

is of course $0$ and `succ`

is $n \mapsto n+1$ and is short for “successor”. This makes plain the principle of childhood counting that we understand one natural number from all the ones that come before it.

Giuseppe Peano provided an axiomatic characterization of the natural numbers in the last 1800s. It was based on this idea that everything is built from an initial element by applying a successor function.

**Definition**. The *natural numbers* are a set $\mathbb{N}$ possessing a specified elements $0 \in \mathbb{N}$ called *zero* and a function $s : \mathbb{N} \to \mathbb{N}$ called the *successor function* and which satisfy the following conditions

- For any $n \in \mathbb{N}$, $0 \neq s(n)$.
- The successor function is injective: if $s(n) = s(m)$ then $n=m$.
- The set $\mathbb{N}$ is generated by $0$ and $s$: suppose we have a set $X$ which satisfies
- $0 \in X$ and
- For any $n \in \mathbb{N}$, if $n \in X$, then $s(n) \in X$

Then $\mathbb{N} \subseteq X$. In other words, if any set contains $0$ and contains a successor of any natural number it already contains, then it has to have all of $\mathbb{N}$ inside it.

Another way to state the final condition: $\mathbb{N}$ is the smallest set to have $0$ and be closed under application of $s$.

In Lean, the injectivity ($0 \neq s(n)$ and $s(n) = s(m) \to n = m$) is built into the notion of an *inductive type*.

It is important to note that, as defined above, $\mathbb{N}$ are a specification and **not** a construction. Lean’s `Nat`

is a construction that meets this specification. Below is another one.

**Example**. We can build the natural numbers starting from nothing! More precisely, the empty set $\varnothing$. We set $0 := \varnothing$ and $s(X) = X \cup \lbrace X \rbrace$. Then, \(0 = \varnothing \\ s(0) = \lbrace \varnothing \rbrace \\ s(s(0)) = \lbrace \varnothing, \lbrace \varnothing \rbrace \rbrace \\ s(s(s(0))) =\lbrace \varnothing, \lbrace \varnothing, \lbrace \varnothing \rbrace \rbrace \rbrace \\ \vdots\) Then the *Von Neumann naturals* is the set containing all these sets as elements. (The axioms of set theory guarantee such a set.)