*Peano's axioms*
(or *postulates*) are five rules, defined in set-theoretical terms, for the construction of natural
numbers. The axioms are named after the Italian mathematician, Peano, who published them in 1889, although he
himself attributed them to the German mathematician Dedekind. Given the set of
natural numbers, `Nat`, whose
initial elements are `0,1,2,3,4, ...`,
the axioms are defined as follows:

- There is a constant
`0:Nat`. (This is also regarded as a*nullary*function to`Nat`). - There exists a
*total*,*unary*function`s`,`s:Nat->Nat`, referred to as the*successor function*, i.e. for each element`x`in`Nat`, there is one and only one element`y`in`Nat`such that`y = s(x)`. - There is one and only one element in Nat, the constant
`0`, which is not the successor of an element in`Nat`. Thus for all`x`in`Nat`,`s(x) =|= 0`, i.e.`0`is not a member of`Ran(s)`. - For all
`x`and`y`in`Nat`,`s(x) = s(y) -> x = y`. In other words for all`x`and`y`in`Nat`,`x =|= y -> s(x) =|= s(y)`(i.e. the successor function is an*injection*). -
For all subsets
`A`of`Nat`, if either`0`is a member of`A`or for all`x`belonging to`A`,`s(x)`is a member of`A`this then implies`A = Nat`. In other words given a collection`A`of elements in`Nat`such that`0`is in`A`and for each`x`in`A``s(x)`is also in`A`, then`A = Nat`. This is referred to as the*induction principle*or the*principle of mathematical induction*. Consequently we can define addition of natural numbers in such a manner that`s(x) = x+1`, for all`x`in`Nat`.

The set `Nat` together with the constant `0:Nat` and the function `s:Nat->Nat` are referred
to as the *Peano system* `(Nat,0,S)`.

The axioms (slightly refined) can also be applied to the set of positive numbers, `Pos`, whose
initial elements are `1,2,3,4,5, ...`.

Created and maintained by Frans Coenen. Last updated 16 September 2000