ゲーデルの不完全性定理

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

真の算術と呼ばれる理論は、ペアノ算術の言語における標準整数に関するすべての真の命題から構成される。この理論は無矛盾かつ完全であり、十分な量の算術を含んでいる。しかしながら、再帰的に列挙可能な公理系を持たないため、不完全性定理の仮定を満たさない。

A set of axioms is (syntactically, or negation-) complete if, for any statement in the axioms' language, that statement or its negation is provable from the axioms.^[3] This is the notion relevant for Gödel's first Incompleteness theorem. It is not to be confused with semantic completeness, which means that the set of axioms proves all the semantic tautologies of the given language. In his completeness theorem (not to be confused with the incompleteness theorems described here), Gödel proved that first-order logic is semantically complete. But it is not syntactically complete, since there are sentences expressible in the language of first-order logic that can be neither proved nor disproved from the axioms of logic alone.

In a system of mathematics, thinkers such as Hilbert believed that it was just a matter of time to find such an axiomatization that would allow one to either prove or disprove (by proving its negation) every mathematical formula.

A formal system might be syntactically incomplete by design, as logics generally are. Or it may be incomplete simply because not all the necessary axioms have been discovered or included. For example, Euclidean geometry without the parallel postulate is incomplete, because some statements in the language (such as the parallel postulate itself) can not be proved from the remaining axioms. Similarly, the theory of dense linear orders is not complete, but becomes complete with an extra axiom stating that there are no endpoints in the order. The continuum hypothesis is a statement in the language of ZFC that is not provable within ZFC, so ZFC is not complete. In this case, there is no obvious candidate for a new axiom that resolves the issue.

The theory of first-order Peano arithmetic seems consistent. Assuming this is indeed the case, note that it has an infinite but recursively enumerable set of axioms, and can encode enough arithmetic for the hypotheses of the incompleteness theorem. Thus by the first incompleteness theorem, Peano Arithmetic is not complete. The theorem gives an explicit example of a statement of arithmetic that is neither provable nor disprovable in Peano's arithmetic. Moreover, this statement is true in the usual model. In addition, no effectively axiomatized, consistent extension of Peano arithmetic can be complete.

公理系は、その公理系から命題とその否定の両方が証明できるような命題が存在しない場合、 （単純に）無矛盾である。そうでない場合は無矛盾である。つまり、無矛盾な公理系とは、矛盾のない公理系のことである。

ペアノ算術はZFCから証明可能で一貫性がありますが、ZFC自体からは証明できません。同様に、ZFC自体からは証明可能で一貫性はありませんが、ZFC + 「到達不可能な基数が存在する」によってZFCの一貫性が証明されます。なぜなら、κがそのような最小の基数であれば、フォン・ノイマン宇宙内に存在するVκ_はZFCのモデルであり、理論が一貫性を持つのはモデルを持つ場合のみだからです。

ペアノ算術の言語におけるすべての命題を公理とみなすならば、この理論は完全であり、再帰的に列挙可能な公理の集合を持ち、加算と乗算を記述することができる。しかしながら、それは矛盾している。

矛盾する理論のさらなる例は、集合論において無制限の理解という公理体系を仮定した場合に生じるパラドックスから生じる。

不完全性定理は、自然数に関する十分な事実の集合を証明できる形式体系にのみ適用されます。十分な事実の集合の一つは、ロビンソン算術の定理の集合Qです。ペアノ算術のような一部の体系は、自然数に関する命題を直接表現できます。ZFC集合論のような他の体系は、自然数に関する命題をその言語に解釈することができます。これらのどちらの選択肢も、不完全性定理には適しています。

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

プレスバーガー算術体系は、自然数に対する加算演算のみを含む公理系から構成される（乗算は省略されている）。プレスバーガー算術は完全性、一貫性、再帰的列挙可能性を備えており、自然数の加算は符号化できるが乗算は符号化できない。このことから、ゲーデルの定理を実現するには、加算だけでなく乗算も符号化できる理論が必要であることがわかる。

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

