ゲーデルの不完全性定理
ゲーデルの不完全性定理（ゲーデルのふかんぜんせいていり、、）又は単に不完全性定理とは、数学基礎論における重要な定理で、クルト・ゲーデルが1930年に証明したものである。ゲーデルの定理でいう証明不能命題は、「は証明できない」という命題と同値である。はゲーデル文と呼ばれる。
が証明可能であれば、Σ完全性により命題「は証明できる」もまた証明可能である。一方は命題「は証明できない」と同値であることが証明可能であるので、両者から矛盾が導かれる。つまり「は証明できる」ならば「矛盾が証明できる」…(A)したがって、対偶を取れば「矛盾が証明できない」ならば「は証明できない」…(B)となる。
また、が証明可能であれば、の性質から命題「は証明できる」も証明可能である。この際、もしそのものが証明不能だとすると、ω矛盾ということになる。ω無矛盾であればも証明可能である。しかしが証明可能であれば「は証明できない」も証明可能であるので、やはり両者から矛盾が導かれる。したがってω無矛盾であればも証明できないのである。よってω無矛盾であれば、もも証明できない（第一不完全性定理）。
なお、証明可能性の代わりに真理性を用いるならば、パラドックスが導かれる。このことから、自然数論における真理性は自然数論の中では表現できないことが示される（タルスキの定理）。
ゲーデル文を構成するためには自然数論の式を自然数に変換するゲーデル数および自己言及で用いられる対角化の技法（を形式化したもの）が必要である。後者は対角化補題と呼ばれる。
自然数を変数とする述語「は…である」の対角化は、左記の述語のに「は…である」のゲーデル数を代入した命題である。その意味は「「は…である」は…である」となる。
ゲーデル文は「「で表される述語の対角化は証明できない」で表される述語の対角化は証明できない」と表される。「で表される述語の対角化は証明できない」の対角化は、自身と同値になる。
さて、自然数論の無矛盾性とは、「自然数論において矛盾を証明できない」ということである。そして、自然数論による自然数論の無矛盾性証明とは、「」内が、自然数論で証明できるということである。
「自然数論で矛盾が証明できない」と自然数論で証明できれば、第一不完全定理での議論中の(B)より「は証明できない」と証明できる。
しかし、「は証明できない」とはと同値であるから、も証明されることとなり、そこから第一不完全定理での議論中の(A)により、矛盾が証明される。
したがって自然数論が無矛盾、すなわち自然数論で矛盾が証明されないならば、そのこと自体も自然数論では証明できない（第二不完全性定理）。
ゲーデルの定理は「自然数論を含む帰納的公理化可能な無矛盾理論」に対して示されているが、ここでは簡単の為、自然数論のみを扱う。一般の場合も同様。
概要でも説明したように、ゲーデル数というテクニックを使って間接的に自己言及を可能とし、ゲーデル文を構成する。
コンピュータでは全てのデータを一意な数値で表しており、特に文字列や論理式そして論理式の列も数値で表す。このように、論理式を数値で表す行為を論理式のゲーデル数化といい、命題formula_1に対応する数値をformula_1のゲーデル数という。
ゲーデル数化により、論理式に関する様々な性質を論理式として表すことができる。たとえば、
といった論理式を作ることができる。ここで、formula_9やformula_10の引数が論理式自身ではなく自然数であることが重要である。前述のように自然数論は「命題に言及する命題」を取り扱うことはできないが、「命題のゲーデル数に言及する命題」なら取り扱うことができるのである。
formula_3やformula_5などを組み合わせれば、
という論理式も作ることができる。
さらにformula_18を「formula_19」と組み合わせることで、
という論理式も作ることができる（上ではformula_1は引数を持たず、formula_27の引数は1つである）。
論理式formula_33のゲーデル数をformula_34とすると、formula_4にformula_34を代入した論理式formula_37がゲーデル文となる（対角化）。
ゲーデル文formula_37のゲーデル数をformula_39とする。
否定命題formula_37が証明可能とすると、formula_41は真である。このときformula_42完全性よりformula_41は証明可能である。
一方formula_37は「formula_34をゲーデル数に持つ論理式にformula_34を代入したものは証明不能」という意味である。
formula_34をゲーデル数に持つ論理式にformula_34を代入したものはformula_39であるからformula_50が証明可能である。したがって、formula_51は証明可能である。
したがってformula_41およびformula_51が証明され、これは矛盾であるが、これは自然数論が無矛盾であるという仮定に反する。
肯定命題formula_54が証明可能だとすると、formula_55によりformula_41が証明可能である。
このときω無矛盾性を前提すると、formula_39をゲーデル数とする論理式formula_37が証明可能である。
それ故、矛盾が証明されるが、これは自然数論が無矛盾であるという仮定に反する。
矛盾を「formula_59」で表し、「formula_59」のゲーデル数をformula_61とする。すると、「自然数論の体系内で自然数論の無矛盾性を証明できる」という言説を
自然数論の体系内で「formula_62」を証明できる
の意味に解することができる。
まずformula_62が自然数論の体系内で証明可能であると仮定する。
第一不完全性定理のところで示したように、formula_37が証明できれば矛盾が証明できる。この議論を自然数論の体系内で行うことで、formula_65が自然数論の体系内で証明可能なことがわかる。故に対偶を取ることでformula_66が自然数論の体系内で証明可能なことがわかる。したがって、仮定およびformula_50からformula_37が自然数論の体系内で証明可能なことがわかる。第一不完全性定理の所で示したように、formula_37が証明可能だと、矛盾が証明される。したがって矛盾が証明されないならば、formula_62は証明されない。
数学と計算機科学（コンピュータ科学）において、「決定不能」という言葉には二つの異なった意味がある。一つ目は証明論の文脈でゲーデルの定理に関連して使われる意味であり、特定の形式的体系の下で或る命題を証明も否定の証明もできないことを言う。二つ目は（本項では詳述しないが）計算可能性理論に関連した用法であり、命題ではなく決定問題に適用される。決定問題とは入力に対して答が真か偽のいずれかになるような問題である。ある問題を全ての入力に対して正しく解答するような計算可能関数が存在しないとき、そうした問題は決定不能であると言う。
このように決定不能という言葉には二つの意味があるので、代わりにという用語をもって「証明も否定の証明もできない」という意味にあてる場合がある。ところが「独立」という用語にしても依然曖昧な部分がある。単に「証明できない」という意味を表し、「否定の証明もできない」かどうかについてはあえて含意していない場合があるからである。
以下、本節では一つ目の意味で「決定不能」と書く。特定の形式的体系の下である命題が決定不能であることは、その命題の真理値がwell-definedであるかどうかや他の手段で決定可能かどうかについては明らかにしない。決定不能ということが意味するのは、あくまで使用されている特定の形式的体系の下ではその命題の真偽をいずれも証明できないということにすぎない。真理値を決して知ることができないか、または真理値の定義自体が無効となるような、いわゆる「絶対的決定不能」命題が存在するのかどうかは数理哲学における論争の的となっている。
ゲーデルとポール・コーエンの仕事を合わせて、決定不能命題の確かな実例が得られた。連続体仮説はZFC（集合論における標準的な公理系）の下では証明も否定の証明もできない。また、選択公理もZF（ZFCに含まれる公理から選択公理を除いたもの）では証明も否定の証明もできない。これらの結果は不完全性定理を必要としない。1940年、ゲーデルはこれらの命題が何れも ZF または ZFC 集合論では否定を証明できないことを証明した。1960年代、コーエンはこれらがいずれも ZF から証明できず、また連続体仮説が ZFC から証明できないことを証明した。
マチャセビッチによるヒルベルトの第10問題によって決定不能な命題の例が得られる。そのような例はディオファントス方程式の外側に存在量化子を幾つか並べた形として得られる。すなわち不完全性定理の前提条件を満たす形式的体系において、解の存在が証明も反証もできないようなディオファントス方程式が存在する。
1973年、群論におけるが標準的な集合論では決定不能であることが示された。
1977年、パリスとハーリントンは、ラムゼーの定理の一種であるが、一階算術の公理体系であるペアノ算術の下では決定不能だが、より大きな二階算術の体系では真であることを証明できることを証明した。カービーとパリスは後にグッドスタインの定理（自然数の数列に関する命題であり、パリス・ハーリントンの原理よりもいくらか易しい）がペアノ算術では決定不能であることを示した。
計算機科学で応用される はペアノ算術では決定不能だが集合論では証明できる。実際、Kruskalの木定理（またはその有限版）は、と呼ばれる数学的哲学に基づいて構築されたもっと強い体系の下でも決定不能である。これに関連し、更に一般的な （2003年）は計算複雑性理論に影響する。
グレゴリー・チャイティンはアルゴリズム情報理論における決定不能命題を発見し、その状況下で新たな不完全性定理を得た。チャイティンの定理によると、十分な算術を表現可能ないかなる理論においても、どのような数であっても formula_71 よりも大きなコルモゴロフ複雑性を有することがその理論上では証明できないような、上限 formula_71 が存在する。ゲーデルの定理が嘘つきのパラドックスと関係しているのに対し、チャイティンの結果はベリーのパラドックスに関係している。
第1不完全性定理はロビンソン算術を含んでいれば十分である。またω無矛盾性の仮定は単なる無矛盾性の仮定に弱められる（後述）。第2不完全性定理はロビンソン算術にΣ論理式に対する数学的帰納法の公理図式を追加した体系（formula_73）を含んでいれば十分である。ペアノ算術はこれを含むから、ペアノ算術を含む理論は第2不完全性定理の適用範囲である。
ゲーデルの定理は無矛盾な理論についてのみ適用できる。一階論理では、"ex falso quodlibet" () により、矛盾した理論 formula_74 はその言語上の如何なる式であれ証明できてしまい、その中には「formula_74 は無矛盾である」と主張する式も含まれる。
ゲーデルの定理が成り立つのは、あくまで定理が必要としている仮定を満足するような形式的体系に限られる。全ての公理系がこれらの仮定を満たす訳ではなく、中には自然数論の標準モデルを部分構造として持つようなモデルを持っていてもなお仮定を満たさないような公理系もある。例えば、ユークリッド幾何学の一階公理化理論、実閉体の理論、乗算が全域で可能なことを証明できないような算術理論、これらは何れもゲーデルの定理に必要な仮定を満たさない。要点は、これらの公理系では自然数の集合を定義することや自然数の基本的な性質を証明することができないことにある。三つ目の例に関して Dan E. Willard は第二不完全性定理に必要な仮定を満たさないような様々な弱い算術理論を調べた（例えば Willard 2001）。
ゲーデルの定理は実効的に生成された（即ち帰納的可算な）理論についてのみ適用できる。自然数に関する真である文を全て公理とするような理論を考えれば、この理論は無矛盾かつ完全であり、かつペアノ算術を含んでいる。これはゲーデルの定理と矛盾しない。何故ならこの理論は帰納的可算ではないからである。
第二不完全性定理が示すのは、ある公理系の無矛盾性はその公理系自身では証明できないということであって、他の無矛盾な公理系からも証明できないとは言っていない。例えば、ペアノ算術の無矛盾性はZFCから証明できるし、算術の理論にεまでの超限帰納法を加えて得られたもある。
不完全性定理は「『自然数論を含む帰納的公理化可能な理論が、無矛盾（ω無矛盾）であれば』～」という形の定理である。したがって、自然数論を含まない公理系や、帰納的公理化可能でない理論が完全であっても、不完全性定理とは矛盾しない。
真の算術やペアノ算術の無矛盾完全拡大などは無矛盾かつ完全であるが、帰納的公理化可能でない。とくに真の算術は算術的に定義不能である。この結果はタルスキの真理定義不可能性として知られる。
プレスバーガー算術は帰納的公理化可能、無矛盾かつ完全である。プレスバーガー算術は加法しか含まない公理系であり、ゲーデル数によるコード化のテクニックを扱えない。そのため、不完全性定理は適用できない。また、実閉体の理論やユークリッド幾何学も完全であり、（直観に反して）算術を含まないため、不完全性定理は適用できない。したがって実閉体の理論は決定可能である。もっと精密にいうと実閉体の理論では量化記号消去が可能である。この事実は数式処理系の実装などに応用されている。
なお、群や環の公理などは、「自然数論を含まない帰納的公理化可能かつ無矛盾な公理系」であり、不完全性定理は適用できないが、不完全である。例えば、可換群と非可換群がともに存在することから、健全性定理より、群の公理からは積の可換性は証明も反証もできない。
ゲーデルの定理は、数学基礎論のうち、数学の無矛盾性の証明を目標としていたヒルベルト・プログラムには、深刻な影響を与えた。ヒルベルトは公理の適切な設定によって完全かつ無矛盾な体系を達成できると楽観視していたが、第二不完全性定理により、ヒルベルトの計画は頓挫した。
上記のような述語論理式を自然数論の体系内に構成し、証明を形式的に進めるために、ゲーデルはゲーデル数化という操作を導入した。自由変数、論理式、証明図などを自然数でコード化し証明可能、反証可能などの概念を数論的関数として表現する。このように、論理式や証明を数学的に表現して数学内に埋め込む上記の手法は、数学そのものを分析する「メタ数学」を、分析すべきの数学の中に写像する技法の先駆けであり、その後数学基礎論や理論計算機科学でよく用いられるようになる。
第一不完全性定理の拡張として、証明の定義に、命題の証明より小さな、否定命題の証明が存在しないという性質を追加した上で、前提のω無矛盾性を無矛盾性に弱めた定理がジョン・バークリー・ロッサー (1936年) によって示された。この事実はω矛盾した算術理論を考える場合などにおいて重要となる。なお算術を内包する真である体系（自然数の標準モデルで真である公理に基づく体系）はω無矛盾なので、第1不完全性定理は原型のままでも適用できる。今日ではこちらの無矛盾性のみを仮定する強い定理もゲーデルの不完全性定理と呼ばれるが、単にロッサーの定理、ゲーデル・ロッサーの定理などと呼ばれることもある。
第二不完全性定理に関しては、ゲーデルによる証明の定義に代えて、ロッサーによる上記の証明の定義を用いれば、体系自身の無矛盾性が証明できることが、クライゼル (1960) によって指摘されている。2つの証明の定義の同値性は体系内では証明できないため、第2不完全性定理とは矛盾しない。
レオン・ヘンキンは、対角化により「Hは証明できる」と同値となる命題H（ヘンキン文）を構成し、その証明可能性に関する問題を1952年に提起した。この問題は3年後の1955年に、マーティン・レーブによって解かれた。彼は、「Hの証明が存在すればHである」が証明可能であれば、Hもまた証明可能であることを示した（レーブの定理）。Hに矛盾を代入すれば、レーブの定理から第二不完全性定理が示せる。
不完全性定理は他の論理構造と同じく抽象代数による簡易な表現が可能である。を次のように定義する。
formula_74 で無条件に証明可能な文 formula_81 は，この順序で最小元となり、formula_74 で formula_88 を証明できるとき、formula_81 はこの順序の最大元となる。よって最大元でも最小元でもないものは独立命題のみ。つまり不完全であるためにはリンデンバウム代数の位数は3以上であることが要請される。一方 formula_82 を，一階述語論理のリンデンバウム代数とすると、どんな理論のリンデンバウム代数 formula_91 についても，あるイデアル formula_92 が存在して、formula_93 と表される。よって formula_74 が生成するイデアル formula_95 が formula_74 が生み出す定理全体となる。このとき、理論 formula_74 のリンデンバウム代数は、剰余代数 formula_98 である。ここでロビンソン算術に対応する formula_82 の部分集合を formula_27 とする。このとき、ゲーデルの第一不完全性定理は次のようにして表現される。
他に、ザリスキ位相や素スペクトルによる表現が知られている。
計算機科学者（コンピュータ科学者）・電子工学者のトルケル・フランセーンによれば、不完全性定理のインパクトと重要性について、しばしば大げさな主張が繰り返されてきた。たとえば
という言があるが、これらは乱暴な誇張とされる。不完全性定理が一番大きな衝撃を与えたと思われる数学においてさえ、「革命」らしきものは何も起きていない。
この定理は、数理論理学（数学の比較的小さな領域）で常に使われているが、普通の数学者の仕事にはほとんど何の役にも立っていない（そもそも計算機科学は、不完全性定理の証明後に、アラン・チューリング主導で成立した。不完全性定理が計算機科学に革命を発生させたと述べるのは、時系列が誤っている）。
ゲーデルの完全性定理と不完全性定理は、革命的出来事ではなく時代の流れの産物だった。ゲーデル以外の誰かがこれらの定理を発見するのは時間の問題だったとされており、ゲーデル自身もそう見ていた。
フランセーンは『ゲーデルの定理：利用と誤用の不完全ガイド』において、ゲーデルの定理が広範に誤用されていることについて論じている。
数学者の田中一之によれば、ゲーデルの名や定理は「知的会話」に頻出している。フランセーンが述べたように、インターネットのどんなニュースグループでも、遅かれ早かれ誰かがゲーデルの定理を持ち出す。そういった一般的な引用における間違いを正すことが、フランセーンの著書の目的となっている。
1931年にゲーデルが示したのは、「特定の形式体系formula_1において決定不能な命題の存在」であり、一般的な意味での不完全性についての定理ではない。
フランセーンによれば、ゲーデルの不完全性定理と結び付けられるテーマはロジック、数学、計算、哲学、物理学、進化論、政治、宗教、無神論、神学、文学、詩歌、写真、建築、音楽、ヒップホップ、デートなど多岐にわたる。
形式論理学のような専門領域の外では、不完全性定理についての言及の多くは、誤解や自由連想に基いており、馬鹿げているとさえ言える。たとえば、
などが見られる。
アラン・ソーカルとジャン・ブリクモンは、ポストモダニズムに対する論評『「知」の欺瞞』の中で、「ゲーデルの定理こそ汲めども尽きぬ知的濫用の泉である」と述べ、レジス・ドブレ、ミシェル・セールらの文章を批判している。ゲーデルの理論の誤解は、さらに一般的な人々の間でも起こっている。たとえば
田中によれば、ゲーデル自身が不完全性定理について明言しているのは、1963年8月28日の次の文言である。
ゲーデルは慎重を重ねて言葉を選んでいるため、この表現を安易に変えようとすると、不具合を生じる。実際、この定理のいずれかの条件が落とされることで、多数の誤解が生じている（特に「有限的算術を含む」という条件が落とされていることが多い）。
「ある程度の有限的算術を含む」という条件を、「十分大きな」「十分複雑な」「十分表現力のある」などといった曖昧な条件に置き換えることは誤りだが、一般向けの解説などには横行している（実際には、大きな理論で完全なものもあれば、小さな理論で不完全なものもある）。
さらに見落とされやすい点は、不完全性定理の前提および結論部に「算術の条件」があることである。要するに不完全性定理は、「算術を含む体系がその算術部分で不完全である」という主張であり、その算術の外側が完全か不完全かについては、この定理は何も語っていない。
高名な物理学者でさえ、間違いを冒すことがある。フリーマン・ダイソンとスティーヴン・ホーキングの論説は、万物理論の可能性を否定するのにゲーデルの定理を持ち出した。しかし仮に物理理論に不完全性定理が適用できたとしても、不完全性はその算術部分に見つかるだけで、その理論が完全か不完全かは別の問題である。
また、哲学者によるゲーデル関係の本が、フランセーンの本と同じ頃に書店販売されていたが、哲学者の本は専門誌によって酷評された。その本は全体として読みやすく一般読者からの評判は高かったが、ゲーデルの証明の核（不動点定理）について、根本的な勘違いをしたまま説明していた。同様の間違いは他の入門書などにもあり、田中は「一般の哲学者は、論理の専門家ではない」と述べている。
フランセーンによれば、次のような講釈さえ存在する。
実際には不完全性定理は、「形式体系の無矛盾性と完全性についての定理」である。確かに「矛盾」「無矛盾」「完全」「不完全」「体系（システム）」という語は、専門用語でない言語とも結びつきがあるが、およそこのような結びつきは不完全性定理と関係が無い。
神学にも不完全性定理は持ち込まれ濫用されており、たとえば『キリスト教と数学の書誌学』（1983年）がある。
ダニエル・グレーブスは次の通り「考察」をしている。
ナジャムディン・モハメッドも、神学的に「応用」している。
これらの考察と、「ポストモダン的状況」という考え方には類似性がある。そうした理屈では、不完全性は無数の様々な無矛盾理論を導き、どこで「真理」が手に入るかは誰も知らない（したがって、理性だけで正しい道を歩むことはできず、信仰が進むべき道となる）。
しかし実際の数学では、そのような枝分かれは無く、「決定不能性の海」の中でもがくようなことも無いため、そのような「混乱」は神学的幻想に過ぎないとされている。
田中はゲーデルの定理の様々な誤用を分類している。その一つは、人間の悟性が陥りやすい間違った傾向である。たとえば、自分が思いつく有意義そうな体系がどれも不完全であるので、「有意義な体系はすべて不完全である」と思い込み、さらにその原因を定理か何かに帰着させようとする傾向である。
別の誤用は、言語の誤用である。不完全性定理に含まれる「矛盾」「完全」「体系（システム）」などの語は、日常では多様に使われている。そこを混同すれば、ゲーデルの定理までがインフォーマル（非公式・非正式）な意味と結び付けられる。