ゲーデルの不完全性定理

出典: フリー百科事典『ウィキペディア（Wikipedia）』

ゲーデルの不完全性定理（ゲーデルのふかんぜんせいていり、独: Gödelsche Unvollständigkeitssatz）又は単に不完全性定理とは、数学基礎論における重要な定理の一つで、クルト・ゲーデルが1931年に発表したもの。

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

[編集] 概要

ゲーデルの第一不完全性定理は、数学の公理系が、自身による証明について記述可能ならば、自身を証明する事も、否定を証明する事もできない命題Gが存在する事を意味する。

数学の命題の真偽が定まっていると前提した場合、Gか￢Gのいずれかは真であるが、どちらも証明できないため、数学的には真であるのに公理系からは証明できない命題があることになる。

ゲーデルの第二不完全性定理は、数学の公理系から矛盾が導かれる証明が存在しない場合、その事柄に関する公理系自身による証明もまた存在しない事を意味する。

[編集] ゲーデルの定理を示す方法（ゲーデル自身による方法）

ゲーデルの定理は「自然数論を含む帰納的に記述可能な公理系」を取り扱うが、簡単の為、自然数論のみに話を限定する。

ゲーデルの定理を示す為の核心となるアイデアは、命題G自身が「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₁,...,y_n,z,x) : zをゲーデル数に持つ論理式をPとするとき、y₁,...,y_nをゲーデル数に持つ論理式達が論理式P(x)の証明になっている。

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

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

Provable(z) : 「∃n∃y₁,...,∃y_n : Proof(y₁,...,y_n,z)」である。すなわち、zをゲーデル数に持つ論理式をPとするとき論理式Pは証明可能である。
ProvableARG(z,x) : 「∃n∃y₁,...,∃y_n : Proof(y₁,...,y_n,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)である。

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

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

￢ProvableARG(m,m)⇔￢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)は証明されない。

[編集] その影響・応用

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

これに対し、採用されている公理系そのものを検討することにより、どんな体系の元で問題が証明可能なのか検証しようという試みがある。また数学に数多く存在する未解決問題とのかかわりも考察されている。特に数論等の分野には直感的には真と予想されるが未解決の問題が数多く存在する。もちろんこれは未解決の問題がすべて決定不能であるという意味ではない。ある予想が決定不能であることを証明するには、ゲーデルが行ったように数論的関数によって厳密で帰納的な定義を行い、その上で超数学的な評価をしなければならないが、これは容易な事ではない。

[編集] ゲーデル以後の展開

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

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

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

[編集] 関連項目

[編集] 脚注

^ 歴史的には論理式のゲーデル数化の概念が先に生まれ、後にコンピュータがデータを数値で表すようになった。なお、ゲーデル自身は、素因数分解の一意性を利用して論理式のゲーデル数化を実現している。
^ 実際、￢ProvableARG(m,m)が証明可能なら￢ProvableARG(m,m)の証明系列 $P_1,\ldots,P_{n_0}$ が存在するので、 $P_1,\ldots,P_{n_0}$ のゲーデル数をそれぞれ $a_1,\ldots,a_{n_0}$ とすると、「Proof $(a_1,\ldots,a_{n_0},m,m)$ 」が証明可能、したがって特に「∃n∃y₁,...,∃y_n : Proof(y₁,...,y_n,m,m)」=「ProvableARG(m,m)」が証明可能。一方我々は「￢ProvableARG(x,x)」が証明可能な事を仮定していたので、矛盾が証明される。
^ ω無矛盾とは∃yP(y)が証明できれば、P(u)を満たす自然数uが実際に存在することを指す。定義より「ProvableARG(m,m)」は「∃y₁,...,∃y_n : Proof(y₁,...,y_n,m,m)」であった。ω無矛盾性より、「Proof( $u_1,\ldots,u_{n_0},m,m$ )」を満たす自然数 $u_1,\ldots,u_{n_0}$ が実際に存在し、 $u_1,\ldots,u_{n_0}$ をゲーデル数に持つ論理式達が￢ProvableARG(m,m)の証明系列になる。

[編集] 参考文献

原論文

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

この項目「ゲーデルの不完全性定理」は、自然科学に関連した書きかけの項目です。加筆・訂正などをして下さる協力者を求めています。

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

[1] 実際、￢ProvableARG(m,m)が証明可能なら￢ProvableARG(m,m)の証明系列 $P_1,\ldots,P_{n_0}$ が存在するので、 $P_1,\ldots,P_{n_0}$ のゲーデル数をそれぞれ $a_1,\ldots,a_{n_0}$ とすると、「Proof $(a_1,\ldots,a_{n_0},m,m)$ 」が証明可能、したがって特に「∃n∃y₁,...,∃y_n : Proof(y₁,...,y_n,m,m)」=「ProvableARG(m,m)」が証明可能。一方我々は「￢ProvableARG(x,x)」が証明可能な事を仮定していたので、矛盾が証明される。

[2] ω無矛盾とは∃yP(y)が証明できれば、P(u)を満たす自然数uが実際に存在することを指す。定義より「ProvableARG(m,m)」は「∃y₁,...,∃y_n : Proof(y₁,...,y_n,m,m)」であった。ω無矛盾性より、「Proof( $u_1,\ldots,u_{n_0},m,m$ )」を満たす自然数 $u_1,\ldots,u_{n_0}$ が実際に存在し、 $u_1,\ldots,u_{n_0}$ をゲーデル数に持つ論理式達が￢ProvableARG(m,m)の証明系列になる。

[1]

[2]

[3]