公理系を選択する際の目標の一つは、誤った結果を証明することなく、できるだけ多くの正しい結果を証明できるようにすることです。例えば、自然数に関するすべての真の算術的主張を証明できるような、真の公理系を想像することができます（Smith 2007 、p. 2）。一階述語論理の標準体系では、矛盾する公理系は、その言語のすべての命題を証明します（これは爆発原理と呼ばれることもあります）。したがって、自動的に完全になります。しかし、完全かつ矛盾のない公理系は、矛盾しない定理の最大集合を証明します。 

前節でペアノ算術、ZFC、およびZFC +「到達不可能な基数が存在する」で示したパターンは、一般に破ることはできません。ここで、ZFC +「到達不可能な基数が存在する」は、それ自体から無矛盾であることを証明することはできません。また、ZFC +「到達不可能な基数が存在する」では解決不可能な連続体仮説^{[ 4 ]}によって示されるように、完全でもありません。

第一不完全性定理は、基本的な算術を表現できる形式体系において、完全かつ無矛盾な有限個の公理リストを作成することは決してできないことを示している。すなわち、無矛盾な命題を公理として追加するたびに、その新しい公理を用いてもなお証明できない他の真の命題が存在する。もし体系を完全化するような公理が追加されるとすれば、それは体系を無矛盾にするという代償を伴う。無限個の公理リストであっても、完全かつ無矛盾で、かつ効果的に公理化されている状態はあり得ない。

The Gödel sentence is designed to refer, indirectly, to itself. The sentence states that, when a particular sequence of steps is used to construct another sentence, that constructed sentence will not be provable in F. However, the sequence of steps is such that the constructed sentence turns out to be G_F itself. In this way, the Gödel sentence G_F indirectly states its own unprovability within F.^[5]

To prove the first incompleteness theorem, Gödel demonstrated that the notion of provability within a system could be expressed purely in terms of arithmetical functions that operate on Gödel numbers of sentences of the system. Therefore, the system, which can prove certain facts about numbers, can also indirectly prove facts about its own statements, provided that it is effectively generated. Questions about the provability of statements within the system are represented as questions about the arithmetical properties of numbers themselves, which would be decidable by the system if it were complete.

