natural numbers type



Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
logical conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type/path type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels


Deduction and Induction




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



The type of natural numbers \mathbb{N} is the inductive type defined as follows.

  1. type formation rule

    :Type \frac{}{\mathbb{N} : Type}
  2. term introduction rules

    0: \frac{}{0 : \mathbb{N}}


    n:sn: \frac{n : \mathbb{N}}{s n : \mathbb{N}}
  3. term elimination rule

    x:P(x):Type;p 0:P(0);x:,p:P(x)p s(x,p):P(sx);n:rec P n(p 0,p s):P(n) \frac{ x : \mathbb{N} \vdash P(x) : Type; \;\; \vdash p_0 : P(0); \;\; x : \mathbb{N}, p : P(x) \vdash p_s(x,p) : P(s x); \;\; \vdash n : \mathbb{N} }{ rec^n_P(p_0,p_s) : P(n) }
  4. computation rules

    x:P(x):Type;p 0:P(0);x:,p:P(x)p s(x,p):P(sx)rec P 0(p 0,p s)=p 0:P(0) \frac{ x : \mathbb{N} \vdash P(x) : Type; \;\; \vdash p_0 : P(0); \;\; x : \mathbb{N}, p : P(x) \vdash p_s(x,p) : P(s x) }{ rec^0_P(p_0,p_s) = p_0 : P(0) }


    x:P(x):Type;p 0:P(0);x:,p:P(x)p s(x,p):P(sx);n:rec P sn(p 0,p s)=p s(n,rec P n(p 0,p s)):P(sn) \frac{ x : \mathbb{N} \vdash P(x) : Type; \;\; \vdash p_0 : P(0); \;\; x : \mathbb{N}, p : P(x) \vdash p_s(x,p) : P(s x); \;\; \vdash n : \mathbb{N} }{ rec^{s n}_P(p_0,p_s) = p_s(n,rec^n_P(p_0,p_s)) : P(s n) }

See for instance (Pfenning, section 2).

In Coq-syntax the natural numbers are the inductive type defined by

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

In the categorical semantics this is interpreted as the initial algebra for the endofunctor FF that sends an object to its coproduct with the terminal object

F(X)=*X, F(X) = * \coprod X \,,

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

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

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

(zero,successor):*. (zero,successor) : * \coprod \mathbb{N} \to \mathbb{N} \,.

In the following we write of course for short 0:*0 : * \to \mathbb{N} and s:s : \mathbb{N} \to \mathbb{N}.




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 PP depending on the natural numbers is true at n=0n = 0 and such that if it is true for some nn then it is true for n+1n+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 PP is a proposition depending on the natural numbers means that it is a dependent type

nP(n):Type. n \in \mathbb{N} \vdash P(n) : Type \,.

The categorical interpretation of this is by a display map

P \array{ P \\ \downarrow \\ \mathbb{N} }

in the given category 𝒞\mathcal{C}.

Next, the fact that PP holds at 0 means that there is a (proof-)term

p 0P(0). \vdash p_0 \in P(0) \,.

In the categorical semantics the substitution of nn for 0 that gives P(0)P(0) is given by the pullback of the above fibration

0 *P P * 0 \array{ 0^* P &\to& P \\ \downarrow && \downarrow \\ * &\stackrel{0}{\to}& \mathbb{N} }

and the term p 0p_0 is interpreted as a section of the resulting fibration over the terminal object

* p 0 0 *P P * 0 . \array{ * &\stackrel{p_0}{\to}& 0^* P &\to& P \\ &\searrow& \downarrow && \downarrow \\ && * &\stackrel{0}{\to}& \mathbb{N} } \,.

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

* p 0 P * 0 . \array{ * &\stackrel{p_0}{\to}& P \\ \downarrow && \downarrow \\ * &\stackrel{0}{\to}& \mathbb{N} } \,.

Next the induction step. Formally it says that for all nn \in \mathbb{N} there is an implication p s(n):P(n)P(n+1)p_s(n) : P(n) \to P(n+1)

np s(n):P(n)P(n+1) n \in \mathbb{N} \vdash p_s(n) : P(n) \to P(n+1)

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

P(()+1) s *P P s \array{ P((-)+1) \coloneqq & s^*P &\to& P \\ & \downarrow && \downarrow \\ & \mathbb{N} &\stackrel{s}{\to}& \mathbb{N} }

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

P p s s *P P s . \array{ P & \stackrel{p_s}{\to} & s^*P &\to& P \\ &\searrow & \downarrow && \downarrow \\ && \mathbb{N} &\stackrel{s}{\to}& \mathbb{N} } \,.

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

P p s P s . \array{ P &\stackrel{p_s}{\to}& P \\ \downarrow && \downarrow \\ \mathbb{N} &\stackrel{s}{\to}& \mathbb{N} } \,.

In summary this shows that the fact that PP is a proposition depending on natural numbers which holds at 0 and which holds at n+1n+1 if it holds at nn is interpreted precisely as an FF-algebra homomorphism

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

The induction principle is supposed to deduce from this that PP holds for every nn, hence that there is a proof p n:P(n)p_n : P(n) for all nn:

np(n):P(n). n \in \mathbb{N} \vdash p(n) : P(n) \,.

The categorical interpretation of this is as a morphism p:Pp : \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, or (equivalently by prop. ) exactly what the initiality of the FF-algebra \mathbb{N} gives.



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

So let AA be an FF-algebra object, hence equipped with a morphism

a 0:*A a_0 : * \to A

and a morphism

h:AA. h : A \to A \,.

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

f:A f : \mathbb{N} \to A

such that the diagram

* 0 ()+1 f f * a 0 A h A \array{ * &\stackrel{0}{\to}& \mathbb{N} &\stackrel{(-)+1}{\to}& \mathbb{N} \\ \downarrow && \downarrow^{\mathrlap{f}} && \downarrow^{\mathrlap{f}} \\ * &\stackrel{a_0}{\to}& A &\stackrel{h}{\to}& A }

commutes. This means precisely that ff is the function defined recursively by

  1. f(0)=a 0f(0) = a_0;

  2. f(n+1)=h(f(n))f(n+1) = h(f(n)).


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

Last revised on August 31, 2019 at 06:41:45. See the history of this page for a list of all contributions to it.