ロビンソン算術
From Wikipedia, the free encyclopedia
別の公理化
Qの基盤となる理論は等号付き一階述語論理である。言語は次の構成要素からなる:
- 定項記号: 0
- 単項関数記号: 後者
- 二項関数記号: 加法 と乗法
次に示すQ'の公理(Q1)–(Q7)はBurgess (2005)による。束縛されていない変数記号は暗黙的に全称量化されているものと考える。すなわちQは以下に示す論理式の全称閉包を公理とする:
-
- 0 はいかなる数の後者でもない。
-
- もし と の後者が等しいならば と も等しい。すなわち (の解釈)は単射である。(1)と(2)より (の解釈)はドメインから 0 (の解釈)を除いた集合への単射である。すなわちドメインはデデキント無限である。
-
- 任意の数は 0 であるかまたはある数の後者である。PAではこの公理は数学的帰納法の公理図式から導くことができるが、Qはこれを持たないので公理として採用しなければならない。
-
- (4)と(5)は加法の再帰的定義である。
-
- (6)と(7)は乗法の再帰的定義である。
Robinsonによる公理化(Robinson (1950))ではQは公理(Q1)–(Q13)からなる(Mendelson (1997: 201))。最初の6つの公理は基盤となる公理が等号を含まないことから要求されるものである。Machoverによる公理化では前述の公理(Q3)を次のように分割する(Machover (1996))。
通常の狭義の全順序 は加法を用いて次のように形式的には定義できる(Burgess (2005)) (全順序性が証明できるわけではない):
上のようにして定義された について次の基本的な要請を公理として(Q1)–(Q7)の後に加える:
別の公理化で を用いたものは Shoenfield (1967: 22) において見られる。
不完全性
Qにおいて加法の交換法則 が証明不能であることを証明する。これによりQが不完全であることを示せる。それにはQのモデルで加法の交換法則が不成立であるようなものを構成すればよい。まずドメインとして
を取る。ここで は相異なる不定元である。関数記号の解釈は 上では通常通りに定める。ただし に対しては次のように定める。まず後者関数の解釈を
で定める。この解釈のもとで(Q1)–(Q3)を満たす。あとは(Q4)–(Q7)を満たすように加法と乗法を適当に解釈すればよい。例えば加法は次のように解釈する(ここで は任意の自然数とする):
その他、積を定義することによりQのモデルが得られるが、ここでは加法の交換法則が成立しない。例えば である。したがって健全性定理によりQにおいては加法の交換法則が証明できない。