Thus, although the Gödel sentence refers indirectly to sentences of the system F, when read as an arithmetical statement the Gödel sentence directly refers only to natural numbers. It asserts that no natural number has a particular property, where that property is given by a primitive recursive relation (Smith 2007, p. 141). As such, the Gödel sentence can be written in the language of arithmetic with a simple syntactic form. In particular, it can be expressed as a formula in the language of arithmetic consisting of a number of leading universal quantifiers followed by a quantifier-free body (these formulas are at level $\displaystyle \Pi _{1}^{0}}$ of the arithmetical hierarchy). Via the MRDP theorem, the Gödel sentence can be re-written as a statement that a particular polynomial in many variables with integer coefficients never takes the value zero when integers are substituted for its variables (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が無矛盾であるという主張の他の形式化は、Fにおいて同値ではない場合があり、中には証明可能なものもあるかもしれません。例えば、一階ペアノ算術（PA）は、「PAの最大の無矛盾部分集合」が無矛盾であることを証明できます。しかし、PAは無矛盾であるため、PAの最大の無矛盾部分集合はPAそのものなので、この意味でPAは「無矛盾であることを証明している」と言えます。PAが証明していないのは、PAの最大の無矛盾部分集合が実際にはPA全体であるということです。（ここでいう「PAの最大の無矛盾部分集合」とは、特定の有効な列挙の下でのPAの公理の最大の無矛盾な初期セグメントを意味します。）

第2不完全性定理の標準的な証明では、証明可能性述語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 ₁は実際には無矛盾であることを証明できるからである。F _{1 が}無矛盾であるという主張は、 「すべての数nに対して、n はF ₁における矛盾の証明のコードではないという決定可能な性質を持つ」という形式をとる。もしF _{1 が}実際には無矛盾であれば、F _{2 は}あるnに対して、nがF ₁における矛盾のコードであることを証明するだろう。しかし、F _{2 が}F ₁が無矛盾であることも証明した場合（つまり、そのようなnが存在しない場合）、F 2 自体が無矛盾となる。この推論は、F _{1において形式化することで、} F ₂が無矛盾であれば、F ₁も無矛盾であることを示すことができる。第二不完全性定理により、F _{1 は自身の無矛盾性を証明していないため、} F ₂の無矛盾性も証明できない。

この第二不完全性定理の系は、例えば、ペアノ算術（PA）においてその一貫性が証明可能な体系で形式化できる有限的な手段を用いてペアノ算術の一貫性を証明することは不可能であることを示している。例えば、有限数学の正確な形式化として広く受け入れられている原始再帰算術（PRA）体系は、PAにおいて一貫性が証明可能である。したがって、PRAはPAの一貫性を証明することはできない。この事実は一般的に、理想的な（無限主義的な）数学原理が「現実の」（有限主義的な）数学的命題の証明において、それらの原理が一貫性を持つことを有限主義的に証明することによって正当化することを目的としたヒルベルトの計画は実行不可能であることを意味すると考えられている。^{[ 7 ]}

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

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

これらは、ゲーデルの「真であるが決定不能」な命題に相当する、数学的に自然な表現である。これらは、一般的に有効な推論形式として認められているより大きな体系では証明できるが、ペアノ算術のようなより限定された体系では決定不能である。

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

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

先ほど述べた証明を具体的に示す際の主な問題は、まず「 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に変換できます。

原則として、ある命題の真偽を証明することは、その命題に一致する数が特定の性質を持つか否かを証明することと同等であることが示せる。形式体系は、一般的に数に関する推論を支えるのに十分な強度を備えているため、数式や命題を表す数に関する推論も支えることができる。重要なのは、この体系が数の性質に関する推論を支えることができるため、その結果は、それらと同等の命題の証明可能性に関する推論と同等であるということである。

原理的には、このシステムが証明可能性について間接的に主張できることを示した上で、主張を表す数値の特性を分析することにより、実際に証明可能性について主張する主張を作成する方法を示すことができる。

A formula F(x) that contains exactly one free variable x is called a statement form or class-sign. As soon as x is replaced by a specific number, the statement form turns into a bona fide statement, and it is then either provable in the system, or not. For certain formulas one can show that for every natural number n, ⁠${\displaystyle F(n)}$⁠ is true if and only if it can be proved (the precise requirement in the original proof is weaker, but for the proof sketch this will suffice). In particular, this is true for every specific arithmetic operation between a finite number of natural numbers, such as "2 × 3 = 6".

Statement forms themselves are not statements and therefore cannot be proved or disproved. But every statement form F(x) can be assigned a Gödel number denoted by G(F). The choice of the free variable used in the form F(x) is not relevant to the assignment of the Gödel number G(F).

The notion of provability itself can also be encoded by Gödel numbers, in the following way: since a proof is a list of statements which obey certain rules, the Gödel number of a proof can be defined. Then, for every statement p, one may ask whether a number x is the Gödel number of its proof. The relation between the Gödel number of p and x, the potential Gödel number of its proof, is an arithmetical relation between two numbers. Therefore, there is a statement form Bew(y) that uses this arithmetical relation to state that a Gödel number of a proof of y exists:

Bew(y) = ∃ x (y is the Gödel number of a formula and x is the Gödel number of a proof of the formula encoded by y).

The name Bew is short for beweisbar, the German word for "provable"; this name was originally used by Gödel to denote the provability formula just described. Note that "Bew(y)" is merely an abbreviation that represents a particular, very long, formula in the original language of T; the string "Bew" itself is not claimed to be part of this language.

式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を前の節で得られた命題とする。

If p were provable, then Bew(G(p)) would be provable, as argued above. But p asserts the negation of Bew(G(p)). Thus the system would be inconsistent, proving both a statement and its negation. This contradiction shows that p cannot be provable.

If the negation of p were provable, then Bew(G(p)) would be provable (because p was constructed to be equivalent to the negation of Bew(G(p))). However, for each specific number x, x cannot be the Gödel number of the proof of p, because p is not provable (from the previous paragraph). Thus on one hand the system proves there is a number with a certain property (that it is the Gödel number of the proof of p), but on the other hand, for every specific number x, we can prove that it does not have this property. This is impossible in an ω-consistent system. Thus the negation of p is not provable.

Thus the statement p is undecidable in our axiomatic system: it can neither be proved nor disproved within the system.

In fact, to show that p is not provable only requires the assumption that the system is consistent. The stronger assumption of ω-consistency is required to show that the negation of p is not provable. Thus, if p is constructed for a particular system:

• If the system is ω-consistent, it can prove neither p nor its negation, and so p is undecidable.
• If the system is consistent, it may have the same situation, or it may prove the negation of p. In the later case, we have a statement ("not p") which is false but provable, and the system is not ω-consistent.

If one tries to "add the missing axioms" to avoid the incompleteness of the system, then one has to add either p or "not p" as axioms. But then the definition of "being a Gödel number of a proof" of a statement changes. which means that the formula Bew(x) is now different. Thus when we apply the diagonal lemma to this new Bew, we obtain a new statement p, different from the previous one, which will be undecidable in the new system if it is ω-consistent.

Boolos (1989) sketches an alternative proof of the first incompleteness theorem that uses Berry's paradox rather than the liar paradox to construct a true but unprovable formula. A similar proof method was independently discovered by Saul Kripke.^[15] Boolos's proof proceeds by constructing, for any computably enumerable set S of true sentences of arithmetic, another sentence which is true but not contained in S. This gives the first incompleteness theorem as a corollary. According to Boolos, this proof is interesting because it provides a "different sort of reason" for the incompleteness of effective, consistent theories of arithmetic.^[16]

The incompleteness theorems are among a relatively small number of nontrivial theorems that have been transformed into formalized theorems that can be completely verified by proof assistant software. Gödel's original proofs of the incompleteness theorems, like most mathematical proofs, were written in natural language intended for human readers.

Computer-verified proofs of versions of the first incompleteness theorem were announced by Natarajan Shankar in 1986 using Nqthm(Shankar 1994), by Russell O'Connor in 2003 using Rocq (previously known as Coq) (O'Connor 2005) and by John Harrison in 2009 using HOL Light(Harrison 2009). A computer-verified proof of both incompleteness theorems was announced by Lawrence Paulson in 2013 using Isabelle(Paulson 2014).

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

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

