nLab natural numbers type

Idea

In type theory: the the natural numbers type is the type of natural numbers.

Definition

Definition

The type of natural numbers $\mathbb{N}$ is the inductive type defined by the following inference rules.

1. type formation rule:

   $$\frac{}{ \mathclap{\phantom{\vert^{\vert}}} \mathbb{N} \,\colon\, Type }$$

2. term introduction rules:

   $$\frac{}{ \mathclap{\phantom{\vert^{\vert}}} 0 \,\colon\, \mathbb{N} } \;\;\;\;\;\;\;\; \frac{ n \,\colon\, \mathbb{N} \mathclap{\phantom{\vert_{\vert}}} }{ \mathclap{\phantom{\vert^{\vert}}} succ(n) \,\colon\, \mathbb{N} }$$

3. term elimination rule:

   $$\frac{ n \,\colon\, \mathbb{N} \;\vdash\; P(n) \,\colon\, Type \;; \;\;\;\; \vdash\; 0_P \,\colon\, P(0) \;; \;\;\;\; n \,\colon\, \mathbb{N} \,, \; p \,\colon\, P(x) \;\vdash\; succ_P(n,\,p) \,\colon\, P\big(succ(n)\big) \mathclap{\phantom{\vert_{\vert}}} }{ \mathclap{\phantom{\vert^{\vert}}} n \,\colon\, \mathbb{N} \;\vdash\; ind_{(P, 0_P, succ_P)}(n) \,\colon\, P(n) }$$

4. computation rules:

   $$\frac{ n \,\colon\, \mathbb{N} \;\vdash\; P(n) \,\colon\, Type \;; \;\;\;\; \vdash\; 0_P \,\colon\, P(0) \;; \;\;\;\; n \,\colon\, \mathbb{N} \,, \; p \,\colon\, P(x) \;\vdash\; succ_P(n,p) \,\colon\, P\big(succ(n)\big) \mathclap{\phantom{\vert_{\vert}}} }{ \mathclap{\phantom{\vert^{\vert}}} ind_{(P, 0_P, succ_P)}(0) \,=\, 0_P }$$

   and

   $$\frac{ n \,\colon\, \mathbb{N} \;\vdash\; P(x) \,\colon\, Type \;; \;\;\;\; \vdash\; 0_P \,\colon\, P(0) \;; \;\;\;\; n \,\colon\, \mathbb{N} \,, \; p \,\colon\, P(x) \;\vdash\; succ_P(x,p) \,\colon\, P(s x) \;; \;\;\;\; \vdash\; n \,\colon\, \mathbb{N} \mathclap{\phantom{\vert_{\vert}}} }{ \mathclap{\phantom{\vert^{\vert}}} ind_{(P, 0_P, succ_P)}\big(succ(n)\big) \,=\, succ_P\big(n,\, ind_{(P, 0_P, succ_P)}(n) \big) }$$

(In the last line, “$=$” denotes judgemental equality.)

That this is the right definition (and a special case of the general principle of inductive types) was clearly understood around Martin-Löf (1984), pp. 38; Coquand & Paulin (1990, p. 52-53); Paulin-Mohring (1993, §1.3); Dybjer (1994, §3). For review see also, e.g., Pfenning (2009, §2); UFP (2013, §1.9); Söhnen (2018, §2.4.5).

In Coq-syntax the natural numbers are the inductive type defined [cf. Paulin-Mohring (2014, p. 6)] by:

Inductive nat : Type :=
 | zero : nat
 | succ : nat -> nat.

In the categorical semantics (via the categorical model of dependent types, see below) this is interpreted as the initial algebra for the endofunctor $F$ that sends an object to its coproduct with the terminal object

(1)$$F(X) \;\coloneqq\; * \sqcup X \,,$$

or in different equivalent notation, which is very suggestive here:

$$F(X) \;=\; 1 + X \,.$$

That initial algebra is (as also explained there) precisely a natural number object $\mathbb{N}$. The two components of the morphism $F(\mathbb{N}) \to \mathbb{N}$ that defines the algebra structure are the 0-element $0 \,\colon\, * \to \mathbb{N}$ and the successor endomorphism $succ \colon \mathbb{N} \to \mathbb{N}$

$$(0 ,\, succ) \;\colon\; * \sqcup \mathbb{N} \longrightarrow \mathbb{N} \,.$$

With typal computation and uniqueness rules

Assuming that identification types, function types and dependent sequence types exist in the type theory, the natural numbers type is the inductive type generated by an element and a function:

Formation rules for the natural numbers type:

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{N} \; \mathrm{type}}$$

