ゲーデル数
ゲーデル数（ゲーデルすう、英: Gödel number）は、数理論理学において何らかの形式言語のそれぞれの記号や整論理式に一意に割り振られる自然数である。クルト・ゲーデルが不完全性定理の証明に用いたことから、このように呼ばれている。また、ゲーデル数を割り振ることをゲーデル数化（英: Gödel numbering）と呼ぶ。
ゲーデル数のアイデアを暗に使っている例としては、コンピュータにおけるエンコードが挙げられる。 コンピュータでは何でも0と1で表し、「apple」のような文字列も0と1による数字で表す。 ゲーデル数化とは、このように文字列に数字を対応させる事を指す。
ゲーデル数化は、数式におけるシンボルに数を割り当てる符号化の一種でもあり、それによって生成された自然数の列が文字列を表現する。この自然数の列をさらに1つの自然数で表現することもでき、自然数についての形式的算術理論を適用可能となる。
ゲーデルの論文が発表された1931年以来、ゲーデル数はより広範囲な様々な数学的オブジェクトに自然数を割り振るのに使われるようになっていった。
Contents
ゲーデルによる符号化
ゲーデルはゲーデル数化を素因数分解に基づいて体系付けた。彼はまず、彼が使っている数式記法で出現する各基本シンボルにユニークな自然数を割り当てた。
シンボルの列である数式全体を符号化するため、ゲーデルは次のような体系を用いた。自然数の列 [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つのレベルで使った。第一に数式を構成するシンボル列を符号化するのに用い、第二に証明を表している数式列の符号化に用いた。これによって彼は、自然数に関する文と自然数の定理の立証性に関する文の間で対応を示した。
数列のゲーデル数化（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]
すると、次のようになる自然数についての算術関数 gr が存在するはずである。
- [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.