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

inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat

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

zero, succ zero, succ (succ zero), succ (succ (succ zero)),...

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.)