ゲーデルの不完全性定理

ゲーデルの不完全性定理（ゲーデルのふかんぜんせいていり、テンプレート:Lang-en-short、テンプレート:Lang-de-short）または不完全性定理とは、数学基礎論テンプレート:Sfnとコンピュータ科学（計算機科学）の重要な基本定理テンプレート:Sfn。（数学基礎論は数理論理学や超数学とほぼ同義な分野で、コンピュータ科学と密接に関連しているテンプレート:Sfn。）　不完全性定理は厳密には「数学」そのものについての定理ではなく、「形式化された数学」についての定理であるテンプレート:Sfn テンプレート:Efn2。クルト・ゲーデルが1931年の論文で証明した定理でありテンプレート:Sfn、テンプレート:仮リンク（形式主義）では自然数論の無矛盾性の証明が成立しないことを示すテンプレート:Sfn テンプレート:Sfn。なお、少し拡張された有限の立場では、自然数論の無矛盾性の証明が成立する（テンプレート:仮リンク）テンプレート:Sfn テンプレート:Efn2。

数学基礎論研究者の菊池誠によると不完全性定理は、20世紀初め以降に哲学から決別した数学基礎論の中で現れたテンプレート:Sfn テンプレート:Efn2。コンピュータ科学者・数理論理学者のトルケル・フランセーンテンプレート:Sfnおよび数学者・数理論理学者の田中一之テンプレート:Sfnによると、不完全性定理が示した不完全性とは、数学用語の意味での「特定の形式体系Pにおいて決定不能な命題の存在」であり、一般的な意味での「不完全性」とは無関係であるテンプレート:Sfn。不完全性定理を踏まえても、数学の形式体系の公理は真であり無矛盾であるしテンプレート:Sfn テンプレート:Efn2、数学の完全性も成立し続けているテンプレート:Sfn。しかし“不完全性定理は数学や理論の「不完全性」を証明した”といった誤解や、“数学には「不完全」な部分があると証明済みであり、数学以外の分野に「不完全」な部分があってもおかしくない”といった誤解が一般社会・哲学・宗教・神学等によって広まり、誤用されているテンプレート:Sfn テンプレート:Efn2。テンプレート:See also 数学の「無矛盾性」を証明することを目指したヒルベルト・プログラムに関して「不完全性定理がヒルベルトのプログラムを破壊した」という類の哲学的発言はよくあるが、これは実際の不完全性定理やゲーデルの見解とは異なる、とフランセーン達は解説しているテンプレート:Sfn。正確には、ゲーデルはヒルベルトと同様の見解を持っており、彼が不完全性定理を証明して示したのは、ヒルベルトの目的（「無矛盾性証明」）を実現するためには手段（ヒルベルト・プログラム）を拡張する必要がある、ということだったテンプレート:Sfn。これについて日本数学会編集の『岩波数学辞典』では「彼テンプレート:Interpの結果はヒルベルトの企図を直接否定するものではなく，実際この定理の発見後に無矛盾性証明のための様々な方法論が開発されている」と記されているテンプレート:Sfn。テンプレート:See also

概要

ゲーデルの不完全性定理は、ゲーデルが1931年の論文で証明した次の内容であるテンプレート:Sfn。

『数学原理（プリンキピア・マセマティカ）』の体系や公理的集合論の中には、「証明も反証もできない「自然数論の命題」」が存在する。
また、これらの体系に公理を追加しても公理が有限個であれば、前述の命題の存在を解消できない。

より正確には、不完全性定理とは次の2つの定理（それぞれ第一/第二不完全性定理と呼ばれる）の総称であるテンプレート:Sfn。テンプレート:Math theorem

テンプレート:Math theorem なお「有限の立場」とは、数学の形式主義における「記号の有限的な操作のみから構成される」立場を指すテンプレート:Sfn。

注意

