ゲーデルの不完全性定理

テンプレート:混同 ゲーデルの不完全性定理（ゲーデルのふかんぜんせいていり、テンプレート:Lang-de-short）又は単に不完全性定理とは、数学基礎論における重要な定理の一つで、クルト・ゲーデルが1930年に証明したものである。

第1不完全性定理: 自然数論を含む帰納的に記述できる公理系が、ω無矛盾であれば、証明も反証もできない命題が存在する。
第2不完全性定理: 自然数論を含む帰納的に記述できる公理系が、無矛盾であれば、自身の無矛盾性を証明できない。さらにω無矛盾であれば、自身の無矛盾性を反証できない。

概要

ゲーデルの定理でいう証明不能命題Gは、「Gは証明できない」という命題と同値である。Gはゲーデル文と呼ばれる。

Gが証明可能であれば、Σ₁完全性により命題「Gは証明できる」もまた証明可能である。一方Gは命題「Gは証明できない」と同値であることが証明可能であるので、両者から矛盾が導かれる。つまり

「Gが証明できる」ならば「矛盾が証明できる」　... (A)

したがって、対偶を取れば

「矛盾が証明できない」ならば「Gが証明できない」 ... (B)

となる。また、￢Gが証明可能であれば、Gの性質から命題「Gは証明できる」も証明可能である。この際、もしGそのものが証明不能だとすると、ω矛盾ということになる。ω無矛盾であればGも証明可能である。しかしGが証明可能であれば「Gは証明できない」も証明可能であるので、やはり両者から矛盾が導かれる。したがってω無矛盾であれば￢Gも証明できないのである。よってω無矛盾であれば、Gも￢Gも証明できない（第一不完全性定理）。

なお、証明可能性の代わりに真理性を用いるならば、パラドックスが導かれる。このことから、自然数論における真理性は自然数論の中では表現できないことが示される（タルスキの定理）。

ゲーデル文を構成するためには自然数論の式を自然数に変換するゲーデル数および自己言及で用いられる対角化の技法が必要である。

自然数を変数とする述語「xは…である」の対角化は、左記の述語のxに「xは…である」のゲーデル数を代入した命題である。その意味は「「xは…である」は…である」となる。

ゲーデル文Gは「「xで表される述語の対角化は証明できない」で表される述語の対角化は証明できない」と表される。「xで表される述語の対角化は証明できない」の対角化は、G自身と同値になる。

さて、自然数論の無矛盾性とは、「自然数論において矛盾が証明できない」ということである。そして、自然数論による自然数論の無矛盾性証明とは、「」内が、自然数論で証明できるということである。

「自然数論で矛盾が証明できない」と自然数論で証明できれば、第一不完全定理での議論中の(B)より「Gが証明できない」と証明できる。

しかし、「Gが証明できない」とはGと同値であるから、Gも証明されることとなり、そこから第一不完全定理での議論中の（A)により、矛盾が証明される。

したがって自然数論が無矛盾、すなわち自然数論で矛盾が証明されないならば、そのこと自体も自然数論では証明できない（第二不完全性定理）。

詳細

ゲーデルの定理は「自然数論を含む帰納的に記述可能な公理系」に対して示されているが、ここでは簡単の為、自然数論のみを扱う。一般の場合も同様。

ゲーデル文の構成

概要でも説明したように、ゲーデル数というテクニックを使って間接的に自己言及を可能とし、ゲーデル文を構成する。

コンピュータでは全てのデータを一意な数値で表しており、特に文字列や論理式そして論理式の列も数値で表す。このように、論理式を数値で表す行為を論理式のゲーデル数化といい、命題Pに対応する数値をPのゲーデル数という^[1]。

ゲーデル数化により、論理式に関する様々な性質を論理式として表すことができる。たとえば、

Axiom(x)： xは公理のゲーデル数である。
MP(x,y,z)： xをゲーデル数に持つ論理式とyをゲーデル数に持つ論理式から三段論法によりzをゲーデル数に持つ論理式が導ける。

