ゲーデルの不完全性定理

ゲーデルの不完全性定理は、形式的な公理理論の証明可能性の限界に関係する数理論理学の2つの定理である。1931年にクルト・ゲーデルによって発表されたこれらの結果は、数理論理学と数学の哲学の両方において重要である。これらの定理は、すべての数学に対して完全で一貫した公理の集合を見つけるというヒルベルトの計画が不可能であることを示すものとして広く解釈されているが、普遍的ではない。

最初の不完全性定理は、有効な手順(つまりアルゴリズム) によって定理を列挙できる一貫した公理系は、自然数の算術に関するすべての真理を証明できないと述べています。このような一貫した形式体系では、自然数に関する真であるが、その体系内では証明できないステートメントが常に存在します。

2 番目の不完全性定理は、最初の定理の拡張であり、システムがそれ自身の一貫性を証明できないことを示しています。

対角線上の議論を採用したゲーデルの不完全性定理は、形式体系の限界に関するいくつかの密接に関連した定理の最初のものでした。その後、真理の形式的な定義不可能性に関するタルスキの定義不可能性定理、ヒルベルトの決定問題が解決不可能であることのチャーチの証明、停止問題を解くアルゴリズムは存在しないというチューリングの定理が続きました。

不完全性定理は、自然数の基本的な算術を表現するのに十分な複雑さがあり、一貫性があり効果的に公理化されている形式体系に適用される。特に一階述語論理の文脈では、形式体系は形式理論とも呼ばれる。一般に、形式体系とは、特定の公理の集合と、その公理から新しい定理を導出することを可能にする記号操作規則（または推論規則）から構成される演繹装置である。そのような体系の一例として、一階ペアノ算術がある。これは、すべての変数が自然数を表すことを意図した体系である。集合論などの他の体系では、形式体系の一部の文だけが自然数に関する陳述を表現する。不完全性定理は、非公式な意味での「証明可能性」ではなく、これらの体系 内での形式的な証明可能性に関するものである。

形式システムが持つことのできる特性には、完全性、一貫性、有効な公理化の存在など、いくつかあります。不完全性定理は、十分な量の算術演算を含むシステムがこれら 3 つの特性すべてを持つことはできないことを示しています。

形式体系は、その定理の集合が再帰的に列挙可能である場合、有効に公理化されている（有効に生成されたとも呼ばれる）と言われる。これは、原理的には、定理ではないステートメントをリストすることなく、体系のすべての定理を列挙できるコンピュータプログラムが存在することを意味する。有効に生成された理論の例には、ペアノ算術やツェルメロ・フランケル集合論（ZFC）などがある。^[1]

真の算術として知られる理論は、ペアノ算術の言語における標準整数に関するすべての真のステートメントで構成されています。この理論は一貫性があり完全で、十分な量の算術を含んでいます。ただし、再帰的に列挙可能な公理セットがないため、不完全性定理の仮説を満たしていません。

公理の集合は、その公理の言語で書かれた任意の文に対して、その文またはその否定が公理から証明できる場合、 （統語的に、または否定的に）完全である。 ^[2]これは、ゲーデルの第一不完全性定理に関連する概念である。これは、公理の集合が与えられた言語のすべての意味的トートロジーを証明することを意味する意味的完全性と混同してはならない。ゲーデルは、完全性定理（ここで説明する不完全性定理と混同しないでください）において、一階述語論理が意味的に完全であることを証明した。しかし、それは統語的に完全ではない。なぜなら、一階述語論理の言語で表現可能でありながら、論理の公理だけでは証明も反証もできない文が存在するからである。

数学の体系において、ヒルベルトなどの思想家は、あらゆる数式を証明または反証（その否定を証明することによって）できるような公理化を見つけるのは時間の問題であると信じていました。

形式体系は、論理学が一般的にそうであるように、意図的に構文的に不完全である場合があります。または、必要な公理がすべて発見または含まれていないというだけの理由で不完全である場合もあります。たとえば、平行線公理のないユークリッド幾何学は不完全です。これは、言語の一部のステートメント (平行線公理自体など) が残りの公理から証明できないためです。同様に、稠密な線形順序の理論は完全ではありませんが、順序に終点がないことを述べる追加の公理によって完全になります。連続体仮説は、 ZFCの言語でのステートメントですが、ZFC 内では証明できないため、ZFC は完全ではありません。この場合、問題を解決する新しい公理の明らかな候補はありません。

1 階ペアノ算術の理論は一貫しているように見える。これが事実であると仮定すると、この理論は無限だが再帰的に列挙可能な公理の集合を持ち、不完全性定理の仮説に十分な算術をエンコードできることに注意する。したがって、最初の不完全性定理により、ペアノ算術は完全ではない。この定理は、ペアノ算術で証明も反証もできない算術のステートメントの明示的な例を与える。さらに、このステートメントは通常のモデルで真である。さらに、ペアノ算術の効果的に公理化された一貫した拡張は完全ではない。

公理の集合は、その文とその否定の両方が公理から証明できるような文がない場合は（単純に）一貫しており、そうでない場合は矛盾している。つまり、一貫した公理体系とは矛盾のない体系である。

ペアノ算術は ZFC からは一貫していることが証明できますが、それ自体からは一貫していません。同様に、ZFC はそれ自体からは一貫していることが証明できませんが、ZFC + 「アクセスできない基数が存在する」は、 κ が最小の基数である場合、フォン ノイマン宇宙内にあるV _{κ が}ZFC のモデルであり、理論が一貫しているのはモデルがある場合のみであるため、ZFC が一貫していることを証明します。

ペアノ算術の言語におけるすべてのステートメントを公理とみなすと、この理論は完全であり、再帰的に列挙可能な公理の集合を持ち、加算と乗算を記述できます。ただし、一貫性はありません。

矛盾した理論のさらなる例は、集合論において 無制限の理解の公理スキーマが想定されるときに生じるパラドックスから生じます。

不完全性定理は、自然数に関する事実の十分な集合を証明できる形式体系にのみ適用されます。十分な集合の 1 つは、ロビンソン算術 Qの定理の集合です。ペアノ算術などの一部の体系では、自然数に関するステートメントを直接表現できます。ZFC 集合論などの他の体系では、自然数に関するステートメントを独自の言語に解釈できます。これらのオプションはどちらも、不完全性定理に適しています。

与えられた特性を持つ代数的に閉じた体の理論は完全かつ無矛盾で、無限だが再帰的に列挙可能な公理の集合を持つ。しかし、この理論に整数をエンコードすることは不可能であり、理論は整数の算術を記述することができない。同様の例として、実閉体の理論があるが、これはユークリッド幾何学に対するタルスキの公理と本質的に同等である。したがって、ユークリッド幾何学自体は（タルスキの定式化では）完全かつ無矛盾で、効果的に公理化された理論の例である。

プレスブルガー算術のシステムは、自然数に対する加算演算のみ（乗算は省略）の公理の集合から構成されます。プレスブルガー算術は完全で、一貫性があり、再帰的に列挙可能であり、自然数の加算をエンコードできますが、乗算はエンコードできません。これは、ゲーデルの定理には、加算だけでなく乗算もエンコードする理論が必要であることを示しています。

ダン・ウィラード (2001) は、ゲーデル数列を形式化するのに十分な算術関係を許容するが、関数として乗算を持つほど強くなく、そのため第二不完全性定理を証明できない算術システムの弱い族を研究した。つまり、これらのシステムは一貫性があり、自身の一貫性を証明できる (自己検証理論を参照)。

公理のセットを選択する際の目標の 1 つは、間違った結果を証明せずに、できるだけ多くの正しい結果を証明できるようにすることです。たとえば、自然数に関するすべての真の算術的主張を証明できる真の公理のセットを想像することができます (Smith 2007、p. 2)。標準的な一階述語論理システムでは、矛盾した公理のセットは、その言語のすべてのステートメントを証明するため (これは爆発の原理と呼ばれることもあります)、自動的に完全です。ただし、完全かつ一貫性のある公理のセットは、矛盾のない定理の最大セットを証明します。 ^{[引用が必要]}

前のセクションでペアノ算術、ZFC、ZFC +「アクセスできない基数が存在する」で示したパターンは、一般的には破ることができません。ここで、ZFC +「アクセスできない基数が存在する」は、それ自体では一貫性があることを証明できません。また、連続体仮説によって示されるように、完全ではありません。連続体仮説は、ZFC +「アクセスできない基数が存在する」では解決できません^[3]。

最初の不完全性定理は、基本的な算術を表現できる形式システムでは、完全で一貫性のある公理の有限リストは決して作成できないことを示しています。一貫性のあるステートメントが公理として追加されるたびに、新しい公理を使用しても証明できない他の真のステートメントが存在します。システムを完成させる公理が追加された場合、それはシステムを矛盾させるという代償を伴います。公理の無限リストが完全で一貫性があり、効果的に公理化されることさえ不可能です。

ゲーデルの第一不完全性定理は、ゲーデルの 1931 年の論文「プリンキピア・マテマティカと関連システムの形式的に決定不可能な命題についてI」で「定理 VI」として初めて登場しました。定理の仮説は、その後まもなく J. バークレー・ロッサー (1936) によってロッサーのトリックを使用して改良されました。結果として得られた定理 (ロッサーの改良を組み込んだもの) は、英語で次のように言い換えることができます。ここで、「形式システム」には、システムが効果的に生成されるという仮定が含まれます。

