Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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.

share|cite|improve this question
up vote 1 down vote accepted

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 ;-)

share|cite|improve this answer
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".

share|cite|improve this answer

I just want to add

is a good resource that has a lot of Peano Arithmatic problems.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.