といった論理式を作ることができる。ここで、AxiomやMPの引数が論理式自身ではなく自然数であることが重要である。前述のように自然数論は「命題に言及する命題」を取り扱うことはできないが、「命題のゲーデル数に言及する命題」なら取り扱うことができるのである。

Axiom(x)やMP(x,y,z)などを組み合わせれば、

Proof(y,z) : zをゲーデル数に持つ論理式をPとするとき、yをゲーデル数に持つ論理式の列が論理式Pの証明になっている。

という論理式も作ることができる。

さらにProofを「∃」と組み合わせることで、

Provable(z) : 「∃y : Proof(y,z)」である。すなわち、zをゲーデル数に持つ論理式をPとするとき論理式Pは証明可能である。
ProvableARG(z,x) : 「∃y : Proof(y,z,x)」である。すなわち、zをゲーデル数に持つ論理式をQとするとき、Q中の変数に自然数xを代入した論理式Q(x)は証明可能である。

という論理式も作ることができる（上ではPは引数を持たず、Qの引数は1つである）。

論理式￢ProvableARG(x,x)のゲーデル数をmとすると、xにmを代入した論理式￢ProvableARG(m,m)がゲーデル文となる（対角化）。

第一不完全性定理の証明

ゲーデル文￢ProvableARG(m,m)のゲーデル数をnpmmとする。

￢ProvableARG(m,m)の証明不能性

￢ProvableARG(m,m)が証明可能とすると、Provable(npmm)は真である。このときΣ₁完全性よりProvable(npmm)は証明可能である。

一方￢ProvableARG(m,m)は「mをゲーデル数に持つ論理式にmを代入したものは証明不能」という意味である。

mをゲーデル数に持つ論理式にmを代入したものはnpmmであるから

￢ProvableARG(m,m)⇔￢Provable(npmm)

が証明可能である。したがって、￢Provable(npmm)は証明可能である。

したがってProvable(npmm)および￢Provable(npmm)が証明され、これは矛盾である　^[2]が、これは自然数論が無矛盾であるという仮定に反する。

ProvableARG(m,m)の証明不能性

ProvableARG(m,m)が証明可能だとすると、

ProvableARG(m,m)⇔Provable(npmm)

によりProvable(npmm)が証明可能である。

このときω無矛盾性を前提すると、npmmをゲーデル数とする論理式￢ProvableARG(m,m)が証明可能である。^[3]

それ故、矛盾が証明されるが、これは自然数論が無矛盾であるという仮定に反する。

第二不完全性定理の証明

矛盾を「⊥」で表し、「⊥」のゲーデル数をbとする。すると、「自然数論の体系内で自然数論の無矛盾性を証明できる」という言説を

自然数論の体系内で「￢Provable(b)」を証明できる

の意味に解することができる。

まず

￢Provable(b)

が自然数論の体系内で証明可能であると仮定する。

第一不完全性定理のところで示したように、￢ProvableARG(m,m)が証明できれば矛盾が証明できる。この議論を自然数論の体系内で行うことで、

Provable(npmm) ⇒ Provable(b)

が自然数論の体系内で証明可能なことがわかる。故に対偶を取ることで

￢Provable(b) ⇒ ￢Provable(npmm)

が自然数論の体系内で証明可能なことがわかる。したがって、仮定および￢ProvableARG(m,m)⇔￢Provable(npmm)から

￢ProvableARG(m,m)

が自然数論の体系内で証明可能なことがわかる。第一不完全性定理の所で示したように、￢ProvableARG(m,m)が証明可能だと、矛盾が証明される。したがって矛盾が証明されないならば、￢Provable(b)は証明されない。

決定不能命題の例

数学と計算機科学において、「決定不能」という言葉には二つの異なった意味がある。一つ目は証明論の文脈でゲーデルの定理に関連して使われる意味であり、特定の形式的体系の下で或る命題を証明も否定の証明もできないことを言う。二つ目は（本項では詳述しないが）計算可能性理論に関連した用法であり、命題ではなく決定問題に適用される。決定問題とは答が YES か NO のいずれかになるような問題の可算無限集合である。ある問題集合に含まれる全ての問題に正しく解答するような計算可能関数が存在しないとき、そうした問題は決定不能であると言う。

