2001年11月15日 作成 不動点定理と不完全性定理 >> 目次 (テーマごと)
2007年 1月16日 補遺  



 不動点定理が 「存在証明」 に使われることを、前回、記述した (ホームページ 72ページを参照されたい)。今回は、その 「からくり」 を説明する。ゲーデル は、不完全性定理のなかで、PM の公理系に ペアノ の公理系を附加して得られる体系を扱っているが、本稿では、説明をわかりやすくするために、PM の公理系と ペアノ の公理系のなかで使われている記号を、そのまま使わないで--数学的な厳密性を、やや犠牲にして--、簡略して解説する。

 まず、理論体系を数式として扱うために、以下のように、論理式に対して数を割り当てる

 1. 体系 P のなかで使われる記号を定義する。

 (1) 定数 (論理定項): ¬, ∨, ∀,...
 (2) 変数 (「タイプ 理論」 を思い出してほしい):
   タイプ 1 の変数: x1, y1, z1,...
   タイプ 2 の変数: x2, y2, z2,...
   タイプ 3 の変数: x3, y3, z3,...
   以下同様にして、すべての タイプ の変数を用意する。

 2. 体系 P のなかで使われる記号に対して、次のように、自然数 (ただし、素数)を 「1 対 1」 に対応させる。

 (1)  ¬, ∨, ∀,...
      1, 3, 5,...
    [ 注意: ¬ には 「1」、∨ には 「3」、∀ には 「5」を対応しているが、ゲーデル の実際の原文とは数値を使っている。]
 (2) タイプ n の変数は pn (p は 13 よりも大きな素数)という形の自然数を対応させる。
   このように素数を使って割り当てられた数を 「ゲーデル数」 という。

 以下の手順で証明する。

 (1) 論理式 f の ゲーデル 数を f' ∈ X とする。
 (2) 文 f (x) について、x と f' との関係は、以下のようになる [ 不動点定理を思い出してほしい ]。
      g: X・X → Y
 (3) したがって、g (x, f') = f (x) が成立する。
   つまり、ゲーデル 数で表現された式 g を使って、f (x) を判断することができる
 (4) g (x, f') = f (x) となるような論理式 g が存在すれば、この数学的構造は整合性がない、ということになる。□

 



[ 補遺 ] (2007年 1月16日)

 本文のなかに示した 「証明法」 は、不動点定理を借用した やりかた であって、ゲーデル が示した証明法そのものではない点に注意されたい。
 ゲーデル の示した証明法を タイプ 理論に沿って逐語的に読み下した書物として、以下を お薦めします。

 不完全性定理 (たのしい すうがく 2)、野崎昭弘、日本評論社

 「不完全性定理」 の証明法を単純に言い切ってしまえば、無矛盾な形式的言語 L のなかで、完全な モテ゛ル を対象にして、自然数 n を考えて、自然数の 「後続 (後者)」 を決定できるかどうかを検討している。そして、その証明法 (無矛盾な自然数体系を前提にした証明法) を使ってケ゛ーテ゛ル が示した点は、「L が無矛盾であれば、L のなかの式 G について、G も ¬G も、L のなかで証明できない」 ことであった。
 もし、「W ⇒ ¬W」 や 「¬W ⇒ W」 という証明であれば、「ハ゜ラト゛ックス の存在証明」 であるが 、無矛盾な体系のなかで、自然数の並びを前提にして、「W ⇒ ¬W」 も 「¬W ⇒ W」 も証明できないことを証明したのが 「不完全性定理」 である。すなわち、自然数の体系 (型 N) に対応できる モテ゛ル ならば、モテ゛ル が無矛盾であっても、真とも偽とも証明できない式があるということ。




  << もどる ベーシックス すすむ >>
  数学基礎論