哲学者JRルーカスや物理学者ロジャー・ペンローズをはじめとする多くの研究者が、ゲーデルの不完全性定理が人間の知能について何を暗示しているのか、あるいは何も示唆していないのかについて議論を重ねてきた。議論の多くは、人間の精神がチューリングマシンと同等であるかどうか、あるいはチャーチ＝チューリングのテーゼによれば、あらゆる有限機械と同等であるかどうかという点に集中している。もしそうであれば、そしてその機械が無矛盾であれば、ゲーデルの不完全性定理が適用されることになる。

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

ウィグダーソン（2010）は、数学的な「認識可能性」の概念は論理的決定可能性ではなく計算複雑性に基づくべきだと提唱している。彼は、「認識可能性が現代の基準、すなわち計算複雑性によって解釈される場合、ゲーデル現象は依然として存在する」と述べている。^{[ 19 ]}

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

公式の意味を知るだけで、公理から体系的に「上へ」と進むという昔ながらの方法で導出する努力をすることなく、その真偽を推論することができる。これは単に奇妙というだけでなく、驚くべきことである。通常、数学的予想が何を言っているかを見て、その記述の内容だけに頼って、その記述が真か偽かを推論することはできない。^{[ 20 ]}

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

このように、人間が世界を認識する通常の方法には奇妙な逆説性がある。現実を動かす実際の原動力は微小な領域にあるように思われるにもかかわらず、私たちは「小さなもの」ではなく「大きなもの」を認識するようにできているのだ。^{[ 20 ]}

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

