# Peano axioms expressed in type theory

I have a very strong understanding of 1st order logic and am trying to lean type theory as an alternative. Could someone express the Peano axioms with type-theory? I am especially interested to see how induction is represented.

-

Let $\bot$ be the uninhabited type of kind $*$, and let the types

• $\mathtt{Zero}$ be of kind $*$,
• $\mathtt{Nat}$ and $\mathtt{S}$ be of kind $* \to *$,
• $\mathtt{Eq}$ be of kind $* \to * \to *$.

Then the Peano axioms can be formalized in type theory by saying that the following types are inhabited (in the format $\mathtt{inhabitant} : \mathtt{type}$, any free variables are quantified universally):

\begin{align} \newcommand{\Zero}{\mathtt{Zero}} \newcommand{\zero}{\mathtt{zero}} \newcommand{\pa}[1]{\mathtt{pa}_{\mathrm{#1}}} \newcommand{\Nat}[1]{(\mathtt{Nat}\ #1)} \newcommand{\Eq}[2]{(\mathtt{Eq}\ #1\ #2)} \newcommand{\S}[1]{(\mathtt{S}\ #1)} \newcommand{\T}[1]{(\mathtt{T}\ #1)} \newcommand{\Plus}[2]{(\mathtt{Plus}\ #1\ #2)} \newcommand{\plus}[1]{\mathtt{plus}_{\mathrm{#1}}} \newcommand{\Comm}[1]{(\mathtt{Comm}\ #1)} \zero &: \Zero \\ \pa1 &: \Nat{\Zero} \\ \pa2 &:\Nat{x} \to \Eq{x}{x} \\ \pa3 &: \Nat{x} \to \Nat{y} \to \Eq{x}{y} \to \Eq{y}{x} \\ \pa4 &: \Nat{x} \to \Nat{y} \to \Nat{z} \to \Eq{x}{y} \to \Eq{y}{z} \to \Eq{x}{z} \\ \pa5 &: \Nat{x} \to \Eq{x}{y} \to \Nat{y} \\ \pa6 &: \Nat{x} \to \Nat{\S{x}} \\ \pa7 &: \Nat{x} \to \Eq{\S{x}}{\Zero} \to \bot \\ \pa8 &: \Nat{x} \to \Nat{y} \to \Eq{\S{x}}{\S{y}} \to \Eq{x}{y} \\ \end{align}

and also, for any type $\mathtt{T}$ of kind $\mathtt{T} : * \to *$ the following type is also inhabited: $$\pa{T} : \T{\Zero} \to (\Nat{x} \to \T{x} \to \T{\S{x}}) \to \Nat{y} \to \T{y}.$$

Those are Peano axioms as in Wikipedia, but I think there also should be something implying that $\mathtt{S}$ is a function (with respect to $\mathtt{Eq}$) instead of any relation, that is:

$$f : \Nat{x} \to \Nat{y} \to \Eq{x}{y} \to \Eq{\S{x}}{\S{y}}.$$

I hope this helps ;-)

-
does this mean "4" has type "$* \to * \to * \to * \to *$" ? – user833970 Mar 26 '13 at 21:44
What do you mean by "4"? – dtldarek Mar 26 '13 at 22:24
the natural number 4 as described by this formulation, s(s(s(s(0)))) – user833970 Mar 27 '13 at 0:01
0 is of kind $*$ and $s$ is of kind $* \to *$ so $s(0)$ is of kind $*$ and so $s(s(0))$ is of kind $*$ etc. – dtldarek Mar 27 '13 at 0:13
Here, $x$ is a natural number iff $Nat\ x$ is inhabited. To prove that 4 is a natural number you would like to prove that $Nat\ (S\ (S\ (S\ (S\ Zero))))$ is inhabited. However, $(pa_5\ (pa_5\ (pa_5\ (pa_5\ pa_1))))$ is exactly of the type you need, i.e. the inhabitant you are looking for. – dtldarek Apr 2 '13 at 19:05

Professor Peter B. Andrews book "An Introduction to Mathematical Logic and Type Theory" (2002) covers exactly this subject. He expresses the postulates like this. (I omit type symbols from variables and constants.)

$1.\ N\ 0$

$2.\ \forall x(N\ x\implies N\ (S \ x))$

$3.\ \forall p(p\ 0\ \land \forall x(N\ x\land p\ x\implies p\ (S\ x))$

$4.\ \forall x(N\ x\implies S\ x \neq 0)$

$5.\ \forall x \forall y(N\ x\ \land\ N\ y\ \land\ S\ x = S\ y \implies x = y)$

Type theory is higher-order logic, and induction quantifies over predicates "p".

-