ペアノの公理

デーデキント＝ペアノの公理系

0 ∈ N

任意の n ∈ N について S(n) ∈ N

任意の n ∈ N について S(n) ≠ 0

任意の n, m ∈ N について n ≠ m ならば S(n) ≠ S(m)

任意の E ⊆ N について ( 0 ∈ E かつ任意の n ∈ N について n ∈ E → S(n) ∈ E ) ならば E = N

この公理系を満たす構造Nは（同型を除いて）一通りとなり自然数の特徴づけとなっている

したがってこれを ℕ で表すことが出来る．

S(n) を n の後者（英: successor）

Sをsuccessor functionと云う。

ペアノ算術

「任意のE ⊆ N」のところで、自然数のすべての部分集合に対して帰納法が適用できる

https://www.youtube.com/watch?v=iQdirsBNYFc

ペアノの公理は自然数を作っていない

ペアノの公理は「自然数がこんな風になってたらいいなー」ということが書いてますが、具体的に自然数を構成していません。

つまりペアノシステムが存在するかはペアノの公理を定義しただけではわかりません。

またペアノシステムの例はたくさん作れます。