ペアノの公理

テンプレート:混同 ペアノの公理（ペアノのこうり、テンプレート:Lang-en-short） とは、自然数の全体を特徴づける公理である。ペアノの公準（テンプレート:Lang-en-short）あるいはデデキント＝ペアノの公理（テンプレート:Lang-en-short）とも呼ばれるテンプレート:Sfn。1891年にイタリアの数学者ジュゼッペ・ペアノにより定式化された。

ペアノの公理を起点にして、初等算術と整数・有理数・実数・複素数の構成などを実際に展開してみせた古典的な書物に、1930年に出版されたランダウによる『解析学の基礎』（テンプレート:Lang）がある。

公理

集合 テンプレート:Math と定数 テンプレート:Math と関数 テンプレート:Mvarと集合テンプレート:Mvarに関する次の公理をペアノの公理というテンプレート:Sfnテンプレート:Efn2。

1. テンプレート:Math
2. 任意の テンプレート:Math について テンプレート:Math
3. 任意の テンプレート:Math について テンプレート:Math
4. 任意の テンプレート:Math について テンプレート:Math ならば テンプレート:Math
5. 任意の テンプレート:Math について テンプレート:Math かつ任意の テンプレート:Math について テンプレート:Math ならば テンプレート:Math

このとき テンプレート:Math の元を自然数といい、自然数 テンプレート:Mvar に対して自然数 テンプレート:Math をその後者 (テンプレート:Lang)テンプレート:Efn2という。

第五公理は、数学的帰納法の原理であるテンプレート:Efn2。

これらの公理は互いに独立であり、いずれも残りから導くことはできないテンプレート:Sfn。

ペアノの公理から テンプレート:Math や テンプレート:Math のような「定理」を証明するには テンプレート:Math などの項を導入したり、加法 テンプレート:Math や乗法 テンプレート:Math の存在や性質を示したりする必要がある。たとえば テンプレート:Harvtxt を見よ。

回帰定理

次の主張を回帰定理（テンプレート:Lang）というテンプレート:Sfn。

集合 テンプレート:Mvar に属する元 テンプレート:Mvar と写像 テンプレート:Math が与えられたとき

$f(0)=x,f\circ S=g\circ f$

を満たす写像

$f:\mathbb{N}\to X$

が一意的に存在する。

たとえば テンプレート:Math のとき写像 テンプレート:Mvar は初項が テンプレート:Mvar の漸化式により定義される数列に他ならない。回帰定理はこのような再帰的に定義される写像の存在と一意性を数学的帰納法の原理により保証する。

範疇性

集合 テンプレート:Math と定数 テンプレート:Math と関数 テンプレート:Math がペアノの公理を満たすとき組 テンプレート:Math をペアノ構造（テンプレート:Lang）という。ペアノ構造は同型を除いてただ一つに定まるテンプレート:Efn2、つまりペアノの公理は範疇的（テンプレート:Lang）であることがわかる。

一方で後述するペアノ算術はレーヴェンハイム＝スコーレムの定理から超準モデルをもつので範疇的ではない。

集合論的な構成

現代数学において標準的な数学の対象はすべて集合として実現されている。集合論における自然数の標準的な構成法としては、

$\mathbb{N}:=\bigcap \{x\subset A\mid \mathrm{\varnothing }\in x\wedge \mathrm{\forall }y[y\in x\to y\cup \{y\}\in x]\}$

$0:=\mathrm{\varnothing }$

$S(x):=x\cup \{x\}$

がある。ただしここでAは無限公理により存在する集合を任意に選んだものである。

これらの集合は存在して、ペアノの公理を満たすことが確かめられる。

このとき具体的な自然数は

• $0=\mathrm{\varnothing }=\{\}$
• $1:=S(0)=\{0\}=\{\{\}\}$
• $2:=S(1)=\{0,1\}=\{\{\},\{\{\}\}\}$
• $3:=S(2)=\{0,1,2\}=\{\{\},\{\{\}\},\{\{\},\{\{\}\}\}\}$

のようになる。この構成法はジョン・フォン・ノイマンによる。

自然数の集合が定義されたとき、その構成と自然数上での帰納法から、自然数上の算術や順序を定めることができる。

加法

自然数の加法は次のように再帰的に定義される。

$n+0=n$

$n+S(m)=S(n+m)$

乗法

自然数の乗法は次のように再帰的に定義される。

$n\cdot 0=0$

$n\cdot S(m)=n\cdot m+n$

順序

自然数の順序は次のように定義される。 ある テンプレート:Mvar について

$n+k=m$

が成り立つとき

$n\le m$

と定義する。

また テンプレート:Math かつ テンプレート:Math のとき テンプレート:Math と定義する。

ペアノ算術

