See also ebooksgratis.com: no banners, no cookies, totally FREE.

CLASSICISTRANIERI HOME PAGE - YOUTUBE CHANNEL
Privacy Policy Cookie Policy Terms and Conditions
ゲーデルの不完全性定理 - Wikipedia

ゲーデルの不完全性定理

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

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

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

目次

[編集] 概要

ゲーデルの第一不完全性定理、第二不完全性定理はいずれも数学の限界を示した定理である。 第一不完全性定理は数学には証明する事もできないし否定を証明する事もできない命題Gが存在する事を意味する。 よって特に数学には正しいのに証明できない事が存在する事になる。 (なぜならGか¬Gのどちらかは正しいはずなのに、Gも¬Gも証明できないのだから。) 第二不完全性定理は、数学が矛盾しない事を数学自身が証明する事はできない事を意味する。

なお、ここでいう「数学」は自然数論ないしそれを含む(そして帰納的に記述可能な)ものの事をさす。

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

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

ゲーデルの定理を示す為の核心となるアイデアは、「俺は証明できない」という趣旨の命題を自然数論の中に作る事にある。 この命題をGと書く。Gはゲーデル文と呼ばれる。

第一不完全性定理を背理法で示す。 Gは「俺は証明できない」という趣旨なのでGが証明可能だとG自身に矛盾するので、Gは証明不能である。 また、¬Gは「Gは証明できる」と同値だが、すでにGが証明不能な事を示したので、¬Gが証明可能だと矛盾する。よって¬Gも証明不能である。 よってGも¬Gも証明不能であり、第一不完全性定理が言えた。

以上から分るように、第一不完全性定理を示す方法は自己言及のパラドックスに酷似する。 よってパラドックスに陥らずに背理法を完遂する為に、本当はより慎重な議論が必要である。 パラドックスを回避しつつ自己言及を可能にするテクニック(ゲーデル数)は「詳細」を参照。

第二不完全性定理を示す。 第一不完全性定理のときの議論より、

  • Gが証明不能なら矛盾が証明可能

である。よって対偶を取る事で

  • 矛盾が証明不能ならGが証明可能 ... (A)

である。

さて、自然数論が矛盾しているというのは、自然数論内で(無条件に)矛盾が証明可能な事を意味する。 よって、「自然数論の無矛盾性」を自然数論内で証明できるというのは、「自然数論内で矛盾が証明不能」な事を自然数論内で証明できる事を意味する。

しかし、

  • (自然数論内で)矛盾が証明不能

な事を(自然数論内で)証明できるなら、

(A)より、

  • Gが証明可能

である事になる。 しかし第一不完全性定理を示したときの議論より、Gは証明不能なので、矛盾。

よって「矛盾が証明不能」ではなく、したがって自然数論の無矛盾性を自然数論内では証明できない。

[編集] 詳細

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

[編集] 定理の意味

ゲーデルの定理やそれを示す方法を正確に理解する為の第一歩は、 ゲーデルの定理中やそれを示す途中で数学という言葉を(少なくとも)2つの意味で用いている事を理解する事である。

第一の「数学」はいわゆる「数学」であり、第二の「数学」は第一の「数学」を外から解析する為の「メタな数学」である。 区別の為、ここでは第一の「数学」を「体系内の数学」と呼ぶ事にする。

2種類の数学を扱うのは、数学基礎論理論計算機科学ではよくある事で、 これは例えば人工知能を考えると理解しやすい。 コンピュータ上にプログラムを書いて人工知能を作り上げ、人工知能に数学をさせる事を考える。 プログラムを走らせると、コンピュータ内で人工知能が定理を自動証明し、証明がコンピュータの画面に表示される。 こうした「コンピュータ内の数学」とは別に、「コンピュータ内の数学」を解析する為の数学が存在する。 すなわち、「このプログラムが出力する証明は本当に正しいのか?」とか「このプログラムはどのような定理を証明できるのか?」といった事を解析する為に 我々がノートにペンで書く「数学」である。 このペンで書く「数学」が、前述の「コンピュータ内の数学」から見れば「メタな数学」に相当するのである。

以上の説明から分るように人工知能から見れば我々やペンで書く数学は「外の世界の人間による外の世界の数学」であり、 逆に我々から見れば人工知能や「コンピュータ内の数学」は「バーチャルな人間によるバーチャルな数学」である。

