Natural Number

Idea

The natural numbers are the collection $\mathbb{N}=\{0,1,2,\dots \}$. They are characterised as the least collection containing a zero element and closed under a successor operation. This minimality principle — that $\mathbb{N}$ contains nothing beyond what is forced by zero and successor — is what gives rise to the induction principle.

In Type Theory

In type theory, $\mathbb{N}$ is sometimes assumed primitive and sometimes constructed from the general notion of an inductive type. The following rules characterise any well-behaved definition of $\mathbb{N}$:

$$\frac{}{\mathbb{N}:\mathcal{U}}\frac{}{\mathrm{zero}:\mathbb{N}}\frac{n:\mathbb{N}}{\mathrm{suc}n:\mathbb{N}}\frac{X:\mathbb{N}\to \mathcal{U}z:X\mathrm{zero}s:(n:\mathbb{N})\to Xn\to X(\mathrm{suc}n)}{\mathrm{eli}{\mathrm{m}}_{\mathbb{N}}Xzs:(n:\mathbb{N})\to Xn}$$ $$\frac{X:\mathbb{N}\to \mathcal{U}z:X\mathrm{zero}s:(n:\mathbb{N})\to Xn\to X(\mathrm{suc}n)}{\mathrm{eli}{\mathrm{m}}_{\mathbb{N}}Xzs\mathrm{zero}\equiv z}$$ $$\frac{X:\mathbb{N}\to \mathcal{U}z:X\mathrm{zero}s:(n:\mathbb{N})\to Xn\to X(\mathrm{suc}n)n:\mathbb{N}}{\mathrm{eli}{\mathrm{m}}_{\mathbb{N}}Xzs(\mathrm{suc}n)\equiv s(\mathrm{suc}n)(\mathrm{eli}{\mathrm{m}}_{\mathbb{N}}Xzsn)}$$

In Agda, $\mathbb{N}$ is defined as an inductive type:

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

In Category Theory

The natural numbers, $\mathbb{N}$ can be defined as an initial algebra of the following endofunctor in Set:

$$\begin{array}{r}{F}_{\mathbb{N}}:\mathrm{Set}\to \mathrm{Set}\\ F_{\mathbb{N}}X=1+X\end{array}$$

In Set Theory

In ZF set theory, the natural numbers are constructed as von Neumann numerals, and their existence as a completed infinite set is guaranteed by the axiom of infinity.

Von Neumann Numerals

Each natural number is identified with the set of all smaller natural numbers: $0:=\varnothing ,s(x):=x\cup \{x\}.$ This gives: $0=\varnothing ,1=\{\varnothing \},2=\{\varnothing ,\{\varnothing \}\},3=\{\varnothing ,\{\varnothing \},\{\varnothing ,\{\varnothing \}\}\},\dots$

Each numeral $n$ is a finite transitive set well-ordered by $\in$, and $n=\{0,1,\dots ,n-1\}$ as a set.

Inductive Sets and the Axiom of Infinity

A set $S$ is called inductive if it contains $0$ and is closed under successor: $I(S)⟺0\in S\wedge \forall x\in S.s(x)\in S.$

The axiom of infinity asserts that at least one inductive set exists: $\exists S.I(S).$

Without this axiom, all sets in ZF could be finite; there would be no guarantee that $\mathbb{N}$ as an infinite set exists.

Definition of $\mathbb{N}$

Given an inductive set $S$, the natural numbers are the intersection of all inductive subsets of $S$: $\mathbb{N}=\bigcap \{T\subseteq S\mid I(T)\}=\{x\in S\mid \forall T\subseteq S.I(T)\to x\in T\}.$

This is well-defined by the axiom of separation applied to $S$, and is independent of the choice of $S$. The result is the smallest inductive set: it contains exactly the von Neumann numerals and nothing else.

Properties in Set Theory

• $\mathbb{N}$ is a transitive set: every element of a natural number is itself a natural number.
• $\mathbb{N}$ is well-ordered by $\in$: for any $m,n\in \mathbb{N}$, exactly one of $m\in n$, $m=n$, $n\in m$ holds, and every non-empty subset of $\mathbb{N}$ has an $\in$-least element.
• $\mathbb{N}$ is the first infinite ordinal, traditionally written $\omega$.
• Mathematical induction on $\mathbb{N}$ corresponds to $\in$-induction on $\omega$: to prove $P(n)$ for all $n\in \omega$, show $P(\varnothing )$ and that $P(n)\to P(n\cup \{n\})$.
• The axiom of foundation ensures $n\notin n$ for all $n$, so the $\in$-ordering is strict and well-behaved.