ペアノの公理系を採用する公理1自然数0が存在する
公理2任意の自然数aにはその後者suc(a)が存在する
公理3 0はいかなる自然数の後者でもない
公理4異なる自然数は異なる後者を持つ a≠bのときsuc(a)≠suc(b)となる
公理5 0がある性質を満たしaがある性質を満たせばその後者suc(a)もその性質を満たすときすべての自然数はその性質を満たす
(数学的帰納法)


定義suc(0)＝1
suc(1)＝suc(suc(0))＝2などと略記する

定義 f(1)＝suc(a)
f(suc(x))＝suc(f(x))を満たす関数fを定義する
この関数はこれから示すが自然数の和の法則を満たしf(b)はaにbを加えた和a+bをあらわすことがわかるのでf(b)＝a+bと略記できる
みたいなかんじ