ゲーデルの不完全性定理
出典: フリー百科事典『ウィキペディア（Wikipedia）』
ゲーデルの不完全性定理（ - ふかんぜんせいていり、Gödel's incompleteness theorems、または不完全性定理）は、数学基礎論における重要な定理の一つで、クルト・ゲーデルが1931年に発表した。
- 第1不完全性定理 自然数論を含む帰納的に記述できる公理系が、ω無矛盾であれば、証明も反証もできない命題が存在する。
- 第2不完全性定理 自然数論を含む帰納的に記述できる公理系が、無矛盾であれば、自身の無矛盾性を証明できない。
なお、第1不完全性定理の拡張として、前提のω無矛盾性を無矛盾性に弱めた定理がジョン・バークリー・ロッサー (1936) によって示された。 また、第2不完全性定理に関して、ロッサーによる証明の定義を用いれば、体系自身の無矛盾性が証明できることが、クライゼル (1960) によって指摘されている。
目次 |
[編集] 証明の概要（ゲーデルによる最初の証明）
証明の核心は自己言及のパラドックスと深い関わりがある。証明チェック述語が記述可能な論理体系Tで次のような述語論理式Gを構成できたとしよう：「Gの証明は存在しない」。この論理式Gが論理体系T内に存在する時、Tが受ける影響について検証するのである。
Gが体系T内で証明（反証）可能ならば、同じく体系T内で￢G＝「Gの証明が存在する」が証明可能である。すると、
となり、矛盾する。
つまりTが無矛盾であれば、Gは体系T内で証明できない。ところで、Tがω無矛盾であればGは明らかに真である。したがって、Tがω無矛盾である限り、真であっても証明できない命題が存在する点で不完全である。ゲーデルは自然数論の体系において証明チェック述語を構成し、これを用いてGを具体的に構成することにより自然数論を含む体系Tは不完全であることを示した（第一不完全性定理）。命題Gをゲーデル文という。
さて、Gを含む体系Tで、無矛盾性は証明できるのであろうか。体系T内で「無矛盾である」という意味を持つ述語をCとする。このCというのは具体的には「証明が存在しない命題が存在する」と表せる。Cを前提すれば、第一不完全性定理の証明をTの中でコード化してGが導ける。したがって
に他ならない。TからCが証明可能ならば、上の結果から、TからGが証明できる。しかし第一不完全性定理により、Gは証明不能であるから矛盾。よって、Gを含む体系Tが無矛盾の場合、TはT自身の無矛盾性Cを証明できない（第二不完全性定理）。
ところでGを「Gが自身を証明できない」と見た場合、直感的に正しい。つまり直感的に真なる命題が数学体系内で必ずしも証明できるとは限らない、ということを示唆している。
[編集] ゲーデル数化
上記のような述語論理式を自然数論の体系内に構成し、証明を形式的に進めるために、ゲーデルはゲーデル数化という操作を導入した。自由変数、論理式、証明図などを自然数でコード化し証明可能、反証可能などの概念を数論的関数として表現する。なお、論理式や証明を数学的に表現して数学内に埋め込む手法を超数学という。（<--Fix me)
[編集] その影響・応用
数学基礎論のうち、数学の無矛盾性の証明を目標としていたヒルベルトプログラムには、深刻な影響を与えた（詳しくは数学基礎論、ゲーデルの項を参照）。ヒルベルトは公理の適切な設定によって完全かつ無矛盾な体系を達成できると楽観視していたが、不完全性定理により、ヒルベルトの計画は頓挫した。
これに対し、採用されている公理系そのものを検討することにより、どんな体系の元で問題が証明可能なのか検証しようという試みがある。また数学に数多く存在する未解決問題とのかかわりも考察されている。特に数論等の分野には直感的には真と予想されるが未解決の問題が数多く存在する。もちろんこれは未解決の問題がすべて決定不能であるという意味ではない。ある予想が決定不能であることを証明するには、ゲーデルが行ったように数論的関数によって厳密で帰納的な定義を行い、その上で超数学的な評価をしなければならないが、これは容易な事ではない。