Introduction rules for the natural numbers type:

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 0:\mathbb{N}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash s:\mathbb{N} \to \mathbb{N}}$$

Elimination rules for the natural numbers type:

$$\frac{\Gamma, x:\mathbb{N} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_s:\prod_{x:\mathbb{N}} C(x) \to C(s(x)) \quad \Gamma \vdash n:\mathbb{N}}{\Gamma \vdash \mathrm{ind}_\mathbb{N}^C(c_0, c_s, n):C(n)}$$

Computation rules for the natural numbers type:

$$\frac{\Gamma, x:\mathbb{N} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_s:\prod_{x:\mathbb{N}} C(x) \to C(s(x))}{\Gamma \vdash \beta_\mathbb{N}^0(c_0, c_s):\mathrm{Id}_{C(0)}\mathrm{ind}_\mathbb{N}^C(c_0, c_s, 0), c_0)}$$

$$\frac{\Gamma, x:\mathbb{N} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_s:\prod_{x:\mathbb{N}} C(x) \to C(s(x)) \quad \Gamma \vdash n:\mathbb{N}}{\Gamma \vdash \beta_\mathbb{N}^s(c_0, c_s, n):\mathrm{Id}_{C(s(n))}(\mathrm{ind}_\mathbb{N}^C(c_0, c_s, s(n)), c_s(n)(\mathrm{ind}_\mathbb{N}^C(c_0, c_s, n)))}$$

Uniqueness rules for the natural numbers type:

$$\frac{\Gamma, x:\mathbb{N} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c:\prod_{x:\mathbb{N}} C(x) \quad \Gamma \vdash n:\mathbb{N}}{\Gamma \vdash \eta_\mathbb{N}(c, n):\mathrm{Id}_{C(n)}(\mathrm{ind}_\mathbb{N}^C(c(0), \lambda x:\mathbb{N}.c(s(x)), n), c(n))}$$

The elimination, computation, and uniqueness rules for the natural numbers type state that the natural numbers type satisfy the dependent universal property of the natural numbers. If the dependent type theory also has dependent sum types and product types, allowing one to define the uniqueness quantifier, the dependent universal property of the natural numbers could be simplified to the following rule:

$$\frac{\Gamma, x:\mathbb{N} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_s:\prod_{x:\mathbb{N}} C(x) \to C(s(x))}{\Gamma \vdash \mathrm{up}_\mathbb{N}^C(c_0, c_s):\exists!c:\prod_{x:\mathbb{N}} C(x).\mathrm{Id}_{C(0)}(c(0), c_0) \times \prod_{x:\mathbb{N}} \mathrm{Id}_{C(s(x))}(c(s(x)), c_s(c(x)))}$$

Properties

General

Example

(natural numbers type as a $\mathcal{W}$-type)
The natural numbers type $(\mathbb{N},\, 0,\, succ)$ (Def. ) is equivalently the $\mathcal{W}$-type $\underset{c \colon C}{\mathcal{W}} A(c)$ with:

• $C \,\coloneqq\, \{0, succ\} \,\simeq\, \ast \sqcup \ast$;

• $A_0 \,\coloneqq\, \varnothing$ (empty type);

  $A_{succ} \,\coloneqq\, \ast$ (unit type)

[Martin-Löf (1984), pp. 45, Dybjer (1997, p. 330, 333)]

Categorical semantics

We spell out how under the canonical categorical model of dependent types, the categorical semantics of the natural numbers types yields a natural numbers object together with its expected recursion and induction principle.

Throughout, we consider an ambient category $\mathcal{C}$ (e.g. $\mathcal{C} =$ Set) and write

(2)$$F Alg(\mathcal{C}) \xrightarrow{underlying} \mathcal{C}$$

for the category of algebras over the endofunctor $F$ (1).

Recursion

We spell out how the fact that $\mathbb{N}$ satisfies Def. is the classical recursion principle.

We begin with a simple special case of recursion (cf. Rem. ), where not only the underlying type but also its successor-map is independent of $\mathbb{N}$ (we come to the general form of recursion further below).

So consider any $F$-algebra $\big(D, (0_D, succ_D)\big) \,\in\, F Alg(\mathcal{C})$ (2), hence an object $D \in \mathcal{C}$ equipped with a morphism

$$0_D \colon * \to D$$

and a morphism

$$succ_D \colon D \to D \,.$$

By initiality of the $F$-algebra $\mathbb{N}$, there is then a (unique) morphism

$$rec \,\colon\, \mathbb{N} \to D$$

such that the following diagram commutes:

$$\array{ * &\stackrel{0}{\longrightarrow}& \mathbb{N} &\stackrel{succ}{\longrightarrow}& \mathbb{N} \\ \big\downarrow && \big\downarrow\mathrlap{^\mathrlap{rec}} && \big\downarrow\mathrlap{^\mathrlap{rec}} \\ * &\underset{0_D}{\longrightarrow}& D &\underset{succ_D}{\longrightarrow}& D }$$

This means precisely that $rec$ is the function defined recursively by

$$rec(0) \;=\; 0_D$$

and

(3)$$rec\big(succ(n)\big) \;=\; succ_D\big(rec(n)\big) \,.$$

More generally, consider an $F$-algebra in the slice over $\big(\mathbb{N}, (0,succ)\big)$, but with the underlying slice object assumed (dropping also this assumption leads to the fully general notion of induction further below) to be independent of $\mathbb{N}$, hence of the form

(4)$$\left[ \array{ \mathbb{N} \times D \\ \big\downarrow\mathrlap{^{pr_{\mathbb{N}}}} \\ \mathbb{N} } \;\;\; \right] \;\in\; \mathcal{C}_{/\mathbb{N}} \,,$$

while the $F$-algebra structure may now depend on $\mathbb{N}$:

in that

$$succ_D \;\colon\; \mathbb{N} \times D \to D$$

may depend on $\mathbb{N}$.

Now, since with $\big(\mathbb{N},(0,\mathrm{succ})\big)$ being the initial object in $F Alg(\mathcal{C})$, the identity morphism on $\big(\mathbb{N},(0,\mathrm{succ})\big)$ is the initial object in the slice category $F Alg(\mathcal{C})_{/\big(\mathbb{N}, (0,succ)\big)}$ (cf. there), it follows that from such data is induced a unique morphism $f$ in the following commuting diagram:

Here the commutativity of the top square means equivalently that

$$\mathrm{rec}(0) \,=\, 0_D$$

and

(5)$$\mathrm{rec}\big( \mathrm{succ}(n) \big) \;=\; \mathrm{succ}_D\big(n,\, \mathrm{rec}(n)\big) \,.$$

Remark

(the need for dependent recursion [cf. Paulin-Mohring (1993, p. 330)])
The appearance of the argument “$n$” on the right of (5) – in contrast to formula (3) for non-dependent recursion – means (in view of the argument “$succ(n)$” on the left) that the recursor $succ_D$ has access to the predecessor partial function $pred \,\colon\,succ(n) \,\mapsto\, n$. This is necessary in order to express all computable functions on the natural numbers inductively and hence explains the need for the dependently typed recursion principle (4)

Induction

Dropping the above constraint (4) on the dependent $F$-algebra, we spell out in detail how the fact that $\mathbb{N}$ satisfied Def. is the classical induction principle.

That principle says informally that if a proposition $P$ depending on the natural numbers is true at $n = 0$ and such that if it is true for some $n$ then it is true for $n+1$, then it is true for all natural numbers.

Here is how this is formalized in type theory and then interpreted in some suitable ambient category $\mathcal{C}$.

First of all, that $P$ is a proposition depending on the natural numbers means that it is a dependent type

$$n \,\colon\, \mathbb{N} \;\;\vdash\;\; P(n) \,\colon\, Type \,.$$

The categorical interpretation of this is by a display map

(6)$$\array{ P \\ \big\downarrow\mathrlap{^{\pi_P}} \\ \mathbb{N} }$$

in the given category $\mathcal{C}$.

With this, the commuting diagram which interprets the induction principle is the following:

We now unwind again how this comes about and what it all means:

First, the fact that $P$ holds at 0 means that there is a (proof-)term

$$\vdash \;\; 0_P \,\colon\, P(0) \,.$$

In the categorical semantics the substitution of $n$ for 0 that gives $P(0)$ is given by the pullback of the given display map (6):

$$\array{ 0^* P &\longrightarrow& P \\ \big\downarrow && \big\downarrow \\ * &\underset{0}{\longrightarrow}& \mathbb{N} }$$

and the term $0_P$ is interpreted as a section of the resulting fibration over the terminal object

$$\array{ * &\overset{p_0}{\longrightarrow}& 0^* P & \longrightarrow & P \\ &\searrow& \big\downarrow && \big\downarrow \\ && * &\underset{0}{\longrightarrow}& \mathbb{N} } \,.$$

But by the defining universal property of the pullback, this is equivalently just a commuting diagram

$$\array{ * &\stackrel{p_0}{\longrightarrow}& P \\ \big\downarrow && \big\downarrow \\ * &\underset{0}{\longrightarrow}& \mathbb{N} } \,.$$