数学や論理学の枠を超えた議論を支持するために、定理の不完全性への訴えや類推が行われることがある。フランツェン (2005)、ラーティカイネン (2005)、ソーカル&ブリックモン (1999) 、スタングルーム&ベンソン (2006)など、数名の著者がこうした拡張や解釈に否定的なコメントをしている。^{[ 24 ]} 例えば、ソーカル&ブリックモン (1999)とスタングルーム&ベンソン (2006)は、レベッカ ゴールドスタインの、ゲーデルが公言するプラトン主義と、彼の考えが時として反実在論的に用いられることとの間の不一致についてのコメントを引用している。ソーカル&ブリックモン (1999)は、社会学の文脈で定理を援用するレジス ドブレイを批判している。ドブレイはこの用法を比喩的なものとして擁護している (同上)。^{[ 25 ]}

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不完全性定理の完全な証明として初めて公表されたものである。

• 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原文のドイツ語と対向する英語訳、およびスティーブン・コール・クリーネによる序文が掲載されています。
• —、1951年、「数学の基礎に関するいくつかの基本定理とその含意」、ソロモン・フェファーマン編、1995年、『クルト・ゲーデル全集』第3巻、オックスフォード大学出版局、 304-323頁。ISBN 978-0195147223。

None of the following agree in all translated words and in typography. The typography is a serious matter, because Gödel expressly wished to emphasize "those metamathematical notions that had been defined in their usual sense before . . ." (van Heijenoort 1967, p. 595). Three translations exist. Of the first John Dawson states that: "The Meltzer translation was seriously deficient and received a devastating review in the Journal of Symbolic Logic; "Gödel also complained about Braithwaite's commentary (Dawson 1997, p. 216). "Fortunately, the Meltzer translation was soon supplanted by a better one prepared by Elliott Mendelson for Martin Davis's anthology The Undecidable . . . he found the translation "not quite so good" as he had expected . . . [but because of time constraints he] agreed to its publication" (ibid). (In a footnote Dawson states that "he would regret his compliance, for the published volume was marred throughout by sloppy typography and numerous misprints" (ibid)). Dawson states that "The translation that Gödel favored was that by Jean van Heijenoort" (ibid). For the serious student another version exists as a set of lecture notes recorded by Stephen Kleene and J. B. Rosser "during lectures given by Gödel at to the Institute for Advanced Study during the spring of 1934" (cf commentary by Davis 1965, p. 39 and beginning on p. 41); this version is titled "On Undecidable Propositions of Formal Mathematical Systems". In their order of publication:

• B. Meltzer (translation) and R. B. Braithwaite (Introduction), 1962. On Formally Undecidable Propositions of Principia Mathematica and Related Systems, Dover Publications, New York (Dover edition 1992), ISBN 0-486-66980-7 (pbk.) This contains a useful translation of Gödel's German abbreviations on pp. 33–34. As noted above, typography, translation and commentary is suspect. Unfortunately, this translation was reprinted with all its suspect content by

• Stephen Hawking editor, 2005. God Created the Integers: The Mathematical Breakthroughs That Changed History, Running Press, Philadelphia, ISBN 0-7624-1922-9. Gödel's paper appears starting on p. 1097, with Hawking's commentary starting on p. 1089.