このように決定不能という言葉には二つの意味があるので、代わりにテンプレート:仮リンクという用語をもって「証明も否定の証明もできない」という意味にあてる場合がある。ところが「独立」という用語にしても依然曖昧な部分がある。単に「証明できない」という意味を表し、「否定の証明もできない」かどうかについてはあえて含意していない場合があるからである。

以下、本節では一つ目の意味で「決定不能」と書く。特定の形式的体系の下である命題が決定不能であることは、その命題の真理値がwell-definedであるかどうかや他の手段で決定可能かどうかについては明らかにしない。決定不能ということが意味するのは、あくまで使用されている特定の形式的体系の下ではその命題の真偽をいずれも証明できないということにすぎない。真理値を決して知ることができないか、または真理値の定義自体が無効となるような、いわゆる「絶対的決定不能」命題が存在するのかどうかは数理哲学における論争の的となっている。

ゲーデルとポール・コーエンの仕事を合わせて、決定不能命題の確かな実例が得られた。連続体仮説はZFC（集合論における標準的な公理系）の下では証明も否定の証明もできない。また、選択公理もZF（ZFCに含まれる公理から選択公理を除いたもの）では証明も否定の証明もできない。これらの結果は不完全性定理を必要としない。1940年、ゲーデルはこれらの命題が何れも ZF または ZFC 集合論では否定を証明できないことを証明した。1960年代、コーエンはこれらがいずれも ZF から証明できず、また連続体仮説が ZFC から証明できないことを証明した。

マチャセビッチによるヒルベルトの第10問題によって決定不能な命題の例が得られる。そのような例はディオファントス方程式の外側に存在量化子を幾つか並べた形として得られる。すなわち不完全性定理の前提条件を満たす形式的体系において、解の存在が証明も反証もできないようなディオファントス方程式が存在する。

1973年、群論におけるテンプレート:仮リンクが標準的な集合論では決定不能であることが示された。

1977年、パリスとハーリントンは、ラムゼーの定理の一種であるテンプレート:仮リンクが、一階算術の公理体系であるペアノ算術の下では決定不能だが、より大きな二階算術の体系では真であることを証明できることを証明した。カービーとパリスは後にグッドスタインの定理（自然数の数列に関する命題であり、パリス・ハーリントンの原理よりもいくらか易しい）がペアノ算術では決定不能であることを示した。

計算機科学で応用されるテンプレート:仮リンクはペアノ算術では決定不能だが集合論では証明できる。実際、Kruskalの木定理（またはその有限版）は、テンプレート:仮リンク^[4]と呼ばれる数学的哲学に基づいて構築されたもっと強い体系の下でも決定不能である。これに関連し、更に一般的なテンプレート:仮リンク（2003年）は計算複雑性理論に影響する。

グレゴリー・チャイティンはアルゴリズム情報理論における決定不能命題を発見し、その状況下で新たな不完全性定理を得た。チャイティンの定理によると、十分な算術を表現可能ないかなる理論においても、どのような数であっても c よりも大きなコルモゴロフ複雑性を有することがその理論上では証明できないような、上限 c が存在する。ゲーデルの定理が嘘つきのパラドックスと関係しているのに対し、チャイティンの結果はベリーのパラドックスに関係している。

ゲーデルの定理に関する制限

ゲーデルの定理は無矛盾な理論についてのみ適用できる。一階論理では、ex falso quodlibet (en) により、矛盾した理論 T はその言語上の如何なる式であれ証明できてしまい、その中には「T は無矛盾である」と主張する式も含まれる。

ゲーデルの定理が成り立つのは、飽くまで定理が必要としている仮定を満足するような形式的体系の中に限られる。全ての公理系がこれらの仮定を満たす訳ではなく、中には自然数を部分集合として含むようなモデルを持っていてもなお仮定を満たさないような公理系もある。例えば、ユークリッド幾何学の一階公理化理論、実閉体の理論、乗算が全域で可能なことを証明できないような算術理論、これらは何れもゲーデルの定理に必要な仮定を満たさない。要点は、これらの公理系では自然数の集合を定義することや自然数の基本的な性質を十分展開することができないことにある。三つ目の例に関して言えば、Dan E. Willard は第二不完全性定理に必要な仮定を満たさないような様々な弱い算術理論を調べた（例えば Willard 2001）。