第一不完全性定理：「一定量の基本的算術を実行できる一貫した形式体系F は不完全である。つまり、 Fの言語のステートメントの中には、 Fでは証明も反証もできないものがある。」 (Raatikainen 2020)

定理によって参照される証明不可能な文G _{F は、}システムFの「ゲーデル文」と呼ばれることがよくあります。証明では、システムFの特定のゲーデル文を構築しますが、システムの言語には、ゲーデル文と任意の論理的に有効な文との結合など、同じ特性を共有する文が無数に存在します。

効果的に生成された各システムには、独自のゲーデル文があります。F 全体と追加の公理としてG _{F を}含む、より大きなシステムF' を定義することは可能です。ゲーデルの定理はF'にも適用され、したがってF'も完全ではなくなるため、この結果完全なシステムは得られません。この場合、G _{F は}公理であるため、確かにF'の定理です。 G _{F は}Fでは証明できないと述べているだけなので、 F'内での証明可能性によって矛盾は生じません。ただし、不完全性定理はF'に適用されるため、 F'に対する新しいゲーデル文G _{F '}が存在し、 F' も不完全であることを示します_。 G F '_は、 F ではなく F'を参照 する_という点でG _Fと異なります。

ゲーデル文は、間接的にそれ自身を参照するように設計されています。この文は、特定の一連の手順を使用して別の文を作成すると、その作成された文はFで証明できないと述べています。ただし、一連の手順により、作成された文はG _F自体になります。このように、ゲーデル文G _{F は、} F内での自身の証明不可能性を間接的に述べています(Smith 2007、p. 135)。

ゲーデルは、最初の不完全性定理を証明するために、システム内の証明可能性の概念は、システムの文のゲーデル数に作用する算術関数だけで表現できることを実証しました。したがって、数に関する特定の事実を証明できるシステムは、それが効果的に生成される限り、そのシステム自身の文に関する事実も間接的に証明できます。システム内の文の証明可能性に関する質問は、数が完全であればシステムによって決定できる数自体の算術的特性に関する質問として表されます。

このように、ゲーデル文は間接的にシステムFの文を参照しているが、算術文として読むと、ゲーデル文は自然数のみを直接参照している。これは、自然数は特定の特性を持たないことを主張しており、その特性は原始的な再帰関係によって与えられる (Smith 2007、p. 141)。このように、ゲーデル文は算術言語で簡単な構文形式で記述することができる。特に、これは算術言語の式として表現することができ、その式はいくつかの先頭の全称量指定子とそれに続く量指定子のない本体から構成される (これらの式は算術階層のレベルにある) 。MRDP 定理を介して、ゲーデル文は、整数係数を持つ多くの変数の特定の多項式は、その変数に整数を代入しても値 0 になることはないという文として書き直すことができる (Franzén 2005、p. 71)。 ${\displaystyle \Pi _{1}^{0}}$

第一不完全性定理は、適切な形式理論Fのゲーデル文G _FがFにおいて証明不可能であることを示している。算術に関する文として解釈すると、この証明不可能性はまさに文が（間接的に）主張していることなので、ゲーデル文は実際は真である（Smoryński 1977、p. 825; Franzén 2005、pp. 28–33も参照）。このため、文G _Fは「真だが証明不可能」であると言われることが多い（Raatikainen 2020）。しかし、ゲーデル文自体は意図した解釈を正式に指定できないため、文G _Fの真偽はシステムの外部からのメタ分析によってのみ到達できる可能性がある。一般に、このメタ分析は、原始再帰算術と呼ばれる弱い形式体系内で実行することができ、 Con ( F )→ G _Fの含意を証明する。ここで、Con ( F )は、 Fの一貫性を主張する標準的な文である(Smoryński 1977、p. 840、Kikuchi & Tanaka 1994、p. 403)。

整合理論のゲーデル文は算術の意図された解釈についての文としては真であるが、ゲーデルの完全性定理(Franzén 2005, p. 135)の結果として、ゲーデル文は算術のいくつかの非標準モデルでは偽となる。その定理は、文が理論から独立している場合、理論には文が真であるモデルと文が偽であるモデルがあることを示している。前述のように、システムFのゲーデル文は、特定の特性を持つ数は存在しないと主張する算術文である。不完全性定理は、この主張がシステムFから独立していることを示しており、ゲーデル文が真であることは、問題の特性を持つ標準的な自然数は存在しないという事実から導かれる。ゲーデル文が偽となるモデルには、そのモデル内の性質を満たす何らかの要素が含まれている必要がある。このようなモデルは「非標準」でなければなりません。つまり、どの標準的な自然数にも対応しない要素を含まなければなりません (Raatikainen 2020、Franzén 2005、p. 135)。

ゲーデルは、特にリチャードのパラドックスと嘘つきのパラドックスを、彼の統語的不完全性の結果の意味論的類似物として「プリンキピア・マテマティカと関連体系における形式的に決定不可能な命題について I」の序論で引用している。嘘つきのパラドックスは「この文は偽である」という文である。嘘つきの文を分析すると、それが真ではあり得ない (そのとき、主張して​​いるように偽である) ことも偽ではあり得ない (そのとき、真である) ことが示される。体系Fのゲーデル文Gは、嘘つきの文と同様の主張をしているが、真実が証明可能性に置き換えられている。つまり、G は「Gは体系Fでは証明できない」と述べている。G の真実性と証明可能性の分析は、嘘つきの文の真実性の分析の形式化されたバージョンである。

ゲーデルの文では、「証明不可能」を「偽」に置き換えることはできません。なぜなら、「Qは偽の式のゲーデル数である」という述語は算術式として表現できないからです。タルスキの定義不可能定理として知られるこの結果は、不完全性定理の証明に取り組んでいたゲーデルと、この定理の名を冠したアルフレッド・タルスキの両者によって独立に発見されました。

ゲーデルの 1931 年の論文で述べられた定理と比較すると、不完全性定理に関する現代の多くの記述は、2 つの点でより一般的です。これらの一般化された記述は、より広範なクラスのシステムに適用できるように表現されており、より弱い一貫性の仮定を組み込むように表現されています。

ゲーデルは、特定の算術体系であるプリンキピア・マテマティカの不完全性を実証したが、ある表現力を持つ有効な体系であればどれでも、同様の実証が可能である。ゲーデルは論文の序論でこの事実についてコメントしているが、具体性のために証明を1つの体系に限定している。この定理の現代的な記述では、有効性と表現力の条件を不完全性定理の仮定として述べるのが一般的であり、特定の形式体系に限定されることはない。これらの条件を述べるために使用される用語は、ゲーデルが結果を発表した1931年にはまだ開発されていなかった。

ゲーデルの不完全性定理の元々の主張と証明では、システムが単に無矛盾であるだけでなくω 無矛盾であるという仮定が必要である。システムがω無矛盾であるとは、それが ω 不矛盾であるとは、システムが特定の自然数mに対して~ P ( m )を証明する述語Pが存在するが、システムがP ( n )となる自然数n が存在することも証明する場合である。つまり、システムは、特性Pを持つ数が存在すると述べながら、それが特定の値を持つことを否定する。システムの ω 無矛盾性はその無矛盾性を意味するが、無矛盾性は ω 無矛盾性を意味するわけではない。J . Barkley Rosser  (1936) は、システムが ω 無矛盾ではなく無矛盾であることのみを要求する証明のバリエーション ( Rosser のトリック) を見つけることで、不完全性定理を強化した。これは主に技術的な興味です。なぜなら、算術の真の形式理論 (公理がすべて自然数に関する真のステートメントである理論) はすべて ω 整合であり、したがって、元々述べられたゲーデルの定理がそれらに適用されるからです。ω 整合ではなく整合のみを仮定する不完全性定理のより強力なバージョンは、現在ではゲーデルの不完全性定理やゲーデル・ロッサーの定理としてよく知られています。

基本的な算術を含む各形式体系Fについて、 Fの一貫性を表す式 Cons( F )を標準的に定義することができます。この式は、「結論が構文上の矛盾である形式的導出をコード化する自然数は体系F内に存在しない」という特性を表します。構文上の矛盾は多くの場合「0=1」とみなされますが、この場合、 Cons( F ) は「 Fの公理から '0=1' の導出をコード化する自然数は存在しない」と述べています。

ゲーデルの第二不完全性定理は、一般的な仮定の下では、この標準的な無矛盾性ステートメント Cons( F ) はFでは証明できないことを示している。この定理は、ゲーデルの 1931 年の論文「プリンキピア・マテマティカと関連システム I における形式的に決定不可能な命題について」で「定理 XI」として初めて登場した。次のステートメントでは、「形式化されたシステム」という用語には、 F が事実上公理化されているという仮定も含まれている。この定理は、ある程度の初等算術を実行できる任意の無矛盾なシステム F について、 F の無矛盾性はF自体では証明できないことを述べている。 ^[4]この定理は、第一不完全性定理で構築されたステートメントがシステムの無矛盾性を直接表現していないため、第一不完全性定理よりも強力である。第二不完全性定理の証明は、システムF自体の中で第一不完全性定理の証明を形式化することによって得られる。

第二不完全性定理には、 Fの無矛盾性をFの言語で式として表現する方法に関して、技術的な微妙な点があります。システムの無矛盾性を表現する方法は多数あり、それらすべてが同じ結果につながるわけではありません。第二不完全性定理の式 Cons( F ) は、無矛盾性の特別な表現です。

