形式数論におけるゲーデル番号付けとは、ある形式言語の各記号や式に、ゲーデル数（GN）と呼ばれる固有の自然数を割り当てる機能のことです。この概念は、クルト・ゲーデルが不完全性定理の証明のために初めて用いました。

ゲーデル番号付けは、数学的表記法の各記号に番号を割り当て、自然数の流れで何らかの形式や機能を表現する符号化と解釈できます。また、計算可能な関数の集合のナンバリングは、ゲーデル数（有効数とも呼ばれる）の流れで表すことができます。ロジャースの等価定理は、計算可能な関数の集合のナンバリングが、どのようなゲーデルナンバリングであるかの基準を示しています。

定義と基本的な仕組み

直感的には、ゲーデル番号付けは「シンボル→自然数」、「式（または列）→自然数」という二段階の対応です。まず各基本記号（論理記号、記号、変項、結合子、括弧など）に互いに異なる自然数を割り当てます。次に、記号列（式や証明など）を一つの自然数に結び付けます。こうして、文や証明といった構文的対象を算術的対象（自然数）として扱えるようになります。

代表的な符号化（実装例）

もっとも典型的な符号化は素因数分解を利用する方法です。手順の一例を示します。

  • 各基本記号 s に自然数 a(s) を割り当てる（例： "("→1, ")"→2, "0"→3, "S"→4, "+"→5 …）。
  • 式が記号列 s1, s2, …, sn からなるとき、これを次のように符号化する： GN( s1…sn ) = 2^{a(s1)} · 3^{a(s2)} · 5^{a(s3)} · … · p_n^{a(sn)} （ここで p_n は n 番目の素数）。
  • この方法は一意的素因数分解定理により復号可能で、列の順序や内容を完全に表現できます。

実際の細部（たとえば指数に 0 を許すか、あるいは a(s)+1 を使って 0 を避けるか）は設計者の選択ですが、重要なのは「エフェクティブ（効果的）に対応が計算可能であり、復号もできる」ことです。ゲーデル自身は指数に記号コードそのものを用い、対応関係を原始再帰的（primitive recursive）な関数で扱えるようにしました。

算術への帰着（構文の算術化）と性質

  • 算術化（arithmetization）：ゲーデル番号付けにより「x は式である」「y はその式の正しい証明である」といった構文的関係が自然数上の述語（算術的命題）として表現できるようになります。これにより「証明可能性」を算術の言葉で語れるようになります。
  • 計算可能性：良いゲーデル番号付けでは、符号化（列→数）と復号（数→列）、および「x が有効な証明であるか」などの判定が計算可能（しばしば原始再帰的）です。これが不完全性定理の技術的基盤になります。
  • 不変性（同値性）：異なる「妥当な」番号付けは互いに計算可能な変換で対応できます。ロジャースの等価定理は、計算可能関数のナンバリングに関する正当な基準とその同値性を示します。

不完全性定理への応用（自己言及と証明）

ゲーデルは番号付けを用いて次のような戦略で不完全性定理を示しました。

  • まず「x が証明であり、その終端式は y である」という関係を算術的述語 Proof(x,y) として表現します。これが表現可能であることは符号化の効果性から導かれます。
  • 次に「y が証明される（存在する x があって Proof(x,y)）」という述語を Prov(y)（しばしば Bew(y) とも記す）として定義します。Prov は自然数を引数に取り「その数が表す式は体系で証明可能である」という意味を与えます。
  • 固定点定理（自己言及補題）を用いて、「自分自身のゲーデル数を参照する」式を構成します。つまりある式 G が自分のゲーデル数 g を用いて「G は証明されない」と言うように表現されます。形式的には G ↔ ¬Prov(⌜G⌝)（⌜G⌝ は G のゲーデル数）となる式が構成されます。
  • この G が体系の中で証明できるならば矛盾が生じ、またその否定が証明できるなら矛盾が生じるため、体系が一貫であれば G も ¬G も証明されません。こうして任意の十分に表現力のある一貫な再帰公理的体系が不完全であることが示されます。

具体的な補助的手法と変種

  • 素因数分解法以外にも、Cantor の対関数やペアリング関数、β-関数、あるいは中国剰余定理を使った符号化など、さまざまな符号化法が使われます。重要なのは任意の方法が計算可能で可逆に復元できることです。
  • Kleene の T 述語（計算過程やチューリング機械の逐次的な記述に対応する述語）は、計算の振る舞いを算術で表すためによく用いられます。これにより「プログラム x が入力 y に対して出力 z を返す」という関係も算術化できます。
  • ロジャースの等価定理は「許容される（acceptable）ナンバリングは互いに効果的に変換可能である」ことを示しており、実用上どのナンバリングを取っても理論結果に影響がないことを保証します。

簡単な例

単純化した例として、記号コードを次のように与えるとします：

  • "(" → 1, ")" → 2, "0" → 3, "S" → 4, "+" → 5

式 S(0) を符号化する場合、記号列は S, (, 0, ) なので素数 2,3,5,7 を使って

GN(S(0)) = 2^{4} · 3^{1} · 5^{3} · 7^{2}

のように表せます。得られた自然数は（素因数分解によって）元の記号列に一意に復元できます。

注意点と限界

  • ゲーデル番号付けそのものは形式体系の意味論（真理）を直接与えるものではなく、あくまで構文を算術に移すための方法です。したがって真理や意味に関する問題は別途扱う必要があります。
  • 不完全性定理の結論（ある種の命題が証明できないこと）は、ゲーデル番号付けを通じた構成を使うが、前提として体系の一貫性や再帰的公理化可能性などの条件が要求されます。

まとめ

ゲーデル番号付けは、形式言語の構文を自然数に対応させる効果的な符号化法であり、これを用いることで「証明」「証明可能性」といった構文的概念を算術の内部で表現できます。この技法が、ゲーデルの不完全性定理や自己言及的命題の構成、計算可能性理論におけるナンバリング（有効数）といった重要な結果を可能にしました。具体的な符号化法には複数の方法があり、ロジャースの等価定理はそれらの方法間の本質的同値性を保証します。