ゲーデルの定理は実効的に生成された（即ち、帰納的可算な）理論についてのみ適用できる。もし自然数に関する真である文を全て公理とするような理論があるとすると、この理論は無矛盾かつ完全であり、ペアノ算術を含みつつゲーデルの定理は全く成立しなくなる。何故ならこの理論は帰納的可算ではないからである^[5]。

第二不完全性定理が示すのは、ある公理系の無矛盾性はその公理系自身では証明できないということであって、他の無矛盾な公理系からも証明できないとは言っていない。例えば、ペアノ算術の無矛盾性はZFCから証明できるし、算術の理論に超限帰納法を加えて得られたテンプレート:仮リンクもある。

不完全性定理の成立しない体系

不完全性定理は「『自然数論を含む帰納的に記述できる公理系が、無矛盾（ω無矛盾）であれば』～」という形の定理である。したがって、自然数論を含まない公理系や、帰納的に記述できない公理系が完全であっても、不完全性定理とは矛盾しない。

真の算術やペアノ算術の無矛盾完全拡大などは完全であるが、帰納的に記述できない。

プレスバーガー算術は完全である。プレスバーガー算術は加法しか含まない公理系であり、ゲーデル数などのテクニックを扱えない。そのため、不完全性定理は適用できない。また、実閉体の理論やユークリッド幾何学も完全であり、（直感に反して）算術を含まないため、不完全性定理は適用できない。

なお、群論などは、「自然数を含まない帰納的に記述できる無矛盾な公理系」であり、不完全性定理は適用できないが、不完全である。

その影響・応用

テンプレート:Main ゲーデルの定理は、数学基礎論のうち、数学の無矛盾性の証明を目標としていたヒルベルト・プログラムには、深刻な影響を与えた。ヒルベルトは公理の適切な設定によって完全かつ無矛盾な体系を達成できると楽観視していたが、第二不完全性定理により、ヒルベルトの計画は頓挫した。

ゲーデルの定理の証明方法は、数学そのものを分析する「メタ数学」を、分析すべきの数学の中に写像する技法の先駆けであり、その後数学基礎論や理論計算機科学でよく用いられるようになる。

ゲーデル以後の展開

第一不完全性定理の拡張として、証明の定義に、命題の証明より小さな、否定命題の証明が存在しないという性質を追加した上で、前提のω無矛盾性を無矛盾性に弱めた定理がジョン・バークリー・ロッサー (1936年) によって示された。ただし、これはどちらかといえば技術的な関心事に過ぎない。算術を内包する真である体系（自然数に関する真である公理に基づく体系）はω無矛盾なので、第1不完全性定理は原型のままでも適用できるからである。今日ではこちらの無矛盾性のみを仮定する強い定理もゲーデルの不完全性定理と呼ばれるが、単にロッサーの定理とかゲーデル・ロッサーの定理とか呼ばれる。

第二不完全性定理に関しては、ゲーデルによる証明の定義に代えて、ロッサーによる上記の証明の定義を用いれば、体系自身の無矛盾性が証明できることが、クライゼル (1960) によって指摘されている。2つの証明の定義の同値性は体系内では証明できないため、第2不完全性定理とは矛盾しない。

レオン・ヘンキンは、対角化により「Hは証明できる」と同値となる命題H（ヘンキン文）を構成し、その証明可能性に関する問題を1952年に提起した。この問題は3年後の1955年に、マーティン・レーブによって解かれた。彼は、「Hの証明が存在すればHである」が証明可能であれば、Hもまた証明可能であることを示した（レーブの定理）。Hに矛盾を代入すれば、レーブの定理から第二不完全性定理が示せる。

不完全性定理の代数化

