ロビンソン算術

ロビンソン算術（Robinson arithmetic）とは

数理論理学におけるロビンソン算術（ロビンソンのQとも呼ばれる）は、ペアノ算術（PA）の有限部分理論として知られています。1950年にロビンソンによって導入され、PAから帰納法の公理図式を取り除いた、より弱い理論です。しかし、QはPAと同じ言語を持ちながら、本質的に決定不能で有限公理化可能という重要な特徴を持っています。

Qの公理

Qの基礎となる理論は、等号付きの一階述語論理です。その言語は以下の要素で構成されます。

定項記号: `0`
単項関数記号: 後者関数 `S`
二項関数記号: 加法 `+` と乗法 `⋅`

Qの公理は、以下の(Q1)から(Q7)までの7つの公理からなります。ここで、束縛されていない変数記号は暗黙的に全称量化されているとみなします。

1. `Sx ≠ 0`: 0はいかなる数の後者でもありません。
2. `Sx = Sy → x = y`: もしxとyの後者が等しいならば、xとyも等しい。つまり、Sは単射です。
3. `y = 0 ∨ ∃x(Sx = y)`: 任意の数は0であるか、またはある数の後者です。
4. `x + 0 = x`: 加法の単位元に関する公理。
5. `x + Sy = S(x + y)`: 加法の再帰的定義。
6. `x ⋅ 0 = 0`: 乗法の0に関する公理。
7. `x ⋅ Sy = x ⋅ y + x`: 乗法の再帰的定義。

これらの公理は、自然数における基本的な演算の性質を形式化したものです。特に、(Q3)の公理は、PAでは帰納法の公理図式から導出されますが、Qでは帰納法がないため公理として採用する必要があります。

別の公理化

ロビンソンによる最初の公理化では、Qは(Q1)から(Q13)までの公理で構成されています。これは、基礎となる公理が等号を含まないことに起因します。また、別の公理化では、(Q3)を分割し、狭義の全順序 `<` を用いることもあります。`<` は以下のように定義されます。

`x < y ↔ ∃z(x + Sz = y)`

この `<` を用いて、以下の公理を(Q1)から(Q7)に追加します。

`¬x < 0`
`0 = x ∨ 0 < x`
`x < y ↔ Sx < y ∨ Sx = y`
`x < Sy ↔ x < y ∨ x = y`

これらの公理は、自然数における大小関係の性質を形式化したものです。

不完全性

Qは、加法の交換法則 `∀x∀y(x + y = y + x)` が証明できないため、不完全であることが知られています。このことを示すために、加法の交換法則が成り立たないQのモデルを構成できます。例えば、ドメインとして自然数と不定元a,bの集合 `N ∪ {a, b}` を考え、S, +, ⋅ の解釈を以下のように定めると、加法の交換法則が成り立たないモデルを構成できます。

`Sa = b`, `Sb = a`
`a + n` は n が偶数なら `a`, 奇数なら `b`
`b + n` は n が偶数なら `b`, 奇数なら `a`
`n + a = a`, `n + b = b`
`a + a = a`, `a + b = b`, `b + a = a`, `b + b = b`

このモデルでは、`a + b = b ≠ a = b + a` となるため、加法の交換法則が成り立ちません。

超数学

Qの標準的な解釈は、自然数に通常の算術演算を適用したものです。QはPAと同様に任意の無限濃度の超準モデルを持ちますが、Qはテンネンバウムの定理を適用できないため、計算可能な超準モデルを持つという点でPAと異なります。

Qの特徴は、帰納法の公理図式の不在です。そのため、Qは個々の自然数に関する事実を証明できますが、任意の自然数に対する普遍的な事実を証明できない場合があります。例えば、`5 + 7 = 7 + 5` は証明できますが、`x + y = y + x` は証明できません。また、`Sx ≠ x` も証明できません。

QはZFC集合論の一部分で解釈可能であり、外延性の公理、空集合の公理、対の公理があれば十分です。また、QはPAよりも弱いものの、ゲーデルの不完全性定理が適用できるほど十分な強さを持っています。ロビンソンは、任意の計算可能関数を表現可能にするために必要なPAの公理を考察した結果、Qの公理を導きました。PAの帰納法の公理図式は、表現可能性の証明において(Q3)を証明するためにのみ必要であり、他の部分には必要ありません。したがって、任意の計算可能関数はQで表現可能です。

ゲーデルの第二不完全性定理はQにも適用できます。つまり、無矛盾なQの帰納的拡大で自身の無矛盾性を証明できるものは存在しません。また、第一不完全性定理はQが不完全で決定不能であることを示すのに利用でき、PAの不完全性と決定不能性は帰納法の公理図式によるものではないことが示唆されます。

Qの公理のいずれかを欠くとゲーデルの定理は成立しなくなりますが、Qよりも弱い理論でもゲーデルの定理が成立しないとは限りません。Qの切片は決定不能ではありますが、本質的決定不能ではありません。つまり、無矛盾かつ決定可能な拡大が存在します。

関連項目

一般集合論
ゲンツェンの無矛盾性証明
ゲーデルの不完全性定理
自然数
二階算術
ペアノ算術

参考文献

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

もう一度検索