Loading article…
ゲーデルの不完全性定理は、形式的な公理理論における証明可能性の限界に関する数学論理学の2つの定理である。1931年にクルト・ゲーデルによって発表されたこれらの結果は、数学論理学と数学哲学の両方において重要である。これらの定理は、すべての数学に対して完全かつ無矛盾な公理系を見つけようとするヒルベルトの計画が不可能であることを示していると解釈される。[ 1 ]
第一不完全性定理は、有効な手順（すなわちアルゴリズム）によって定理を列挙できるような、一貫性のある公理系は、自然数の算術に関するすべての真理を証明できないと述べている。このような一貫性のある形式体系には、自然数に関する真であるが体系内では証明できない命題が必ず存在する。言い換えれば、自然数に関する偽であるが体系内で偽であることを証明できない命題が必ず存在する。
第2の不完全性定理は、第1の不完全性定理の拡張であり、そのようなシステムは自身の一貫性を証明できないことを示している。
対角線論法を用いたゲーデルの不完全性定理は、形式体系の限界に関する一連の密接に関連した定理の最初のもののひとつであった。これに続いて、タルスキによる真理の形式的定義不可能性に関する定義不可能性定理、ヒルベルトの決定問題が解けないことをチャーチが証明した定理、そして停止問題を解くアルゴリズムは存在しないことをチューリングが定理した。
不完全性定理は、自然数の基本的な算術を表現するのに十分な複雑さを持ち、かつ一貫性があり、効果的に公理化されている形式体系に適用されます。特に一階述語論理の文脈では、形式体系は形式理論とも呼ばれます。一般に、形式体系とは、特定の公理の集合と、公理から新しい定理を導出するための記号操作規則（または推論規則）からなる演繹装置です。このような体系の一例として、すべての変数が自然数を表すことを意図した一階ペアノ算術があります。集合論などの他の体系では、形式体系の一部の文のみが自然数に関する記述を表現します。不完全性定理は、非形式的な意味での「証明可能性」ではなく、これらの体系における形式的な証明可能性に関するものです。
形式体系が持ちうる特性には、完全性、一貫性、有効な公理系の存在など、いくつかある。不完全性定理によれば、十分な量の算術演算を含む体系は、これら3つの特性すべてを持つことはできない。
形式体系は、その定理の集合が再帰的に列挙可能である場合、効果的に公理化されている（効果的に生成されているとも呼ばれる）と言われます。これは、原理的には、定理ではない命題を列挙することなく、体系のすべての定理を列挙できるコンピュータ プログラムが存在することを意味します。効果的に生成された理論の例としては、ペアノ算術やツェルメロ・フレンケル集合論（ZFC）などがあります。[ 2 ]
真の算術と呼ばれる理論は、ペアノ算術の言語における標準整数に関するすべての真の命題から構成される。この理論は無矛盾かつ完全であり、十分な量の算術を含んでいる。しかしながら、再帰的に列挙可能な公理系を持たないため、不完全性定理の仮定を満たさない。
公理の集合は、その公理の言語の任意の命題について、その命題またはその否定が公理から証明できる場合に、 （構文的に、または否定的に）完全である。 [ 3 ]これは、ゲーデルの第一不完全性定理に関連する概念である。これは、公理の集合が与えられた言語のすべての意味的トートロジーを証明することを意味する意味的完全性と混同してはならない。ゲーデルは、完全性定理（ここで説明する不完全性定理と混同してはならない）において、一階述語論理が意味的に完全であることを証明した。しかし、一階述語論理の言語で表現できる文の中には、論理の公理だけでは証明も反証もできないものがあるため、構文的に完全ではない。
数学体系において、ヒルベルトのような思想家は、あらゆる数学的公式を証明したり（その否定を証明することによって）反証したりできるような公理系を見つけるのは時間の問題だと信じていた。
形式体系は、論理体系全般に言えるように、設計上、構文的に不完全な場合がある。あるいは、必要な公理がすべて発見または含まれていないために不完全な場合もある。例えば、平行線公準のないユークリッド幾何学は不完全である。なぜなら、言語内のいくつかの命題（平行線公準自体など）は、残りの公理から証明できないからである。同様に、稠密線形順序の理論は完全ではないが、順序に端点がないことを示す追加の公理を加えることで完全になる。連続体仮説は、 ZFCの言語における命題であるが、ZFC内では証明できないため、ZFCは完全ではない。この場合、問題を解決する新たな公理の候補は明らかに存在しない。
1階ペアノ算術の理論は一貫性があるように見える。これが実際にそうであると仮定すると、ペアノ算術は無限だが再帰的に列挙可能な公理系を持ち、不完全性定理の仮説を満たすのに十分な算術を符号化できることに注意する必要がある。したがって、最初の不完全性定理により、ペアノ算術は完全ではない。この定理は、ペアノ算術において証明も反証もできない算術命題の明示的な例を示している。さらに、この命題は通常のモデルでは真である。加えて、効果的に公理化された一貫性のあるペアノ算術の拡張は、完全ではあり得ない。
公理系は、その公理系から命題とその否定の両方が証明できるような命題が存在しない場合、 （単純に）無矛盾である。そうでない場合は無矛盾である。つまり、無矛盾な公理系とは、矛盾のない公理系のことである。
ペアノ算術はZFCから証明可能で一貫性がありますが、ZFC自体からは証明できません。同様に、ZFC自体からは証明可能で一貫性はありませんが、ZFC + 「到達不可能な基数が存在する」によってZFCの一貫性が証明されます。なぜなら、κがそのような最小の基数であれば、フォン・ノイマン宇宙内に存在するVκはZFCのモデルであり、理論が一貫性を持つのはモデルを持つ場合のみだからです。
ペアノ算術の言語におけるすべての命題を公理とみなすならば、この理論は完全であり、再帰的に列挙可能な公理の集合を持ち、加算と乗算を記述することができる。しかしながら、それは矛盾している。
矛盾する理論のさらなる例は、集合論において無制限の理解という公理体系を仮定した場合に生じるパラドックスから生じる。
不完全性定理は、自然数に関する十分な事実の集合を証明できる形式体系にのみ適用されます。十分な事実の集合の一つは、ロビンソン算術の定理の集合Qです。ペアノ算術のような一部の体系は、自然数に関する命題を直接表現できます。ZFC集合論のような他の体系は、自然数に関する命題をその言語に解釈することができます。これらのどちらの選択肢も、不完全性定理には適しています。
与えられた標数の代数的閉体の理論は、完全かつ無矛盾であり、無限ではあるが再帰的に列挙可能な公理系を持つ。しかしながら、この理論に整数を符号化することは不可能であり、整数の算術を記述することもできない。同様の例として、実閉体の理論があり、これは本質的にタルスキのユークリッド幾何学の公理系と同等である。したがって、ユークリッド幾何学自体（タルスキの定式化において）は、完全かつ無矛盾で、効果的に公理化された理論の一例である。
プレスバーガー算術体系は、自然数に対する加算演算のみを含む公理系から構成される（乗算は省略されている）。プレスバーガー算術は完全性、一貫性、再帰的列挙可能性を備えており、自然数の加算は符号化できるが乗算は符号化できない。このことから、ゲーデルの定理を実現するには、加算だけでなく乗算も符号化できる理論が必要であることがわかる。
ダン・ウィラード（2001 ）は、ゲーデル数体系を形式化するのに十分な関係としての算術を可能にするが、乗算を関数として持つほど強くなく、したがって第二不完全性定理を証明できない、弱い算術体系のいくつかの族を研究した。つまり、これらの体系は一貫性があり、自身の一貫性を証明できる（自己検証理論を参照）。
公理系を選択する際の目標の一つは、誤った結果を証明することなく、できるだけ多くの正しい結果を証明できるようにすることです。例えば、自然数に関するすべての真の算術的主張を証明できるような、真の公理系を想像することができます（Smith 2007 、p. 2）。一階述語論理の標準体系では、矛盾する公理系は、その言語のすべての命題を証明します（これは爆発原理と呼ばれることもあります）。したがって、自動的に完全になります。しかし、完全かつ矛盾のない公理系は、矛盾しない定理の最大集合を証明します。
前節でペアノ算術、ZFC、およびZFC +「到達不可能な基数が存在する」で示したパターンは、一般に破ることはできません。ここで、ZFC +「到達不可能な基数が存在する」は、それ自体から無矛盾であることを証明することはできません。また、ZFC +「到達不可能な基数が存在する」では解決不可能な連続体仮説[ 4 ]によって示されるように、完全でもありません。
第一不完全性定理は、基本的な算術を表現できる形式体系において、完全かつ無矛盾な有限個の公理リストを作成することは決してできないことを示している。すなわち、無矛盾な命題を公理として追加するたびに、その新しい公理を用いてもなお証明できない他の真の命題が存在する。もし体系を完全化するような公理が追加されるとすれば、それは体系を無矛盾にするという代償を伴う。無限個の公理リストであっても、完全かつ無矛盾で、かつ効果的に公理化されている状態はあり得ない。
ゲーデルの第一不完全性定理は、ゲーデルの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 'が存在します。G F 'は、 FではなくF 'を参照するという点でG Fとは異なります。
ゲーデル文は、間接的にそれ自身を参照するように設計されている。この文は、ある特定の手順のシーケンスを使用して別の文を構成する場合、その構成された文はF内で証明できないと述べている。しかし、その手順のシーケンスは、構成された文がG F自体となるようなものである。このようにして、ゲーデル文G F は、間接的にF内での自身の証明不可能性を述べている。[ 5 ]
第一不完全性定理を証明するために、ゲーデルは、システム内の証明可能性の概念は、システムの文のゲーデル数に作用する算術関数のみで表現できることを示した。したがって、数に関する特定の事実を証明できるシステムは、それが効果的に生成されている限り、自身の命題に関する事実も間接的に証明できる。システム内の命題の証明可能性に関する疑問は、数自体の算術的性質に関する疑問として表され、システムが完全であれば、これらの疑問はシステムによって決定可能となる。
したがって、ゲーデルの命題は間接的に体系Fの命題を参照するものの、算術的な命題として読むと、直接的には自然数のみを参照する。それは、原始再帰関係によって与えられる特定の性質を持つ自然数は存在しないと主張する（Smith 2007 、p. 141）。このように、ゲーデルの命題は、単純な構文形式で算術の言語で記述することができる。特に、それは、多数の先頭の全称量化子とそれに続く量化子のない本体からなる算術の言語の式として表現することができる（これらの式はレベル 算術的階層の）。MRDP定理により、ゲーデルの文は、整数係数を持つ多変数多項式は、その変数に整数を代入してもゼロの値を取ることはないという文として書き直すことができる（Franzén 2005 、p. 71）。
第一不完全性定理は、適切な形式理論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つの点でより一般化されている。これらの一般化された定理は、より広範なシステムに適用できるように表現されており、また、より弱い無矛盾性仮定を組み込むように表現されている。
ゲーデルは、特定の算術体系である『プリンキピア・マテマティカ』の体系の不完全性を証明したが、同様の証明は、一定の表現力を持つ任意の有効な体系に対しても可能である。ゲーデルはこの事実を論文の序文で言及しているが、具体性を保つために証明を一つの体系に限定した。現代の定理の記述では、有効性と表現力の条件を不完全性定理の仮説として述べるのが一般的であり、特定の形式体系に限定されないようになっている。これらの条件を述べるための用語は、ゲーデルが研究成果を発表した1931年にはまだ確立されていなかった。
ゲーデルの不完全性定理の元の記述と証明では、システムが単に一貫性があるだけでなく、ω-一貫性があるという仮定が必要です。システムがω-一貫性があるとは、ω-矛盾がない場合であり、ω-矛盾があるとは、任意の特定の自然数mに対してシステムが~ P ( m )を証明するような述語Pが存在し、かつシステムがP ( n )となるような自然数nが存在することも証明する場合です。つまり、システムは、性質Pを持つ数が存在すると言いながら、それが特定の値を持つことを否定します。システムのω-一貫性は、その一貫性を意味しますが、一貫性はω-一貫性を意味しません。J .バークレー・ロッサー（1936 ）は、システムがω-一貫性ではなく一貫性を持つことだけを要求する証明の変形（ロッサーのトリック）を見つけることで、不完全性定理を強化しました。これは主に技術的な関心事である。なぜなら、すべての真の形式的算術理論（公理がすべて自然数に関する真の命題である理論）はω-無矛盾であり、したがって、ゲーデルの定理は元の形でそれらに適用されるからである。ω-無矛盾ではなく無矛盾性のみを仮定する不完全性定理のより強いバージョンは、一般にゲーデルの不完全性定理、またはゲーデル＝ロッサーの定理として知られるようになった。
基本算術を含む各形式体系Fに対して、 Fの一貫性を表す式 Cons( F ) を標準的に定義することができる。この式は、「体系F内の形式的導出を符号化する自然数で、その結論が構文的矛盾となるものは存在しない」という性質を表す。構文的矛盾はしばしば「0=1」とされ、その場合 Cons( F ) は「 Fの公理から '0=1' の導出を符号化する自然数は存在しない」と述べる。
ゲーデルの第二不完全性定理は、一般的な仮定の下では、この標準的な無矛盾性命題 Cons( F ) はFで証明できないことを示しています。この定理は、ゲーデルの 1931 年の論文「プリンキピア・マテマティカおよび関連システムにおける形式的に決定不可能な命題について I」の「定理 XI」として初めて登場しました。次の記述では、「形式化されたシステム」という用語には、F が効果的に公理化されているという仮定も含まれています。この定理は、一定量の初等算術を実行できる無矛盾なシステムFについては、 F自体でFの無矛盾性を証明できないと述べています。[ 6 ]この定理は、第一不完全性定理で構築された命題がシステムの無矛盾性を直接表現していないため、第一不完全性定理よりも強力です。第二不完全性定理の証明は、第一不完全性定理の証明をシステムF自体で形式化することによって得られます。
第二不完全性定理には、 Fの一貫性をFの言語で式として表現する方法に関して、技術的な微妙な点があります。システムの一貫性を表現する方法は数多くあり、必ずしも同じ結果になるとは限りません。第二不完全性定理の式 Cons( F ) は、一貫性の特定の表現です。
Fが無矛盾であるという主張の他の形式化は、Fにおいて同値ではない場合があり、中には証明可能なものもあるかもしれません。例えば、一階ペアノ算術（PA）は、「PAの最大の無矛盾部分集合」が無矛盾であることを証明できます。しかし、PAは無矛盾であるため、PAの最大の無矛盾部分集合はPAそのものなので、この意味でPAは「無矛盾であることを証明している」と言えます。PAが証明していないのは、PAの最大の無矛盾部分集合が実際にはPA全体であるということです。（ここでいう「PAの最大の無矛盾部分集合」とは、特定の有効な列挙の下でのPAの公理の最大の無矛盾な初期セグメントを意味します。）
第2不完全性定理の標準的な証明では、証明可能性述語Prov A ( P )がヒルベルト・ベルネイスの証明可能性条件を満たすことを前提としている。式Pのゲーデル数を#( P )とすると、証明可能性条件は次のようになる。
ロビンソン算術のような体系は、第一不完全性定理の仮定を満たすほど強力ではあるものの、ヒルベルト＝ベルネイズ条件を証明するものではない。しかし、ペアノ算術はこれらの条件を検証するのに十分な強さを持ち、ペアノ算術よりも強力なすべての理論も同様である。
ゲーデルの第二不完全性定理は、上記の技術的条件を満たすシステムF 1は、 F 1の無矛盾性を証明するシステムF 2の無矛盾性を証明できないことも示唆している。これは、そのようなシステムF 1 は、 F 2 がF 1の無矛盾性を証明すれば、F 1は実際には無矛盾であることを証明できるからである。F 1 が無矛盾であるという主張は、 「すべての数nに対して、n はF 1における矛盾の証明のコードではないという決定可能な性質を持つ」という形式をとる。もしF 1 が実際には無矛盾であれば、F 2 はあるnに対して、nがF 1における矛盾のコードであることを証明するだろう。しかし、F 2 がF 1が無矛盾であることも証明した場合（つまり、そのようなnが存在しない場合）、F 2 自体が無矛盾となる。この推論は、F 1において形式化することで、 F 2が無矛盾であれば、F 1も無矛盾であることを示すことができる。第二不完全性定理により、F 1 は自身の無矛盾性を証明していないため、 F 2の無矛盾性も証明できない。
この第二不完全性定理の系は、例えば、ペアノ算術（PA）においてその一貫性が証明可能な体系で形式化できる有限的な手段を用いてペアノ算術の一貫性を証明することは不可能であることを示している。例えば、有限数学の正確な形式化として広く受け入れられている原始再帰算術（PRA）体系は、PAにおいて一貫性が証明可能である。したがって、PRAはPAの一貫性を証明することはできない。この事実は一般的に、理想的な（無限主義的な）数学原理が「現実の」（有限主義的な）数学的命題の証明において、それらの原理が一貫性を持つことを有限主義的に証明することによって正当化することを目的としたヒルベルトの計画は実行不可能であることを意味すると考えられている。[ 7 ]
この系は、第二不完全性定理の認識論的重要性も示している。システムF がその無矛盾性を証明したとしても、興味深い情報は得られないだろう。なぜなら、矛盾した理論は、その無矛盾性を含め、すべてを証明するからである。したがって、FにおけるFの無矛盾性証明は、 Fが無矛盾であるかどうかの手がかりを与えず、そのような無矛盾性証明によってFの無矛盾性に関する疑念が解消されることはない。無矛盾性証明の興味深い点は、システムFの無矛盾性を、ある意味でF自体よりも疑わしいものが少ない、例えばFよりも弱いシステムF 'で証明できる可能性にある。多くの自然発生的な理論FとF'、例えばF = ツェルメロ・フレンケル集合論とF' = 原始再帰算術の場合、 F'の無矛盾性はFで証明可能であり、したがって、F' は上記の第二不完全性定理の系によってFの無矛盾性を証明することはできない。
第二不完全性定理は、異なる公理を持つ別の体系の無矛盾性を証明する可能性を完全に排除するものではない。例えば、ゲルハルト・ゲンツェンは、ε₀と呼ばれる順序数が整礎的であるという公理を含む別の体系において、ペアノ算術の無矛盾性を証明した（ゲンツェンの無矛盾性証明を参照）。ゲンツェンの定理は、証明論における順序数解析の発展を促した。
数学とコンピュータ科学において、「決定不能」という言葉には2つの異なる意味があります。1つ目は、ゲーデルの定理に関連して用いられる証明論的な意味で、特定の演繹体系において、ある命題が証明も反駁もできない状態を指します。2つ目の意味は、ここでは触れませんが、計算可能性理論に関連して用いられるもので、命題ではなく、可算無限個の質問からなる決定問題に適用されます。決定問題とは、それぞれが「はい」か「いいえ」の答えを必要とする質問の集合です。このような問題は、問題集合内のすべての質問に正しく答える計算可能な関数が存在しない場合、決定不能であると言われます（決定不能問題を参照）。
「決定不能」という言葉には二つの意味があるため、「証明も反証もできない」という意味では、「決定不能」の代わりに「独立」という言葉が使われることがある。
ある特定の演繹体系における命題の決定不能性は、それ自体では、その命題の真偽値が明確に定義されているか、あるいは他の手段で決定できるかという問題には答えない。決定不能性とは、検討対象の特定の演繹体系ではその命題の真偽を証明できないことを意味するにすぎない。真偽値が決して分からない、あるいは明確に定義されていない、いわゆる「絶対的に決定不能な」命題が存在するかどうかは、数学哲学において議論の的となっている。
ゲーデルとポール・コーエンの共同研究により、決定不能な命題（第一の意味で）の具体的な例が2つ示された。連続体仮説はZFC （集合論の標準的な公理系）では証明も反証もできず、選択公理はZF（選択公理を除くZFCのすべての公理）では証明も反証もできない。これらの結果は不完全性定理を必要としない。ゲーデルは1940年に、これらの命題はいずれもZFまたはZFC集合論では反証できないことを証明した。1960年代にコーエンは、どちらもZFからは証明できず、連続体仮説はZFCからは証明できないことを証明した。
シェラ（1974）は、群論におけるホワイトヘッド問題は、標準集合論においては、その用語の最初の意味で決定不能であることを示した。 [ 8 ]
グレゴリー・チャイティンは、アルゴリズム情報理論において決定不能な命題を生み出し、その枠組みの中で別の不完全性定理を証明した。チャイティンの不完全性定理は、十分な算術演算を表現できる任意のシステムに対して、ある上限cが存在し、そのシステムにおいて特定の数値のコルモゴロフ複雑度がcより大きいことを証明することはできないと述べている。ゲーデルの定理が嘘つきのパラドックスに関連しているのに対し、チャイティンの結果はベリーのパラドックスに関連している。
これらは、ゲーデルの「真であるが決定不能」な命題に相当する、数学的に自然な表現である。これらは、一般的に有効な推論形式として認められているより大きな体系では証明できるが、ペアノ算術のようなより限定された体系では決定不能である。
1977年、パリスとハリントンは、無限ラムゼーの定理の一種であるパリス＝ハリントン原理が（一階）ペアノ算術では決定不能であるが、より強力な二階算術体系では証明できることを証明した。その後、カービーとパリスは、パリス＝ハリントン原理よりもやや単純な自然数列に関する定理であるグッドスタインの定理も、ペアノ算術では決定不能であることを示した。
コンピュータ科学に応用されているクラスカルの木の定理は、ペアノ算術では決定不能だが、集合論では証明可能である。実際、クラスカルの木の定理（またはその有限形式）は、予測主義と呼ばれる数学の哲学に基づいて許容される原理をコード化した、はるかに強力なシステムATR 0では決定不能である。[ 9 ] 関連するが、より一般的なグラフ小定理（2003）は、計算複雑性理論に影響を与える。
不完全性定理は、再帰理論における決定不能集合に関するいくつかの結果と密接に関連している。
クリーネ（1943）は、計算可能性理論の基本結果を用いてゲーデルの不完全性定理の証明を提示した。そのような結果の一つは、停止問題が決定不能であることを示している。つまり、任意のプログラムPを入力として与えられた場合、特定の入力で実行したときにP が最終的に停止するかどうかを正しく判定できるコンピュータ プログラムはない。クリーネは、ある一定の一貫性特性を持つ完全な有効算術体系が存在すると、停止問題が決定可能になることを示し、これは矛盾であるとした。 [ 10 ]この証明方法は、ショーエンフィールド（1967）、チャールズワース（1981）、ホップクロフト＆ウルマン（1979）によっても提示されている。[ 11 ]
Franzén (2005)は、ヒルベルトの第 10 問題に対するMatiyasevich の解が、ゲーデルの第 1 不完全性定理の証明を得るためにどのように使用できるかを説明しています。 [ 12 ] Matiyasevich は、整数係数を持つ多変数多項式p ( x 1 , x 2 ,..., x k )が与えられたときに、方程式p = 0 に整数解が存在するかどうかを判定するアルゴリズムは存在しないことを証明しました。整数係数を持つ多項式と整数自体は算術の言語で直接表現できるため、多変数整数多項式方程式p = 0 が整数に解を持つ場合、十分強力な算術システムTはこれを証明します。さらに、システムTが ω-整合的であると仮定します。その場合、整数に解がない場合、特定の多項式方程式に解が存在することを証明することはありません。したがって、T が完全かつ ω-整合的であれば、マティヤセビッチの定理に反して、「p には解がある」または「p には解がない」のいずれかが見つかるまでTの証明を列挙するだけで、多項式方程式に解があるかどうかをアルゴリズム的に決定することが可能になります。したがって、 T はω-整合的かつ完全ではあり得ません。さらに、整合的に有効に生成されたシステムTごとに、整数上の多変数多項式p を有効に生成して、方程式p = 0 が整数上で解を持たないようにすることは可能ですが、解がないことはTでは証明できません。[ 13 ]
スモリンスキー（1977）は、再帰的に分離不可能な集合の存在を利用して、最初の不完全性定理を証明する方法を示した。この証明は、ペアノ算術のようなシステムが本質的に決定不能であることを示すために拡張されることが多い。[ 14 ]
チャイティンの不完全性定理は、コルモゴロフ複雑性に基づいて独立文を生成する別の方法を提供する。前述のクリーネによる証明と同様に、チャイティンの定理は、すべての公理が自然数の標準モデルで真であるという追加特性を持つ理論にのみ適用される。ゲーデルの不完全性定理は、標準モデルに偽の命題を含むにもかかわらず、一貫性のある理論に適用できるという点で区別される。これらの理論はω-不一貫性として知られている。
背理法には3つの重要な部分があります。まず、提案された基準を満たす形式体系を選択します。
先ほど述べた証明を具体的に示す際の主な問題は、まず「 pは証明できない」と同等の命題pを構成するには、 pが何らかの形でpへの参照を含まなければならず、それが容易に無限後退を引き起こす可能性があるように思われることである。ゲーデルの手法は、命題を数値に対応付けることができる（しばしば構文の算術化と呼ばれる）ことを示すことで、「命題を証明する」ことを「数値が与えられた性質を持つかどうかをテストする」に置き換えることができるようにすることである。これにより、定義の無限後退を回避する形で自己参照的な式を構築することができる。同じ手法は後にアラン・チューリングが決定問題に関する研究で使用した。
簡単に言えば、システム内で定式化できるすべての数式や文に、ゲーデル数と呼ばれる固有の数値を割り当てる方法を考案すれば、数式とゲーデル数の間を機械的に相互変換することが可能になります。関係する数値は（桁数的に）非常に長くなる可能性がありますが、これは障害にはなりません。重要なのは、そのような数値を構築できることです。簡単な例として、英語を各文字に対応する数値のシーケンスとして格納し、それらを組み合わせて1つの大きな数値にする方法が挙げられます。
原則として、ある命題の真偽を証明することは、その命題に一致する数が特定の性質を持つか否かを証明することと同等であることが示せる。形式体系は、一般的に数に関する推論を支えるのに十分な強度を備えているため、数式や命題を表す数に関する推論も支えることができる。重要なのは、この体系が数の性質に関する推論を支えることができるため、その結果は、それらと同等の命題の証明可能性に関する推論と同等であるということである。
原理的には、このシステムが証明可能性について間接的に主張できることを示した上で、主張を表す数値の特性を分析することにより、実際に証明可能性について主張する主張を作成する方法を示すことができる。
自由変数x をちょうど 1 つ含む式F ( x )は、ステートメント形式またはクラス記号と呼ばれます。xを特定の数に置き換えると、ステートメント形式は正真正銘のステートメントに変わり、システム内で証明可能か、そうでないかが決まります。特定の式については、すべての自然数nに対して、が成り立つことを示すことができます。 は、証明できる場合に限り真である（元の証明における厳密な要件はより緩いが、証明の概略としてはこれで十分である）。特に、これは「2 × 3 = 6」のような、有限個の自然数間のあらゆる具体的な算術演算について真である。
命題形式そのものは命題ではないため、証明も反証もできません。しかし、すべての命題形式F ( x )には、ゲーデル数G ( F )を割り当てることができます。形式F ( x )で使用される自由変数の選択は、ゲーデル数G ( F )の割り当てには関係ありません。
証明可能性の概念自体も、ゲーデル数によって次のように表現できます。証明は特定の規則に従う命題のリストであるため、証明のゲーデル数を定義できます。すると、任意の命題pに対して、数xがその証明のゲーデル数であるかどうかを問うことができます。p のゲーデル数と、その証明の潜在的なゲーデル数であるxとの関係は、2 つの数の間の算術的関係です。したがって、この算術的関係を用いて、 yの証明のゲーデル数が存在することを示す命題形式Bew ( y )が存在します。
Bewという名前は、ドイツ語で「証明可能」を意味するbeweisbarの略です。この名前はもともとゲーデルが、先ほど説明した証明可能性の公式を表すために使用しました。「Bew ( y ) 」は、 Tの元の言語における特定の非常に長い公式を表す単なる略語であり、文字列「Bew」自体はこの言語の一部であるとは主張されていません。
式Bew ( y )の重要な特徴は、命題p がシステム内で証明可能であれば、Bew ( G ( p ))も証明可能であるということです。これは、 pの証明には対応するゲーデル数が存在し、その存在によってBew( G ( p ))が満たされるためです。
証明の次のステップは、間接的に自身の証明不可能性を主張する命題を得ることである。ゲーデルはこの命題を直接構成したが、少なくとも1つのそのような命題の存在は、対角線補題から導かれる。対角線補題は、十分強い形式体系と任意の命題形式Fに対して、体系が証明するような命題pが存在すると述べている。
F をBew ( x )の否定とすることで、次の定理が得られます。
そして、これによって定義される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に対して、pは証明可能ではないため (前の段落から)、x はpの証明のゲーデル数にはなり得ません。したがって、一方では、ある性質 (それがpの証明のゲーデル数であること) を持つ数が存在することを証明しますが、他方では、特定の数xに対して、それがこの性質を持たないことを証明できます。これは ω-整合的なシステムでは不可能です。したがって、 pの否定は証明できません。
したがって、命題pは我々の公理系においては決定不能である。すなわち、この体系内では証明も反証もできない。
実際、pが証明不可能であることを示すには、システムが無矛盾であるという仮定だけで十分です。pの否定が証明不可能であることを示すには、より強いω無矛盾性の仮定が必要です。したがって、pが特定のシステムに対して構築されている場合、次のようになります。
システムの不完全性を回避するために「不足している公理を追加」しようとすると、pまたは「not p」のいずれかを公理として追加する必要があります。しかし、そうすると、命題の「証明のゲーデル数である」という定義が変わります。つまり、式Bew ( x )が異なってしまうということです。したがって、この新しい Bew に対角補題を適用すると、以前の命題とは異なる新しい命題pが得られます。この命題が ω-無矛盾であれば、新しいシステムでは決定不能になります。
ブーロス（1989）は、嘘つきのパラドックスではなくベリーのパラドックスを用いて、真であるが証明不可能な式を構成する、第一不完全性定理の別の証明を概説している。同様の証明方法は、ソール・クリプキによって独立に発見された。[ 15 ]ブーロスの証明は、算術の真の文の任意の計算可能列挙可能な集合Sに対して、 Sに含まれない真である別の文を構成することによって進められる。これにより、第一不完全性定理が系として得られる。ブーロスによれば、この証明は、有効で一貫性のある算術理論の不完全性に対する「異なる種類の理由」を提供する点で興味深い。[ 16 ]
不完全性定理は、証明支援ソフトウェアによって完全に検証可能な形式化された定理へと変換された、比較的少数の非自明な定理の一つである。ゲーデルによる不完全性定理の元の証明は、ほとんどの数学的証明と同様に、人間が理解できるように自然言語で書かれていた。
最初の不完全性定理のコンピュータ検証証明は、1986年にナタラジャン・シャンカーがNqthmを用いて発表し（シャンカー 1994 ）、2003年にラッセル・オコナーがRocq （以前はCoqとして知られていた）を用いて発表し（オコナー 2005 ）、2009年にジョン・ハリソンがHOL Lightを用いて発表した（ハリソン 2009 ）。両方の不完全性定理のコンピュータ検証証明は、2013年にローレンス・ポールソンがIsabelleを用いて発表した（ポールソン 2014 ）。
第二不完全性定理を証明する際の主な難点は、第一不完全性定理の証明で用いられる証明可能性に関する様々な事実を、証明可能性を表す形式述語Pを用いてシステムS内で形式化できることを示すことである。これができれば、システムS内で第一不完全性定理の証明全体を形式化することで、第二不完全性定理が導かれる。
上記で構築した決定不能な文をpとし、矛盾を得るために、システムSの一貫性がシステムS自体の内部から証明できると仮定します。これは、「システムS は一貫性がある」という命題を証明することと同等です。次に、命題cを考えます。ここで、c = 「システムSが一貫性がある場合、pは証明できない」です。文cの証明はシステムS内で形式化できるため、命題c、「pは証明できない」（または同様に、「not P ( p )」）はシステムS内で証明できます。
ここで注目すべきは、システムS が無矛盾であることを証明できれば (すなわち、仮説cの記述が証明できれば)、 p が証明不可能であることを証明したことになる、という点です。しかし、これは矛盾です。なぜなら、第一不完全性定理によれば、この文 (すなわち、文cに含まれる「pは証明不可能である」) は、証明不可能であると構築されるものだからです。これが、第一不完全性定理をSで形式化する必要がある理由です。第二不完全性定理を証明するには、第一不完全性定理との矛盾を得る必要がありますが、これは定理がSで成り立つことを示すことによってのみ可能です。したがって、システムSが無矛盾であることを証明することはできません。そして、第二不完全性定理の記述が導き出されます。
不完全性に関する結果は、数学の哲学、特に単一の形式論理体系を用いて原理を定義する形式主義の諸形態に影響を与える。
不完全性定理は、ゴットロープ・フレーゲとバートランド・ラッセルが提唱した論理主義のプログラム（論理によって自然数を定義することを目的としていた）にとって深刻な結果をもたらすとされることがある。[ 17 ]ボブ・ヘイルとクリスピン・ライトは、不完全性定理は算術と同様に一階述語論理にも適用されるため、論理主義にとって問題ではないと主張する。彼らは、この問題は自然数が一階述語論理によって定義されるべきだと信じている人だけが抱えていると主張する。
多くの論理学者は、ゲーデルの不完全性定理が、数学における有限的無矛盾性の証明を求めたダヴィッド・ヒルベルトの第二問題に致命的な打撃を与えたと考えている。特に第二不完全性定理は、この問題を不可能にしたとみなされることが多い。しかし、すべての数学者がこの分析に同意しているわけではなく、ヒルベルトの第二問題の現状はまだ確定していない（「問題の現状に関する現代の見解」を参照）。
哲学者JRルーカスや物理学者ロジャー・ペンローズをはじめとする多くの研究者が、ゲーデルの不完全性定理が人間の知能について何を暗示しているのか、あるいは何も示唆していないのかについて議論を重ねてきた。議論の多くは、人間の精神がチューリングマシンと同等であるかどうか、あるいはチャーチ＝チューリングのテーゼによれば、あらゆる有限機械と同等であるかどうかという点に集中している。もしそうであれば、そしてその機械が無矛盾であれば、ゲーデルの不完全性定理が適用されることになる。
パトナム（1960）は、ゲーデルの定理は人間には適用できないが、人間は間違いを犯し、したがって矛盾しているため、科学や数学全般における人間の能力には適用できると示唆した。それが矛盾しないと仮定すると、その矛盾性を証明できないか、チューリングマシンで表現できないかのどちらかである。[ 18 ]
ウィグダーソン（2010）は、数学的な「認識可能性」の概念は論理的決定可能性ではなく計算複雑性に基づくべきだと提唱している。彼は、「認識可能性が現代の基準、すなわち計算複雑性によって解釈される場合、ゲーデル現象は依然として存在する」と述べている。[ 19 ]
ダグラス・ホフスタッターは著書『ゲーデル、エッシャー、バッハ』および『私は奇妙なループ』の中で、ゲーデルの定理を、彼が「奇妙なループ」と呼ぶものの例として挙げている。これは、公理的な形式体系の中に存在する階層的で自己参照的な構造である。彼は、これが人間の心における意識、つまり「私」という感覚を生み出すのと同じ種類の構造であると主張する。ゲーデルの定理における自己参照は、プリンキピア・マテマティカの形式体系の中で証明不可能性を主張するゲーデルの定理文に由来するが、人間の心における自己参照は、脳が刺激を抽象化し、「シンボル」、つまり概念に反応するニューロンのグループに分類する方法に由来する。これもまた実質的には形式体系であり、最終的には知覚を行う実体の概念をモデル化したシンボルを生み出すのである。ホフスタッターは、十分に複雑な形式体系における奇妙なループが、「下方」または「逆さま」の因果関係、つまり通常の因果関係の階層が逆転する状況を生み出す可能性があると主張する。ゲーデルの定理の場合、これは簡単に言えば次のようになる。
公式の意味を知るだけで、公理から体系的に「上へ」と進むという昔ながらの方法で導出する努力をすることなく、その真偽を推論することができる。これは単に奇妙というだけでなく、驚くべきことである。通常、数学的予想が何を言っているかを見て、その記述の内容だけに頼って、その記述が真か偽かを推論することはできない。[ 20 ]
はるかに複雑な形式体系である心の場合、この「下方因果律」は、ホフスタッターの見解では、私たちの心の因果関係は、ニューロン間の相互作用や素粒子といった低レベルではなく、欲望、概念、人格、思考、アイデアといった高レベルにあるという、言い表せない人間の本能として現れる。もっとも、物理学によれば、後者が因果力を持っているように見えるのだが。
このように、人間が世界を認識する通常の方法には奇妙な逆説性がある。現実を動かす実際の原動力は微小な領域にあるように思われるにもかかわらず、私たちは「小さなもの」ではなく「大きなもの」を認識するようにできているのだ。[ 20 ]
ゲーデルの定理は通常、古典論理の文脈で研究されるが、矛盾のない論理や本質的に矛盾する命題（ダイアレテイア）の研究においても役割を果たしている。プリースト（1984、2006 ）は、ゲーデルの定理における形式的証明の概念を通常の非形式的証明の概念に置き換えることで、素朴数学が矛盾していることを示すことができ、これをダイアレテイアの証拠として用いている。[ 21 ]この矛盾の原因は、システムの言語内にシステムの真理述語が含まれていることである。[ 22 ]シャピロ（2002）は、ゲーデルの定理のダイアレテイアへの応用について、より複雑な評価を下している。[ 23 ]
数学や論理学の枠を超えた議論を支持するために、定理の不完全性への訴えや類推が行われることがある。フランツェン (2005)、ラーティカイネン (2005)、ソーカル&ブリックモン (1999) 、スタングルーム&ベンソン (2006)など、数名の著者がこうした拡張や解釈に否定的なコメントをしている。[ 24 ] 例えば、ソーカル&ブリックモン (1999)とスタングルーム&ベンソン (2006)は、レベッカ ゴールドスタインの、ゲーデルが公言するプラトン主義と、彼の考えが時として反実在論的に用いられることとの間の不一致についてのコメントを引用している。ソーカル&ブリックモン (1999)は、社会学の文脈で定理を援用するレジス ドブレイを批判している。ドブレイはこの用法を比喩的なものとして擁護している (同上)。[ 25 ]
ゲーデルは1929年に博士論文として完全性定理の証明を発表した後、教授資格取得のための2つ目の問題に取り組んだ。彼の当初の目標は、ヒルベルトの2つ目の問題に対する肯定的な解を得ることであった。[ 26 ]当時、2階算術に似た自然数と実数の理論は「解析学」として知られており、自然数のみの理論は「算術」として知られていた。
ゲーデルだけが無矛盾性の問題に取り組んでいたわけではない。アッカーマンは1925年に解析学の無矛盾性の証明を発表したが、その証明には欠陥があり、ヒルベルトが最初に開発したε置換法を用いようとしていた。同年後半、フォン・ノイマンは帰納法の公理を用いない算術体系の証明を修正することができた。1928年までに、アッカーマンは修正した証明をベルネイスに伝えた。この修正された証明を受けて、ヒルベルトは1929年に算術の無矛盾性が証明され、解析学の無矛盾性の証明も間もなく得られるだろうと確信していると発表した。不完全性定理の発表によってアッカーマンの修正された証明が誤りであることが明らかになった後、フォン・ノイマンはその主要な手法が不健全であることを示す具体的な例を示した。[ 27 ]
ゲーデルは研究の過程で、その偽を主張する文はパラドックスを引き起こすが、その証明不可能性を主張する文はパラドックスを引き起こさないことを発見した。特に、ゲーデルは後にタルスキの不確定性定理と呼ばれる結果を認識していたが、それを公表することはなかった。ゲーデルは1930年8月26日にカルナップ、ファイグル、ワイスマンに最初の不完全性定理を発表した。4人は翌週にケーニヒスベルクで開催された重要な会議である第2回精密科学認識論会議に出席した。
1930年のケーニヒスベルク会議は、3つの学術団体の合同会議であり、当時の主要な論理学者の多くが出席した。カルナップ、ハイティング、フォン・ノイマンはそれぞれ、論理主義、直観主義、形式主義の数学的哲学について1時間の講演を行った。[ 28 ]この会議には、ゲッティンゲン大学の職を辞するヒルベルトの退任講演も含まれていた。ヒルベルトはこの講演で、すべての数学的問題は解決できるという自身の信念を主張した。彼は講演を次のように締めくくった。
数学者にとって無知な者など存在しない。そして私の意見では、自然科学においても全く存在しない。……誰も解決不可能な問題を見つけられなかった真の理由は、私の意見では、解決不可能な問題など存在しないからである。愚かな無知な者とは対照的に、我々の信条はこう断言する。「我々は知らなければならない。我々は必ず知るのだ！」
この演説はすぐにヒルベルトの数学に関する信念の要約として知られるようになった（最後の6語「我々は知らなければならない。我々は知ることになる！」は1943年にヒルベルトの墓碑銘として使われた）。ゲーデルはおそらくヒルベルトの演説に出席していたが、二人は直接会うことはなかった。[ 29 ]
ゲーデルは、会議の3日目の円卓討論会で、自身の最初の不完全性定理を発表した。この発表は、ゲーデルを呼び出して話をしたフォン・ノイマンを除いて、ほとんど注目を集めなかった。その年の後半、フォン・ノイマンは、最初の不完全性定理の知識を基に独自に研究を進め、2番目の不完全性定理の証明を得て、1930年11月20日付の手紙でゲーデルにそのことを伝えた。[ 30 ]ゲーデルは独自に2番目の不完全性定理を得て、それを提出した原稿に含め、 1930年11月17日にMonatshefte für Mathematikに受理された。
ゲーデルの論文は、1931年に『Monatshefte』に「Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I」（「プリンキピア・マテマティカおよび関連システムにおける形式的に決定不可能な命題について I 」）というタイトルで掲載された。タイトルが示すように、ゲーデルは当初、この論文の第二部を『 Monatshefte』の次の巻に掲載する予定だったが、第一部がすぐに受理されたことが、彼が計画を変更した理由の一つだった。[ 31 ]
ゲーデルは1933年から1934年にかけてプリンストン大学で、チャーチ、クリーネ、ロッサーらを聴衆に、自身の定理に関する一連の講義を行った。この時までに、ゲーデルは自身の定理に必要な重要な性質は、体系が有効であること（当時は「一般再帰性」という用語が使われていた）であると理解していた。ロッサーは1936年に、ゲーデルの元の証明の不可欠な部分であったω-無矛盾性の仮説は、ゲーデルの命題を適切に変更すれば、単純な無矛盾性で置き換えることができることを証明した。これらの進展により、不完全性定理は基本的に現代の形になった。
ゲンツェンは1936年に一階算術の無矛盾性証明を発表した。ヒルベルトはこの証明を「有限」なものとして受け入れたが、（ゲーデルの定理が既に示していたように）無矛盾性が証明されている算術体系の中で形式化することはできない。
不完全性定理がヒルベルトの研究計画に与えた影響はすぐに認識された。ベルネイズは『数学の基礎』（1939年）第2巻に、不完全性定理の完全な証明を掲載し、さらにアッカーマンによるε置換法に関する結果やゲンツェンによる算術の無矛盾性証明も併せて紹介した。これは、第2不完全性定理の完全な証明として初めて公表されたものである。
フィンスラー（1926）は、リチャードのパラドックスの一種を用いて、彼が開発した特定の非形式的な枠組みでは偽であるが証明不可能な式を構築した。[ 32 ]ゲーデルは、不完全性定理を証明した時（『著作集』第4巻、 9ページ）、この論文の存在を知らなかった。フィンスラーは1931年にゲーデルに手紙を書き、この論文について知らせた。フィンスラーは、この論文が不完全性定理の優先権を持つと考えていた。フィンスラーの方法は形式化された証明可能性に依拠しておらず、ゲーデルの研究とは表面的な類似点しかなかった。[ 33 ]ゲーデルはこの論文を読んだが、重大な欠陥があると見なし、フィンスラーへの返答の中で形式化の欠如について懸念を表明した。[ 34 ]フィンスラーは、その後も形式化を避ける自身の数学哲学を主張し続けた。
1931 年 9 月、エルンスト・ツェルメロはゲーデルに手紙を書き、ゲーデルの議論に「本質的な欠陥」があると告げた。[ 35 ] 10 月、ゲーデルは 10 ページの手紙で返信し、ツェルメロがシステムにおける真理の概念はそのシステム内で定義可能であると誤って仮定していることを指摘した。タルスキの定義不可能性定理によれば、それは一般には真ではない。[ 36 ]しかし、ツェルメロは譲歩せず、「若い競争相手に対するかなり辛辣な段落」を添えて批判を出版した。[ 37 ]ゲーデルは、この問題をさらに追求するのは無意味だと判断し、カルナップも同意した。[ 38 ]ツェルメロのその後の研究の多くは、一階述語論理よりも強い論理に関連しており、彼はそれを用いて数学理論の一貫性と範疇性の両方を示すことを望んでいた。
ルートヴィヒ・ヴィトゲンシュタインは、不完全性定理についていくつかの文章を書いており、それらは1953年に死後出版された『数学の基礎に関する考察』に収められている。特に、ラッセルの体系における「真」と「証明可能」の概念を混同しているように見える「悪名高い段落」と呼ばれる箇所がある。ゲーデルは、ヴィトゲンシュタインの初期の理想言語哲学と『論理哲学論考』がウィーン学団の思想を支配していた時期に、ウィーン学団の一員であった。ヴィトゲンシュタインが不完全性定理を誤解していたのか、それとも単に不明瞭に表現していただけなのかについては、議論がある。ゲーデルの遺稿には、ヴィトゲンシュタインが自分の考えを誤解していたという見解が示されている。
複数の評論家がウィトゲンシュタインはゲーデルを誤解していると解釈しているが、フロイドとパトナム（2000）およびプリースト（2004）は、ほとんどの評論がウィトゲンシュタインを誤解していると主張するテキスト解釈を提供している。[ 39 ]出版後、バーネイズ、ダメット、クライゼルはウィトゲンシュタインの発言についてそれぞれレビューを書いたが、いずれも極めて否定的だった。[ 40 ]この批判の一致により、ウィトゲンシュタインの不完全性定理に関する発言は論理学界にほとんど影響を与えなかった。1972年、ゲーデルは「ウィトゲンシュタインは正気を失ったのか？彼は本気で言っているのか？彼は意図的に自明なナンセンスな発言をしている」と述べ、カール・メンガーに ウィトゲンシュタインの発言は不完全性定理の誤解を示していると書き送った。
あなたが引用した箇所から明らかなように、ウィトゲンシュタインは（第一不完全性定理を）理解していなかった（あるいは理解していないふりをしていた）。彼はそれを一種の論理的パラドックスとして解釈したが、実際には正反対で、数学の全く議論の余地のない分野（有限数論または組み合わせ論）における数学的定理である。[ 41 ]
2000年にウィトゲンシュタインの遺稿が出版されて以来、哲学分野では、ウィトゲンシュタインの発言に対する当初の批判が正当であったかどうかを評価しようとする一連の論文が発表されている。フロイドとパトナム（2000）は、ウィトゲンシュタインは不完全性定理について、これまで想定されていたよりも完全な理解を持っていたと主張している。彼らは特に、ω-矛盾体系に対するゲーデル文を「私は証明できない」と解釈することに懸念を抱いている。なぜなら、その体系には、証明可能性述語が実際の証明可能性に対応するモデルが存在しないからである。ロディッチ（2003）は、彼らのウィトゲンシュタイン解釈は歴史的に正当化されていないと主張している。ベルト（2009）は、ウィトゲンシュタインの著作と矛盾しない論理の理論との関係を探求している。[ 42 ]
以下の翻訳はいずれも、翻訳された単語や活字において一致していません。活字は重大な問題です。なぜなら、ゲーデルは「以前に通常の意味で定義されていたメタ数学的概念」を強調したいと明確に望んでいたからです（van Heijenoort 1967 、p. 595） 。3つの翻訳が存在します。最初の翻訳について、ジョン・ドーソンは次のように述べています。「メルツァーの翻訳は深刻な欠陥があり、『 Journal of Symbolic Logic 』で酷評されました。ゲーデルはブライスウェイトの解説についても不満を述べていました（Dawson 1997 、p. 216）。 「幸いなことに、メルツァー訳はすぐにエリオット・メンデルソンがマーティン・デイヴィスのアンソロジー『決定不可能なもの』のために用意したより良い訳に取って代わられた…彼はその翻訳が期待していたほど「良くない」と感じた…[しかし時間の制約のため]出版に同意した」（同上）。（脚注でドーソンは「出版された巻は全体的にずさんな活字と多数の誤植で台無しになっていたので、彼は同意したことを後悔するだろう」と述べている（同上）。ドーソンは「ゲーデルが好んだ翻訳はジャン・ファン・ヘイエノールトによるものだった」と述べている（同上）。真剣な学生のために、別のバージョンとして、1934年の春にゲーデルが高等研究所で行った講義中にスティーブン・クリーネとJB・ロッサーによって記録された一連の講義ノートが存在する（デイヴィスの解説1965、39ページおよび41ページ以降を参照）。この版のタイトルは「形式数学体系の決定不能命題について」です。出版順に：
Boolos (1998
, pp.
383–388)
に再録
