ゲーデル数

ゲーデル数とは

ゲーデル数（Gödel number）とは、数理論理学において、形式言語の各記号や論理式に一意に対応する自然数のことです。この概念は、クルト・ゲーデルが自身の不完全性定理を証明する際に用いたことで知られています。ゲーデル数を割り当てる行為を「ゲーデル数化（Gödel numbering）」と呼びます。

ゲーデル数の基本的な考え方

ゲーデル数のアイデアは、コンピュータにおけるエンコード処理と類似しています。コンピュータでは、あらゆる情報が0と1の組み合わせで表現されます。例えば、「apple」という文字列も、0と1で構成された数値として表現可能です。ゲーデル数化は、このような文字列と数値の対応関係を数学的な記号や論理式に適用するものです。

具体的には、数式に登場するシンボルに対して自然数を割り当てることで、数式の文字列を自然数の列として表現します。さらに、この自然数の列を一つの自然数として表すことで、数式を自然数として扱うことができ、算術理論の枠組みで形式的に操作することが可能になります。

ゲーデルがこの概念を発表した1931年以降、ゲーデル数は様々な数学的対象に自然数を割り当てるために広く利用されています。

ゲーデルによる符号化

ゲーデルは、素因数分解を用いてゲーデル数化を体系化しました。まず、彼が用いる数式表記に現れる各シンボルに固有の自然数を割り当てました。そして、シンボルの列である数式全体を符号化するために、以下の体系を用いました。

自然数の列\( x_1, x_2, x_3, ..., x_n \)があるとき、その数列のゲーデル数\( enc(x_1 x_2 x_3 ... x_n) \)は、小さい方からn番目の素数を用いて以下のように表されます。

\[
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}
\]

ここで、\( p_n \)はn番目の素数を示します。例えば、\( p_1 = 2 \), \( p_2 = 3 \), \( p_3 = 5 \)といった具合です。

算術の基本定理によれば、このようにして得られた数値の素因数分解は一意に定まります。したがって、ゲーデル数から元の数列を効率的に復元することが可能です。

ゲーデルはこの手法を2段階で適用しました。第一段階では数式を構成するシンボル列を符号化し、第二段階では証明を表す数式列を符号化しました。この手法により、自然数に関する文と、自然数の定理の証明可能性に関する文との間に対応関係を示すことができました。

なお、数列のゲーデル数化には、より洗練された簡潔な方法も存在します。

一意性の欠如

ゲーデル数化は一意ではありません。ゲーデル数を用いた証明では、様々な定義方法が考えられます。K個の基本シンボルが存在すると仮定し、各基本シンボルと基数Kの位取り記数法の数字との写像をhとします。この写像を用いて別のゲーデル数化を構築することが可能です。

n個のシンボルからなる数式 \( s_1, s_2, s_3, ..., s_n \) は、以下の数値に写像されます。

\[
h(s_1) \times K^{(n-1)} + h(s_2) \times K^{(n-2)} + ... + h(s_{n-1}) \times K^1 + h(s_n) \times K^0
\]

形式数学への応用

形式理論においてゲーデル数化が確立されると、その理論の各推論規則は自然数に関する関数として表現できます。例えば、論理式AとBから推論規則rによって論理式Cが得られるとします。

\[
A, B \vdash_r C
\]

この時、以下の条件を満たす自然数の数論的関数\( g_r \)が存在します。

\[
g_r(f(A), f(B)) = f(C)
\]

ここで、fはゲーデル写像を表します。これは、ゲーデルが用いたナンバリングや、符号化された論理式がゲーデル数から算術的に復元可能な他のナンバリング方式でも成り立ちます。

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

一般化

計算可能性理論では、「ゲーデル数化」という用語は、より広い意味で使われます。

形式言語の構成要素に自然数を割り当てることで、形式言語の操作を、数を操作するアルゴリズムでシミュレートできるようにします。
より一般的には、枚挙可能な数学的対象（例：枚挙可能な群）に自然数を割り当てることで、その数学的対象に対してアルゴリズム的な操作を可能にします。

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

参考文献

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.

関連項目

ゲーデルの不完全性定理
* レーヴェンハイム-スコーレムの定理

もう一度検索