Next the induction step. Formally it says that for all $n \in \mathbb{N}$ there is an implication $succ_P(n) \,\colon\, P(n) \to P(n+1)$

$$n \in \mathbb{N} \;\;\;\vdash\;\;\; succ_P(n) \,\colon\, P(n) \to P(n+1) \,.$$

The categorical semantics of the substitution of $n+1$ for $n$ is given by the pullback

$$\array{ P\big(\ast \sqcup (-)\big) \coloneqq & s^*P &\longrightarrow& P \\ & \big\downarrow && \big\downarrow \\ & \mathbb{N} &\underset{s}{\longrightarrow}& \mathbb{N} }$$

and the interpretation of the implication term $succ_P(n)$ is as a morphism $P \to s^* P$ in $\mathcal{C}_{/\mathbb{N}}$

$$\array{ P & \overset{p_s}{\longrightarrow} & s^*P &\longrightarrow& P \\ &\searrow & \big\downarrow && \big\downarrow \\ && \mathbb{N} &\overset{s}{\longrightarrow}& \mathbb{N} } \,.$$

Again by the universal property of the pullback this is equivalently a commuting diagram

$$\array{ P &\overset{succ_P}{\longrightarrow}& P \\ \big\downarrow && \big\downarrow \\ \mathbb{N} &\underset{s}{\longrightarrow}& \mathbb{N} } \,.$$

In summary this shows that

• $P$ being a proposition depending on natural numbers which holds at 0 and which holds at $n+1$ if it holds at $n$

is interpreted precisely as an endofunctor-algebra homomorphism

$$\array{ P \\ \downarrow \\ \mathbb{N} } \,.$$

for the endofunctor $F$ (1).

The induction principle is supposed to deduce from this that $P$ holds for every $n$, hence that there is a proof $ind(n) \colon P(n)$ for all $n$:

$$n \,\colon\, \mathbb{N} \;\;\;\vdash\;\;\; ind(n) \,\colon\, P(n) \,.$$

The categorical interpretation of this is as a morphism $p \,\colon\, \mathbb{N} \to P$ in $\mathcal{C}_{/\mathbb{N}}$. The existence of this is indeed exactly what the interpretation of the elimination rule (Def. ) gives exactly what the initiality of the $F$-algebra $\mathbb{N}$ gives.

Related concepts

• natural numbers, natural numbers object

• decimal numeral representation of the natural numbers

• dependent sequence type

References

Original articles with emphasis on the nature of $\mathbb{N}$ as an inductive type:

• Per Martin-Löf (notes by Giovanni Sambin), pp. 38 of: Intuitionistic type theory, Lecture notes Padua 1984, Bibliopolis, Napoli (1984) [pdf, pdf]

• Thierry Coquand, Christine Paulin, p. 52-53 in: Inductively defined types, COLOG-88 Lecture Notes in Computer Science 417, Springer (1990) 50-66 [doi:10.1007/3-540-52335-9_47]

• Christine Paulin-Mohring, §1.3 in: Inductive definitions in the system Coq – Rules and Properties, in: Typed Lambda Calculi and Applications TLCA 1993, Lecture Notes in Computer Science 664 Springer (1993) [doi:10.1007/BFb0037116]

• Peter Dybjer, §3 in: Inductive families, Formal Aspects of Computing 6 (1994) 440–465 $[$doi:10.1007/BF01211308, doi:10.1007/BF01211308, pdf$]$

The syntax in Coq:

• Christine Paulin-Mohring, p. 6 in: Introduction to the Calculus of Inductive Constructions, contribution to: Vienna Summer of Logic (2014) [hal:01094195, pdf, pdf slides]

See also:

• Frank Pfenning, Lecture notes on natural numbers (2009) [pdf, pdf]

Discussion in a context of homotopy type theory and in view of higher inductive types:

• Univalent Foundations Project, §1.9 in: Homotopy Type Theory – Univalent Foundations of Mathematics (2013) [web, pdf]

• Kajetan Söhnen, §2.4.5 in: Higher Inductive Types in Homotopy Type Theory, Munich (2018) [pdf, pdf]

Equivalence to binary presentations:

• Nicolas Magaud?, Yves Bertot?, Changing Data Structures in Type Theory: A Study of Natural Numbers, in Types for Proofs and Programs. TYPES 2000, Lecture Notes in Computer Science 2277 [doi:10.1007/3-540-45842-5_12, pdf]

• Nicolas Magaud?, Changing Data Representation within the Coq, in Theorem Proving in Higher Order Logics. TPHOLs 2003, Lecture Notes in Computer Science 2758 [doi:10.1007/10930755_6]