ペンで書く「メタな数学」における「定理」や「証明」は「コンピュータ内の数学」で人工知能が出力する「定理」や「証明」とははっきり区別しなければならない。 そこで「メタな数学」における「定理」や「証明」をそれぞれ「メタ定理」、「メタ証明」と呼ぶ事にする。

ゲーデルの第一不完全性定理は、「自然数論には(体系内には)証明も否定の証明も存在しない(体系内の)定理が存在する」というメタ定理である。 したがって「ゲーデルの第一不完全性定理」と呼ばずに「ゲーデルの第一不完全性メタ定理」と呼んだ方が正確だし、 「ゲーデルの第一不完全性定理を証明する」と言わずに「ゲーデルの第一不完全性メタ定理をメタ証明する」と言った方が正確である。 これは第二不完全性定理も同様で、本当は「ゲーデルの第二不完全性メタ定理をメタ証明する」と言った方が正確である。

なお、ゲーデルのメタ定理のメタ証明中では後述するゲーデル数の技法を用いて「体系内の数学」の中にさらに「体系内の数学から見てもバーチャルな数学」を作り上げるので、 ゲーデルのメタ定理のメタ証明中には都合3つの数学が登場する事になる。

第二不完全性定理に関して注釈をいれると、このメタ定理が「自然数論は自己の無矛盾性を証明できない」という趣旨である事に注意されたい。 つまり自然数論より多い公理を持つメタ数学を使えば自然数論の無矛盾性を証明できる可能性がある。 (もっとも安直には、「自然数論は無矛盾性である」という公理を持つメタ数学は明らかに自然数論の無矛盾性を証明できる。)