形式的体系 S と S' に対して（言語を適当に拡張した）S' が S を含むとは、S の論理式全体の集合Fml(S)から S' の論理式全体の集合Fml(S')への次のような写像T:Fml(S)→Fml(S')が存在するときを言う：φ∈Fml(S)がS で証明できるときT(φ)は S' で証明できる。このTはしばしば「翻訳」と呼ばれる。この意味でペアノ算術PAはツェルメロ＝フレンケル集合論ZFCに含まれるテンプレート:Sfn。
「初等的な自然数論」について、ゲーデル自身はペアノの公理と原始帰納法による関数の定義を前提に自然数論の体系を構築したテンプレート:Harv。この体系は、加法・乗法・べき乗・階乗・順序関係などを帰納的に定義する十分な表現力を持っている。それぞれの定理の前提条件は、ロビンソン算術を含む半決定可能な理論（第一）、 $𝐈 Σ_{1}$ を含む半決定可能な理論（第二）に置き換えても証明することができる^[1]。

証明の概要

準備

帰納的公理化可能な理論が自然数論を含むならば、当該理論における証明可能性が原始帰納的述語として表現できる。この証明可能性述語を用いて、「テンプレート:Mvarは証明できない」と同値となる証明不能命題テンプレート:Mvar（ゲーデル文）が構成できる。ゲーデル文を構成するためには自然数論の式を自然数に変換するゲーデル数および自己言及で用いられる対角化の技法（を形式化したもの）が必要である。後者は対角化補題と呼ばれる。

自然数を変数とする述語「テンプレート:Mvarは…である」の対角化は、上記の述語のテンプレート:Mvarに「テンプレート:Mvarは…である」自身のゲーデル数を代入した命題である。その意味は

「「テンプレート:Mvarは…である」は…である」

となる。ゲーデル文テンプレート:Mvarは

「「テンプレート:Mvarで表される述語の対角化は証明できない」で表される述語の対角化は証明できない」

と表される。「テンプレート:Mvarで表される述語の対角化は証明できない」の対角化は、テンプレート:Mvar自身と同値になる。

第一不完全性定理の証明の概要

さて、ゲーデル文テンプレート:Mvarが証明可能であれば、Σ₁完全性により命題「テンプレート:Mvarは証明できる」もまた証明可能である。一方テンプレート:Mvarは命題「テンプレート:Mvarは証明できない」と同値であることが証明可能であるので、両者から矛盾が導かれる。つまり

「テンプレート:Mvarは証明できる」ならば「矛盾が証明できる」 … (A)

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

「矛盾が証明できない」ならば「テンプレート:Mvarは証明できない」 … (B)

となる。

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

なお、証明可能性の代わりに真理性を用いれば、パラドックスが導かれることから、帰納的公理化された自然数論（以下、自然数論）における真理性は自然数論の中では算術的述語として表現できない、と示される（タルスキの定理）。

第二不完全性定理の証明の概要

自然数論の無矛盾性を

「自然数論において矛盾を証明できない」…(C)

と表す。このとき、自然数論による自然数論の無矛盾性証明とは、(C)が自然数論で証明できるということである。 (C)が自然数論で証明できれば、第一不完全定理での議論中の(B)より

「テンプレート:Mvarは証明できない」

と証明できる。しかし、

「テンプレート:Mvarは証明できない」

とはテンプレート:Mvarと同値であるから、テンプレート:Mvarも証明されることとなり、そこから第一不完全性定理での議論中の(A)により、矛盾が証明される。

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

詳細

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

ゲーデル文の構成

概要でも説明したように、ゲーデル数というテクニックを使って間接的に自己言及を可能とし、ゲーデル文を構成する。コンピュータでは全てのデータを一意な数値で表しており、特に文字列や論理式そして論理式の列も数値で表す。このように、論理式を数値で表す行為を論理式のゲーデル数化といい、命題 $P$ に対応する数値を $P$ のゲーデル数というテンプレート:Efn2。

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

$A x i o m (x)$ ： $x$ は公理のゲーデル数である。
$M P (x, y, z)$ ： $x$ をゲーデル数に持つ論理式と $y$ をゲーデル数に持つ論理式からモーダスポネンスにより $z$ をゲーデル数に持つ論理式が導ける。

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

$A x i o m (x)$ や $M P (x, y, z)$ などを組み合わせれば、

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

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

さらに $P r o o f$ を「 $\exists$ 」と組み合わせることで、

$P r o v a b l e (z)$ : 「 $\exists y : P r o o f (y, z)$ 」である。すなわち、 $z$ をゲーデル数に持つ論理式を $P$ とするとき論理式Pは証明可能である。
$P r o v a b l e A R G (z, x)$ : 「 $\exists y : P r o o f (y, z, x)$ 」である。すなわち、 $z$ をゲーデル数に持つ論理式を $Q$ とするとき、 $Q$ 中の変数に自然数 $x$ を代入した論理式 $Q (x)$ は証明可能である。

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

論理式 $\neg P r o v a b l e A R G (x, x)$ のゲーデル数を $m$ とすると、 $x$ に $m$ を代入した論理式 $\neg P r o v a b l e A R G (m, m)$ がゲーデル文となる（対角化）。

第一不完全性定理の証明

ゲーデル文 $\neg P r o v a b l e A R G (m, m)$ のゲーデル数を $n p m m$ とする。

否定命題の証明不能性

否定命題 $\neg P r o v a b l e A R G (m, m)$ が証明可能とすると、 $P r o v a b l e (n p m m)$ は真である。このとき $Σ_{1}$ 完全性より $P r o v a b l e (n p m m)$ は証明可能である。

一方 $\neg P r o v a b l e A R G (m, m)$ は

「

m

をゲーデル数に持つ論理式に

m

を代入したものは証明不能」

という意味である。

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

\neg P r o v a b l e A R G (m, m) \Leftrightarrow \neg P r o v a b l e (n p m m)

が証明可能である。したがって、

\neg P r o v a b l e (n p m m)

は証明可能である。

したがって $P r o v a b l e (n p m m)$ および $\neg P r o v a b l e (n p m m)$ が証明され、これは矛盾であるテンプレート:Efn2が、これは自然数論が無矛盾であるという仮定に反する。

肯定命題の証明不能性

肯定命題 $P r o v a b l e A R G (m, m)$ が証明可能だとすると、

P r o v a b l e A R G (m, m) \Leftrightarrow P r o v a b l e (n p m m)

により

P r o v a b l e (n p m m)

が証明可能である。

このときω無矛盾性を前提すると、 $n p m m$ をゲーデル数とする論理式 $\neg P r o v a b l e A R G (m, m)$ が証明可能である。テンプレート:Efn2

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

第二不完全性定理の証明

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

自然数論の体系内で「

\neg P r o v a b l e (b)

」を証明できる

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

まず

\neg P r o v a b l e (b)

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

第一不完全性定理のところで示したように、 $\neg P r o v a b l e A R G (m, m)$ が証明できれば矛盾が証明できる。この議論を自然数論の体系内で行うことで、

P r o v a b l e (n p m m) \Rightarrow P r o v a b l e (b)

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

\neg P r o v a b l e (b) \Rightarrow \neg P r o v a b l e (n p m m)

が自然数論の体系内で証明可能なことがわかる。したがって、仮定および $\neg P r o v a b l e A R G (m, m) \Leftrightarrow \neg P r o v a b l e (n p m m)$ から

\neg P r o v a b l e A R G (m, m)

が自然数論の体系内で証明可能なことがわかる。第一不完全性定理の所で示したように、 $\neg P r o v a b l e A R G (m, m)$ が証明可能だと、矛盾が証明される。したがって矛盾が証明されないならば、 $\neg P r o v a b l e (b)$ は証明されない。

決定不能命題の例

数学と計算機科学（コンピュータ科学）において、「決定不能」という言葉には二つの異なった意味がある。一つ目は証明論の文脈でゲーデルの定理に関連して使われる意味であり、特定の形式的体系の下で或る命題を証明も反証もできないことを言う。二つ目は計算可能性理論に関連した用法であり、命題ではなく決定問題に適用される。決定問題とは入力に対して答が真か偽のいずれかになるような問題である。ある問題を全ての入力に対して正しく解答するようなアルゴリズムが存在しないとき（すなわち特性関数が計算可能関数でないとき）、そうした問題は決定不能であると言う。

不完全性定理は、自然数論が一つ目の意味で決定不能であることを主張している。一方、述語論理の論理式が充足可能か否かを判定する充足可能性問題は決定問題にあたるが、不完全性定理によって、二番目の意味で決定不能である。つまり、述語論理の論理式が充足不能であれば、その論理式から矛盾を導く証明を見つけることができるが、充足可能であるときにその旨、回答を返すアルゴリズムは存在し得ない。

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

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

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

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

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

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

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

テンプレート:複数の問題第1不完全性定理はロビンソン算術を含んでいれば十分である。またω無矛盾性の仮定は単なる無矛盾性の仮定に弱められる（後述）。第2不完全性定理はロビンソン算術にΣ₁論理式に対する数学的帰納法の公理図式を追加した体系（ $I Σ_{1}$ ）を含んでいれば十分である。ペアノ算術はこれを含むから、ペアノ算術を含む理論は第2不完全性定理の適用範囲である。

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

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

ゲーデルの定理は実効的に生成された（即ち帰納的可算な）理論についてのみ適用できる。自然数に関する真である文を全て公理とするような理論を考えれば、この理論は無矛盾かつ完全であり、かつペアノ算術を含んでいる。これはゲーデルの定理と矛盾しない。何故ならこの理論は帰納的可算ではないからであるテンプレート:Efn2。

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

不完全性定理が適用されない体系

不完全性定理が適用されない例としてはユークリッド幾何学テンプレート:Sfn、プレスバーガー算術テンプレート:Sfn、実閉体と代数的閉体の理論におけるタルスキの定理などがあるテンプレート:Sfn。

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

真の算術やペアノ算術の無矛盾完全拡大などは無矛盾かつ完全であるが、帰納的公理化可能でない。とくに真の算術は算術的に定義不能である。この結果はタルスキの真理定義不可能性として知られる。

プレスバーガー算術は帰納的公理化可能、無矛盾かつ完全である。プレスバーガー算術は加法しか含まない公理系であり、ゲーデル数によるコード化のテクニックを扱えない。そのため、不完全性定理は適用できない。また、実閉体の理論やユークリッド幾何学も帰納的公理化可能、無矛盾かつ完全であり、（直観に反して）算術を含まないため、不完全性定理は適用できない。したがって実閉体の理論は（計算可能性の意味で）決定可能である。もっと精密にいうと実閉体の理論では量化記号消去が可能である。この事実は数式処理系の実装などに応用されている。

なお、群や環の公理などは、「帰納的公理化可能だが自然数論を含まない無矛盾な公理系」であり、不完全性定理は適用できないが、不完全である。例えば、可換群と非可換群がともに存在することから、健全性定理より、群の公理からは積の可換性は証明も反証もできない。

不完全性定理によるヒルベルト・プログラムの発展

テンプレート:See also フランセーンによれば、数学者ダヴィット・ヒルベルトは「数学に“イグノラビムス（ignorabimus, 永遠に知られないこと）”はない」と述べたテンプレート:Sfn。数学上に不可知は無く、全ての問題は最終的に解決されるというヒルベルトのこの見方は、「ノン・イグノラビムス」として知られているテンプレート:Sfn。ゲーデルの不完全性定理は、「決してこのヒルベルトの楽天的な見方を否定するものではない」とされているテンプレート:Sfn。何故なら、不完全性定理によって否定されたものとは単に、「ノン・イグノラビムス」へ到達する手段の一つとしてヒルベルトが提案したもの ―― すなわち、「すべての数学の問題が解けるような単一の形式体系」 ―― であり、「ノン・イグノラビムス」自体は否定されていないからであるテンプレート:Sfn。

実際ゲーデル自身は以下のような、「ノン・イグノラビムス」的なヒルベルト流の見解を持っていたテンプレート:Sfn。テンプレート:Quote

こうした見解に基づき、ゲーデルは現代数学を拡張する手段として「巨大基数公理」を提案したテンプレート:Sfn。哲学等において「不完全性定理がヒルベルトのプログラムを破壊した」という類の発言がよくあるが、これは実際の不完全性定理やゲーデルの見解とは異なるテンプレート:Sfn。正確に言えば、ヒルベルトの目的（数学の「無矛盾性証明」）を実現するには手段（ヒルベルト・プログラム）を拡張する必要がある、ということをゲーデルが不完全性定理を通して示したのだったテンプレート:Sfn。

菊池誠の『不完全性定理』によるとヒルベルトは、「ゲーデルの結果により証明論が実行不可能となったという見解は間違いであり，それは有限の立場の拡張が必要であることが判明しただけだ」と述べているテンプレート:Sfn。ゲーデルも不完全性定理の論文の中で、この定理とヒルベルト・プログラムとの関係を取り上げて、不完全性定理は「Hilbertテンプレート:Interpの形式主義的な視点とまったく矛盾しない」、と注意を書いているテンプレート:Sfn。

日本数学会が編集した『岩波　数学辞典』第4版では、不完全性定理について次の通り記述されているテンプレート:Sfn。テンプレート:Quote テンプレート:See also 述語論理式を自然数論の体系内に構成し、証明を形式的に進めるために、ゲーデルはゲーデル数化という操作を導入した。自由変数、論理式、証明図などを自然数でコード化し証明可能、反証可能などの概念を数論的関数として表現する。このように、論理式や証明を数学的に表現して数学内に埋め込む上記の手法は、数学そのものを分析する「超数学（メタ数学）」を、分析すべき数学の中に写像する技法の先駆けであり、その後数学基礎論や理論計算機科学でよく用いられるようになる。

ゲーデル以後の展開

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

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

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

不完全性定理の代数化

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

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

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

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

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

数学と哲学の分離

理学博士・数学基礎論研究者である菊池誠テンプレート:Sfnの『不完全性定理』によれば、数学史上で「数学の正しさと無矛盾性に対する確信が揺らいだことがかつて一度だけあった」テンプレート:Sfn。19世紀末～20世紀初めには、数学の中でいくつも逆理が発見され、数学の基礎についての「不安の時代」が発生したテンプレート:Sfn。そうして数学の無矛盾性や「そもそも定理や証明とは何なのか」といった哲学的な問いに対し、伝統的な哲学の手法ではなく数学の手法（形式主義）で答える試みがなされ、そこから数学の一分野「数学基礎論」が生まれたテンプレート:Sfn テンプレート:Efn2。

数学の世界全体の無矛盾性を「有限の立場」で証明して数学を危機から救おうとしたヒルベルト・プログラムが、実現不可能であることをゲーデルの不完全性定理が明らかにしたテンプレート:Sfn。ヒルベルト・プログラムは破綻した一方で、公理的集合論が整備されて「無矛盾」と見なされたこと、「算術の世界の無矛盾性」が証明されたことなどによって「不安の時代」は終わり、数学基礎論が哲学から決別したテンプレート:Sfn。数学基礎論上で不完全性定理は、哲学的なものとしてでなく、数学的な応用可能性として重視されるようになったテンプレート:Sfn。またこの定理は、電子技術を伴うコンピュータ科学（計算機科学）の重要な基本定理でもあるテンプレート:Sfn テンプレート:Efn2。

前掲書によると、20世紀初めは数学者と哲学者は共に数学の基礎について論じていたが、「今では数学者と哲学者は極めて疎遠である」テンプレート:Sfn。数学についての哲学的議論を、数学者は「最近の数学を無視した色褪せた100年前の論争の焼き直し」と見なしているテンプレート:Sfn。不完全性定理を含む数学分野（数学基礎論）を数学者が「哲学のようなもの」と呼ぶ場合、それは「哲学のような深い立派なもの」ではなく「哲学のようなツマラナイコト」を意味していると言うテンプレート:Sfn テンプレート:Efn2。

誤解（哲学等による誤解・誤用）

コンピュータ科学者・数理論理学者・哲学博士（Ph.D. in Philosophy）のトルケル・フランセーンテンプレート:Sfn テンプレート:Sfnによれば、不完全性定理のインパクトと重要性について、しばしば大げさな主張が繰り返されてきたテンプレート:Sfn テンプレート:Efn2。たとえばテンプレート:Quotation という言があるが、これらは乱暴な誇張とされるテンプレート:Sfn。不完全性定理が一番大きな衝撃を与えたと思われる数学においてさえ、「革命」らしきものは何も起きていないテンプレート:Sfn。

この定理は、数理論理学（数学の比較的小さな領域）で常に使われているが、普通の数学者の仕事にはほとんど何の役にも立っていないテンプレート:Sfn（そもそも計算機科学は、不完全性定理の証明後に、アラン・チューリング主導で成立したテンプレート:Sfn。不完全性定理が計算機科学に革命を発生させたと述べるのは、時系列が誤っているテンプレート:Sfn）。

ゲーデルの完全性定理と不完全性定理は、革命的出来事ではなく時代の流れの産物だったテンプレート:Sfn。ゲーデル以外の誰かがこれらの定理を発見するのは時間の問題だったとされており、ゲーデル自身もそう見ていたテンプレート:Sfn。

数学上の「無矛盾性」と不完全性定理について、フランセーンは以下の通り解説しているテンプレート:Sfn。テンプレート:Quote

誤用例

フランセーンは『ゲーデルの定理：利用と誤用の不完全ガイド』において、ゲーデルの定理が広範に誤用されていることについて論じているテンプレート:Sfn。

一般社会・インターネット

数学者・数理論理学者の田中一之によれば、ゲーデルの名や定理は「知的会話」に頻出しているテンプレート:Sfn。フランセーンが述べたように、インターネットのどんなニュースグループでも、遅かれ早かれ誰かがゲーデルの定理を持ち出すテンプレート:Sfn。そういった一般的な引用における間違いを正すことが、フランセーンの著書の目的となっているテンプレート:Sfn。

1931年にゲーデルが示したのは、「特定の形式体系 $P$ において決定不能な命題の存在」であり、一般的な意味での「不完全性」についての定理ではないテンプレート:Sfn。

フランセーンによれば、ゲーデルの不完全性定理と結び付けられるテーマはロジック、数学、計算、哲学、物理学、進化論、政治、宗教、無神論、神学、文学、詩歌、写真、建築、音楽、ヒップホップ、デートなど多岐にわたるテンプレート:Sfn。形式論理学のような専門領域の外では、不完全性定理についての言及の多くが、哲学的であり「ひどい誤解や自由連想に基いている」ため、馬鹿げているとさえ言えるテンプレート:Sfn。たとえば、テンプレート:Quotation テンプレート:Quotation テンプレート:Quotation などが見られるテンプレート:Sfn。ゲーデルの理論の誤解は、一般的な人々の間でも起こっているテンプレート:Sfn。たとえばテンプレート:Quotation テンプレート:Quotation テンプレート:Quotation などであるテンプレート:Sfn。

数学以外の学問

田中によれば、ゲーデル自身が不完全性定理について明言しているのは、1963年8月28日の次の文言であるテンプレート:Sfn。テンプレート:Quote ゲーデルは慎重を重ねて言葉を選んでいるため、この表現を安易に変えようとすると、不具合を生じるテンプレート:Sfn。実際、この定理のいずれかの条件が落とされることで、多数の誤解が生じている（特に「有限的算術を含む」という条件が落とされていることが多い）テンプレート:Sfn。「ある程度の有限的算術を含む」という条件を、「十分大きな」「十分複雑な」「十分表現力のある」などといった曖昧な条件に置き換えることは誤りだが、一般向けの解説などには横行している（実際には、大きな理論で完全なものもあれば、小さな理論で不完全なものもある）テンプレート:Sfn。さらに見落とされやすい点は、不完全性定理の前提および結論部に「算術の条件」があることであるテンプレート:Sfn。

要するに不完全性定理は、「算術を含む体系がその算術部分で不完全である」という主張であり、その算術の外側が完全か不完全かについては、この定理は何も語っていないテンプレート:Sfn。

高名な物理学者でさえ、間違いを冒すことがあるテンプレート:Sfn。フリーマン・ダイソンとスティーヴン・ホーキングの論説は、万物理論の可能性を否定するのにゲーデルの定理を持ち出したテンプレート:Sfn。しかし仮に物理理論に不完全性定理が適用できたとしても、不完全性はその算術部分に見つかるだけで、その理論が完全か不完全かは別の問題であるテンプレート:Sfn。

哲学

ゲーデルは「合理的な神学」の可能性を信じてはいたが、特定の宗教組織に所属することはなく、不完全性定理から哲学的・神学的解釈を引き出そうと試みることもしなかったテンプレート:Sfn。しかし一方で哲学や神学は、ゲーデルや不完全性定理を自分たちへ結びつけようとしてきたテンプレート:Sfn。

アラン・ソーカルとジャン・ブリクモンは、脱近代主義（ポストモダニズム）に対する論評『「知」の欺瞞』の中で、「ゲーデルの定理こそ汲めども尽きぬ知的濫用の泉である」と述べ、レジス・ドブレ、ミシェル・セールらの文章を批判しているテンプレート:Sfn テンプレート:Sfn。また、哲学者によるゲーデル関係の本が、フランセーンの本と同じ頃に書店販売されていたが、哲学者の本は専門誌によって酷評されたテンプレート:Sfn。その本は全体として読みやすく一般読者からの評判は高かったが、ゲーデルの証明の核（不動点定理）について、根本的な勘違いをしたまま説明していたテンプレート:Sfn。同様の間違いは他の入門書などにもあり、田中はテンプレート:Quote と述べているテンプレート:Sfn。哲学者または宗教家が、テンプレート:Quotation といった考えを表明することは珍しくないテンプレート:Sfn。しかし、不完全性定理とは「算術の公理系PAや公理的集合論 ZFCのような形式体系を扱う数学の定理」であり、哲学や宗教はこの点を踏まえていないテンプレート:Sfn。要するに不完全性定理とは、数学内の「形式体系」（フォーマルシステム）についての定理であるテンプレート:Sfn。確かに、思想・哲学・神学・信仰・聖書・法律・裁判等を「形式」や「体系」や「形式体系」と呼ぶ人も存在するが、それらは数学内の一分野「形式体系」ではないテンプレート:Sfn。数学内の「形式体系」を研究し応用できる範囲は、数学や計算機（コンピュータ）であるテンプレート:Sfn。

嘘つきのパラドックス（「ウソつきの逆理」）には、「この文は偽である」といった代表的表明があるが、このパラドックスも、不完全性定理が誤用されている一例として挙げられているテンプレート:Sfn。定理を非数学的に「応用」した文章や嘘つき文は、以下のような長い（あるいは果てしない）議論を呼び起こしているテンプレート:Sfn。テンプレート:Quotation テンプレート:Quotation テンプレート:Quotation このような誤用や議論は、人々の心に謎や「愉快な混乱」を発生させているかもしれないし、「哲学的に重要性をもっている」かもしれないが、不完全性定理とは関係が無いテンプレート:Sfn。そもそも数学上では、「真偽」や「証明」といった用語が既に明確に定義されており、不完全性定理もそれらの数学用語に従っているテンプレート:Sfn。

宗教

フランセーンによれば、次のような講釈さえ存在するテンプレート:Sfn。テンプレート:Quotation 実際には不完全性定理は、「形式体系の無矛盾性と完全性についての定理」であるテンプレート:Sfn。確かに「矛盾」「無矛盾」「完全」「不完全」「体系（システム）」という語は、専門用語でない言語とも結びつきがあるが、およそこのような結びつきは不完全性定理と関係が無いテンプレート:Sfn。

神学

神学にも不完全性定理は持ち込まれ濫用されており、たとえば『キリスト教と数学の書誌学』（1983年）があるテンプレート:Sfn。テンプレート:Quotation テンプレート:Quotation テンプレート:Quotation テンプレート:Quotation

ダニエル・グレーブスは次の通り「考察」をしている。テンプレート:Sfn テンプレート:Quotation

ナジャムディン・モハメッドも、神学的に「応用」しているテンプレート:Sfn。テンプレート:Quotation

これらの考察と、「ポストモダン的状況」（脱近代的状況）という考え方には類似性があるテンプレート:Sfn。そうした理屈では、不完全性は無数の様々な無矛盾理論を導き、どこで「真理」が手に入るかは誰も知らない（したがって、理性だけで正しい道を歩むことはできず、信仰が進むべき道となるテンプレート:Sfn）。

しかし実際の数学では、そのような枝分かれは無く、「決定不能性の海」の中でもがくようなことも無いため、そのような「混乱」は神学的幻想に過ぎないとされているテンプレート:Sfn。

誤用の分類

田中はゲーデルの定理の様々な誤用を分類しているテンプレート:Sfn。その一つは、人間の悟性が陥りやすい間違った傾向であるテンプレート:Sfn。たとえば、自分が思いつく有意義そうな体系がどれも不完全であるので、「有意義な体系はすべて不完全である」と思い込み、さらにその原因を定理か何かに帰着させようとする傾向であるテンプレート:Sfn。

別の誤用は、言語の誤用であるテンプレート:Sfn。不完全性定理に含まれる「矛盾」「完全」「体系（システム）」などの語は、日常では多様に使われているテンプレート:Sfn。そこを混同すれば、ゲーデルの定理までが非形式的（インフォーマル）な意味と結び付けられるテンプレート:Sfn。

脚注

注釈

テンプレート:Notelist2

出典

テンプレート:Reflist

参照文献

外部リンク

テンプレート:Metalogic テンプレート:Normdaten

↑ テンプレート:Cite web

[1] テンプレート:Cite web

[1]

ゲーデルの不完全性定理

概要

証明の概要

準備

第一不完全性定理の証明の概要

第二不完全性定理の証明の概要

詳細

ゲーデル文の構成

第一不完全性定理の証明

否定命題の証明不能性

肯定命題の証明不能性

第二不完全性定理の証明

決定不能命題の例

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

不完全性定理が適用されない体系

不完全性定理によるヒルベルト・プログラムの発展

ゲーデル以後の展開

不完全性定理の代数化

数学と哲学の分離

誤解（哲学等による誤解・誤用）

誤用例

一般社会・インターネット

数学以外の学問

哲学

宗教

神学

誤用の分類

脚注

注釈

出典

参照文献

数学書・数理論理学書

数学辞典

科学書・学術書

Webサイト

関連文献

原論文

原論文の日本語訳

原論文の英訳

教科書

講義ノート

関連項目

外部リンク

ナビゲーション メニュー

検索

ナビゲーションメニュー