非論理記号として定数記号 テンプレート:Math と関数記号 テンプレート:Mvar, テンプレート:Math, テンプレート:Math と述語記号 テンプレート:Math をもつ等号つき一階述語論理の形式言語上で、以下の公理によって定まる理論をペアノ算術（テンプレート:Lang）あるいは PA というテンプレート:Sfn（形式言語や公理の選び方には本質的に同じものが色々とある。）。

1. $\mathrm{\forall }n\mathrm{\neg }[S(n)=0]$
2. $\mathrm{\forall }n\mathrm{\forall }m[S(n)=S(m)\to n=m]$
3. $\mathrm{\forall }n[n+0=n]$
4. $\mathrm{\forall }n\mathrm{\forall }m[n+S(m)=S(n+m)]$
5. $\mathrm{\forall }n[n\cdot 0=0]$
6. $\mathrm{\forall }n\mathrm{\forall }m[n\cdot S(m)=n\cdot m+n]$
7. $\mathrm{\forall }n\mathrm{\neg }[n<0]$
8. $\mathrm{\forall }n\mathrm{\forall }m[[n<S(m)]\leftrightarrow [n<m]\vee [n=m]]$
9. $[\phi (0)\wedge \mathrm{\forall }n[\phi (n)\to \phi (S(n))]]\to \mathrm{\forall }n[\phi (n)]$

自然数の標準モデル テンプレート:Math において真である テンプレート:Math 閉論理式はペアノ算術から証明ができること（PA の テンプレート:Math 完全性）が知られているテンプレート:Sfn。

一方でゲーデルの第一不完全性定理によりペアノ算術からは証明も反証もできない命題が存在する。有名な例としてはグッドスタインの定理やパリス＝ハーリントンの定理がある。

歴史

ペアノは 1889年に「Arithmetices Principia, nova methodo exposita（算術原理）」と題するラテン語で書かれた論文で自然数の公理の原型となるべきものを発表しているが、それらは自然数以外の公理を含み本来必要とされるよりも多くの命題が述べられているなど、自然数の公理系としては不十分なものであった。1889 年の記載は以下の通り。原論文には誤植があるが正しい形に修正。本論文では、この後、四則演算の定義などが続き、ここでは明示的に自然数を定義しようとしている。

1. 1 は自然数
2. a が自然数なら a = a
3. a, b が自然数で a = b なら b = a
4. a, b, c が自然数で a = b, b = c なら a = c
5. a = b で b が自然数なら a は自然数
6. a が自然数なら a + 1 は自然数
7. a, b が自然数で a = b なら a + 1 = b + 1
8. a が自然数なら、a + 1 と 1 は等しくない
9. もし集合 K が、1 を含み かつ 自然数 x が K に含まれるなら x + 1 が K に含まれる、という条件を満たすなら K は全ての自然数を含む

現在ペアノの公理系として知られる形のものが発表されたのは 1891年の「数の概念について」である。 この論文の中でペアノは次の 5 項目を自然数の満たすべき原始命題として与え、さらにこれら 5 つの命題が互いに独立であることを証明した。ペアノは現代の用語で言うところの公理と推論規則を合わせて原始命題と呼んだ。ここで挙げているものは公理にあたる。

1. 1 は自然数である
2. 任意の自然数 a に対して、a+ が自然数を与えるような右作用演算 + が存在する
3. もし a, b を自然数とすると、 a+ = b+ ならば a = b である
4. a+ = 1 を満たすような自然数 a は存在しない
5. 集合s が二条件「(i) 1 は s に含まれる, (ii) 自然数 a が s に含まれるならば a+ も s に含まれる」を満たすならば、あらゆる自然数は s に含まれる。

ペアノがこれらの原始命題によって自然数そのものを定義しようとはしなかった点には注意を払う必要がある。 彼は自然数の持つべき性質を挙げ、自然数 や 1 などの原始命題中に現れる用語を無定義述語として扱っている。 これは後にヒルベルトらによって強力に進められることになる、形式主義的方法の格好の例といえる。

参考文献

• テンプレート:Cite book
• テンプレート:Cite book
• テンプレート:Citation
• テンプレート:Cite book
• テンプレート:Cite book
• テンプレート:Citation
  • テンプレート:Cite book
  • テンプレート:Cite book - 「数とは何かそして何であるべきか？」・「連続性と無理数」を収録。
• テンプレート:Cite book
• テンプレート:Citation
  • テンプレート:Citation
  • テンプレート:Citation
  • テンプレート:Citation
• テンプレート:Cite book
  • テンプレート:Cite book

関連項目

• 算術の超準モデル
• プレスバーガー算術
• ラムダ計算
• レーヴェンハイム＝スコーレムの定理
• ロビンソン算術

外部リンク

• テンプレート:Kotobank
• テンプレート:Kotobank
• テンプレート:SpringerEOM