natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory
basic constructions:
:
:
:
strong axioms
further
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.
and
and
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 $F$ that sends an object to its coproduct with the terminal object
or in different equivalent notation, which is very suggestive here:
That initial algebra is (as 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 $zero : * \to \mathbb{N}$ and the successor endomorphism $successor : \mathbb{N} \to \mathbb{N}$
In the following we write of course for short $0 : * \to \mathbb{N}$ and $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 $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
The categorical interpretation of this is by a display map
in the given category $\mathcal{C}$.
Next, the fact that $P$ holds at 0 means that there is a (proof-)term
In the categorical semantics the substitution of $n$ for 0 that gives $P(0)$ is given by the pullback of the above fibration
and the term $p_0$ is interpreted as a section of the resultig fibration over the terminal object
But by the defining universal property of the pullback, this is equivalently just a commuting diagram
Next the induction step. Formally it says that for all $n \in \mathbb{N}$ there is an implication $p_s(n) : P(n) \to P(n+1)$
The categorical semantics of the substitution of $n+1$ for $n$ is now given by the pullback
and the interpretation of the implication term $p_s(n)$ is as a morphism $P \to s^* P$ in $\mathcal{C}_{/\mathbb{N}}$
Again by the universal property of the pullback this is the same as a commuting diagram
In summary this shows that the fact that $P$ is 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 $F$-algebra homomorphism
The induction principle is supposed to deduce from this that $P$ holds for every $n$, hence that there is a proof $p_n : P(n)$ for all $n$:
The categorical interpretation of this is as a morphism $p : \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 $F$-algebra $\mathbb{N}$ gives.
We spell out how the fact that $\mathbb{N}$ satisfies def. is the classical recursion principle.
So let $A$ be an $F$-algebra object, hence equipped with a morphism
and a morphism
By initiality of the $F$-algebra $\mathbb{N}$, there is then a (unique) morphism
such that the diagram
commutes. This means precisely that $f$ is the function defined recursively by
$f(0) = a_0$;
$f(n+1) = h(f(n))$.
Last revised on January 22, 2017 at 03:11:11. See the history of this page for a list of all contributions to it.