第一不完全性定理も同様で、第一不完全性定理は「自然数論には(体系内には)証明も否定の証明も存在しない(体系内の)定理Gが存在する」としか言っていないので、 自然数論より多くの公理を持つ数学ではGを証明できるかも知れない。 実際、自然数論だけでは証明できないが集合論を使うと証明できる自然数論の定理が存在する。(グッドスタインの定理

[編集] ゲーデルの定理を示す為の準備

以下では体系内の証明とメタ証明を混同しないようにする為、メタ証明の方は「示す」、「導く」、「議論」といった言葉を使って「証明」という言葉を使わず、 逆に体系内の証明の方は「示す」、「導く」、「議論」という言葉を使わずに必ず「証明」という言葉を使う。

なお、第一不完全性定理を示す為の議論は停止性問題の決定不能性を示す際の議論に酷似しているので、停止性問題の項も併せて読むと理解が深まる。

「概要」のところで示したように、ゲーデルの定理を示す方法の核心は「俺は証明できない」という自己言及命題を作る事であった。 しかし自然数論は「命題に言及する命題」を取り扱う事はできないし、自己言及はパラドックスを引き起こし兼ねない。 そこで自己言及命題を直接取り扱う事を諦め、代わりにゲーデル数というテクニックを使って間接的に自己言及を可能にする。

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

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

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

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

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

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

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

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

  • Provable(w) : 「∃n∃y1,...,∃yn : Proof(y1,...,yn,z)」である。すなわち、wをゲーデル数に持つ論理式をPとするとき論理式Pは証明可能である。
  • ProvableARG(z,x) : 「∃n∃y1,...,∃yn : Proof(y1,...,yn,z,x)」である。すなわち、zをゲーデル数に持つ論理式をQとするとき論理式Q(x)は証明可能である。

という論理式も作る事ができる。(上ではPは引数を持たず、Qの引数は1つである事を暗に仮定している。)

[編集] 第一不完全性定理を示す議論

論理式M(x)を、

  • M(x)=¬ProvableARG(x,x)

と定義し、Mのゲーデル数をmとする。 そして、M(m)という命題を考える。(M(m)が「概要」におけるGに当たる)。 すると、M(m)も¬M(m)も証明できない。 実際、

  • 定義よりM(m)=¬ProvableARG(m,m)である。¬ProvableARG(m,m)は「mをゲーデル数に持つ論理式(=M)にmを代入したものは証明不能」という意味なので、M(m)は証明できない。[2]
  • また、¬M(m)=ProvableARG(m,m)が証明可能だとする。ProvableARG(m,m)は「mをゲーデル数に持つ論理式(=M)にmを代入したものは証明可能」という意味なので、これはM(m)が証明可能な事を意味する。[3]しかし前述のように¬M(m)も証明可能だったので、矛盾が証明可能である事になる。これは自然数論が無矛盾であるという仮定に反する。

[編集] 第二不完全性定理を示す議論

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

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

の意味に解する事ができる。 よって「¬Provable(b)」が自然数論の体系内で証明不能な事を示せばよい。

そこで仮に

  • ¬Provable(b)

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

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

  • ProvableARG(m,m) ⇒ Provable(b)

が自然数論の体系内で証明可能な事がわかる。

Mの定義よりProvableARG(m,m)は¬M(m)と同値なので、対偶を取る事で

  • ¬Provable(b) ⇒ M(m)

が自然数論の体系内で証明可能な事がわかる。 仮定より「¬Provable(b)」が自然数論の体系内で証明可能であるので、 上と併せる事で、

  • M(m)

が自然数論の体系内で証明可能な事がわかる。 第一不完全性定理の所で示したように、自然数論が無矛盾ならM(m)は自然数論の体系内で証明不能だったので、これは自然数論が無矛盾であるという仮定に反する。


[編集] その影響・応用

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

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

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

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

[編集] 関連項目

[編集] 脚注

  1. ^ 歴史的には論理式のゲーデル数化の概念が先に生まれ、後にコンピュータがデータを数値で表すようになった。 なお、ゲーデル自身は、素因数分解の一意性を利用して論理式のゲーデル数化を実現している。
  2. ^ 実際、M(m)が証明可能なら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∃y1,...,∃yn : Proof(y1,...,yn,m,m)」=「ProvableARG(m,m)」が証明可能。一方我々は「M(x)」=「¬ProvableARG(x,x)」が証明可能な事を仮定していたので、矛盾が証明可能な事になる。これは自然数論が無矛盾であるという仮定に反する。
  3. ^ ここでω無矛盾性を使う。ω無矛盾性は∃yP(y)が証明できれば、P(u)を満たす自然数uが実際に存在する、という趣旨である。定義より「ProvableARG(m,m)」は「∃y1,...,∃yn : Proof(y1,...,yn,m,m)」であった。ω無矛盾性より、「Proof(u_1,\ldots,u_{n_0},m,m)」を満たす自然数u_1,\ldots,u_{n_0}が実際に存在し、u_1,\ldots,u_{n_0}をゲーデル数に持つ論理式達が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

原論文の邦訳

(前半の58頁が原論文の邦訳、残りの233頁が歴史的な背景を中心とした詳細な解説、という構成)


aa - ab - af - ak - als - am - an - ang - ar - arc - as - ast - av - ay - az - ba - bar - bat_smg - bcl - be - be_x_old - bg - bh - bi - bm - bn - bo - bpy - br - bs - bug - bxr - ca - cbk_zam - cdo - ce - ceb - ch - cho - chr - chy - co - cr - crh - cs - csb - cu - cv - cy - da - de - diq - dsb - dv - dz - ee - el - eml - en - eo - es - et - eu - ext - fa - ff - fi - fiu_vro - fj - fo - fr - frp - fur - fy - ga - gan - gd - gl - glk - gn - got - gu - gv - ha - hak - haw - he - hi - hif - ho - hr - hsb - ht - hu - hy - hz - ia - id - ie - ig - ii - ik - ilo - io - is - it - iu - ja - jbo - jv - ka - kaa - kab - kg - ki - kj - kk - kl - km - kn - ko - kr - ks - ksh - ku - kv - kw - ky - la - lad - lb - lbe - lg - li - lij - lmo - ln - lo - lt - lv - map_bms - mdf - mg - mh - mi - mk - ml - mn - mo - mr - mt - mus - my - myv - mzn - na - nah - nap - nds - nds_nl - ne - new - ng - nl - nn - no - nov - nrm - nv - ny - oc - om - or - os - pa - pag - pam - pap - pdc - pi - pih - pl - pms - ps - pt - qu - quality - rm - rmy - rn - ro - roa_rup - roa_tara - ru - rw - sa - sah - sc - scn - sco - sd - se - sg - sh - si - simple - sk - sl - sm - sn - so - sr - srn - ss - st - stq - su - sv - sw - szl - ta - te - tet - tg - th - ti - tk - tl - tlh - tn - to - tpi - tr - ts - tt - tum - tw - ty - udm - ug - uk - ur - uz - ve - vec - vi - vls - vo - wa - war - wo - wuu - xal - xh - yi - yo - za - zea - zh - zh_classical - zh_min_nan - zh_yue - zu -