ゲーデル数のソースを表示

'''ゲーデル数'''（ゲーデルすう、{{lang-en-short|Gödel number}}）は、[[数理論理学]]において何らかの[[形式言語]]のそれぞれの記号や[[well-formed formula|論理式]]に一意に割り振られる[[自然数]]である。[[クルト・ゲーデル]]が[[ゲーデルの不完全性定理|不完全性定理]]の証明に用いたことから、このように呼ばれている。また、ゲーデル数を割り振ることを'''ゲーデル数化'''（{{lang-en-short|Gödel numbering}}）と呼ぶ。

<!--数学に詳しくない人に向けた説明-->
ゲーデル数のアイデアを暗に使っている例としては、コンピュータにおける[[エンコード]]が挙げられる。
コンピュータでは何でも0と1で表し、「apple」のような文字列も0と1による数字で表す。
ゲーデル数化とは、このように文字列に数字を対応させる事を指す。

ゲーデル数化は、数式における[[シンボル]]に数を割り当てる[[エンコード|符号化]]の一種でもあり、それによって生成された[[自然数]]の列が文字列を表現する。この自然数の列をさらに1つの自然数で表現することもでき、自然数についての形式的算術理論を適用可能となる。

ゲーデルの論文が発表された1931年以来、ゲーデル数はより広範囲な様々な数学的オブジェクトに自然数を割り振るのに使われるようになっていった。

== ゲーデルによる符号化 ==
ゲーデルはゲーデル数化を素因数分解に基づいて体系付けた。彼はまず、彼が使っている数式記法で出現する各基本シンボルにユニークな自然数を割り当てた。

シンボルの列である数式全体を符号化するため、ゲーデルは次のような体系を用いた。自然数の列 <math>x_1 x_2 x_3 ... x_n</math> があるとき、ゲーデルによるその数列の符号化とは、小さいほうから ''n'' 個の素数を数列の各数値でべき乗したものの積となる。
:<math>\mathrm{enc}(x_1 x_2 x_3 ... x_n) = 2^{x_1}\cdot 3^{x_2}\cdot 5^{x_3}\cdot ...\cdot {p_n}^{x_n}</math>
[[算術の基本定理]]によれば、このようにして得られた値の素因数分解は一意に定まる。従って、ゲーデル数から元の数列を効率的に復元可能である。

ゲーデルはこの手法を2つのレベルで使った。第一に数式を構成するシンボル列を符号化するのに用い、第二に証明を表している数式列の符号化に用いた。これによって彼は、自然数に関する文と自然数の定理の立証性に関する文の間で対応を示した。

数列のゲーデル数化（[[:en:Gödel numbering for sequences|Gödel numbering for sequences]]）には、より洗練され簡潔な方法が存在する。

== 一意性の欠如 ==
ゲーデル数化は一意ではなく、ゲーデル数を使った証明では様々な定義方法が存在する。

''K'' 個の基本シンボルがあるとする。各基本シンボルと基数 ''K'' の[[位取り記数法]]の数字との写像（ここでは ''h'' と名づける）によって別のゲーデル数化を構築する。すると、''n'' 個のシンボルからなる文字列で構成される数式 <math> s_1 s_2 s_3 \dots s_n</math> は次の数に写像される。

:<math> h(s_1) \times K^{(n-1)} + h(s_2) \times K^{(n-2)} + \cdots + h(s_{n-1}) \times K^1 + h(s_n) \times K^0 </math>

== 形式数学への応用 ==
ある形式理論のゲーデル数化が確立されると、その理論の各[[推論規則]]は自然数についての関数として表される。''f'' がゲーデル写像で、論理式 ''A'' と ''B'' から推論規則 ''r'' によって数式 ''C'' が得られるとする。
:<math> A, B \vdash_r C \ </math>
すると、次を満たす自然数の[[数論的関数]] ''g<sub>r</sub>'' が存在するはずである。
:<math> g_r(f(A),f(B)) = f(C) \ </math>
これはゲーデルの用いた[[ナンバリング_(計算可能性理論)|ナンバリング]]においては真であり、符号化された論理式がそのゲーデル数から算術的に復元可能な他のナンバリング方式でも成り立つ。

従って、[[ペアノの公理]]のような数とその間の算術的関係に関する文を作ることができる形式理論においては、ゲーデル数化を使えば間接的にその理論自体に関する文を作ることができる。このような技法によってゲーデルは形式体系の属性の無矛盾性と完全性に関する結果の証明を行った。

== 一般化 ==
[[計算可能性理論]]において、「ゲーデル数化」は上述よりさらに一般化した意味を持つ用語として使われる。
# [[形式言語]]の構成要素に自然数を割り当てて、形式言語の構成要素の操作を、数を操作する[[アルゴリズム]]でシミュレートできるようにする。
# より一般化して、枚挙可能な数学的オブジェクト（例えば枚挙可能な[[群 (数学)|群]]）に自然数を割り当てて、その数学的オブジェクトにアルゴリズム的操作ができるようにする。

ゲーデル数化という用語は、文字列としての「数」を割り当てる場合にも使われることがある。これは数というよりも文字列を操作する[[計算模型]]（[[チューリングマシン]]など）に必須の考え方である。

== 参考文献 ==
* Gödel, Kurt, "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I", Monatsheft für Math. und Physik '''38''', 1931, S.173-198.
* ''[[ゲーデル、エッシャー、バッハ]]''、[[ダグラス・ホフスタッター]]（作）
*''Gödel's Proof'' by Ernest Nagel and James R. Newman.  

== 関連項目 ==
* [[ゲーデルの不完全性定理]]
* [[レーヴェンハイム-スコーレムの定理]]

{{Normdaten}}
{{DEFAULTSORT:けえてるすう}}
[[Category:数理論理学]]
[[Category:計算理論]]
[[Category:クルト・ゲーデル]]
[[Category:数学に関する記事]]