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」を対応しているが、ゲーデル の実際の原文とは数値を使っている。]
　（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） に対応できる モテ゛ル ならば、モテ゛ル が無矛盾であっても、真とも偽とも証明できない式があるということ。




　 << もどる HOME すすむ >>
　 ベーシックス