ロビンソン算術のソースを表示

[[数理論理学]]において'''ロビンソン算術'''({{lang-en-short|Robinson arithmetic}})あるいは'''ロビンソンのQ'''とは[[ペアノ算術]]('''PA''')の有限部分理論であり、{{harvtxt|Robinson|1950}}において最初に導入された。'''Q'''は本質的には'''PA'''から[[数学的帰納法|帰納法]]の[[公理図式]]を取り除いたものである。それゆえ'''Q'''は'''PA'''よりも弱いが同一の言語を持つ[[完全性|不完全]]な理論である。'''Q'''は重要かつ興味深い対象である。というのも'''Q'''は[[本質的決定不能]]かつ[[有限公理化可能]]な'''PA'''の部分理論だからである。

== 公理 ==
'''Q'''の基盤となる理論は等号付き[[一階述語論理]]である。言語は次の構成要素からなる：
* 定項記号: {{Math|0}}
* 単項関数記号: 後者 <math>S</math>
* 二項関数記号: 加法 <math>+</math> と乗法 <math>\cdot</math>

次に示す''Q'''の公理(Q1)–(Q7)は{{harvtxt|Burgess|2005}}による。束縛されていない変数記号は暗黙的に全称量化されているものと考える。すなわち'''Q'''は以下に示す論理式の全称閉包を公理とする：

# <math>Sx \neq 0</math>
#*{{Math|0}} はいかなる数の後者でもない。
# <math>Sx=Sy \to x=y</math> 
#* もし <math>x</math> と <math>y</math> の後者が等しいならば <math>x</math> と <math>y</math> も等しい。すなわち <math>S</math> (の解釈)は単射である。(1)と(2)より <math>S</math> (の解釈)はドメインから {{Math|0}} (の解釈)を除いた集合への単射である。すなわちドメインは[[デデキント無限]]である。
# <math>y = 0 \vee \exists x (Sx=y)</math>
#* 任意の数は {{Math|0}} であるかまたはある数の後者である。'''PA'''ではこの公理は数学的帰納法の公理図式から導くことができるが、'''Q'''はこれを持たないので公理として採用しなければならない。
# <math>x+0=x</math>
# <math>x+Sy=S(x+y)</math>
#* (4)と(5)は加法の再帰的定義である。
# <math>x\cdot 0 = 0</math>
# <math>x \cdot Sy = x\cdot y + x</math>
#* (6)と(7)は乗法の再帰的定義である。

=== 別の公理化 ===
Robinsonによる公理化({{harvtxt|Robinson|1950}})では'''Q'''は公理(Q1)–(Q13)からなる(Mendelson (1997: 201))。最初の6つの公理は基盤となる公理が等号を含まないことから要求されるものである。Machoverによる公理化では前述の公理(Q3)を次のように分割する({{harvtxt|Machover|1996}})。

通常の狭義の[[全順序]] <math><</math> は加法を用いて次のように形式的には定義できる({{harvtxt|Burgess|2005}})
（全順序性が証明できるわけではない）：
:<math>x < y \leftrightarrow \exists z(x+Sz = y)</math>

上のようにして定義された <math><</math> について次の基本的な要請を公理として(Q1)–(Q7)の後に加える：
* <math> \neg x < 0</math>
* <math>0 = x \vee 0 < x</math>
* <math>x < y \leftrightarrow Sx < y \vee Sx = y</math>
* <math>x < Sy \leftrightarrow x < y \vee x = y</math>

別の公理化で <math><</math> を用いたものは Shoenfield (1967: 22) において見られる。

== 不完全性 ==
'''Q'''において加法の交換法則 <math>\forall x\forall y (x+y=y+x)</math> が証明不能であることを証明する。これにより'''Q'''が不完全であることを示せる。それには'''Q'''のモデルで加法の交換法則が不成立であるようなものを構成すればよい。まずドメインとして
:<math>\mathbb{N} \cup \{a, b\}</math>
を取る。ここで <math>a,b</math> は相異なる不定元である。関数記号の解釈は <math>\mathbb N</math> 上では通常通りに定める。ただし <math>a,b</math> に対しては次のように定める。まず後者関数の解釈を
:<math>Sa = b</math>
:<math>Sb = a</math>
で定める。この解釈のもとで(Q1)–(Q3)を満たす。あとは(Q4)–(Q7)を満たすように加法と乗法を適当に解釈すればよい。例えば加法は次のように解釈する（ここで <math>n</math> は任意の自然数とする）：
:<math>a + n = \begin{cases} a & \mbox{if }n\equiv 0 \mod 2 \\ b & \mbox{if }n \equiv 1 \mod 2 \end{cases} </math>
:<math>b + n = \begin{cases} b & \mbox{if }n\equiv 0 \mod 2 \\ a & \mbox{if }n \equiv 1 \mod 2 \end{cases} </math>
:<math>n + a = a</math>
:<math>n + b = b</math>
:<math>a + a = a</math>
:<math>a + b = b</math>
:<math>b + a = a</math>
:<math>b + b = b</math>
その他、積を定義することにより'''Q'''のモデルが得られるが、ここでは加法の交換法則が成立しない。例えば <math>a + b = b \neq a = b + a</math> である。したがって[[健全性定理]]により'''Q'''においては加法の交換法則が証明できない。

== 超数学 ==
[[超数学]]における'''Q'''については{{harvtxt|Boolos|Jeffery|2002}}, {{harvtxt|Tarski et al.|1953}}, {{harvtxt|Smullyan|1991}}, {{harvtxt|Mendelson|1997}}, {{harvtxt|Burgess|2005}}などを見よ。

'''Q'''の標準的な解釈は自然数に通常の算術を考えたものである。すなわち、'''Q''' の各記号に対して、0を自然数0に、{{Mvar|S}} を自然数の後者関数 <math>S^{\mathbb{N}}\colon n\mapsto n+1</math>に、加法と乗法もそれぞれ通常の加法と乗法とすると、<math>\mathbb N</math>はロビンソン算術の公理をすべて満たす。

'''Q'''は'''PA'''と同様に任意の無限[[濃度_(数学)|濃度]]の[[超準モデル]]を持つ。しかしながら'''Q'''は'''PA'''と異なり[[テンネンバウムの定理]]を適用することができない。すなわち'''Q'''は計算可能な超準モデルを持つ。例えば、計算可能な'''Q'''の超準モデルとして最高次係数が正である整数係数多項式の全体に通常の演算を入れたものが考えられる。

'''Q'''の特徴は帰納法の公理図式の不在にある。すなわち'''Q'''はしばしば個々の具体的な自然数に対する事実を証明することが可能であるが、任意の自然数に対する普遍的な事実の多くを証明できない。正確にいえば'''Q'''は量化子を持たない真な論理式、真な有界論理式、真な&Sigma;<sub>1</sub>論理式は証明できるが、真な&Pi;<sub>1</sub>論理式は必ずしも証明できない。例えば 5 + 7 = 7 + 5 は'''Q'''で証明可能だが、一般的な言明 ''x'' + ''y'' = ''y'' + ''x'' は証明できない。同様に ''Sx'' ≠ ''x'' は証明できない({{harvtxt|Burgess|2005}})。

'''Q'''は公理系[[ツェルメロ=フレンケル集合論|'''ZFC''']]のある部分理論で解釈できる。詳しくいえば[[外延性の公理]]、[[空集合の公理]]、[[対の公理]]を持てばよい。この公理は'''S''''({{harvtxt|Tarski et al.|1953}})や'''ST'''({{harvtxt|Burgess|2005}})などという。詳しくは[[一般集合論]]を見よ。

'''Q'''の状況は非常に複雑である。'''Q'''は'''PA'''よりも弱い有限公理化可能な一階の理論と考えられ、それらの公理は存在量化をただひとつ持ち、'''PA'''が不完全であるのと同様に[[ゲーデルの不完全性定理]]の意味で不完全であり、本質的に決定不能である。ロビンソンは({{harvtxt|Robinson|1950}})において、任意の[[計算可能関数]]が表現可能ならしめる'''PA'''の公理が何であるかを考えることにより、'''Q'''の公理(Q1)–(Q7)を導き出した。'''PA'''の帰納法の公理図式は上記(Q3)の証明にのみ必要であり、表現可能性の証明の他の部分には全く必要がない。それゆえ任意の計算可能関数は'''Q'''において表現可能である({{harvtxt|Mendelson|1997}}: Th 3.33, {{harvtxt|Rautenberg|2010}}: 246})。

ゲーデルの第二不完全性定理の結論は'''Q'''においても成り立つ：無矛盾な'''Q'''の帰納的拡大で自身の無矛盾性が証明可能であるものは存在せず、証明図のゲーデル数をdefinable cutに制限したとしても同様である({{harvtxt|Bezboruah|Shepherdson|1976}}, {{harvtxt|Pudlák|1985}}, {{harvtxt|Hájek and Pudlák|1993}}:387)。ただし第二不完全性定理の通常の証明には&Sigma;<sub>1</sub>帰納法が必要となるから、'''PA'''における証明をそのまま'''Q'''に対して適用することはできない。

第一不完全性定理は形式的体系をコーディングしてその基本的性質を証明できるような形式的体系にのみ適用できる。'''Q'''の公理はこの目的に十分な強さとなるように選ばれている。したがって第一不完全性定理の通常の証明は'''Q'''が不完全で決定不能であることを示すのに使える。このことは'''PA'''の不完全性と決定不可能性は帰納法の公理図式によるものではないということを示唆している。

ゲーデルの定理は'''Q'''の7つの公理のどれかひとつを落とすと成立しなくなる。ただしこのことは'''Q'''よりも弱い理論ではゲーデルの定理が成立しないということを'''意味しない'''。これら'''Q'''の切片は決定不能である。しかし本質的決定不能ではない; すなわち無矛盾かつ決定可能な拡大が存在する。

== 関連項目 ==
* [[一般集合論]]
* {{仮リンク|ゲンツェンの無矛盾性証明|en|Gentzen's consistency proof|preserve=1}}
* [[ゲーデルの不完全性定理]]
* [[自然数]]
* [[二階算術]]
* [[ペアノ算術]]

== 参考文献 ==
*{{Citation|last=Bezboruah|first=A.|last2=Shepherdson|first2=John C.|ref=harv|title=Gödel's Second Incompleteness Theorem for Q|Journal=Journal of Symbolic Logic|year=1976|volume=41|number=2|pages=503-512}}
*{{Citation|last=Boolos|first=George|last2=Jeffrey|first2=Richard|ref=harv|title=Computability and Logic|publisher=[[Cambridge University Press]]|year=2002|edition=4th}}
*{{Citation|last=Burgess|first=John P.|ref=harv|title=Fixing Frege|publisher=Princeton University Press|year=2005}}
*{{Citation|last=Hájek|first=Petr|last2=Pudlák|first2=Pavel|ref=harv|title=Metamathematics of first-order arithmetic|publisher=[[Springer-Verlag]]|year=1998|edition=2nd}}
*Lucas, J. R., 1999. ''Conceptual Roots of Mathematics''. [[Routledge]].
*{{Citation|last=Machover|first=Moshe|ref=harv|title=Set Theory, Logic, and Their Limitation|publisher=[[Cambridge University Press]]|year=1996}}
*{{Citation|last=Mendelson|first=E.|ref=harv|title=Introduction to Mathematical Logic|publisher=Chapman & Hall|edition=4th|year=1997}}
*Pavel Pudlák, 1985. "Cuts, consistency statements and interpretations". ''Journal of Symbolic Logic'' v.&nbsp;50 n.&nbsp;2, pp.&nbsp;423–441. 
*{{Citation|last=Rautenberg|first=W.|doi=10.1007/978-1-4419-1221-3|ref=harv|title=A Concise Introduction to Mathematical Logic|url=http://www.springerlink.com/content/978-1-4419-1220-6/|publisher=[[Springer Science+Business Media]]|location=New York|edition=3rd|isbn=978-1-4419-1220-6|year=2010}}.
*{{Citation|last=Robinson|first=R. M.|ref=harv|title=An Essentially Undecidable Axiom System|journal=Proceedings of the International Congress of Mathematics|year=1950|pages=729-730}}
*Joseph R. Shoenfield, 1967. ''Mathematical logic''. Addison Wesley. (Reprinted by Association for Symbolic Logic and A K Peters in 2000.)
*{{Citation|last=Smullyan|first=R. M.|ref=harv|title=Gödel's Incompleteness Theorems|publisher=[[Oxford University Press]]|year=1991}}
*{{Citation|last=Tarski|first=Alfred|last2=Mostowski|first2=A.|last3=Robinson|first3=R. M.|ref={{Harvid|Tarski et al.|1953}}|title=Undecidable theories|publisher=North Holland|year=1953}}

{{DEFAULTSORT:ろひんそんさんしゆつ}}
[[Category:算術の形式理論]]
[[Category:数学に関する記事]]
[[Category:数学のエポニム]]