ロビンソン算術

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

公理

Qの基盤となる理論は等号付き一階述語論理である。言語は次の構成要素からなる：

• 定項記号: テンプレート:Math
• 単項関数記号: 後者 $S$
• 二項関数記号: 加法 $+$ と乗法 $\cdot$

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

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

別の公理化

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

通常の狭義の全順序 $<$ は加法を用いて次のように形式的には定義できる(テンプレート:Harvtxt) （全順序性が証明できるわけではない）：

$x<y\leftrightarrow \mathrm{\exists }z(x+Sz=y)$

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

• $\mathrm{\neg }x<0$
• $0=x\vee 0<x$
• $x<y\leftrightarrow Sx<y\vee Sx=y$
• $x<Sy\leftrightarrow x<y\vee x=y$

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

不完全性

Qにおいて加法の交換法則 $\mathrm{\forall }x\mathrm{\forall }y(x+y=y+x)$ が証明不能であることを証明する。これによりQが不完全であることを示せる。それにはQのモデルで加法の交換法則が不成立であるようなものを構成すればよい。まずドメインとして

$\mathbb{N}\cup \{a,b\}$

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

$Sa=b$

$Sb=a$

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

$a+n=\{\begin{array}{cc}a& \text{if }n\equiv 0mod2\\ b& \text{if }n\equiv 1mod2\end{array}$

$b+n=\{\begin{array}{cc}b& \text{if }n\equiv 0mod2\\ a& \text{if }n\equiv 1mod2\end{array}$

$n+a=a$

$n+b=b$

$a+a=a$

$a+b=b$

$b+a=a$

$b+b=b$

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

超数学

超数学におけるQについてはテンプレート:Harvtxt, テンプレート:Harvtxt, テンプレート:Harvtxt, テンプレート:Harvtxt, テンプレート:Harvtxtなどを見よ。

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

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

Qの特徴は帰納法の公理図式の不在にある。すなわちQはしばしば個々の具体的な自然数に対する事実を証明することが可能であるが、任意の自然数に対する普遍的な事実の多くを証明できない。正確にいえばQは量化子を持たない真な論理式、真な有界論理式、真なΣ₁論理式は証明できるが、真なΠ₁論理式は必ずしも証明できない。例えば 5 + 7 = 7 + 5 はQで証明可能だが、一般的な言明 x + y = y + x は証明できない。同様に Sx ≠ x は証明できない(テンプレート:Harvtxt)。

Qは公理系ZFCのある部分理論で解釈できる。詳しくいえば外延性の公理、空集合の公理、対の公理を持てばよい。この公理はS'(テンプレート:Harvtxt)やST(テンプレート:Harvtxt)などという。詳しくは一般集合論を見よ。

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

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

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

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

関連項目

• 一般集合論
• テンプレート:仮リンク
• ゲーデルの不完全性定理
• 自然数
• 二階算術
• ペアノ算術

参考文献

• テンプレート:Citation
• テンプレート:Citation
• テンプレート:Citation
• テンプレート:Citation
• Lucas, J. R., 1999. Conceptual Roots of Mathematics. Routledge.
• テンプレート:Citation
• テンプレート:Citation
• Pavel Pudlák, 1985. "Cuts, consistency statements and interpretations". Journal of Symbolic Logic v. 50 n. 2, pp. 423–441.
• テンプレート:Citation.
• テンプレート:Citation
• Joseph R. Shoenfield, 1967. Mathematical logic. Addison Wesley. (Reprinted by Association for Symbolic Logic and A K Peters in 2000.)
• テンプレート:Citation
• テンプレート:Citation