ロビンソン算術

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

公理 Qの基盤となる理論は等号付き一階述語論理である。言語は次の構成要素からなる：定項記号: 単項関数記号: 後者二項関数記号: 加法と乗法

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

はいかなる数の後者でもない。

もしとの後者が等しいならばとも等しい。すなわち (の解釈)は単射である。(1)と(2)より (の解釈)はドメインから (の解釈)を除いた集合への単射である。すなわちドメインはデデキント無限である。

任意の数はであるかまたはある数の後者である。PAではこの公理は数学的帰納法の公理図式から導くことができるが、Qはこれを持たないので公理として採用しなければならない。

(4)と(5)は加法の再帰的定義である。

(6)と(7)は乗法の再帰的定義である。

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

通常の狭義の全順序は加法を用いて次のように形式的には定義できる() （全順序性が証明できるわけではない）：

上のようにして定義されたについて次の基本的な要請を公理として(Q1)–(Q7)の後に加える：

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

不完全性 Qにおいて加法の交換法則が証明不能であることを証明する。これによりQが不完全であることを示せる。それにはQのモデルで加法の交換法則が不成立であるようなものを構成すればよい。まずドメインとして

を取る。ここでは相異なる不定元である。関数記号の解釈は上では通常通りに定める。ただしに対しては次のように定める。まず後者関数の解釈を

で定める。この解釈のもとで(Q1)–(Q3)を満たす。あとは(Q4)–(Q7)を満たすように加法と乗法を適当に解釈すればよい。例えば加法は次のように解釈する（ここでは任意の自然数とする）：

その他、積を定義することによりQのモデルが得られるが、ここでは加法の交換法則が成立しない。例えばである。したがって健全性定理によりQにおいては加法の交換法則が証明できない。

超数学超数学におけるQについては, , , , などを見よ。Qの標準的な解釈は自然数に通常の算術を考えたものである。すなわち、Q の各記号に対して、0を自然数0に、を自然数の後者関数に、加法と乗法もそれぞれ通常の加法と乗法とすると、はロビンソン算術の公理をすべて満たす。QはPAと同様に任意の無限濃度の超準モデルを持つ。しかしながらQはPAと異なりテンネンバウムの定理を適用することができない。すなわちQは計算可能な超準モデルを持つ。例えば、計算可能なQの超準モデルとして最高次係数が正である整数係数多項式の全体に通常の演算を入れたものが考えられる。Qの特徴は帰納法の公理図式の不在にある。すなわちQはしばしば個々の具体的な自然数に対する事実を証明することが可能であるが、任意の自然数に対する普遍的な事実の多くを証明できない。正確にいえばQは量化子を持たない真な論理式、真な有界論理式、真なΣ1論理式は証明できるが、真なΠ1論理式は必ずしも証明できない。例えば 5 + 7 = 7 + 5 はQで証明可能だが、一般的な言明 x + y = y + x は証明できない。同様に Sx ≠ x は証明できない()。Qは公理系ZFCのある部分理論で解釈できる。詳しくいえば外延性の公理、空集合の公理、対の公理を持てばよい。この公理はS'()やST()などという。詳しくは一般集合論を見よ。Qの状況は非常に複雑である。QはPAよりも弱い有限公理化可能な一階の理論と考えられ、それらの公理は存在量化をただひとつ持ち、PAが不完全であるのと同様にゲーデルの不完全性定理の意味で不完全であり、本質的に決定不能である。ロビンソンは()において、任意の計算可能関数が表現可能ならしめるPAの公理が何であるかを考えることにより、Qの公理(Q1)–(Q7)を導き出した。PAの帰納法の公理図式は上記(Q3)の証明にのみ必要であり、表現可能性の証明の他の部分には全く必要がない。それゆえ任意の計算可能関数はQにおいて表現可能である(: Th 3.33, : 246})。

ゲーデルの第二不完全性定理の結論はQにおいても成り立つ：無矛盾なQの帰納的拡大で自身の無矛盾性が証明可能であるものは存在せず、証明図のゲーデル数をdefinable cutに制限したとしても同様である(, , :387)。ただし第二不完全性定理の通常の証明にはΣ1帰納法が必要となるから、PAにおける証明をそのままQに対して適用することはできない。

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

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

ロビンソン算術

Źródło i licencja