• Martin Davis editor, 1965. The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable problems and Computable Functions, Raven Press, New York, no ISBN. Gödel's paper begins on page 5, preceded by one page of commentary.
• Jean van Heijenoort編、1967 年、第 3 版 1967 年。『フレーゲからゲーデルへ：数学論理学の資料集、1879-1931』、ハーバード大学出版局、マサチューセッツ州ケンブリッジ、ISBN 0-674-32449-8（ペーパーバック版）。翻訳はファン・ヘイエノールトが担当した。彼は「ゲーデル教授はこの翻訳を承認し、多くの箇所で教授の意向に沿ったものとなった」と述べている（ 595ページ）。ゲーデルの論文は595ページから始まり 、ファン・ヘイエノールトの解説は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、「ゲーデルの第一不完全性定理の適用範囲（ 2016年3月6日にWayback Machineにアーカイブ）」、Logica Universalis、第8巻、499 ～ 552ページ。doi ：10.1007/s11787-014-0107-3 
• Charlesworth, Arthur (1981). 「コンピュータプログラムによるゲーデルの定理の証明」. Mathematics Magazine . 54 (3): 109–121 . doi : 10.2307/2689794 . JSTOR 2689794 . 
• デイビス、マーティン（1965）。『決定不能なもの：決定不能な命題、解決不能な問題、計算可能な関数に関する基礎論文集』レイヴン・プレス。ISBN 978-0-911216-01-1。
• Davis, Martin (2006). 「不完全性定理」(PDF) . Notices of the 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 . 
• ジョン・バークレー・ロッサー、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、第4巻（1939年）53-60ページからの再録 、Martin Davis 1965年、『The Undecidable』（前掲書） 223-230ページ。
• スモリンスキー、 C. ( 1977). 「不完全性定理」。ジョン・バーワイズ編『数理論理学ハンドブック』所収。アムステルダム：ノースホランド出版。pp. 821–866。ISBN  978-0-444-86388-1。
• Willard, Dan E. (2001). "自己検証公理系、不完全性定理および関連する反射原理". Journal of Symbolic Logic . 66 (2): 536–596 . doi : 10.2307/2695030 . JSTOR 2695030 . 
• Zach, Richard (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』所収。エルゼビア。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-8MR 2146326 .​ 
• ダグラス・ホフスタッター、1979年。『ゲーデル、エッシャー、バッハ：永遠の黄金の鎖』。ヴィンテージブックス。ISBN 0-465-02685-01999年再版：ISBN 0-465-02656-7MR 0530196​ 
•  —、2007年。『私は奇妙なループ』。ベーシックブックス。ISBN 978-0-465-03078-1ISBN​ 0-465-03078-5MR 2360307​ 
• スタンリー・ジャキ、OSB、2005年。『量のドラマ』リアルビューブックス。
• Per Lindström、1997年。「不完全性の側面」、Lecture Notes in Logic v. 10。
• JRルーカス、FBA、1970年。 『意志の自由』クラレンドン・プレス、オックスフォード、1970年。
• エイドリアン・ウィリアム・ムーア、2022年。『ゲーデルの定理：超入門』オックスフォード大学出版局、オックスフォード、2022年。
• アーネスト・ネーゲル、ジェームズ・ロイ・ニューマン、ダグラス・ホフスタッター、2002年（1958年）。『ゲーデルの証明』改訂版 。ISBN 0-8147-5816-9MR 1871678​ 
• ルディ・ラッカー、1995年（1982年）。『無限と精神：無限の科学と哲学』プリンストン大学出版局。MR 0658492 
• スミス、ピーター（2007）。ゲーデルの定理入門。ケンブリッジ、英国：ケンブリッジ大学出版局。ISBN 978-0-521-67453-9. MR 2384958 . 2005年10月23日にオリジナルからアーカイブされました。2005年10月29日に取得。 
• シャンカール、N. (1994).メタ数学、機械、そしてゲーデルの証明. 理論計算機科学ケンブリッジ論文集、第 38巻. ケンブリッジ：ケンブリッジ大学出版局. ISBN 0-521-58533-3。
• レイモンド・スムリアン、1987年。『永遠に未決定』ISBN 0192801414- 形式体系における決定不能性に基づくパズル
• —、1992年。『ゲーデルの不完全性定理』オックスフォード大学出版局。ISBN 0195046722
• —、1994年。『対角化と自己参照』オックスフォード大学出版局。MR 1318913。ISBN  0198534507
• —、2013年。『ゴデルのパズルブック：パズル、パラドックス、証明』。クーリエ・コーポレーション。ISBN 978-0-486-49705-1。
• 王浩（1996）。『論理の旅：ゲーデルから哲学へ』 MIT Press。ISBN 0-262-23189-1。MR 1433803 

• ベルト、フランチェスコ（2009）。「ゲーデルのパラドックスとウィトゲンシュタインの理由」。Philosophia Mathematica。III （ 17）。
• ドーソン、ジョン・W・ジュニア（1996）。論理的ジレンマ：クルト・ゲーデルの生涯と業績。テイラー＆フランシス。ISBN 978-1-56881-025-6。
• ドーソン、ジョン・W・ジュニア（1997）。論理的ジレンマ：クルト・ゲーデルの生涯と業績。マサチューセッツ州ウェルズリー：AKピーターズ。ISBN 978-1-56881-256-4OCLC 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-12019年5月8日にオリジナルからアーカイブされました。 2018年10月24日に取得。
• Jones, James P. (1980). "決定不能なディオファントス方程式" (PDF) . Bulletin of the American Mathematical Society . 3 (2): 859– 862. doi : 10.1090/S0273-0979-1980-14832-6 .
• Kleene, Stephen Cole (1967). "数理論理学". Nature . 216 (5111): 201. Bibcode : 1967Natur.216..201G . doi : 10.1038/216201b0 .ドーバー社より2002年に復刻。ISBN 0-486-42533-9
• O'Connor, Russell ( 2005). 「Coq で検証された算術の本質的不完全性」。高階論理における定理証明。Lecture Notes in Computer Science、第 3603 巻、pp. 245–260。arXiv : cs/ 0505034。doi : 10.1007 / 11541868_16。ISBN  978-3-540-28372-0. S2CID 15610367 . 
• Paulson, Lawrence (2014). "A machine-assisted proof of Gödel's incompleteness theorems for the theory of hereditarily finite sets". Review of Symbolic Logic. 7 (3): 484–498. arXiv:2104.14260. doi:10.1017/S1755020314000112. S2CID 13913592.
• Priest, Graham (1984). "Logic of Paradox Revisited". Journal of Philosophical Logic. 13 (2): 153–179. doi:10.1007/BF00453020.
• Priest, Graham (2004). "Wittgenstein's Remarks on Gödel's Theorem". In Max Kölbel (ed.). Wittgenstein's lasting significance. Psychology Press. pp. 207–227. ISBN 978-1-134-40617-3.
• Priest, Graham (2006). In Contradiction: A Study of the Transconsistent. Oxford University Press. ISBN 0-19-926329-9.
• Putnam, Hilary (1960). "Minds and Machines". In Sidney Hook (ed.). Dimensions of Mind: A Symposium. New York University Press. Reprinted in Anderson, A. R., ed., 1964. Minds and Machines. Prentice-Hall: 77.
• Wolfgang Rautenberg, 2010, A Concise Introduction to Mathematical Logic, 3rd. ed., Springer, ISBN 978-1-4419-1220-6
• Rodych, Victor (2003). "Misunderstanding Gödel: New Arguments about Wittgenstein and New Remarks by Wittgenstein". Dialectica. 57 (3): 279–313. doi:10.1111/j.1746-8361.2003.tb00272.x.doi:10.1111/j.1746-8361.2003.tb00272.x
• Shelah, Saharon (1974). "Infinite Abelian groups, Whitehead problem and some constructions". Israel Journal of Mathematics. 18 (3): 243–256. doi:10.1007/BF02757281. MR 0357114.
• Shapiro, Stewart (2002). "Incompleteness and Inconsistency". Mind. 111 (444): 817–32. doi:10.1093/mind/111.444.817.
• Sokal, Alan; Bricmont, Jean (1999). Fashionable Nonsense: Postmodern Intellectuals' Abuse of Science. Picador. 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
• ウィグダーソン、アヴィ（2010）。「数学におけるゲーデル現象：現代的視点」（PDF）。クルト・ゲーデルと数学の基礎：真理の地平。ケンブリッジ大学出版局。
• ハオ・ワン、1996年、『論理の旅：ゲーデルから哲学へ』、MITプレス、マサチューセッツ州ケンブリッジ、ISBN 0-262-23189-1。
• ザック、リチャード（ 2007）。「ヒルベルトのプログラム：過去と現在」。ジャケット、デール編『論理の哲学』。科学哲学ハンドブック第5巻。アムステルダム： エルゼビア。411–447頁。arXiv ： math /0508572。doi：10.1016/b978-044451541-4 / 50014-2。ISBN  978-0-444-51541-4. OCLC 162131413 . S2CID 291599 .