Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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|improve this question
add comment

3 Answers

up vote 1 down vote accepted
+50

Let $\bot$ be the uninhabited type of kind $*$, and let 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 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|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
1  
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
show 10 more comments

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|improve this answer
add comment

I just want to add

http://people.inf.elte.hu/divip/AgdaTutorial/Index.html

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

share|improve this answer
add comment

Your Answer

 
discard

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.