Peano axioms expressed in type theory

Question

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.

Answer 1

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

Answer 2

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)))\implies \forall x (N\ x \implies p\ 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".