Natural numbers

natural numbers

One of the most basic mathematical types is ${{\mathbb{N} }}$, the natural numbers. This type is formed by the rule $H \vdash {{\mathbb{N} }} \in$ Type. The type is inductively defined by the rules which say that $0 \in {{\mathbb{N} }}$, and if $n \in {{\mathbb{N} }}$ then $suc(n) \in {{\mathbb{N} }}$. The typing judgments we need are

$H \vdash 0 \in {{\mathbb{N} }}$	type_of_zero
$H \vdash suc(n) \in {{\mathbb{N} }}$	type_of_successor
$H \vdash n \in {{\mathbb{N} }}$

To express the fact that ${{\mathbb{N} }}$ is inductively defined we use the rule of mathematical induction. In its unrestricted form, this essentially says that nothing else is a member of ${{\mathbb{N} }}$ except what can be generated from 0 using suc. But the form of the rule given here does not quantify over all propositional functions on ${{\mathbb{N} }}$, so it is not a full statement of the principle.

Suppose $P\!:\!({{\mathbb{N} }} \times A) \rightarrow\ Prop$, then

$\bar{x}\!:\!\bar{H},\ n\!:\!{{\mathbb{N} }} \vdash P(n, \bar{x})\ \ \mbox{by}\ \ ind(n; p_o; u, i,\: p_s(u, i, \bar{x}))$

$\bar{x}\!:\!\bar{H}, n\!:\!{{\mathbb{N} }} \vdash P(0)\ \mbox{by}\ \ p_o$

$\bar{x}\!:\!\bar{H}, n\!:\!{{\mathbb{N} }}, u\!:\!{{\mathbb{N} }}, i\!:\!P(u, \bar{x}) \vdash P(suc(u), \bar{x})\ \mbox{by}\ \ p_s(u, i, \bar{x})$