第一不完全性定理
算術の基礎を表現できるほど強力な無矛盾の形式体系Fには、Fの内部では証明できないが真である命題が存在します。証明は自己言及を用いたものです。ゲーデルは「この命題はFでは証明できない」と主張する命題Gを構築しました。もしFでGが証明可能なら、Fは矛盾を孕んでいます。もしFでGが証明できないなら、Gは真（証明できないと主張しているため）ですが証明不能です。どちらにせよ、Fは不完全か不整合のいずれかになります。
第二不完全性定理
算術の基礎を表現できるほど強力な無矛盾の形式体系は、それ自身の無矛盾性を証明することができません。あるシステムを使って、そのシステムが矛盾を導かないことを保証することは不可能なのです。これはより深い結果であり、数学的な手段を用いて数学の無矛盾性を証明しようとしたヒルベルトのプログラムが不可能であることを意味します。
ゲーデルは何を証明していないのか
不完全性定理は、数学が信頼できないとか「何でもあり」であるという意味ではありません。これらは（機械的な証明規則を持つ）形式体系に適用されるものであり、数学的直感一般に適用されるものではありません。すべての数学的問題が決定不能であるというわけではなく、有限の公理系ではすべての問いを決定できないというだけのことです。ゲーデル自身はプラトニストであり、形式的な証明を超えていても、数学的真理は客観的に実在し、数学的直感によってアクセス可能であると考えていました。
数学を超えた意味
ゲーデルの定理は、人工知能、人間の知識の限界、意識の性質（ペンローズの議論）に関しても意味を持つと解釈（しばしば過剰解釈）されてきました。最も妥当な解釈は、形式体系に基づく十分に強力なAIは「死角」、つまり証明できない数学的真理を持つというものです。人間の数学的直感がこの制限を免れているかどうかについては、激しい議論が続いています。
よくある質問
ゲーデルの不完全性定理は何を語っているのですか？
第一定理：算術を扱うのに十分強力な無矛盾の形式体系は、証明不能な真の命題を含みます。第二定理：そのようなシステムは自身の無矛盾性を証明できません。これらを合わせると、数学は完全に公理化できないことが分かります。固定された証明体系の枠組みを超えた数学的真理が常に存在するのです。
ゲーデルの定理はAIが人間に追いつけないことを証明していますか？
ロジャー・ペンローズは「イエス」と主張します。もし心が形式体系ならゲーデルの定理が適用され、数学者は形式的証明を超えた真理を認識できるため、心はそれ以上の何かでなければならないという論法です。批判者（多くのAI研究者を含む）は、これは定理の誤用だと主張します。ゲーデルは固定された形式体系に適用されるものであり、学習するシステムや公理を変えるシステムは同じではないからです。
ゲーデルの定理は人間の知識の限界に関わるものですか？
それはあくまで形式的な公理系についてであり、一般的な人間の知識についてではありません。ゲーデルは、人間は特定の形式体系を超越する数学的直感を持っていると信じていました（彼はプラトニストでした）。この定理は、機械的な証明手順では数学のすべてを捉えきれないことを示していますが、人間の数学的理解が機械的手順を超越しているかどうかは、別の哲学的な問題です。