「ゲーデルの不完全性定理」の版間の差分

2016年9月20日 (火) 19:29時点における版

2025年4月27日 (日) 06:47時点における最新版

(82人の利用者による、間の159版が非表示)

1行目:

'''ゲーデルの不完全性定理'''（ゲーデルのふかんぜんせいていり、{{Lang-en-short|Gödel's incompleteness theorems}}、{{Lang-de-short|Gödelscher Unvollständigkeitssatz}}）または'''不完全性定理'''とは、[[数学基礎論]]{{sfn|青本|上野|加藤|神保|2005|p=510}}と[[コンピュータ科学]]（計算機科学）の重要な基本[[定理]]{{Sfn|菊池|2014|p=iii}}。（数学基礎論は[[数理論理学]]や[[超数学]]とほぼ同義な分野で、コンピュータ科学と密接に関連している{{sfn|青本|上野|加藤|神保|2005|p=294}}。）　不完全性定理は厳密には「[[数学]]」そのものについての定理ではなく、「[[形式体系|形式化された数学]]」についての定理である{{Sfn|菊池|2014|p=9}}{{Efn2|原文：{{行内引用|数学の基礎をめぐる論争の実質的な勝者が[[形式主義_(数学)|形式主義]]である … ．不完全性定理は数学そのものについての定理ではなく，「形式化された数学」に関する定理であり，形式主義的な数学観についての定理である．}}{{Sfn|菊池|2014|p=9}}}}。[[クルト・ゲーデル]]が1931年の論文で[[証明 (数学)#証明の形式的定義|証明]]した定理であり{{sfn|日本数学会（編）|2011|p=357}}、{{仮リンク|有限の立場|en|finitism}}（[[形式主義_(数学)|形式主義]]）<!--「有限の立場（形式主義）」は『岩波　数学入門辞典』の原文ママ-->では[[自然数論]]の[[無矛盾性]]の証明が成立しないことを示す{{sfn|青本|上野|加藤|神保|2005|p=294}}{{sfn|日本数学会（編）|2011|p=357}}。なお、少し拡張された有限の立場では、自然数論の無矛盾性の証明が成立する（{{仮リンク|ゲンツェンの無矛盾性証明|en|Gentzen's consistency proof|preserve=1}}）{{sfn|青本|上野|加藤|神保|2005|p=294}}{{Efn2|原文：{{行内引用|ゲーデルの不完全性定理は有限の立場（形式主義）で数学の無矛盾性を証明することはできないことを示した．ゲンツェン（Gentzen）は，有限の立場より緩い制限のもとで自然数論の無矛盾性を証明した．}}{{sfn|青本|上野|加藤|神保|2005|p=294}}}}。

'''ゲーデルの不完全性定理'''（ゲーデルのふかんぜんせいていり、{{Lang-de-short|''Gödelscher Unvollständigkeitssatz''}}）又は単に'''不完全性定理'''とは、[[数学基礎論]]における重要な[[定理]]で、[[クルト・ゲーデル]]が[[1930年]]に証明したものである。

数学基礎論研究者の菊池誠によると不完全性定理は、20世紀初め以降に[[哲学]]から決別した数学基礎論の中で現れた{{Sfn|菊池|2014|pp=ii-iii}}{{Efn2|{{詳細記事|[[ゲーデルの不完全性定理#数学と哲学の分離]]}}}}。コンピュータ科学者・[[数理論理学者]]の[[:en:Torkel_Franzén|トルケル・フランセーン]]{{sfn|フランセーン|2011|p=奥付け}}および[[数学者]]・数理論理学者の[[田中一之]]{{sfn|フランセーン|2011|p=奥付け}}によると、不完全性定理が示した不完全性とは、数学用語の意味での「特定の[[形式体系]]Pにおいて決定不能な[[命題]]の存在」であり、一般的な意味での「不完全性」とは無関係である{{sfn|フランセーン|2011|p=230}}。不完全性定理を踏まえても、数学の形式体系の[[公理]]は真であり[[無矛盾]]であるし{{sfn|フランセーン|2011|p=145}}{{Efn2|{{詳細記事|[[ゲーデルの不完全性定理#誤解（哲学等による誤解・誤用）|フランセーン 2011, p. 145.『これらの体系の公理が真であり、そして無矛盾であるという絶対確実な知識をもっていると主張しても、ゲーデルの定理のどこにも相反しないのである』]]}}}}、数学の[[完全性]]も成立し続けている{{sfn|フランセーン|2011|p=230}}。しかし“不完全性定理は数学や理論の「不完全性」を証明した”といった誤解や、“数学には「不完全」な部分があると証明済みであり、数学以外の分野に「不完全」な部分があってもおかしくない”といった誤解が一般[[社会]]・[[哲学]]・[[宗教]]・[[神学]]等によって広まり、誤用されている{{sfn|フランセーン|2011|p=4, 7, 126-127}}{{Efn2|{{詳細記事|ゲーデルの不完全性定理#誤用例}}}}。{{See also|[[#不完全性定理が適用されない体系|不完全性定理が適用されない体系]]|ゲーデルの完全性定理}}

; 第1不完全性定理 : 自然数論を含む[[帰納的集合|帰納的]]公理化可能な理論が、[[ω無矛盾]]であれば、[[証明#証明の形式的定義|証明]]も反証もできない[[論理式#閉論理式|命題]]が存在する。

数学の「[[無矛盾性]]」を証明することを目指した[[ヒルベルト・プログラム]]に関して「不完全性定理がヒルベルトのプログラムを破壊した」という類の哲学的発言はよくあるが、これは実際の不完全性定理やゲーデルの見解とは異なる、とフランセーン達は解説している{{sfn|フランセーン|2011|p=54}}。正確には、ゲーデルはヒルベルトと同様の見解を持っており、彼が不完全性定理を証明して示したのは、ヒルベルトの目的（「無矛盾性証明」）を実現するためには手段（ヒルベルト・プログラム）を拡張する必要がある、ということだった{{sfn|フランセーン|2011|p=54}}。これについて[[日本数学会]]編集の『[[岩波数学辞典]]』では「彼{{Interp|ゲーデル|原文では「ゲーデルも書いているように…彼の結果はヒルベルトの企図を…」|和文=1}}の結果はヒルベルトの企図を直接否定するものではなく，実際この定理の発見後に無矛盾性証明のための様々な[[方法論]]が開発されている」と記されている{{sfn|日本数学会（編）|2011|p=357}}。

; 第2不完全性定理 : 自然数論を含む帰納的公理化可能な理論が、無矛盾であれば、自身の無矛盾性を証明できない。

{{See also|{{仮リンク|ゲンツェンの無矛盾性証明|en|Gentzen's consistency proof|preserve=1}}|[[ゲーデルの不完全性定理#不完全性定理によるヒルベルト・プログラムの発展|不完全性定理によるヒルベルト・プログラムの発展]]}}

== 概要 ==

ゲーデルの不完全性定理は、ゲーデルが1931年の論文で証明した次の内容である{{sfn|日本数学会（編）|2011|p=357}}。

ゲーデルの定理でいう証明不能命題Gは、「'''Gは証明できない'''」という命題と同値である。Gは'''ゲーデル文'''と呼ばれる。

* 『[[数学原理]]（プリンキピア・マセマティカ）』の体系や[[公理的集合論]]の中には、「証明も反証もできない「[[自然数論]]の[[命題]]」」が存在する。

* また、これらの体系に公理を追加しても公理が有限個であれば、前述の命題の存在を解消できない。

より正確には、不完全性定理とは次の2つの定理（それぞれ第一/第二不完全性定理と呼ばれる）の総称である{{sfn|日本数学会（編）|2011|p=357}}。

Gが証明可能であれば、&Sigma;₁完全性により[[命題]]「Gは証明できる」もまた[[証明]]可能である。一方Gは命題「Gは証明できない」と[[同値]]であることが証明可能であるので、両者から[[矛盾]]が導かれる。

{{math theorem|第一不完全性定理|"初等的な自然数論"を含む[[ω無矛盾]]な公理的理論<math>T</math>は不完全である。つまり<math>T</math>内で[[証明 (数学)#証明の形式的定義|証明]]も反証もされない[[論理式 (数学)#閉論理式|命題]]（[[決定可能性#理論の決定可能性|決定不能命題]](undecidable proposition)、あるいは[[ZFCから独立な命題の一覧|独立命題]]）が存在する。}}

つまり

*「Gが証明できる」ならば「矛盾が証明できる」　... (A)

したがって、[[対偶 (論理学)|対偶]]を取れば

*「矛盾が証明できない」ならば「Gが証明できない」 ... (B)

となる。

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

{{math theorem|第二不完全性定理|"初等的な自然数論"を含む理論<math>T</math>が[[無矛盾]]ならば，<math>T</math>の無矛盾性を表す命題 Con(<math>T</math>) がその体系で証明できない。}}

なお、証明可能性の代わりに真理性を用いるならば、[[パラドックス]]が導かれる。このことから、自然数論における真理性は自然数論の中では表現できないことが示される（[[タルスキの定理]]）。

なお「有限の立場」とは、[[数学の形式主義]]における「[[数学記号|記号]]の有限的な操作のみから構成される」立場を指す{{Sfn|菊池|2014|p=5}}。

'''注意'''

ゲーデル文を構成するためには自然数論の式を自然数に変換する'''ゲーデル数'''および[[自己言及]]で用いられる対角化の技法（を形式化したもの）が必要である。後者は[[対角化補題]]と呼ばれる。

* 形式的体系 S と S' に対して（言語を適当に拡張した）S' が S を含むとは、S の論理式全体の集合Fml(S)から S' の論理式全体の集合Fml(S')への次のような写像T:Fml(S)→Fml(S')が存在するときを言う：φ∈Fml(S)がS で証明できるときT(φ)は S' で証明できる。このTはしばしば「翻訳」と呼ばれる。この意味でペアノ算術PAは[[ツェルメロ＝フレンケル集合論]]ZFCに含まれる{{Sfn|菊池|2014|p=248}}。

* 「初等的な自然数論」について、ゲーデル自身は[[ペアノの公理]]と[[原始再帰関数|原始帰納法]]による関数の定義を前提に自然数論の体系を構築した {{Harv|Gödel|1931}}。この体系は、[[加法]]・[[乗法]]・[[冪乗|べき乗]]・[[階乗]]・[[順序集合|順序関係]]などを帰納的に定義する十分な表現力を持っている。それぞれの定理の前提条件は、[[ロビンソン算術]]を含む[[帰納的可算集合|半決定可能]]な理論（第一）、<math display="inline">\mathbf{I}\Sigma_1</math>を含む半決定可能な理論（第二）に置き換えても証明することができる<ref>{{Cite web|和書|url=https://www.kurims.kyoto-u.ac.jp/~terui/kistec2018b.pdf |title=数理論理学 II (不完全性定理) |access-date=2023-04-06 |author=照井一成 |year=2018 |format=PDF}}</ref>。

=== 証明の概要 ===

自然数を変数とする述語「xは…である」の'''対角化'''は、左記の述語のxに「xは…である」のゲーデル数を代入した命題である。その意味は「「xは…である」は…である」となる。

==== 準備 ====

ゲーデル文Gは「「xで表される述語の対角化は証明できない」で表される述語の[[対角化]]は証明できない」と表される。「xで表される述語の対角化は証明できない」の対角化は、G自身と同値になる。

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

自然数を変数とする述語「{{mvar|x}}は…である」の'''対角化'''は、上記の述語の{{mvar|x}}に「{{mvar|x}}は…である」自身のゲーデル数を代入した命題である。その意味は

:「「{{mvar|x}}は…である」は…である」

となる。ゲーデル文{{mvar|G}}は

:「「{{mvar|x}}で表される述語の対角化は証明できない」で表される述語の[[対角化]]は証明できない」

と表される。「{{mvar|x}}で表される述語の対角化は証明できない」の対角化は、{{mvar|G}}自身と同値になる。

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

さて、ゲーデル文{{mvar|G}}が証明可能であれば、&Sigma;₁完全性により[[命題]]「{{mvar|G}}は証明できる」もまた[[証明 (数学)|証明]]可能である。一方{{mvar|G}}は命題「{{mvar|G}}は証明できない」と[[同値]]であることが証明可能であるので、両者から[[矛盾]]が導かれる。つまり

:「{{mvar|G}}は証明できる」ならば「矛盾が証明できる」 &hellip; (A)

したがって、[[対偶 (論理学)|対偶]]を取れば

:「矛盾が証明できない」ならば「{{mvar|G}}は証明できない」 &hellip; (B)

となる。

また、{{math|￢''G''}}が証明可能であれば、{{mvar|G}}の性質から命題「{{mvar|G}}は証明できる」も証明可能である。この際、もし{{mvar|G}}そのものが証明不能だとすると、ω矛盾ということになる。ω無矛盾であれば{{mvar|G}}も証明可能である。しかし{{mvar|G}}が証明可能であれば「{{mvar|G}}は証明できない」も証明可能であるので、やはり両者から矛盾が導かれる。したがってω無矛盾であれば{{math|￢''G''}}も証明できないのである。よってω無矛盾であれば、{{mvar|G}}も{{math|￢''G''}}も証明できない（第一不完全性定理）。

さて、自然数論の無矛盾性とは、「自然数論において矛盾が証明できない」ということである。そして、自然数論による自然数論の無矛盾性証明とは、「」内が、自然数論で証明できるということである。

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

「自然数論で矛盾が証明できない」と自然数論で証明できれば、第一不完全定理での議論中の(B)より「Gが証明できない」と証明できる。

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

しかし、「Gが証明できない」とはGと同値であるから、Gも証明されることとなり、そこから第一不完全定理での議論中の（A)により、矛盾が証明される。

自然数論の無矛盾性を

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

と表す。このとき、自然数論による自然数論の無矛盾性証明とは、(C)が自然数論で証明できるということである。

(C)が自然数論で証明できれば、第一不完全定理での議論中の(B)より

:「{{mvar|G}}は証明できない」

と証明できる。しかし、

:「{{mvar|G}}は証明できない」

とは{{mvar|G}}と同値であるから、{{mvar|G}}も証明されることとなり、そこから第一不完全性定理での議論中の(A)により、矛盾が証明される。

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

== 詳細 ==

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

=== ゲーデル文の構成 ===

概要でも説明したように、'''[[ゲーデル数]]'''というテクニックを使って間接的に[[自己言及]]を可能とし、ゲーデル文を構成する。コンピュータでは全てのデータを一意な数値で表しており、特に[[文字列]]や[[論理式 (数学)|論理式]]そして論理式の列も数値で表す。このように、論理式を数値で表す行為を論理式の'''ゲーデル数化'''といい、命題<math>P</math>に対応する数値を<math>P</math>の'''ゲーデル数'''という{{efn2|歴史的には論理式のゲーデル数化の概念が先に生まれ、後にコンピュータがデータを数値で表すようになった。なお、ゲーデル自身は、素因数分解の一意性を利用して論理式のゲーデル数化を実現している。}}。

コンピュータでは全てのデータを一意な数値で表しており、特に[[文字列]]や[[論理式]]そして論理式の列も数値で表す。このように、論理式を数値で表す行為を論理式の'''ゲーデル数化'''といい、命題Pに対応する数値をPの'''ゲーデル数'''という<ref>歴史的には論理式のゲーデル数化の概念が先に生まれ、後にコンピュータがデータを数値で表すようになった。なお、ゲーデル自身は、素因数分解の一意性を利用して論理式のゲーデル数化を実現している。</ref>。

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

* <math>Axiom(x)</math>： <math>x</math>は公理のゲーデル数である。

* <math>MP(x,y,z)</math>： <math>x</math>をゲーデル数に持つ論理式と<math>y</math>をゲーデル数に持つ論理式から三段論法[[モーダスポネンス]]により<math>z</math>をゲーデル数に持つ論理式が導ける。

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

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

* <math>Proof(y,z)</math> : <math>z</math>をゲーデル数に持つ論理式を<math>P</math>とするとき、<math>y</math>をゲーデル数に持つ論理式の列が論理式<math>P</math>の証明になっている。

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

さらに<math>Proof</math>を「∃<math>\exists</math>」と組み合わせることで、

* <math>Provable(z)</math> : 「∃y<math>\exists y : Proof(y,z)</math>」である。すなわち、<math>z</math>をゲーデル数に持つ論理式を<math>P</math>とするとき論理式Pは証明可能である。

* <math>ProvableARG(z,x)</math> : 「∃y<math>\exists y : Proof(y,z,x)</math>」である。すなわち、<math>z</math>をゲーデル数に持つ論理式を<math>Q</math>とするとき、<math>Q</math>中の変数に自然数<math>x</math>を代入した論理式<math>Q(x)</math>は証明可能である。

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

論理式￢ProvableARG<math>\lnot ProvableARG(x,x)</math>のゲーデル数を<math>m</math>とすると、<math>x</math>に<math>m</math>を代入した論理式￢ProvableARG<math>\lnot ProvableARG(m,m)</math>がゲーデル文となる（対角化）。

=== 第一不完全性定理の証明 ===

ゲーデル文￢ProvableARG<math>\lnot ProvableARG(m,m)</math>のゲーデル数を<math>npmm</math>とする。

*==== ￢ProvableARG(m,m)否定命題の証明不能性 ====

否定命題<math>\lnot ProvableARG(m,m)</math>が証明可能とすると、<math>Provable(npmm)</math>は真である。このとき<math>\Sigma_1</math>完全性より<math>Provable(npmm)</math>は証明可能である。

一方<math>\lnot ProvableARG(m,m)</math>は

￢ProvableARG(m,m)が証明可能とすると、Provable(npmm)は真である。このとき&Sigma;₁完全性よりProvable(npmm)は証明可能である。

:「<math>m</math>をゲーデル数に持つ論理式に<math>m</math>を代入したものは証明不能」

という意味である。

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

:<math>\lnot ProvableARG(m,m) \Leftrightarrow \lnot Provable(npmm)</math>

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

:<math>\lnot Provable(npmm)</math>

は証明可能である。

したがって<math>Provable(npmm)</math>および<math>\lnot Provable(npmm)</math>が証明され、これは矛盾である{{efn2|実際、<math>\lnot ProvableARG(m,m)</math>が証明可能なら<math>\not ProvableARG(m,m)</math>の証明系列<math>P_1,\ldots,P_{n_0}</math>が存在するので、論理式の列<math>P_1,\ldots,P_{n_0}</math>のゲーデル数を<math>a</math>とすると、「Proof<math>(a,m,m)</math>」が証明可能、したがって特に「<math>\exists y : Proof(y,m,m)</math>」<nowiki>=</nowiki>「<math>ProvableARG(m,m)</math>」が証明可能。一方我々は「<math>\lnot ProvableARG(x,x)</math>」が証明可能な事を仮定していたので、これは矛盾である。}}が、これは自然数論が無矛盾であるという仮定に反する。

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

==== 肯定命題の証明不能性 ====

￢ProvableARG(m,m)⇔￢Provable(npmm)

肯定命題<math>ProvableARG(m,m)</math>が証明可能だとすると、

:<math>ProvableARG(m,m) \Leftrightarrow Provable(npmm)</math>

により

:<math>Provable(npmm)</math>

が証明可能である。

このとき[[ω無矛盾性]]を前提すると、<math>npmm</math>をゲーデル数とする論理式<math>\lnot ProvableARG(m,m)</math>が証明可能である。{{efn2|ω無矛盾とは<math>\exists yP(y)</math>が証明できれば、<math>P(u)</math>を満たす自然数<math>u</math>が実際に存在することを指す。定義より「<math>ProvableARG(m,m)</math>」は「<math>\exists y : Proof(y,m,m)</math>」であった。ω無矛盾性より、「<math>Proof(u,m,m)</math>」を満たす自然数<math>u</math>が実際に存在し、<math>u</math>をゲーデル数に持つ論理式の列が<math>\not ProvableARG(m,m)</math>の証明系列になる。}}

が証明可能である。したがって、￢Provable(npmm)は証明可能である。

したがってProvable(npmm)および￢Provable(npmm)が証明され、これは矛盾である<ref>実際、￢ProvableARG(m,m)が証明可能なら￢ProvableARG(m,m)の証明系列<math>P_1,\ldots,P_{n_0}</math>が存在するので、論理式の列<math>P_1,\ldots,P_{n_0}</math>のゲーデル数を<math>a</math>とすると、「Proof<math>(a,m,m)</math>」が証明可能、したがって特に「∃y : Proof(y,m,m)」=「ProvableARG(m,m)」が証明可能。一方我々は「￢ProvableARG(x,x)」が証明可能な事を仮定していたので、これは矛盾である。</ref>が、これは自然数論が無矛盾であるという仮定に反する。

* ProvableARG(m,m)の証明不能性

ProvableARG(m,m)が証明可能だとすると、

ProvableARG(m,m)⇔Provable(npmm)

によりProvable(npmm)が証明可能である。

このとき[[ω無矛盾性]]を前提すると、npmmをゲーデル数とする論理式￢ProvableARG(m,m)が証明可能である。<ref>ω無矛盾とは∃yP(y)が証明できれば、P(u)を満たす自然数uが実際に存在することを指す。定義より「ProvableARG(m,m)」は「∃y : Proof(y,m,m)」であった。ω無矛盾性より、「Proof(<math>u,m,m</math>)」を満たす自然数<math>u</math>が実際に存在し、<math>u</math>をゲーデル数に持つ論理式の列が￢ProvableARG(m,m)の証明系列になる。</ref>

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

=== 第二不完全性定理の証明 ===

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

* :自然数論の体系内で「￢Provable<math>\lnot Provable(b)</math>」を証明できる

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

まず

:<math>\lnot Provable(b)</math>

* ￢Provable(b)

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

第一不完全性定理のところで示したように、￢ProvableARG<math>\lnot ProvableARG(m,m)</math>が証明できれば矛盾が証明できる。この議論を自然数論の体系内で行うことで、

* :<math>Provable(npmm) ⇒\Rightarrow Provable(b) </math>

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

:<math>\lnot Provable(b) \Rightarrow \lnot Provable(npmm)</math>

* ￢Provable(b) ⇒ ￢Provable(npmm)

が自然数論の体系内で証明可能なことがわかる。したがって、仮定および￢ProvableARG<math>\lnot ProvableARG(m,m)⇔￢Provable \Leftrightarrow \lnot Provable(npmm)</math>から

:<math>\lnot ProvableARG(m,m)</math>

* ￢ProvableARG(m,m)

が自然数論の体系内で証明可能なことがわかる。第一不完全性定理の所で示したように、￢ProvableARG<math>\lnot ProvableARG(m,m)</math>が証明可能だと、矛盾が証明される。したがって矛盾が証明されないならば、￢Provable<math>\lnot Provable(b)</math>は証明されない。

== 決定不能命題の例 ==

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

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

このように決定不能という言葉には二つの意味があるので、代わりに{{仮リンク|独立 (数理論理学)|label=独立|en|Independence (mathematical logic)}}という用語をもって「証明も否定の証明もできない」という意味にあてる場合がある。ところが「独立」という用語にしても依然曖昧な部分がある。単に「証明できない」という意味を表し、「否定の証明もできない」かどうかについてはあえて含意していない場合があるからである。

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

以下、本節では一つ目の意味で「決定不能」と書く。特定の形式的体系の下である命題が決定不能であることは、その命題の[[真理値]]が[[well-defined]]であるかどうかや他の手段で決定可能かどうかについては明らかにしない。決定不能ということが意味するのは、あくまで使用されている特定の形式的体系の下ではその命題の真偽をいずれも証明できないということにすぎない。真理値を決して知ることができないか、または真理値の定義自体が無効となるような、いわゆる「絶対的決定不能」命題が存在するのかどうかは[[数学の哲学|数理哲学]]における論争の的となっている。

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

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

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

1973年、[[群 (数学)|群論]]における{{仮リンク|ホワイトヘッドの問題|en|Whitehead problem}}が標準的な集合論では決定不能であることが示された。

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

計算機科学で応用される {{仮リンク|Kruskal の木定理|en|Kruskal's tree theorem}}はペアノ算術では決定不能だが集合論では証明できる。実際、Kruskalの木定理（またはその有限版）は、{{仮リンク|可述主義|en|predicativism}}<ref>{{efn2|訳注：自己言及的でないこと。</ref>}}と呼ばれる数学的哲学に基づいて構築されたもっと強い体系の下でも決定不能である。これに関連し、更に一般的な {{仮リンク|graph minors 定理|en|graph minor theorem}}（2003年）は[[計算複雑性理論]]に影響する。

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

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

{{複数の問題|出典の明記=2023年3月|独自研究=2023年3月|section=1}}

第1不完全性定理は[[ロビンソン算術]]を含んでいれば十分である。またω無矛盾性の仮定は単なる無矛盾性の仮定に弱められる（後述）。第2不完全性定理はロビンソン算術に[[算術的階層|&Sigma;₁]]論理式に対する[[数学的帰納法]]の[[公理型|公理図式]]を追加した体系（I&Sigma;₁）を含んでいれば十分である。[[ペアノ算術]]はこれを含むから、ペアノ算術を含む理論は第2不完全性定理の適用範囲である。

第1不完全性定理は[[ロビンソン算術]]を含んでいれば十分である。またω無矛盾性の仮定は単なる無矛盾性の仮定に弱められる（後述）。第2不完全性定理はロビンソン算術に[[算術的階層|&Sigma;₁]]論理式に対する[[数学的帰納法]]の[[公理図式]]を追加した体系（<math>I\Sigma_1</math>）を含んでいれば十分である。[[ペアノ算術]]はこれを含むから、ペアノ算術を含む理論は第2不完全性定理の適用範囲である。

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

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

ゲーデルの定理は実効的に生成された（即ち[[帰納的可算集合|帰納的可算]]な）理論についてのみ適用できる。自然数に関する真である文を全て公理とするような理論を考えれば、この理論は無矛盾かつ完全であり、かつペアノ算術を含んでいる。これはゲーデルの定理と矛盾しない。何故ならこの理論は帰納的可算ではないからである<ref>{{efn2|訳注：この場合の「帰納的可算」とは、すべての定理のゲーデル数を枚挙する計算可能関数が存在する（実効的に枚挙可能）ことを意味する。[[クレイグのトリック]]によれば、このことは定理集合が帰納的な公理系から生成される（演繹閉包である）ことと同値である。</ref>}}。

第二不完全性定理が示すのは、ある公理系の無矛盾性はその公理系自身では証明できないということであって、他の無矛盾な公理系からも証明できないとは言っていない。例えば、[[ペアノ算術]]の無矛盾性は[[公理的集合論#ZFC選択公理|ZFC]]から証明できるし、算術の理論に[[エプシロン・ノート|&epsilon;₀]]までの[[数学的帰納法#超限帰納法|超限帰納法]]を加えて得られた{{仮リンク|ゲンツェンによる無矛盾性の証明|en|Gentzen's consistency proof}}もある。

== 不完全性定理の成立しが適用されない体系 ==

不完全性定理が適用されない例としては[[ユークリッド幾何学]]{{sfn|青本|上野|加藤|神保|2005|p=116}}、[[プレスバーガー算術]]{{sfn|日本数学会（編）|2011|p=355}}、[[実閉体]]と代数的[[閉体]]の理論における[[タルスキの定理]]などがある{{sfn|日本数学会（編）|2011|p=355}}。

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

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

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

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

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

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

== その影響・応用 ==

{{MainSee also|無矛盾性|ヒルベルト・プログラム|数学基礎論|ゲーデル}}

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

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

実際ゲーデル自身は以下のような、「ノン・イグノラビムス」的なヒルベルト流の見解を持っていた{{sfn|フランセーン|2011|p=47}}。

上記のような述語論理式を自然数論の体系内に構成し、証明を形式的に進めるために、ゲーデルは[[ゲーデル数]]化という操作を導入した。自由変数、論理式、証明図などを自然数でコード化し[[証明可能]]、[[反証可能]]などの概念を数論的関数として表現する。このように、論理式や証明を数学的に表現して数学内に埋め込む上記の手法は、数学そのものを分析する「メタ数学」を、分析すべきの数学の中に写像する技法の先駆けであり、その後[[数学基礎論]]や[[理論計算機科学]]でよく用いられるようになる。

{{Quote|

「あらゆる算術の問題をその中で解決する単一の形式体系を定めることは不可能であっても、<br>

新しい公理や[[推論規則]]による数学の拡張が限りなく続いていくなかで、どんな算術の問題もいずれどこかで決定されるという可能性は排除されていない。」{{sfn|フランセーン|2011|p=47}}

}}

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

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

[[日本数学会]]が編集した『岩波　数学辞典』第4版では、不完全性定理について次の通り記述されている{{sfn|日本数学会（編）|2011|p=357}}。

{{Quote|

「ゲーデルも書いているように，[[:en:finitism|有限の立場]]は特定の[[演繹]]体系として規定されるものではないから，彼の結果はヒルベルトの企図を直接否定するものではなく，実際この定理の発見後に無矛盾性証明のための様々な方法論が開発されている．」{{sfn|日本数学会（編）|2011|p=357}}

}}

{{See also|[[:en:Gentzen's consistency proof|ゲンツェンの無矛盾性証明]]}}

述語論理式を自然数論の体系内に構成し、証明を形式的に進めるために、ゲーデルは[[ゲーデル数]]化という操作を導入した。自由変数、論理式、証明図などを自然数でコード化し[[証明可能]]、[[反証可能]]などの概念を数論的関数として表現する。このように、論理式や証明を数学的に表現して数学内に埋め込む上記の手法は、数学そのものを分析する「[[超数学]]（メタ数学）」を、分析すべき数学の中に写像する技法の先駆けであり、その後[[数学基礎論]]や[[理論計算機科学]]でよく用いられるようになる。

== ゲーデル以後の展開 ==

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

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

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

== 不完全性定理の代数化 ==

不完全性定理は他の論理構造と同じく[[抽象代数]]による簡易な表現が可能である。{{仮リンク|リンデンバウム代数|en|Lindenbaum algebra}}を次のように定義する。

* 理論 <math>T</math> のリンデンバウム代数 T<supmath>LT_L</supmath> は，[[文]]に[[順序構造]]を入れたものである。

* 順序は、もし理論 <math>T</math> で <math>A →\Rightarrow B</math> を証明できるならば <math>A ≧\ge B</math> と定義される。

* <math>A</math> と <math>B</math> の順序が等しいなら、<math>A</math> と <math>B</math> を同一視する。

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

* <math>( Q )</math> を含む再帰的可算素イデアル <math>p ⊂\subset B</math> は存在しない。

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

== 数学と哲学の分離 ==

[[理学博士]]・[[数学基礎論]]研究者である菊池誠{{Sfn|菊池|2014|p=奥付け}}の『不完全性定理』によれば、数学史上で「数学の正しさと[[無矛盾性]]に対する確信が揺らいだことがかつて一度だけあった」{{Sfn|菊池|2014|p=i}}。[[19世紀]]末～[[20世紀]]初めには、数学の中でいくつも[[パラドックス#数学における概要|逆理]]が発見され、数学の基礎についての「不安の時代」が発生した{{Sfn|菊池|2014|pp=i-ii}}。そうして数学の無矛盾性や「そもそも[[定理]]や[[証明 (数学)|証明]]とは何なのか」といった[[哲学]]的な問いに対し、[[伝統]]的な哲学の手法ではなく数学の手法（[[形式主義 (数学)|形式主義]]）で答える試みがなされ、そこから数学の一分野「数学基礎論」が生まれた{{Sfn|菊池|2014|p=ii}}{{Efn2|

{{Quote|'''数学基礎論と不完全性定理'''<br>

… <br>

数学の正しさには一分の隙もなく，数学では矛盾する二つの結論が導かれることは決して無いと昔から信じられている． … そもそも「信じられている」という言葉を使うことは不適切であり，不謹慎でさえあるかも知れない．

この数学の正しさと無矛盾性に対する確信が揺らいだことがかつて一度だけあった． … 19世紀末から20世紀初めにかけて数学の中で次々と逆理が発見された．正しさは数学の絶対的な規範であり，たとえ一ヵ所にでも亀裂が入れば数学の世界全体は粉々に砕けてしまう．{{Sfn|菊池|2014|p=i}} … <br>

この数学の基礎に関する「不安の時代」には … 果たして数学は正しく無矛盾なのか，そもそも定理や証明とは何なのかといった哲学的な問題に対して，伝統的な哲学的手法によってではなく，数学的手法を用いて答えようとする形式主義の試みの中から数学基礎論と呼ばれる数学の一分野が生まれた．{{Sfn|菊池|2014|p=ii}}

}}

}}。

数学の世界全体の無矛盾性を「有限の立場」で証明して数学を危機から救おうとしたヒルベルト・プログラムが、実現不可能であることをゲーデルの不完全性定理が明らかにした{{Sfn|菊池|2014|p=ii}}。<!--ゲーデルの不完全性定理は、数学の世界全体の無矛盾性を「有限の立場」で証明することで数学を危機から救うヒルベルト・プログラムが実現可能であることを明らかにした{{Sfn|菊池|2014|p=ii}}。--><!--←出典（{{Sfn|菊池|2014|p=ii}}）の内容ではこのプログラムは実現「不可能」-->ヒルベルト・プログラムは破綻した一方で、公理的集合論が整備されて「無矛盾」と見なされたこと、「算術の世界の無矛盾性」が証明されたことなどによって「不安の時代」は終わり、数学基礎論が哲学から決別した{{Sfn|菊池|2014|p=iii}}<!--ヒルベルト・プログラムが破綻し、（公理的集合論の整備と、ゲンツェンによる算術の無矛盾性証明により）「不安の時代」が通りすぎた後、数学基礎論が哲学から決別した{{Sfn|菊池|2014|p=iii}}。--><!--←出典（{{Sfn|菊池|2014|p=iii}}）にゲンツェン Gentzen の名前は無い-->。数学基礎論上で不完全性定理は、哲学的なものとしてでなく、数学的な応用可能性として重視されるようになった{{Sfn|菊池|2014|p=iii}}。またこの定理は、[[電子技術]]を伴う[[コンピュータ科学]]（計算機科学）の重要な基本定理でもある{{Sfn|菊池|2014|p=iii}}{{Efn2|

{{Quote|'''宴のあと'''<br>

… <br>

数学の危機が真面目に論じられていた「不安の時代{{Interp|19世紀末～20世紀初頭|原文では「「不安の時代」は簡単に…」|和文=1}}」は意外に簡単に終わった．現在，数学の基礎を本気で心配している数学者はまずいない． … 「不安の時代」が通り過ぎた後，数学基礎論は哲学と袂を分かち，独自の数学的な問題意識や価値観を見出した．数学基礎論の専門家は「哲学的な動機のもとで数学基礎論を語る時代は終わった」と考えるようになり … 数字基礎論は普通の数学に生まれ変わった．

不完全性定理についても数学基礎論の専門家の間では，哲学的な意義よりも様々な[[応用数学|数学的応用]]可能性のほうが大切であると考えられるようになった．<br>

電子技術の爆発的な発展と共に成長した[[理論計算機科学|計算機の基礎理論]]においても不完全性定理は重要な基本定理の一つであるが，そこでも不完全性定理は定理の主張そのものよりも，定理の証明の中で提案され用いられた様々な考え万や，不完全性定理から導かれる事実のほうが遥かに重要であると考えられているであろう．{{Sfn|菊池|2014|p=iii}}

}}

}}。

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

{{Quote|

'''数学と哲学'''

20世紀初頭の数学の基礎に関する「不安の時代」には，数学者と哲学者は共に数学の基礎について論じていた．<br>

それが今では数学者と哲学者は極めて疎遠である．数学者，特に数学基礎論の専門家は哲学者による数学の基礎についての議論を最近の数学を無視した色褪せた100年前の論争の焼き直しに過ぎないと感じ，哲学者は最近の数学としての数学基礎論の進展を重箱の隅をつつくような[[技術]]的で瑣末な話題だと考えている．{{Sfn|菊池|2014|p=11}} …

数学基礎論が哲学との繋がりを失ったことを知らない数学者は今でも数学基礎論のことを「哲学のようなもの」と考えている． … この，数学基礎論が「哲学のようなもの」であるという考えは，「哲学のような深い立派なもの」ではなく，「哲学のようなツマラナイコト」という意味であるため，このような考えを「他愛ない無邪気なもの」とは見過ごせない数学基礎論の専門家は，数学基礎論が哲学ではなく数学であることの説得を，何度となく試みてきた．{{Sfn|菊池|2014|pp=11-12}}

}}

}}。

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

[[コンピュータ科学者]]・[[数理論理学者]]・[[博士（哲学）|哲学博士]]（Ph.D. in Philosophy）のトルケル・フランセーン{{sfn|フランセーン|2011|p=奥付け}}{{sfn|Franzén|2008|p=Torkel Franzén}}によれば、不完全性定理のインパクトと重要性について、しばしば大げさな主張が繰り返されてきた{{sfn|フランセーン|2011|p=9}}{{Efn2|フランセーンは[[ストックホルム大学]]で[[哲学]]を専攻し、1987年に「[[Ph.D.]]（哲学）」を取得{{sfn|フランセーン|2011|p=奥付け}}。[[ルレオ工科大学]]でのフランセーンのページによると、「（哲学における）自分の博士論文　“my PhD thesis (in philosophy)”」は世界各国の大学図書館で閲覧できる{{sfn|Franzén|2008|p=Torkel Franzén}}。}}。たとえば

{{quotation|数学の思考に変革をもたらした

数学ばかりでなく、[[科学]]全体も一新した

数学だけではなく、[[哲学]]、[[言語学]]、計算機科学と[[宇宙論]]にまで[[革命]]を起こした}}

という言があるが、これらは乱暴な[[誇張]]とされる{{sfn|フランセーン|2011|p=9}}。不完全性定理が一番大きな衝撃を与えたと思われる数学においてさえ、「革命」らしきものは何も起きていない{{sfn|フランセーン|2011|p=9}}。

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

ゲーデルの完全性定理と不完全性定理は、革命的出来事ではなく時代の流れの産物だった{{sfn|フランセーン|2011|p=10}}。ゲーデル以外の誰かがこれらの定理を発見するのは時間の問題だったとされており、ゲーデル自身もそう見ていた{{sfn|フランセーン|2011|p=10}}。

数学上の「無矛盾性」と不完全性定理について、フランセーンは以下の通り解説している{{sfn|フランセーン|2011|p=145}}。

{{quote|「ゲーデルの定理のどこを見ても、“数学で使われているどんな形式体系も、その無矛盾性にはまったく疑いがない”という立場と矛盾してはいない。実際、これらの体系の公理が真であり、そして無矛盾であるという絶対確実な知識をもっていると主張しても、ゲーデルの定理のどこにも相反しないのである。」{{sfn|フランセーン|2011|p=145}}

}}

=== 誤用例 ===

フランセーンは『ゲーデルの定理：利用と誤用の不完全ガイド』において、ゲーデルの定理が広範に誤用されていることについて論じている{{sfn|フランセーン|2011|p=4}}。

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

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

1931年にゲーデルが示したのは、「特定の[[形式体系]]<math>P</math>において決定不能な[[命題]]の存在」であり、一般的な意味での「不完全性」についての定理ではない{{sfn|フランセーン|2011|p=230}}。

フランセーンによれば、ゲーデルの不完全性定理と結び付けられるテーマは[[ロジック]]、数学、[[計算]]、[[哲学]]、[[物理学]]、[[進化論]]、[[政治]]、[[宗教]]、[[無神論]]、[[神学]]、[[文学]]、[[詩歌]]、[[写真]]、[[建築]]、[[音楽]]、[[ヒップホップ]]、[[デート]]など多岐にわたる{{sfn|フランセーン|2011|pp=3-4}}。[[形式論理学]]のような専門領域の外では、不完全性定理についての言及の多くが、哲学的であり「ひどい誤解や[[自由連想]]に基いている」ため、馬鹿げているとさえ言える{{sfn|フランセーン|2011|p=4}}。たとえば、

{{quotation|ゲーデルの不完全性定理は、[[客観]]的[[現実]]の存在は証明できないことを示している}}

{{quotation|ゲーデルの不完全性定理によって、すべての[[情報]]は本質的に不完全で、[[自己言及]]的である}}

{{quotation|[[存在]]と[[意識]]を同等に考えることによって、私たちはゲーデルの不完全性定理を進化論に応用できる}}

などが見られる{{sfn|フランセーン|2011|p=4}}。ゲーデルの理論の誤解は、一般的な人々の間でも起こっている{{sfn|フランセーン|2011|p=4}}。たとえば

{{quotation|ある種の[[事実]]は、[[論理]]や数学でうまく証明できない}}

{{quotation|何ものも確実に知り尽くすことはできない}}

{{quotation|人間の心は[[計算機]]（[[コンピュータ]]）ができないこともできる}}

などである{{sfn|フランセーン|2011|p=4}}。

==== 数学以外の学問 ====

田中によれば、ゲーデル自身が不完全性定理について明言しているのは、[[1963年]]8月28日の次の文言である{{sfn|フランセーン|2011|p=230}}。

{{quote|「ある程度の[[有限]]的[[算術]]を含むどんな無矛盾な形式体系にも決定不能な算術命題が存在し、さらにそのような体系の無矛盾性はその体系においては証明できない。」{{sfn|フランセーン|2011|p=230}}}}

ゲーデルは慎重を重ねて言葉を選んでいるため、この表現を安易に変えようとすると、不具合を生じる{{sfn|フランセーン|2011|p=230}}。実際、この定理のいずれかの[[条件]]が落とされることで、多数の誤解が生じている（特に「有限的算術を含む」という条件が落とされていることが多い）{{sfn|フランセーン|2011|p=230}}。「ある程度の有限的算術を含む」という条件を、「十分大きな」「十分複雑な」「十分表現力のある」などといった曖昧な条件に置き換えることは誤りだが、一般向けの解説などには横行している（実際には、大きな[[理論]]で完全なものもあれば、小さな理論で不完全なものもある）{{sfn|フランセーン|2011|p=230}}。さらに見落とされやすい点は、不完全性定理の前提および結論部に「算術の条件」があることである{{sfn|フランセーン|2011|pp=230-231}}。

要するに不完全性定理は、「算術を含む体系がその算術部分で不完全である」という主張であり、その算術の外側が完全か不完全かについては、この定理は何も語っていない{{sfn|フランセーン|2011|p=231}}。

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

===== 哲学 =====

ゲーデルは「合理的な神学」の可能性を信じてはいたが、特定の宗教組織に所属することはなく、不完全性定理から哲学的・神学的解釈を引き出そうと試みることもしなかった{{sfn|フランセーン|2011|pp=125-126}}。しかし一方で哲学や神学は、ゲーデルや不完全性定理を自分たちへ結びつけようとしてきた{{sfn|フランセーン|2011|p=126}}。

[[アラン・ソーカル]]と[[ジャン・ブリクモン]]は、[[脱近代主義]]（ポストモダニズム）に対する論評『[[「知」の欺瞞]]』の中で、「ゲーデルの定理こそ汲めども尽きぬ知的濫用の泉である」と述べ、[[レジス・ドブレ]]、[[ミシェル・セール]]らの文章を批判している{{sfn|ソーカル|ブリクモン|2012|p=262}}{{sfn|フランセーン|2011|p=4}}。また、哲学者によるゲーデル関係の本が、フランセーンの本と同じ頃に書店販売されていたが、哲学者の本は[[専門誌]]によって酷評された{{sfn|フランセーン|2011|p=233}}。その本は全体として読みやすく一般読者からの評判は高かったが、ゲーデルの証明の核（[[不動点定理]]）について、根本的な勘違いをしたまま説明していた{{sfn|フランセーン|2011|p=233}}。同様の間違いは他の入門書などにもあり、田中は

{{quote|「一般の哲学者は、[[論理]]の[[専門家]]ではない」}}

と述べている{{sfn|フランセーン|2011|p=233}}。哲学者または宗教家が、

{{Quotation|不完全性定理には数学の外に無数の応用例がある}}

といった考えを表明することは珍しくない{{sfn|フランセーン|2011|p=107}}。しかし、不完全性定理とは「算術の公理系PAや[[公理的集合論]][[ツェルメロ＝フレンケル集合論|ZFC]]のような形式体系を扱う数学の定理」であり、哲学や宗教はこの点を踏まえていない{{sfn|フランセーン|2011|p=108}}。要するに不完全性定理とは、数学内の「形式体系」（フォーマルシステム）についての定理である{{sfn|フランセーン|2011|p=108}}。確かに、[[思想]]・哲学・神学・[[信仰]]・[[聖書]]・[[法律]]・[[裁判]]等を「[[形式]]」や「[[体系]]」や「形式体系」と呼ぶ人も存在するが、それらは数学内の一分野「形式体系」ではない{{sfn|フランセーン|2011|pp=108-109}}。数学内の「形式体系」を研究し応用できる範囲は、数学や[[計算機]]（[[コンピュータ]]）である{{sfn|フランセーン|2011|pp=112-113}}。

[[嘘つきのパラドックス]]（「ウソつきの逆理」）には、「この文は偽である」といった代表的表明があるが、このパラドックスも、不完全性定理が誤用されている一例として挙げられている{{sfn|フランセーン|2011|p=120}}。定理を非数学的に「応用」した文章や嘘つき文は、以下のような長い（あるいは果てしない）議論を呼び起こしている{{sfn|フランセーン|2011|p=120}}。

{{Quotation|証明とは何か}}

{{Quotation|真なる言明とは、健全な論証とは何か}}

{{Quotation|何かが真であると示すこととは、何かが納得できるとは、何かを信じるとは、意味ある言明とは何か}}

このような誤用や議論は、人々の心に謎や「愉快な混乱」を発生させているかもしれないし、「哲学的に重要性をもっている」かもしれないが、不完全性定理とは関係が無い{{sfn|フランセーン|2011|p=120}}。そもそも数学上では、「真偽」や「[[証明 (数学)|証明]]」といった用語が既に明確に定義されており、不完全性定理もそれらの数学用語に従っている{{sfn|フランセーン|2011|p=120}}。

===== 宗教 =====

フランセーンによれば、次のような講釈さえ存在する{{sfn|フランセーン|2011|p=7}}。

{{quotation|ゲーデルの不完全性定理は、数学的な[[wikt:アプローチ|アプローチ]]や[[証明 (数学)|証明]]なしにも[[直観]]的に理解しうるものである。実際、[[禅]][[仏教]]思想のなかにも明瞭にそれとわかる形で不完全性の[[概念]]が出現しているからだ。{{sfn|フランセーン|2011|p=7}}}}

実際には不完全性定理は、「形式体系の無矛盾性と完全性についての定理」である{{sfn|フランセーン|2011|p=7}}。確かに「[[矛盾]]」「無矛盾」「完全」「不完全」「[[体系]]（[[システム]]）」という語は、専門用語でない言語とも結びつきがあるが、およそこのような結びつきは不完全性定理と関係が無い{{sfn|フランセーン|2011|p=7}}。

===== 神学 =====

[[神学]]にも不完全性定理は持ち込まれ濫用されており、たとえば『キリスト教と数学の書誌学』（1983年）がある{{sfn|フランセーン|2011|p=126}}。

{{quotation|ゲーデルの不完全性定理は … [[神]]の[[自由]]への道を示す。{{sfn|フランセーン|2011|p=126}}}}

{{quotation|〔この論文では〕ゲーデルの定理を用いて、物理学者が[[物質]]的[[実在]]の最終的理論を決して定式化できないことを示す。 … [[人間]]の[[心]]がたんなる論理[[機械]]以上のものであるという適切な見方を発展させる{{sfn|フランセーン|2011|p=126}}}}

{{quotation|数学者も彼らのシステムで数学的[[真理]]のすべてを把握できないのだから、神学者が、すでに明らかになった真理をうまく体系化できなくても気に病むには及ばない。{{sfn|フランセーン|2011|p=126}}}}

{{quotation|科学の方法、技法、仮定が、完全に科学に基礎づけられるはずはないことは、ゲーデルの定理からの[[類推]]によって説明される。それらの妥当性を判定するためには、科学の外の[[リソース]]を使わなくてはならない。{{sfn|フランセーン|2011|p=127}}}}

ダニエル・グレーブスは次の通り「考察」をしている。{{sfn|フランセーン|2011|p=126}}

{{quotation|[[ユダヤ教|ユダヤ]]・[[キリスト教]]は、真理はたんなる[[理性]]で推し量れる域を越えていると長い間考えてきた。[[霊]]的な真理は、[[霊魂]]によってのみ理解される、と私たちは教えられている。それも、そうあるべくしてそのようにある。ゲーデル流の構図は、キリスト教徒が[[宇宙]]について信じていることに適っている。{{sfn|フランセーン|2011|p=128}}}}

ナジャムディン・モハメッドも、神学的に「応用」している{{sfn|フランセーン|2011|p=131}}。

{{quotation|あなたが[[世界]]をどのように（論理的[[規則]]で）記述しても、あなたに[[真]]か[[偽]]か判定できない「何ものか」がつねにあるであろうことが指摘されている。 … これは、ゲーデルの不完全性定理の基本である。

もし私たちが論理や[[推論]]だけに頼るなら、互いに矛盾しているが論理的に自己無矛盾な推論・論理システムが多数生じ、完全な[[混乱]]状態で終わることもありうる。どっちが正しいか？　すべての事柄は、何がよいか悪いかのように現在の[[心理]]的な傾向に依存するものなのか？　こういう場合には「正しさ」は意味をもたず、まさにこのことが[[不可知論]]的[[無神論]]の立場を招きうるのだ。{{sfn|フランセーン|2011|p=131}}}}

これらの考察と、「[[ポストモダン]]的状況」（脱近代的状況）という考え方には類似性がある{{sfn|フランセーン|2011|pp=131-132}}。そうした理屈では、不完全性は無数の様々な無矛盾理論を導き、どこで「真理」が手に入るかは誰も知らない（したがって、理性だけで正しい道を歩むことはできず、[[信仰]]が進むべき道となる{{sfn|フランセーン|2011|p=132}}）。

しかし実際の数学では、そのような枝分かれは無く、「[[決定可能性#理論の決定可能性|決定不能性]]の海」の中でもがくようなことも無いため、そのような「混乱」は神学的[[幻想]]に過ぎないとされている{{sfn|フランセーン|2011|p=132}}。

=== 誤用の分類 ===

田中はゲーデルの定理の様々な誤用を分類している{{sfn|フランセーン|2011|p=234}}。その一つは、人間の[[悟性]]が陥りやすい間違った傾向である{{sfn|フランセーン|2011|p=234}}。たとえば、自分が思いつく有意義そうな体系がどれも不完全であるので、「有意義な体系はすべて不完全である」と思い込み、さらにその原因を[[定理]]か何かに帰着させようとする傾向である{{sfn|フランセーン|2011|pp=234-235}}。

別の誤用は、言語の誤用である{{sfn|フランセーン|2011|p=234}}。不完全性定理に含まれる「矛盾」「完全」「体系（システム）」などの語は、[[日常生活|日常]]では多様に使われている{{sfn|フランセーン|2011|p=234}}。そこを混同すれば、ゲーデルの定理までが[[自然言語|非形式的]]（インフォーマル）な意味と結び付けられる{{sfn|フランセーン|2011|p=234}}。

== 脚注 ==

=== 注釈 ===

{{脚注ヘルプ}}

{{Reflistnotelist2}}

=== 出典 ===

== 参考文献 == <!-- {{Cite book}}、{{Cite journal}} -->

{{reflist|3}}

{{参照方法|date=2016年4月}}

; 原論文

:* K. Gödel (1931), ''Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I.'' ''Monatshefte für Mathematik und Physik 38'': 173-98.

:

; 原論文の日本語訳

:* [[林晋]]・[[八杉満利子]]訳・解説 (2006), ゲーデル 不完全性定理, [[岩波書店]], ISBN 4-00-339441-0

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

:* [[廣瀬健]]・[[横田一正]] (1985),ゲーデルの世界: [[完全性定理]]と不完全性定理, [[海鳴社]], ISBN 4-87525-106-8

:*:（ゲーデルの完全性定理と不完全性定理の解説書。両方の原論文の邦訳が収録されている）

:

; 教科書

:* [[前原昭二]] (2006), 数学基礎論入門, [[朝倉書店]], ISBN 4-254-11723-X

:* [[新井敏康]] (2011), 数学基礎論, [[岩波書店]], ISBN 4-000-05536-4

:* [[田中一之]] 編著 (1997), 数学基礎論講義―不完全性定理とその発展, [[日本評論社]], ISBN 4-535-78241-5

:* Per Lindstrom (1997), Aspects of Incompleteness, Springer-Verlag, ISBN 3-540-63213-1

:* Petr Hajek and Pavel Pudlak (1993), Metamathematics of First-Order Arithmetic, Springer-Verlag, ISBN 3-540-63648-X

:

; 講義ノート

:* [[照井一成]], [http://www.kurims.kyoto-u.ac.jp/~terui/mita05.pdf 再帰的関数論（２００５年度、慶應義塾大学文学部）], 最終閲覧日 2015年1月25日

:

; 誤用と誤解について

:* [[トルケル・フランセーン]] (2006), ゲーデルの定理: 利用と誤用の不完全ガイド, [[みすず書房]], ISBN 4-622-07569-5

== 参照文献 ==

== 関連項目 ==<!-- {{Commonscat|Gödel's incompleteness theorems}} -->

=== 数学書・数理論理学書 ===

* [[グッドスタインの定理]]

* {{Cite book|和書

* [[ゲーデルの完全性定理]]

|last = 菊池

* [[自己言及]]

|first = 誠

* [[自己言及のパラドックス]]

|authorlink = 菊池誠_(神戸大学)

* [[対角線論法]] - ゲーデルによる不完全性定理の証明は対角線論法を用いている。

|date = 2014-10-25<!--Amazon.co.jpでは「2014/10/23」-->

* [[タルスキの定理]]

|title = 不完全性定理

* [[チューリングマシン]]

|edition = 初版1刷

* [[チューリングマシンの停止問題]]

|publisher = [[共立出版]]

* [[プリンキピア・マテマティカ]]

|isbn = 978-4320110960

* [[パリス＝ハーリントンの定理]]

|ref = harv}}

* [[ライスの定理]]

* [[算術的階層]]

* {{Cite book|和書

* [[ZFCから独立な命題の一覧]]

|last = フランセーン

|first = トルケル

|authorlink = :en:Torkel_Franzén

|translator = [[田中一之]]

|date = 2011-03-25

|title = ゲーデルの定理：利用と誤用の不完全ガイド

|publisher = [[みすず書房]]

|isbn = 978-4-622-07569-1

|ref = harv}}

=== 数学辞典 ===

* {{Citation|和書

|last1 = 青本

|first1 = 和彦（編）

|last2 = 上野

|first2 = 健爾（編）

|last3 = 加藤

|first3 = 和也（編）

|last4 = 神保

|first4 = 道夫（編）

|last5 = 砂田

|first5 = 利一（編）

|last6 = 高橋

|first6 = 陽一郎（編）

|last7 = 深谷

|first7 = 賢治（編）

|last8 = 俣野

|first8 = 博（編）

|last9 = 室田

|first9 = 一雄（編）

|authorlink1 = 青本和彦

|authorlink2 = 上野健爾

|authorlink3 = 加藤和也_(数学者)

|authorlink4 = 神保道夫

|date = 2005-09-29

|title = 岩波　数学入門辞典

|edition = 第1刷

|publisher = 岩波書店

|isbn = 978-4000802093

|ref = harv}}

* {{Cite book|和書

|author = 日本数学会（編）

|authorlink = 日本数学会

|date = 2011-10-25

|title = 岩波　数学辞典

|edition = 第4版第3刷

|publisher = 岩波書店

|isbn = 978-4000803090

|ref = harv}}

=== 科学書・学術書 ===

* {{Cite book|和書|author1=アラン・ソーカル|authorlink1=アラン・ソーカル|author2=ジャン・ブリクモン|authorlink2=ジャン・ブリクモン|title=[[「知」の欺瞞]]――ポストモダン思想における科学の濫用|chapter=11 ゲーデルの定理と集合論――濫用のいくつかの例|date=2012-02-16|publisher=[[岩波書店]]|series=[[岩波現代文庫]] 学術 261|isbn=978-4-00-600261-9|translator=田崎晴明・大野克嗣・堀茂樹|pages=262-269|ref={{harvid|ソーカル|ブリクモン|2012}}}}

=== Webサイト ===

* {{Cite web

|last = Franzén

|first = Torkel

|url = http://www.sm.luth.se/~torkel/

|title = Torkel Franzén

|publisher = Luleå University of Technology (Department of [[計算機科学|Computer Science]] and [[電気工学|Electrical Engineering]])

|year = 2008

|accessdate = 2021-01-11

|archiveurl = https://web.archive.org/web/20081018160401/http://www.sm.luth.se/~torkel/

|archivedate = 2008-10-18

|ref = harv}}

== 関連文献 ==

=== 原論文 ===

*{{Citation

|last=Gödel

|first=Kurt

|author-link=クルト・ゲーデル

|year=1931

|洋書|ref=harv|title=Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I.

|journal=Monatshefte für Mathematik und Physik

|volume=38

|pages=173–198

|doi=10.1007/BF01700692

|url=http://www.zentralblatt-math.org/zbmath/search/?q=an:57.0054.02

}}.

*{{Citation

|last=Rosser

|first=John Barkley

|author-link=ジョン・バークリー・ロッサー

|year=1936

|title=Extensions of some theorems of Gödel and Church

|journal=Journal of Symbolic Logic

|volume=1

|issue=3

|pages=87–91

|doi=10.2307/2269028

|url=https://www.jstor.org/stable/2269028

}}.

=== 原論文の日本語訳 ===

*{{Cite book|和書

|author1=廣瀬健|authorlink1=廣瀬健

|author2=横田一正|authorlink2=横田一正

|date=1985-05-10

|title=ゲーデルの世界　[[完全性定理]]と不完全性定理

|publisher=[[海鳴社]]

|isbn=4-87525-106-8

|ref={{Harvid|廣瀬|横田|1985}}

}} - ゲーデルの完全性定理と不完全性定理の解説書。両方の原論文の日本語訳が収録されている。

*{{Cite book|和書

|author=ゲーデル

|translator=[[林晋]]・[[八杉満利子]]

|date=2006-09-15

|title=ゲーデル　不完全性定理

|series=岩波文庫 青944-1

|publisher=[[岩波書店]]

|isbn=4-00-339441-0

|ref={{Harvid|ゲーデル|林|八杉|2006}}

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

*{{Cite book|和書

|author=田中一之|authorlink=田中一之

|others=藤村まりこ イラストレーション

|date=2012-04-26

|title=ゲーデルに挑む　証明不可能なことの証明

|publisher=[[東京大学出版会]]

|isbn=978-4-13-063900-2

|ref={{Harvid|田中|2012}}

}} - 原論文の邦訳と解説。

=== 原論文の英訳 ===

*{{Citation

|last=Gödel

|first=Kurt

|editor1-last=Feferman

|editor1-first=Solomon

|year=1986

|title=Kurt Gödel: Collected Works: Volume I: Publications 1929-1936

|publisher=Oxford University Press

|pages=144-195

|isbn=978-0-19-503964-1

|url={{Google books|5ya4A0w62skC|Kurt Gödel: Collected Works: Volume I: Publications 1929-1936|page=144|plainurl=yes}}

}}

*{{Citation

|last=Gödel

|first=Kurt

|translator=Meltzer, B.

|year=1992

|origdate=1962

|title=On Formally Undecidable Propositions of Principia Mathematica and Related Systems

|publisher=Dover Publications

|series=Dover Books on Mathematics

|isbn=978-0-486-66980-9

|url={{Google books|R7cHCYzIdWYC|On Formally Undecidable Propositions of Principia Mathematica and Related Systems|page=1|plainurl=yes}}

}}

*{{Citation

|last=Gödel

|first=Kurt

|last2=Hirzel

|first2=Martin

|date=2000-11-27

|title=On formally undecidable propositions of Principia Mathematica and related systems I

|journal=Boulder

|publisher=

|pages=173-196

|url=http://hirzels.com/martin/papers/canon00-goedel.pdf

|format=PDF

}}

*{{Citation

|editor-last=van Heijenoort

|editor-first=Jean

|last=Gödel

|first=Kurt

|year=2002

|title=From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931

|chapter=Some metamathematical results on completeness and consistency, On formally undecidable propositions of Principia mathematica and related systems I, and On completeness and consistency

|series=Source Books in the History of the Sciences

|publisher=Harvard University Press

|edition=Fourth Printing

|isbn=978-0-674-32449-7

|pages=592-617

|url={{Google books|v4tBTBlU05sC|From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931|page=592|plainurl=yes}}

}}

*{{Citation

|editor-last=Davis

|editor-first=Martin

|last=Gödel

|first=Kurt

|year=2004

|title=The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions

|chapter=On Formally Undecidable Propositions of the Principia Mathematica and Related Systems. I.

|publisher=Courier Corporation

|series=Dover Books on Mathematics

|pages=4-38

|isbn=978-0-486-43228-1

|url={{Google books|qW8x7sQ4JXgC|The Undecidable|page=4|plainurl=yes}}

}}

=== 教科書 ===

*{{Cite book|和書

|author=前原昭二|authorlink=前原昭二

|origdate=1977-06-01

|date=2006-03-20

|title=数学基礎論入門（復刊）

|series=基礎数学シリーズ 23

|publisher=[[朝倉書店]]

|isbn=978-4-254-11723-3

|ref={{Harvid|前原|2006}}

}}

*{{Cite book|和書

|author=新井敏康|authorlink=新井敏康

|origdate=2011-05-18

|date=2016-08-16

|title=数学基礎論

|publisher=岩波書店

|id=ISBN 978-4-00-005536-9 ISBN 978-4-00-730459-0

|ref={{Harvid|新井|2016}}

}}

*{{Cite book|和書

|author=田中一之 編著|authorlink=田中一之

|date=1997-03

|title=数学基礎論講義　不完全性定理とその発展

|publisher=[[日本評論社]]

|isbn=4-535-78241-5

|ref={{Harvid|田中ほか|1997}}

}}

*{{Cite book|和書

|editor=田中一之

|date=2006-07

|title=ゲーデルと20世紀の{{Ruby|論理学|ロジック}} 1 ゲーデルの20世紀

|publisher=東京大学出版会

|isbn=978-4-13-064095-4

|ref={{Harvid|田中ほか|2006a}}

}}

*{{Cite book|和書

|editor=田中一之

|date=2006-10

|title=ゲーデルと20世紀の{{Ruby|論理学|ロジック}} 2 完全性定理とモデル理論

|publisher=東京大学出版会

|isbn=978-4-13-064096-1

|ref={{Harvid|田中ほか|2006b}}

}}

*{{Cite book|和書

|editor=田中一之

|date=2007-03

|title=ゲーデルと20世紀の{{Ruby|論理学|ロジック}} 3 不完全性定理と算術の体系

|publisher=東京大学出版会

|isbn=978-4-13-064097-8

|ref={{Harvid|田中ほか|2007a}}

}}

*{{Cite book|和書

|editor=田中一之

|date=2007-07

|title=ゲーデルと20世紀の{{Ruby|論理学|ロジック}} 4 集合論とプラトニズム

|publisher=東京大学出版会

|isbn=978-4-13-064098-5

|ref={{Harvid|田中ほか|2007b}}

}}

*{{Citation

|last=Lindstrom

|first=Per

|year=1997

|title=Aspects of Incompleteness

|publisher=Springer-Verlag

|series=Lecture Notes in Logic 10

|isbn=3-540-63213-1

}}

*{{Citation

|last1=Hajek

|first1=Petr

|last2=Pudlak

|first2=Pavel

|origyear=1993

|date=2013-10-04

|title=Metamathematics of First-Order Arithmetic

|publisher=Springer-Verlag

|edition=Softcover reprint

|series=Perspectives in Mathematical Logic

|isbn=978-3-540-63648-9

}}

=== 講義ノート ===

*{{Cite web|和書 |author=照井一成 |url=https://www.kurims.kyoto-u.ac.jp/~cs/cs2011_terui.pdf |format=PDF |title=再帰的関数論（2005年度、慶應義塾大学文学部） |publisher=京都大学数理解析研究所 |accessdate=2018-12-24 |ref={{Harvid|照井|2005}}}}

== 関連項目 ==

<!-- {{Commonscat|Gödel's incompleteness theorems}} -->

{{Div col}}

*[[グッドスタインの定理]]

*[[ゲーデルの完全性定理]]

*[[:en:Gentzen's consistency proof|ゲンツェンの無矛盾性証明]]

*[[算術的階層]]

*[[対角線論法]] - ゲーデルによる不完全性定理の証明は対角線論法を用いている。

*[[タルスキの定理]]

*[[チューリングマシン]]

*[[チューリングマシンの停止問題]]

*[[パリス＝ハーリントンの定理]]

*[[プリンキピア・マテマティカ]]

*[[ライスの定理]]

*[[ZFCから独立な命題の一覧]]

*[[自己言及]]

*[[自己言及のパラドックス]]

{{Div col end}}

== 外部リンク ==

*{{Kotobank |word=ゲーデルの不完全性定理}}

*{{Cite web |url=http://100.yahoo.co.jp/detail/%E3%82%B2%E3%83%BC%E3%83%87%E3%83%AB%E3%81%AE%E4%B8%8D%E5%AE%8C%E5%85%A8%E6%80%A7%E5%AE%9A%E7%90%86/ |title=ゲーデルの不完全性定理 - [[Yahoo!百科事典]] |publisher=[[Yahoo! JAPAN]] |author=[[西村敏男]] |accessdate=2013-08-02 |archiveurl=https://archive.is/Z52jo |archivedate=2013-08-02 |deadlinkdate= 2013年12月 }}

*{{Kotobank|ゲーデルの不完全性定理|2=知恵蔵2013}}

*[http://mathematics-pdf.com/column/incomplete.html ゲーデルの不完全性定理について : MATHEMATICS.PDF]

*{{MathWorld|title=Gödel's Incompleteness Theorem|urlname=GoedelsIncompletenessTheorem}}

*{{MathWorld|title=Gödel's First Incompleteness Theorem|urlname=GoedelsFirstIncompletenessTheorem}}

*{{MathWorld|title=Gödel's Second Incompleteness Theorem|urlname=GoedelsSecondIncompletenessTheorem}}

{{Metalogic}}

{{Normdaten}}

{{DEFAULTSORT:けえてるのふかんせんせいていり}}

[[Category:クルト・ゲーデル]]

[[Category:数理論理学]]

[[Category:自然数論]]

[[Category:数学基礎論の定理]]

[[Category:メタ定理]]

[[Category:自然数論]]

[[Category:数学に関する記事]]

[[Category:数学のエポニム]]

[[Category:理論計算機科学]]