Fが一貫しているという主張の他の形式化は、Fにおいて同等ではない可能性があり、いくつかは証明可能であるかもしれません。たとえば、1 階ペアノ算術 (PA) は、「PA の最大の一貫したサブセット」が一貫していることを証明できます。しかし、PA は一貫しているため、PA の最大の一貫したサブセットは PA であり、この意味では PA は「一貫していることを証明」します。PA が証明しないのは、PA の最大の一貫したサブセットが、実際には PA 全体であるということです。(「PA の最大の一貫したサブセット」という用語は、ここでは、特定の有効な列挙の下での PA の公理の最大の一貫した初期セグメントを意味します。)

第二不完全性定理の標準的な証明では、証明可能性述語Prov _A ( P ) がヒルベルト・バーネイズの証明可能性条件を満たすことを前提としています。#( P ) を式Pのゲーデル数を表すとすると、証明可能性条件は次のようになります。

1. F がP を証明する場合、F はProv _A (#( P ))を証明します。
2. Fは1を証明します。つまり、FはProv _A (#( P )) → Prov _A (#( Prov _A (#( P ))))を証明します。
3. F はProv _A (#( P → Q )) ∧ Prov _A (#( P )) → Prov _A (#( Q ))を証明します (法 ponens   の類似物)。

ロビンソン算術など、第一不完全性定理の仮定を満たすほど強力だが、ヒルベルト・バーネイズの条件を証明できないシステムもあります。しかし、ペアノ算術はこれらの条件を検証できるほど強力であり、ペアノ算術よりも強力なすべての理論も同様です。

ゲーデルの第二不完全性定理は、上で概説した技術的条件を満たすシステムF _1は、 F ₁の無矛盾性を証明するいかなるシステムF ₂の無矛盾性も証明できないことも意味します。これは、そのようなシステムF _1は、 F _{2 が}F ₁の無矛盾性を証明すれば、F _{1 は}実際に無矛盾であることを証明できるためです。 F ₁が無矛盾であるという主張は、 「すべての数nについて、n はF ₁の矛盾の証明のコードではないという決定可能な特性を持つ」という形式です。F ₁が実際に無矛盾であれば、F _{2 は}、あるnについて、 nがF ₁の矛盾のコードであることを証明するでしょう。しかし、F _{2 が}F ₁が無矛盾であることも証明した場合 (つまり、そのようなn は存在しない場合)、 F 2 自体が無矛盾になります。この推論はF _{1で形式化でき、} F ₂が無矛盾であれば、F _{1 も}無矛盾であることを示します。第二不完全性定理により、F _{1 は}その一貫性を証明していないため、F ₂の一貫性も証明できません。

この第二不完全性定理の系は、例えばペアノ算術の無矛盾性を、ペアノ算術 (PA) で無矛盾性が証明できるシステムで形式化できる有限論的手段を使って証明する望みがないことを示しています。例えば、有限論的数学の正確な形式化として広く受け入れられている原始再帰算術(PRA) のシステムは、PA で無矛盾であることが証明できます。したがって、PRA は PA の無矛盾性を証明できません。この事実は、一般的に、理想の原理が無矛盾であるという有限論的証明を与えることによって、「実在の」(有限論的) 数学的命題の証明における「理想の」(無限論的) 数学的原理の使用を正当化することを目指したヒルベルトのプログラムが実行できないことを意味しているとみなされています。^[5]

この系は、第二不完全性定理の認識論的関連性も示している。システムFがその無矛盾性を証明したとしても、それは何ら興味深い情報を提供しないであろう。これは、無矛盾な理論が、その無矛盾性を含めてすべてを証明するからである。したがって、FにおけるFの無矛盾性の証明は、 Fが無矛盾であるかどうかについて何の手がかりも与えないであろう。すなわち、そのような無矛盾性の証明によって、 Fの無矛盾性についての疑問が解決されることはないであろう。無矛盾性の証明における興味は、ある意味でF自体よりも疑いの少ない、例えばFよりも弱いシステムF'におけるシステムFの無矛盾性を証明できる可能性にある。 F = ツェルメロ–フレンケル集合論やF' = 原始的再帰算術など、多くの自然発生的な理論FおよびF'では、 F'の無矛盾性はFにおいて証明可能であり、したがってF'は、第二不完全性定理の上記の系によってFの無矛盾性を証明できない。

第二不完全性定理は、異なる公理を持つ異なるシステムの無矛盾性を証明する可能性を完全に排除するものではない。例えば、ゲルハルト・ゲンツェンは、ε ₀と呼ばれる順序数が整根拠であると主張する公理を含む異なるシステムでペアノ算術の無矛盾性を証明した。ゲンツェンの無矛盾性証明を参照。ゲンツェンの定理は、証明理論における 順序数解析の発展を促した。

数学とコンピュータサイエンスにおいて、「決定不能」という言葉には 2 つの異なる意味があります。1 つ目は、ゲーデルの定理に関連して使用される証明論的な意味であり、指定された演繹システムでは証明も反証もできないステートメントのことです。2 つ目の意味は、ここでは説明しませんが、計算可能性理論に関連して使用され、ステートメントではなく、それぞれがはいまたはいいえで答える必要がある質問の可算無限セットである決定問題に適用されます。問題セット内のすべての質問に正しく答える計算可能な関数が存在しない場合に、そのような問題は決定不能であると言われます (決定不能問題を参照)。

「決定不能」という単語には 2 つの意味があるため、「証明も反駁もできない」という意味で、「決定不能」の代わりに 「独立」という用語が使用されることがあります。

特定の演繹システムにおけるステートメントの決定不能性は、それ自体では、ステートメントの真理値が明確に定義されているかどうか、または他の手段で決定できるかどうかという問題には対処しません。決定不能性は、検討中の特定の演繹システムがステートメントの真偽を証明しないことを意味するだけです。真理値が決してわからない、または適切に指定されていない、いわゆる「絶対的に決定不能な」ステートメントが存在するかどうかは、数学の哲学における議論の的となっています。

ゲーデルとポール・コーエンの共同研究により、決定不可能な命題（最初の意味で）の具体的な例が2つ示されている。連続体仮説はZFC （集合論の標準的な公理化）では証明も反証もできず、選択公理はZF（選択公理を除くすべてのZFC公理）では証明も反証もできない。これらの結果には不完全性定理は不要である。ゲーデルは1940年に、これらの命題はどちらもZFやZFC集合論では反証できないことを証明した。1960年代にコーエンは、どちらもZFからは証明できず、連続体仮説はZFCから証明できないことを証明した。

シェラ（1974）は、群論におけるホワイトヘッド問題は、標準的な集合論では、その言葉の最初の意味で決定不可能であることを示した。 ^[6]

グレゴリー・チャイティンは、アルゴリズム情報理論において決定不可能なステートメントを作成し、その設定で別の不完全性定理を証明しました。チャイティンの不完全性定理は、十分な算術を表現できる任意のシステムに対して、そのシステムでcより大きいコルモゴロフ複雑度を持つ特定の数が証明できないような上限cが存在すると述べています。ゲーデルの定理は嘘つきのパラドックスに関連していますが、チャイティンの結果はベリーのパラドックスに関連しています。

これらは、ゲーデルの「真だが決定不能」という文の自然な数学的等価物です。これらは、一般に有効な推論形式として受け入れられているより大規模なシステムでは証明できますが、ペアノ算術などのより限定されたシステムでは決定不能です。

1977年、パリスとハリントンは、無限ラムゼー定理の一種であるパリス＝ハリントン原理が（一階）ペアノ算術では決定不可能であるが、より強い二階算術システムでは証明できることを証明した。カービーとパリスは後に、パリス＝ハリントン原理よりもいくぶん単純な自然数の列に関する命題であるグッドスタインの定理もペアノ算術では決定不可能であることを示した。

コンピュータサイエンスに応用されているクラスカルの木定理も、ペアノ算術からは決定不可能だが、集合論では証明可能である。実際、クラスカルの木定理（またはその有限形式）は、述語主義と呼ばれる数学の哲学に基づいて受け入れられる原理をコード化したはるかに強力なシステムATR ₀では決定不可能である。^[7] 関連するがより一般的なグラフマイナー定理（2003）は、計算複雑性理論に影響を与えている。

不完全性定理は、再帰理論における決定不可能な集合に関するいくつかの結果と密接に関連しています。

クリーネ (1943) は、計算可能性理論の基本的な結果を用いてゲーデルの不完全性定理の証明を提示した。その 1 つの結果は、停止問題は決定不可能であることを示している。つまり、任意のプログラムP を入力として与えた場合、特定の入力で実行したときにP が最終的に停止するかどうかをコンピュータ プログラムが正しく判断することはできない。クリーネは、一定の一貫性特性を持つ完全で効果的な算術システムが存在すると、停止問題は決定可能になるが、これは矛盾であることを示した。^[8]この証明方法は、ショーンフィールド (1967)、チャールズワース (1981)、ホップクロフト & ウルマン (1979) によっても提示されている。^[9]

フランツェン (2005) は、ヒルベルトの第 10 問題に対するマティヤセビッチの解法を使ってゲーデルの第 1 不完全性定理の証明を得る方法を説明しています。^[10]マティヤセビッチは、整数係数を持つ多変数多項式p ( x ₁、x ₂、...、x _k )が与えられたときに、方程式p = 0に整数解があるかどうかを判断するアルゴリズムは存在しないことを証明しました。整数係数を持つ多項式、および整数自体は算術言語で直接表現できるため、多変数整数多項式方程式p = 0 に整数の解がある場合、十分に強力な算術システムT はこれを証明します。さらに、システムT がω 整合であると仮定します。その場合、整数に解がない場合、特定の多項式方程式に解があることは決して証明されません。したがって、T が完全かつω無矛盾であれば、単にTの証明を列挙して「p には解がある」または「p には解がない」のいずれかが見つかるまで続けるだけで、多項式方程式に解があるかどうかをアルゴリズム的に決定することが可能になるが、これはマティヤセビッチの定理に反する。したがって、T はω無矛盾かつ完全ではあり得ない。さらに、各整合した有効生成システムTに対して、方程式p = 0 が整数に対して解を持たないような多変数多項式p を整数に対して有効に生成することは可能であるが、解が存在しないことはTでは証明できない。^[11]

スモリニスキ（1977）は、再帰的に分離不可能な集合の存在がどのようにして第一不完全性定理を証明するために使われるかを示している。この証明は、ペアノ算術のようなシステムが本質的に決定不可能であることを示すためにしばしば拡張される。^[12]

チャイティンの不完全性定理は、コルモゴロフ複雑性に基づいて、独立した文を生成する別の方法を提供します。上で述べたクリーネによって提示された証明と同様に、チャイティンの定理は、すべての公理が自然数の標準モデルで真であるという追加の特性を持つ理論にのみ適用されます。ゲーデルの不完全性定理は、標準モデルに誤ったステートメントが含まれているにもかかわらず、矛盾のない理論に適用できるという点で区別されます。これらの理論は、ω 矛盾として知られています。

背理法による証明には3つの重要な部分があります。まず、提案された基準を満たす形式システムを選択します。

1. システム内のステートメントは、自然数 (ゲーデル数と呼ばれる) で表すことができます。これの意味は、ステートメントの真偽などの特性は、そのゲーデル数が特定の特性を持つかどうかを判断することと同等であり、したがって、ステートメントの特性はゲーデル数を調べることによって実証できるということです。この部分は、「ステートメントSはシステム内で証明可能である」という考えを表現する式の構築で終わります (これは、システム内の任意のステートメント「 S 」に適用できます)。
2. 形式体系では、解釈すると自己参照的になり、本質的には（つまりステートメント自体が）証明不可能であることを示す数値を構築することができます。これは、「対角化」と呼ばれる手法（カントールの対角線論証に由来するためこのように呼ばれています）を使用して行われます。
3. 形式システム内では、このステートメントはシステム内で証明も反証もできないことを実証することを可能にし、したがってシステムは実際にはω整合ではない可能性があります。したがって、提案されたシステムが基準を満たしているという当初の仮定は誤りです。

上で説明した証明を具体化する上での主な問題は、一見すると、 「 p は証明できない」と同等のステートメントp を構成するには、 p が何らかの形でpへの参照を含む必要があり、それが簡単に無限後退を引き起こす可能性があるように思われることです。ゲーデルの手法は、ステートメントを数値と一致させることができることを示すことです (多くの場合、構文の算術化と呼ばれます)。これにより、 「ステートメントを証明する」が「数値が特定のプロパティを持っているかどうかをテストする」に置き換えられます。これにより、定義の無限後退を回避する方法で自己参照式を構築できます。同じ手法は、後にアラン・チューリングによって、定義問題に関する研究で使用されました。

簡単に言えば、システムで定式化できるすべての式や文に、ゲーデル数と呼ばれる一意の番号が割り当てられるようにする方法を考案できます。これにより、式とゲーデル数を機械的に変換できるようになります。関係する数字は、桁数で言うと非常に長くなる可能性がありますが、これは障害にはなりません。重要なのは、そのような数字を作成できることです。簡単な例としては、英語を各文字の数字のシーケンスとして保存し、それを結合して 1 つの大きな数字にする方法があります。

• この単語はASCIIhelloでは 104-101-108-108-111 としてエンコードされており、これは数値 104101108108111 に変換できます。
• 論理ステートメントは、 ASCIIx=y => y=xでは 120-061-121-032-061-062-032-121-061-120 としてエンコードされ、数値 120061121032061062032121061120 に変換できます。

原則として、文が真か偽かを証明することは、文に一致する数が特定の特性を持っているか持っていないかを証明することと同等であると示せます。形式体系は一般的な数についての推論をサポートするのに十分強力であるため、式や文を表す数についての推論もサポートできます。重要なのは、システムが数の特性についての推論をサポートできるため、結果はそれらの同等の文の証明可能性についての推論と同等であるということです。

原理的にはシステムが間接的に証明可能性に関するステートメントを作成できることが示されており、ステートメントを表す数値の特性を分析することで、実際にこれを行うステートメントを作成する方法を示すことが可能になりました。

ちょうど 1 つの自由変数x を含む式F ( x )は、ステートメント形式またはクラス符号と呼ばれます。 x が特定の数に置き換えられるとすぐに、ステートメント形式は正当なステートメントに変わり、システムで証明可能か、証明不可能かのいずれかになります。特定の式では、すべての自然数nに対して、⁠ ⁠ が真であるのは、それが証明できる場合のみであることを示すことができます (元の証明の正確な要件はより弱いですが、証明の概要ではこれで十分です)。特に、これは「2  ×  3 = 6」など、有限個の自然数間のすべての特定の算術演算に当てはまります。 ${\displaystyle F(n)}$

文形式自体は文ではないため、証明または反証することはできません。ただし、すべての文形式F ( x )には、 G ( F )で表されるゲーデル数を割り当てることができます。形式F ( x )で使用される自由変数の選択は、ゲーデル数G ( F )の割り当てとは関係ありません。

証明可能性の概念自体も、次のようにゲーデル数でコード化できます。証明は特定の規則に従うステートメントのリストであるため、証明のゲーデル数を定義できます。ここで、すべてのステートメントpに対して、数xがその証明のゲーデル数であるかどうかを尋ねることができます。 pのゲーデル数と、その証明の潜在的なゲーデル数であるxの関係は、2 つの数間の算術関係です。したがって、この算術関係を使用してyの証明のゲーデル数が存在することを述べるステートメント形式Bew ( y )があります。

Bew ( y ) = ∃ x（ y は式のゲーデル数であり、 x はyによってエンコードされた式の証明のゲーデル数です）。

Bewという名前は、ドイツ語で「証明可能」を意味するbeweisbarの略です。この名前はもともと、ゲーデルが先ほど説明した証明可能性の式を表すために使用しました。「 Bew ( y ) 」は、 Tの元の言語で特定の非常に長い式を表す単なる略語であり、文字列「Bew」自体はこの言語の一部であるとは主張されていないことに注意してください。

式Bew ( y )の重要な特徴は、システム内でステートメントp が証明可能であれば、 Bew ( G ( p ))も証明可能であることです。これは、 pの証明には対応するゲーデル数があり、その存在によってBew( G ( p ))が満たされるためです。

証明の次のステップは、間接的にそれ自身の証明不可能性を主張する文を得ることである。ゲーデルはこの文を直接構築したが、少なくとも1つのそのような文の存在は対角補題から導かれる。これは、十分に強い形式体系とF形式の文に対して、システムが証明する 文pが存在するというものである。

p ↔ F ( G ( p ) )。

FをBew ( x )の否定とすると、定理が得られる。

p ↔ ~ Bew ( G ( p ))

そしてこれによって定義されるp は、大まかに言えば、それ自身のゲーデル数が証明不可能な式のゲーデル数であることを示しています。

pという文は、文字通り~ Bew ( G ( p ))に等しいわけではありません。むしろ、p は、特定の計算を実行すると、結果として得られるゲーデル数が証明不可能な文のゲーデル数になることを示しています。しかし、この計算を実行すると、結果として得られるゲーデル数はp自体のゲーデル数になります。これは、英語では次の文に似ています。

「」が引用符で囲まれて単独で存在する場合、証明できません。「」が引用符で囲まれて単独で存在する場合、証明できません。

この文は直接的にはそれ自身を参照していないが、述べられた変換が行われると結果として元の文が得られるため、この文は間接的にそれ自身の証明不可能性を主張している。対角補題の証明でも同様の方法が用いられる。

ここで、公理系がω-無矛盾であると仮定し、pを前のセクションで得られたステートメントとします。

pが証明可能であれば、上で述べたように、 Bew ( G ( p )) も証明可能になります。しかし、p はBew ( G ( p ))の否定を主張します。したがって、このシステムは矛盾しており、ステートメントとその否定の両方が証明されます。この矛盾は、 p が証明可能ではないことを示しています。

pの否定が証明可能であれば、Bew ( G ( p ))も証明可能になります ( p はBew ( G ( p ))の否定と同等になるように構築されているため)。ただし、各特定の数xに対して、x はpの証明のゲーデル数にはなり得ません。これは、 p が証明可能ではないためです (前の段落から)。したがって、一方では、システムは特定のプロパティ ( pの証明のゲーデル数である) を持つ数が存在することを証明しますが、他方では、すべての特定の数xに対して、それがこのプロパティを持たないことを証明できます。これは、ω 整合システムでは不可能です。したがって、 pの否定は証明できません。

したがって、ステートメントp は私たちの公理システムでは決定不可能であり、システム内で証明することも反証することもできません。

実際、pが証明不可能であることを示すには、システムが一貫しているという仮定のみが必要です。p の否定が証明不可能であることを示すには、より強い ω 一貫性の仮定が必要です。したがって、p が特定のシステムに対して構築されている場合:

• システムがω-無矛盾である場合、p もその否定も証明できず、したがってp は決定不可能です。
• システムが一貫している場合、同じ状況になるか、pの否定が証明される可能性があります。後者の場合、偽ではあるが証明可能なステートメント (「pではない」) があり、システムは ω 一貫性がありません。

システムの不完全性を避けるために「欠けている公理を追加」しようとすると、公理としてpまたは「pでない」のいずれかを追加する必要があります。しかし、その場合、ステートメントの「証明のゲーデル数である」という定義が変わります。つまり、式Bew ( x )が異なります。したがって、この新しい Bew に対角補題を適用すると、以前のステートメントとは異なる新しいステートメントpが得られます。このステートメントは、ω 整合である場合、新しいシステムでは決定不可能になります。

Boolos (1989) は、嘘つきのパラドックスではなくベリーのパラドックスを使用して、真だが証明不可能な式を構築する、第一不完全性定理の別の証明を概説している。同様の証明方法は、ソール・クリプキによって独立に発見された。^[13] Boolos の証明は、計算可能で列挙可能な任意の算術文の集合Sに対して、真だがSに含まれない別の文を構築することによって進められる。これにより、第一不完全性定理が系として得られる。Boolos によると、この証明は、算術の有効で一貫した理論の不完全性に対する「異なる種類の理由」を提供するため興味深い。^[14]

不完全性定理は、証明支援ソフトウェアによって完全に検証できる形式化された定理に変換された、比較的少数の非自明な定理の 1 つです。ゲーデルの不完全性定理の元の証明は、ほとんどの数学的証明と同様に、人間の読者向けに 自然言語で記述されました。

最初の不完全性定理のバージョンのコンピュータ検証済み証明は、1986 年にNatarajan ShankarによってNqthm を使用して(Shankar 1994)、2003 年に Russell O'Connor によってCoq を使用して(O'Connor 2005)、2009 年に John Harrison によってHOL Light を使用して(Harrison 2009) 発表されました。両方の不完全性定理のコンピュータ検証済み証明は、2013 年にLawrence PaulsonによってIsabelle を使用して発表されました(Paulson 2014)。

第二不完全性定理を証明する上での主な難しさは、第一不完全性定理の証明で使用された証明可能性に関するさまざまな事実が、証明可能性の形式述語P を使用してシステムS内で形式化できることを示すことです。これが完了すると、第二不完全性定理は、第一不完全性定理の証明全体をシステムS自体内で形式化することによって続きます。

p は上で構築された決定不可能な文を表し、矛盾を得るために、システムSの一貫性はシステムS自体の内部から証明できると仮定します。これは、「システムS は一貫している」というステートメントを証明することと同じです。次に、ステートメントcを考えます。ここで、c = 「システムSが一貫している場合、p は証明できません」。文cの証明はシステムS内で形式化できるため、ステートメントc、「p は証明できません」(または「P ( p )ではない」) はシステムSで証明できます。

ここで、システムSが一貫していることを証明できれば(つまり、 cの仮説のステートメント)、 p は証明不可能であることが証明されたことになります。しかし、これは矛盾です。なぜなら、第 1 不完全性定理によれば、この文 (つまり、文cで暗示されている「p 」は証明不可能である) は、証明不可能であると私たちが構築するものであるからです。これが、 Sで第 1 不完全性定理を形式化する必要がある理由であることに注意してください。第 2 不完全性定理を証明するには、定理がSで成り立つことを示すことによってのみ証明できる第 1 不完全性定理との矛盾が発生します。したがって、システムSが一貫していることを証明することはできません。そして、第 2 不完全性定理のステートメントが続きます。

不完全性の結果は数学の哲学、特に原理を定義するために単一の形式論理システムを使用する形式 主義のバージョンに影響を与えます。

不完全性定理は、自然数を論理の観点から定義することを目指したゴットロープ・フレーゲとバートランド・ラッセルによって提唱された論理主義のプログラムに深刻な影響を及ぼすと考えられることがある。 ^[15]ボブ・ヘイルとクリスピン・ライトは、不完全性定理は算術と同様に一階述語論理にも等しく適用されるため、論理主義にとっては問題ではないと主張している。彼らは、自然数は一階述語論理の観点から定義されるべきであると信じる人だけがこの問題を抱えていると主張している。

多くの論理学者は、ゲーデルの不完全性定理が、数学の有限無矛盾性の証明を求めるデイヴィト・ヒルベルトの第二問題に致命的な打撃を与えたと考えている。特に第二不完全性定理は、問題を不可能にするものとして見られることが多い。しかし、すべての数学者がこの分析に同意するわけではなく、ヒルベルトの第二問題の地位はまだ決まっていない（「問題の地位に関する現代の見解」を参照）。

哲学者JRルーカスや物理学者ロジャー・ペンローズなどの著述家たちは、ゲーデルの不完全性定理が人間の知能について何を示唆するのか、もし示唆するならば、何なのかについて議論してきた。議論の多くは、人間の心がチューリングマシンと同等であるのか、あるいはチャーチ＝チューリングのテーゼによれば、有限の機械と同等であるのかどうかに集中している。もし同等であり、機械が一貫しているなら、ゲーデルの不完全性定理がそれに当てはまるだろう。

パトナム（1960）は、ゲーデルの定理は人間には当てはまらないが、人間は間違いを犯し、矛盾するからであるが、人間の科学や数学の能力全般には当てはめられるかもしれないと示唆した。それが矛盾しないと仮定すると、その矛盾は証明できないか、チューリングマシンで表現できない。^[16]

ウィグダーソン（2010）は、数学的な「認識可能性」の概念は、論理的決定可能性ではなく計算複雑性に基づくべきだと提案している。彼は、「認識可能性が現代の基準、つまり計算複雑性によって解釈される場合、ゲーデル現象はまさに私たちの身近にある」と書いている。^[17]

ダグラス・ホフスタッターは、著書『ゲーデル、エッシャー、バッハ』および『わたしは奇妙なループ』の中で、ゲーデルの定理を、彼が奇妙なループと呼ぶものの例として挙げている。奇妙なループとは、公理的形式体系内に存在する階層的かつ自己言及的な構造である。彼は、これが人間の心の中に意識、つまり「わたし」という感覚を生み出すのと同じ種類の構造であると主張している。ゲーデルの定理における自己言及は、プリンキピア・マテマティカの形式体系内でその証明不可能性を主張するゲーデル文に由来するのに対し、人間の心における自己言及は、脳が刺激を抽象化して「記号」、つまり概念に反応するニューロンのグループに分類する方法に由来しており、これは事実上これも形式体系であり、最終的には知覚を行っている実体そのものの概念をモデル化する記号を生み出す。ホフスタッターは、十分に複雑な形式体系における奇妙なループによって、「下向き」または「逆さま」の因果関係、つまり因果関係の通常の階層が逆さまになる状況が生じる可能性があると主張しています。ゲーデルの定理の場合、これは簡単に言えば、次のようになります。

単に公式の意味を知るだけで、公理から系統的に「上へ」と進む旧式の方法で導出する努力をすることなく、その真偽を推論することができます。これは単に奇妙なだけでなく、驚くべきことです。通常、数学的推測が述べていることを見て、その文の内容だけを頼りにして、その文が真か偽かを推論することはできません。^[18]

はるかに複雑な形式システムである心の場合、この「下向きの因果関係」は、ホフスタッターの見解では、私たちの心の因果関係は、ニューロンや基本粒子間の相互作用の低レベルではなく、欲望、概念、性格、思考、アイデアの高レベルにあるという言い表せない人間の本能として現れます。物理学によれば、後者が因果関係の力を持っているように見えますが。

このように、私たち人間の通常の世界認識方法には奇妙な逆転があります。私たちは「小さなもの」ではなく「大きなもの」を認識するようにできていますが、現実を動かす実際の原動力は小さなものの領域にあるようです。^[18]

ゲーデルの定理は通常、古典論理の文脈で研究されるが、矛盾論理や本質的に矛盾した命題（二元論）の研究にも役立つ。プリースト（1984、2006）は、ゲーデルの定理における形式的証明の概念を通常の非形式的証明の概念に置き換えることで、素朴数学が矛盾していることを示すことができると主張し、これを二元論の証拠として用いている。^[19]この矛盾の原因は、システムの言語内にシステムの真理述語が含まれていることである。^[20]シャピロ（2002）は、ゲーデルの定理の二元論への応用について、より複雑な評価を与えている。^[21]

数学や論理を超えた議論の根拠として、定理の不完全性に訴えたり類推したりすることが時々ある。フランツェン (2005)、ラーティカイネン (2005)、ソーカル & ブリクモント (1999)、スタングルーム & ベンソン (2006) など、こうした拡張や解釈に対して否定的なコメントをしている著者は数人いる。^[22] たとえば、ソーカル & ブリクモント (1999) とスタングルーム & ベンソン (2006) は、ゲーデルの公言したプラトン主義と、彼の考えが時々用いられる反実在論的な使用法との間の相違に関するレベッカ・ゴールドスタインのコメントを引用している。ソーカル & ブリクモント (1999) は、レジス・ドゥブレイが社会学の文脈で定理を引用したことを批判している。ドゥブレイはこの使用法を比喩的であると擁護している (同上)。^[23]

ゲーデルは1929年に博士論文として完全性定理の証明を発表した後、博士号取得のための2番目の問題に取り組んだ。彼の当初の目標は、ヒルベルトの2番目の問題に対する肯定的な解を得ることだった。^[24]当時、2階算術に似た自然数と実数の理論は「解析学」と呼ばれ、自然数のみの理論は「算術」と呼ばれていた。

一貫性の問題に取り組んでいたのはゲーデルだけではなかった。アッカーマンは1925年に解析学の一貫性の証明に欠陥があるが、その中でヒルベルトが最初に開発したε置換法を使おうとした。その年の後半、フォン・ノイマンは帰納法の公理を一切使わずに算術のシステムで証明を修正することができた。1928年までにアッカーマンは修正した証明をベルナイスに伝えた。この修正した証明により、ヒルベルトは1929年に算術の一貫性が証明され、解析学の一貫性のある証明もすぐに続くだろうという確信を発表した。不完全性定理の発表によりアッカーマンの修正した証明が間違いであることが示された後、フォン・ノイマンはその主な手法が不健全であることを示す具体的な例を示した。^[25]

研究の過程で、ゲーデルは、文が偽であることを主張するとパラドックスが生じるが、証明不可能性を主張する文はパラドックスが生じないことを発見した。特に、ゲーデルはタルスキの定義不可能性定理と呼ばれる結果に気づいていたが、公表することはなかった。ゲーデルは1930年8月26日にカルナップ、ファイゲル、ワイスマンに最初の不完全性定理を発表し、4人全員が翌週 ケーニヒスベルクで行われた重要な会議である第二回厳密科学の認識論に関する会議に出席した。

1930年のケーニヒスベルク会議は3つの学会の合同会議で、当時の主要な論理学者の多くが出席した。カルナップ、ヘイティング、フォン・ノイマンはそれぞれ論理主義、直観主義、形式主義という数学哲学について1時間の講演を行った。^[26]この会議では、ゲッティンゲン大学を退任するヒルベルトの退職演説も行われた。ヒルベルトはこの演説で、すべての数学の問題は解けるという信念を主張した。彼は演説の最後で次のように述べた。

数学者にとって、無知というものは存在しません。そして、私の意見では、自然科学にも全く存在しません。... [誰も] 解決不可能な問題を見つけることに成功していない本当の理由は、私の意見では、解決不可能な問題が存在しないからです。愚かな無知とは対照的に、私たちの信条は「私たちは知らなければならない。私たちは知るだろう」と断言しています。

この演説はすぐにヒルベルトの数学に対する信念の要約として知られるようになった（最後の6語「Wir müssen wissen. Wir werden wissen!」は1943年にヒルベルトの墓碑銘として使われた）。ゲーデルはヒルベルトの演説に出席していたと思われるが、2人が直接会うことはなかった。^[27]

ゲーデルは会議3日目の円卓討論会で第一不完全性定理を発表した。この発表はフォン・ノイマンの注目を除けばほとんど注目されなかった。ノイマンはゲーデルを呼び出し会話をした。その年の後半、フォン・ノイマンは第一不完全性定理の知識をもとに独自に研究し、第二不完全性定理の証明にたどり着き、1930年11月20日付けの手紙でゲーデルに発表した。 ^{[28]ゲーデルは第二不完全性定理を独自に得て、1930年11月17日に}Monatshefte für Mathematikに提出した原稿にそれを含めた。

ゲーデルの論文は1931年に「プリンキピア・マテマティカと関連体系Iにおける形式的に決定不可能な命題について」という題名でモナトシェフテ誌に掲載された。題名が示すように、ゲーデルは当初、モナトシェフテ誌の次巻に論文の第2部を掲載する予定だったが、第1部がすぐに受け入れられたことが計画変更の理由の1つとなった。^[29]

ゲーデルは 1933 年から 1934 年にかけてプリンストンでチャーチ、クリーネ、ロッサーを含む聴衆を前に自身の定理に関する一連の講義を行った。この頃までにゲーデルは、自身の定理に必要な主要な特性はシステムが効果的でなければならないということだと理解していた (当時は「一般再帰」という用語が使われていた)。ロッサーは 1936 年に、ゲーデルの当初の証明の不可欠な部分であった ω 一貫性の仮説は、ゲーデル文を適切に変更すれば単純な一貫性に置き換えられることを証明した。これらの発展により、不完全性定理は本質的に現代的な形になった。

ゲンツェンは 1936 年に一階算術の無矛盾性の証明を発表しました。ヒルベルトはこの証明を「有限」なものとして受け入れましたが、(ゲーデルの定理がすでに示していたように) 無矛盾であることが証明されている算術システム内では形式化できませんでした。

不完全性定理がヒルベルトのプログラムに与えた影響はすぐに認識された。ベルナイスは不完全性定理の完全な証明を『数学基礎』（1939年）第2巻に、アッカーマンのε置換法に関する追加結果とゲンツェンの算術の無矛盾性証明とともに収録した。これは第2不完全性定理の完全な証明として初めて公表された。

フィンスラー（1926）はリチャードのパラドックスの一種を使って、彼が開発した特定の非公式な枠組みでは偽だが証明不可能な表現を構築した。^[30]ゲーデルは不完全性定理を証明したときこの論文を知らなかった（Collected Works Vol. IV., p. 9）。フィンスラーは1931年にゲーデルに手紙を書き、この論文について知らせた。フィンスラーは不完全性定理にはこの論文が優先されると感じていた。フィンスラーの方法は形式化された証明可能性に依存せず、ゲーデルの研究と表面的にしか似ていなかった。^[31]ゲーデルは論文を読んだが大きな欠陥があることに気づき、フィンスラーへの返答で形式化の欠如に対する懸念を示した。^[32]フィンスラーはその後のキャリアを通じて、形式化を避ける数学の哲学を主張し続けた。

1931年9月、エルンスト・ツェルメロはゲーデルに手紙を書き、ゲーデルの議論には「本質的な欠陥」があると告げた。^[33] 10月、ゲーデルは10ページの手紙で返事を出し、ツェルメロはシステム内の真理の概念はそのシステム内で定義可能であると誤って想定しており、タルスキの定義不可能性定理によれば一般には正しくないと指摘した。^[34]しかしツェルメロは譲らず、「若い競争相手に対するかなり痛烈な一節」を添えて批判を印刷物として発表した。^[35]ゲーデルはこの問題をこれ以上追求するのは無意味であると判断し、カルナップも同意した。^[36]ツェルメロのその後の研究の多くは、一階述語論理よりも強い論理に関するものであり、それによって数学理論の一貫性と範疇性の両方を示すことを目指した。

ルートヴィヒ・ヴィトゲンシュタインは、1953年に死後に出版された『数学の基礎に関する注釈』の中で、不完全性定理についていくつかの文章を書いている。特に、ラッセルの体系における「真」と「証明可能」の概念を混同しているように思われる「悪名高い段落」と呼ばれるセクションがある。ゲーデルは、ヴィトゲンシュタインの初期の理想言語哲学と『論理哲学論考』がウィーン学団の思想を支配していた時期に、ウィーン学団のメンバーだった。ヴィトゲンシュタインが不完全性定理を誤解していたのか、それとも単に表現が曖昧だっただけなのかについては論争がある。ゲーデルの「後日談」の文章に​​は、ヴィトゲンシュタインが自分の考えを誤読したという信念が表明されている。

複数の評論家はウィトゲンシュタインがゲーデルを誤解していると読んでいるが、フロイドとパトナム（2000年）やプリースト（2004年）は、ほとんどの評論がウィトゲンシュタインを誤解していると主張するテキストの読みを提供している。^[37]出版時に、バーネイズ、ダメット、クライゼルはウィトゲンシュタインの発言について別々のレビューを書いたが、そのすべては非常に否定的だった。^[38]この批判が一致していたため、不完全性定理に関するウィトゲンシュタインの発言は論理学界にほとんど影響を与えなかった。1972年、ゲーデルは「ウィトゲンシュタインは正気を失ってしまったのか？本気で言っているのか？意図的に取るに足らない無意味な発言をしている」と述べ、カール・メンガーに宛てて、 ウィトゲンシュタインのコメントは不完全性定理の誤解を示していると書き送った。

あなたが引用した文章から、ウィトゲンシュタインが[第一不完全性定理]を理解していなかった（あるいは理解していないふりをしていた）ことは明らかです。彼はそれを一種の論理的パラドックスとして解釈しましたが、実際は正反対であり、つまり数学のまったく議論の余地のない部分（有限数論または組合せ論）内の数学定理です。^[39]

2000年にウィトゲンシュタインの『後日談』が出版されて以来、哲学の分野ではウィトゲンシュタインの発言に対する当初の批判が正当であったかどうかを評価しようとする論文が相次いでいる。フロイドとパトナム（2000）は、ウィトゲンシュタインは不完全性定理について、これまで想定されていたよりも完全な理解を持っていたと主張する。彼らは特に、ω不整合システムに対するゲーデル文を「私は証明可能ではない」と解釈することに関心がある。なぜなら、このシステムには証明可能性述語が実際の証明可能性に対応するモデルがないからである。ロディッチ（2003）は、彼らのウィトゲンシュタイン解釈は歴史的に正当ではないと主張する。ベルト（2009）は、ウィトゲンシュタインの著作と矛盾論理の理論との関係を研究している。^[40]

• Kurt Gödel、1931 年、「正式な数学と物理学の原理、I」、Monatshefte für Mathematik und Physik、v. 38 n. 1、173–198ページ。土井：10.1007/BF01700692
• —、1931 年、「数学と数学の原理、I」、ソロモン フェフェルマン編、1986 年。クルト ゲーデル作品集、第 1 巻。私。オックスフォード大学出版局、144 ～ 195 ページ。ISBN 978-0195147209。ドイツ語の原文と英語の対訳があり、その前にStephen Cole Kleeneによる紹介文が付けられています。 
• —、1951、「数学の基礎に関するいくつかの基本定理とその意味」、ソロモン・フェファーマン編、1995年。クルト・ゲーデル全集、第3巻、オックスフォード大学出版局、pp. 304–323。ISBN 978-0195147223。 

以下の翻訳はどれも、すべての翻訳語とタイポグラフィが一致していません。タイポグラフィは深刻な問題です。なぜなら、ゲーデルは「以前に通常の意味で定義されていたメタ数学的概念」を強調することを明確に望んでいたからです (van Heijenoort 1967、p. 595)。3 つの翻訳が存在します。最初の翻訳について、ジョン・ドーソンは「メルツァーの翻訳は重大な欠陥があり、Journal of Symbolic Logicで壊滅的な批評を受けました。ゲーデルはブレイスウェイトの解説についても不満を述べています (Dawson 1997、p. 216)。」と述べています。 「幸いにも、メルツァーの翻訳は、マーティン・デイビスのアンソロジー『The Undecidable』のためにエリオット・メンデルソンが準備した、より優れた翻訳にすぐに取って代わられた。…彼は、その翻訳が「期待していたほど良くはなかった」と感じた。…[しかし、時間の制約のため]出版に同意した」(同上)。(脚注でドーソンは「出版された本は、ずさんな印刷と多数の誤植で全体的に損なわれていたため、応じたことを後悔するだろう」(同上)と述べている。ドーソンは「ゲーデルが好んだ翻訳は、ジャン・ファン・ヘイエノールトの翻訳だった」(同上)と述べている。真剣な学生のために、別のバージョンが存在する。それは、スティーブン・クリーネとJB・ロッサーが「1934年春にゲーデルが高等研究所で行った講義」中に記録した講義ノートのセットである(デイビスによる1965年の解説、39ページと41ページ以降を参照)。このバージョンのタイトルは「形式数学システムの決定不可能な命題について」です。出版順に並べると次のようになります。

• B. メルツァー（翻訳）とRBブレイスウェイト（序論）、1962年。プリンキピア・マテマティカと関連システムの形式的に決定不可能な命題について、ドーバー出版、ニューヨーク（ドーバー版1992）、ISBN 0-486-66980-7（ペーパーバック）。これには、33〜34ページにゲーデルのドイツ語略語の便利な翻訳が含まれています。前述のように、印刷、翻訳、解説は疑わしいものです。残念ながら、この翻訳は、疑わしい内容をすべて含んだまま、 

• スティーブン・ホーキング編著、2005年。神は整数を創造した：歴史を変えた数学的ブレークスルー、ランニング・プレス、フィラデルフィア、ISBN 0-7624-1922-9。ゲーデルの論文は1097ページから、ホーキングの解説は1089ページから始まります。 

• マーティン・デイビス編、1965年。『The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions』、レイヴン・プレス、ニューヨーク、ISBNなし。ゲーデルの論文は5ページ目から始まり、その前に1ページの解説がある。
• Jean van Heijenoort編著、1967 年、第 3 版 1967 年。From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931、Harvard University Press、ケンブリッジ、マサチューセッツ州、ISBN 0-674-32449-8 (pbk)。van Heijenoort が翻訳しました。彼は、「ゲーデル教授は、多くの点で彼の希望に沿った翻訳を承認しました」と述べています (p. 595)。ゲーデルの論文は p. 595 から始まり、van Heijenoort の解説は p. 592 から始まります。 
• マーティン・デイビス編著、1965年、同書。「形式数学体系の決定不可能な命題について」。ゲーデルの正誤表の訂正とゲーデルの追加注釈が入ったコピーは、41ページ目から始まり、その前にデイビスの解説が2ページ続く。デイビスがこれを本に収録するまで、この講義は謄写版の注釈としてのみ存在していた。

• Boolos, George (1989)。「ゲーデルの不完全性定理の新しい証明」。アメリカ数学会誌36 : 388–390, 676。Boolos (1998, pp. 383–388) に再掲載。
• ブーロス、ジョージ（1998年）。 『論理、論理、そして論理』ハーバード大学出版局、p.443。ISBN 0-674-53766-1。
• Bernd Buldt、2014、「ゲーデルの第一不完全性定理の範囲」、 Wayback Machineで 2016-03-06 にアーカイブ済み、Logica Universalis、v. 8、pp. 499–552。doi :10.1007/ s11787-014-0107-3
• チャールズワース、アーサー(1981) 。「コンピュータプログラムによるゲーデルの定理の証明」。数学雑誌。54 (3): 109–121。doi :10.2307/2689794。JSTOR  2689794。
• デイビス、マーティン (1965)。『決定不能: 決定不能な命題、解決不能な問題、計算可能な関数に関する基本論文』。レイヴン プレス。ISBN 978-0-911216-01-1。
• デイビス、マーティン(2006) 「不完全性定理」(PDF) AMSの通知53 ( 4): 414。
• ポール・フィンスラー（1926年）。 「形式的なBeweise und die Entscheidbarkeit」。数学的ツァイシュリフト。25 : 676–682。土井：10.1007/bf01283861。S2CID  121054124。
• グラッタン=ギネス、アイヴァー編 (2005)。『西洋数学のランドマーク著作 1640-1940』エルゼビア。ISBN 9780444508713。
• ファン・ハイエノールト、ジャン(1967)。 「ゲーデルの定理」。エドワーズ、ポール編著。哲学百科事典。 Vol. 3. マクミラン。 348–357ページ。
• ヘルマン、ジェフリー(1981)。「ゲーデルをフレーゲ＝ラッセルにする方法：ゲーデルの不完全性定理と論理主義」。Noûs . 15 ( 4 - 数学哲学特集号): 451–468。doi : 10.2307/2214847。ISSN 0029-4624。JSTOR  2214847  。
• デイヴィッド・ヒルベルト、1900 年、「数学の問題」。パリの国際数学者会議で行われた講演の英訳。ヒルベルトの第二の問題に関する発言が含まれています。
• Martin Hirzel、2000、「プリンキピア・マテマティカと関連システムの形式的に決定不可能な命題について I.」 ゲーデルの論文の英語訳。オリジナルからアーカイブ。2004 年 9 月 16 日。
• 菊池誠、田中一之（1994年7月）。「ゲーデルの定理のモデル理論的証明の形式化について」。ノートルダム形式論理ジャーナル。35 （3）：403–412。doi ： 10.1305/ ndjfl /1040511346。MR  1326122 。
• Kleene, SC (1943). 「再帰述語と量指定子」.アメリカ数学会誌. 53 (1): 41–73. doi :10.1090/S0002-9947-1943-0007371-8.デイビス1965年、255-287ページに再録
• Raatikainen, Panu (2020). 「ゲーデルの不完全性定理」. スタンフォード哲学百科事典. 2022年11月7日閲覧。
• Raatikainen, Panu (2005). 「ゲーデルの不完全性定理の哲学的関連性について」Revue Internationale de Philosophie . 59 (4): 513–534. doi :10.3917/rip.234.0513. S2CID  52083793.
• John Barkley Rosser、1936年、「ゲーデルとチャーチの定理の拡張」、Journal of Symbolic Logic、v. 1 (1936) pp. 87–91 から再版、Martin Davis 1965年、The Undecidable (loc. cit.) pp. 230–235。
• —、1939年、「ゲーデルの定理とチャーチの定理の証明の非公式な解説」、Journal of Symbolic Logic、v. 4 (1939) pp. 53–60 から転載、マーティン・デイビス 1965年、The Undecidable (loc. cit.) pp. 223–230
• Smoryński, C. (1977) 「不完全性定理」Jon Barwise (編) 『数理論理学ハンドブック』 アムステルダム: North-Holland Pub. Co. pp. 821–866. ISBN 978-0-444-86388-1。
• ウィラード、ダンE. (2001)。「自己検証公理システム、不完全性定理、および関連する反射原理」。Journal of Symbolic Logic。66 ( 2): 536–596。doi :10.2307/2695030。JSTOR  2695030。
• ザック、リチャード(2003)。「有限主義の実践: イプシロン計算とヒルベルトのプログラムにおける無矛盾性の証明」(PDF)。Synthese。137 ( 1  ) 。Springer Science and Business Media LLC: 211–259。arXiv : math/0102189。doi : 10.1023  / a:1026247421383。ISSN 0039-7857。S2CID 16657040。
• ザック、リチャード(2005)。「クルト・ゲーデル、不完全性定理に関する論文 (1931)」。グラッタン・ギネス、アイヴァー(編)。西洋数学のランドマーク著作 1640-1940。エルゼビア。pp. 917–925。doi :10.1016/b978-044450871-3/ 50152-2。ISBN 9780444508713。

• フランチェスコ・ベルト。『ゲーデルの秘密: 不完全性定理の完全ガイド』ジョン・ワイリー・アンド・サンズ。2010 年。
• Norbert Domeisen、1990年。アンチノミアンの論理。ベルン：ピーター・ラング。 142 S. 1990。ISBN 3-261-04214-1。Zbl  0724.03003。 
• フランツェン、トルケル（2005年）。ゲーデルの定理：その使用と濫用に関する不完全なガイド。ウェルズリー、マサチューセッツ州：AKピーターズ。ISBN 1-56881-238-8. MR  2146326。
• ダグラス・ホフスタッター、1979年。ゲーデル、エッシャー、バッハ：永遠の黄金の編み紐。ヴィンテージブックス。ISBN 0-465-02685-0。1999年再版：ISBN 0-465-02656-7。MR 530196  
• —  、2007年。私は奇妙なループです。ベーシックブックス。ISBN 978-0-465-03078-1。ISBN 0-465-03078-5。MR 2360307  
• スタンレー・ジャキ、OSB、2005年。量のドラマ。リアルビューブックス。
• Per Lindström、1997年。「不完全性の側面」、論理学講義ノートv.10。
• JR ルーカス、FBA、1970 年。 『意志の自由』クラレンドン プレス、オックスフォード、1970 年。
• エイドリアン・ウィリアム・ムーア、2022年。 『ゲーデルの定理：非常に短い入門』オックスフォード大学出版局、オックスフォード、2022年。
• アーネスト・ネーゲル、ジェームズ・ロイ・ニューマン、ダグラス・ホフスタッター、2002年（1958年）。ゲーデルの証明、改訂版 。ISBN 0-8147-5816-9。MR 1871678 
• ルディ・ラッカー、1995年（1982年）。『無限と心：無限の科学と哲学』プリンストン大学出版局。MR 658492
• スミス、ピーター（2007）。ゲーデルの定理入門。ケンブリッジ、イギリス：ケンブリッジ大学出版局。ISBN 978-0-521-67453-9. MR  2384958. 2005-10-23 にオリジナルからアーカイブ。2005-10-29に閲覧。
• Shankar, N. (1994)。メタ数学、マシン、ゲーデルの証明。ケンブリッジ理論計算機科学論文集。第38巻。ケンブリッジ：ケンブリッジ大学出版局。ISBN 0-521-58533-3。
• レイモンド・スマリヤン、1987年。永遠の未決定 ISBN 0192801414 - 形式体系における決定不能性に基づくパズル 
• —、1992年。ゲーデルの不完全性定理。オックスフォード大学出版局。ISBN 0195046722 
• —、1994年。対角化と自己言及。オックスフォード大学出版局。MR 1318913。ISBN 0198534507 
• —、2013年。『ゴデルのパズルブック：パズル、パラドックス、証明』。Courier Corporation。ISBN 978-0-486-49705-1。 
• 王昊（1996年）。『論理の旅：ゲーデルから哲学へ』MIT出版。ISBN 0-262-23189-1。 MR1433803​

• ベルト、フランチェスコ（2009）。「ゲーデルのパラドックスとウィトゲンシュタインの理由」。哲学数学III （17）。
• ドーソン、ジョン W. ジュニア (1996)。論理的ジレンマ: クルト・ゲーデルの生涯と業績。テイラー&フランシス。ISBN 978-1-56881-025-6。
• ドーソン、ジョン W. ジュニア (1997)。論理的ジレンマ: クルト・ゲーデルの生涯と業績。マサチューセッツ州ウェルズリー: AK ピーターズ。ISBN 978-1-56881-256-4. OCLC  36104240.
• レベッカ・ゴールドスタイン、2005年、「不完全性：クルト・ゲーデルの証明とパラドックス」、WWノートン＆カンパニー。ISBN 0-393-05169-2 
• フロイド、ジュリエット、パトナム、ヒラリー (2000)。「ゲーデルの定理に関するウィトゲンシュタインの「悪名高い段落」に関する注釈」。哲学ジャーナル。97 ( 11 )。JSTOR: 624–632。doi :10.2307 / 2678455。ISSN 0022-362X。JSTOR  2678455  。
• ハリソン、J. (2009)。『実用論理と自動推論ハンドブック』ケンブリッジ：ケンブリッジ大学出版局。ISBN 978-0521899574。
• David HilbertとPaul Bernays、Grundlagen der Mathematik、Springer-Verlag。
• ホップクロフト、ジョン E. ;ウルマン、ジェフリー(1979)。オートマトン理論、言語、計算入門。マサチューセッツ州レディング: アディソンウェスレー。ISBN 0-201-02988-X。
• ホフスタッター、ダグラス R. (2007) [2003]。「第 12 章 下向きの因果関係について」。私は奇妙なループです。ベーシック ブックス。ISBN 978-0-465-03078-1. 2019年5月8日時点のオリジナルよりアーカイブ。2018年10月24日閲覧。
• ジョーンズ、ジェームズ P. (1980)。「決定不可能なディオファントス方程式」(PDF)。アメリカ数学会報。3 (2): 859–862。doi : 10.1090/ S0273-0979-1980-14832-6。
• クリーネ、スティーブン・コール（1967）。数学論理学。ドーバー社、2002年再版。ISBN 0-486-42533-9 
• O'Connor, Russell (2005)。「Coq で検証された算術の本質的不完全性」。高階論理における定理証明。コンピュータサイエンスの講義ノート。第 3603 巻。pp. 245–260。arXiv : cs /0505034。doi :10.1007/ 11541868_16。ISBN 978-3-540-28372-0. S2CID  15610367。
• ポールソン、ローレンス(2014)。「遺伝的有限集合の理論に対するゲーデルの不完全性定理の機械支援による証明」。シンボリックロジックレビュー。7 (3): 484–498。arXiv : 2104.14260。doi : 10.1017  / S1755020314000112。S2CID 13913592。
• プリースト、グラハム（1984年）。「パラドックスの論理再考」。哲学論理ジャーナル。13 （2）：153-179。doi ： 10.1007/BF00453020。
• プリースト、グラハム (2004)。「ゲーデルの定理に関するウィトゲンシュタインのコメント」。マックス・ケルベル (編) 著『ウィトゲンシュタインの永続的な意義』。心理学出版。207～227 ページ。ISBN 978-1-134-40617-3。
• プリースト、グラハム（2006年）。 『矛盾の中で：超一貫性の研究』オックスフォード大学出版局。ISBN 0-19-926329-9。
• パトナム、ヒラリー(1960)。「心と機械」。シドニー・フック(編) 『心の次元: シンポジウム』。ニューヨーク大学出版局。アンダーソン、AR編、1964年『Minds and Machines』Prentice-Hall: 77に再版。
• Wolfgang Rautenberg、2010 年、「A Concise Introduction to Mathematical Logic」、第 3 版、Springer、ISBN 978-1-4419-1220-6 
• ロディッチ、ヴィクター（2003年）。「ゲーデルの誤解：ウィトゲンシュタインに関する新たな議論とウィトゲンシュタインによる新たな発言」。弁証法。57 （ 3）：279–313。doi ：10.1111/j.1746-8361.2003.tb00272.x 。 土井:10.1111/j.1746-8361.2003.tb00272.x
• シェラ、サハロン(1974)。「無限アーベル群、ホワイトヘッド問題、およびいくつかの構成」。 イスラエル数学ジャーナル。18 (3): 243–256。doi : 10.1007/ BF02757281。MR 0357114。
• シャピロ、スチュワート(2002)。「不完全性と不一致」。マインド。111 (444): 817–32。doi :10.1093/mind/111.444.817。
• ソーカル、アラン、ブリクモント、ジーン（1999）。『ファッショナブル・ナンセンス：ポストモダン知識人による科学の濫用』ピカドール。ISBN 0-312-20407-8。
• ショーンフィールド、ジョセフ R. (1967)。『数理論理学』マサチューセッツ州ネイティック：記号論理協会（2001 年出版）。ISBN 978-1-56881-135-2。
• スタングルーム、ジェレミー、ベンソン、オフィーリア（2006）。なぜ真実が重要なのか。コンティニュアム。ISBN 0-8264-9528-1。
• ジョージ・トゥーラキス『論理と集合論の講義』第 1 巻、数理論理学、ケンブリッジ大学出版局、2003 年。ISBN 978-0-521-75373-9 
• Wigderson, Avi (2010)。「数学におけるゲーデル現象: 現代的視点」(PDF)。Kurt Gödel と数学の基礎: 真実の地平。ケンブリッジ大学出版局。
• Hao Wang、1996、「論理の旅：ゲーデルから哲学へ」、MITプレス、ケンブリッジMA、ISBN 0-262-23189-1。 
• ザック、リチャード (2007)。「ヒルベルトのプログラムの過去と現在」。ジャケット、デール (編)。論理の哲学。科学哲学ハンドブック。第 5 巻。アムステルダム: エルゼビア。pp. 411–447。arXiv : math/0508572。doi : 10.1016/b978-044451541-4/ 50014-2。ISBN 978-0-444-51541-4. OCLC  162131413. S2CID  291599.

• BBCのIn Our Timeにおけるゲーデルの不完全性定理
• 2011 年 7 月 5 日、スタンフォード哲学百科事典に掲載されたジュリエット・ケネディによる「クルト・ゲーデル」の項目。
• スタンフォード哲学百科事典の Panu Raatikainen による「ゲーデルの不完全性定理」のエントリ、2013 年 11 月 11 日。
• スタンフォード哲学百科事典の矛盾論理§算術とゲーデルの定理の項目。
• MacTutor の経歴:
  • クルト・ゲーデル。2005年10月13日、 Wayback Machineにアーカイブ
  • ゲルハルト・ゲンツェン。
• 数学とは何か:ゲーデルの定理とその周辺、Karlis Podnieks著。オンラインの無料書籍。
• 印刷機を例にゲーデルの定理を世界最短で解説。
• 2011 年 10 月の RadioLab エピソード (ゲーデルの不完全性定理に関する内容を含む)
• 「ゲーデルの不完全性定理」、数学百科事典、EMS Press、2001 [1994]
• ゲーデルの証明の仕組み、ナタリー・ウォルチョーヴァー著、Quanta Magazine、2020年7月14日。
• [1] および [2] Isabelle/HOLで形式化されたゲーデルの不完全性定理

`