不完全性定理は他の論理構造と同じく抽象代数による簡易な表現が可能である。テンプレート:仮リンクを次のように定義する。

理論 T のリンデンバウム代数 T^L は，文に順序構造を入れたものである。
順序は、もし理論 T で A → B を証明できるならば A ≧ B と定義される。
A と B の順序が等しいなら、A と B を同一視する。

T で無条件に証明可能な文 A は，この順序で最小元となり、T で￢A を証明できるとき、A はこの順序の最大元となる。よって最大元でも最小元でもないものは独立命題のみ。つまり不完全であるためにはリンデンバウム代数の位数は3以上であることが要請される。一方 B を，一階述語論理のリンデンバウム代数とすると、どんな理論のリンデンバウム代数 L についても，あるイデアル I ⊆ B が存在して、L= B/I と表される。よって T が生成するイデアル (T) が T が生み出す定理全体となる。このとき、理論 T のリンデンバウム代数は、剰余代数 B/(T) である。ここでロビンソン算術に対応する B の部分集合を Q とする。このとき、ゲーデルの第一不完全性定理は次のようにして表現される。

( Q ) を含む再帰的可算素イデアル p ⊂ B は存在しない。

他に、ザリスキ位相や素スペクトルによる表現が知られている。

脚注

テンプレート:脚注ヘルプテンプレート:Reflist

参考文献

原論文 K. Gödel Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I. Monatshefte für Mathematik und Physik 38: 173-98. 1931
原論文の日本語訳 林晋・八杉満利子訳・解説『ゲーデル不完全性定理』岩波書店〈岩波文庫〉, 2006年。ISBN 4-00-339441-0 （前半の58頁が原論文の邦訳、残りの233頁が歴史的な背景を中心とした解説、という構成）

廣瀬健・横田一正著『ゲーデルの世界: 完全性定理と不完全性定理』海鳴社、1985年。ISBN 4-87525-106-8

（ゲーデルの完全性定理と不完全性定理の解説書。両方の原論文の邦訳が収録されている）

教科書

前原昭二『数学基礎論入門』朝倉書店〈復刊基礎数学シリーズ〉、2006年。ISBN 4-254-11723-X
新井敏康『数学基礎論』岩波書店、2011年。ISBN 4-000-05536-4

誤用と誤解について

トルケル・フランセーン『ゲーデルの定理: 利用と誤用の不完全ガイド』みすず書房、2006年。ISBN 4-622-07569-5

外部リンク

↑ 歴史的には論理式のゲーデル数化の概念が先に生まれ、後にコンピュータがデータを数値で表すようになった。なお、ゲーデル自身は、素因数分解の一意性を利用して論理式のゲーデル数化を実現している。

↑ 実際、￢ProvableARG(m,m)が証明可能なら￢ProvableARG(m,m)の証明系列<math>P_1,\ldots,P_{n_0}</math>が存在するので、論理式の列<math>P_1,\ldots,P_{n_0}</math>のゲーデル数を<math>a</math>とすると、「Proof<math>(a,m,m)</math>」が証明可能、したがって特に「∃y : Proof(y,m,m)」=「ProvableARG(m,m)」が証明可能。一方我々は「￢ProvableARG(x,x)」が証明可能な事を仮定していたので、これは矛盾である。

↑ ω無矛盾とは∃yP(y)が証明できれば、P(u)を満たす自然数uが実際に存在することを指す。定義より「ProvableARG(m,m)」は「∃y : Proof(y,m,m)」であった。ω無矛盾性より、「Proof(<math>u,m,m</math>)」を満たす自然数<math>u</math>が実際に存在し、<math>u</math>をゲーデル数に持つ論理式の列が￢ProvableARG(m,m)の証明系列になる。

↑ 訳注：自己言及的でないこと。

↑ 訳注：この場合の「帰納的可算」とは、すべての定理のゲーデル数を枚挙する計算可能関数が存在する（実効的に枚挙可能）ことを意味する。クレイグのトリックによれば、このことは定理集合が帰納的な公理系から生成される（演繹閉包である）ことと同値である。

[1]

[2]

[3]

[4]

[5]