ゲーデルの不完全性定理（ゲーデルのふかんぜんせいていり、英: Godel's incompleteness theorems、独: Godelscher Unvollstandigkeitssatz）または不完全性定理とは、数学基礎論[1]とコンピュータ科学（計算機科学）の重要な基本定理[2]。（数学基礎論は数理論理学や超数学とほぼ同義な分野で、コンピュータ科学と密接に関連している[3]。）　不完全性定理は厳密には「数学」そのものについての定理ではなく、「形式化された数学」についての定理である[4][注 1]。クルト・ゲーデルが1931年の論文で証明した定理であり[5]、有限の立場（英語版）（形式主義）では自然数論の無矛盾性の証明が成立しないことを示す[3][5]。なお、少し拡張された有限の立場では、自然数論の無矛盾性の証明が成立する（ゲンツェンの無矛盾性証明（英語版））[3][注 2]。

数学基礎論研究者の菊池誠によると不完全性定理は、20世紀初め以降に哲学から決別した数学基礎論の中で現れた[6][注 3]。コンピュータ科学者・数理論理学者のトルケル・フランセーン[7]および数学者・数理論理学者の田中一之[7]によると、不完全性定理が示した不完全性とは、数学用語の意味での「特定の形式体系Pにおいて決定不能な命題の存在」であり、一般的な意味での「不完全性」とは無関係である[8]。不完全性定理を踏まえても、数学の形式体系の公理は真であり無矛盾であるし[9][注 4]、数学の完全性も成立し続けている[8]。しかし“不完全性定理は数学や理論の「不完全性」を証明した”といった誤解や、“数学には「不完全」な部分があると証明済みであり、数学以外の分野に「不完全」な部分があってもおかしくない”といった誤解が一般社会・哲学・宗教・神学等によって広まり、誤用されている[10][注 5]。「不完全性定理が成立しない体系」および「ゲーデルの完全性定理」も参照

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

ゲーデルの不完全性定理は、ゲーデルが1931年の論文で証明した次の内容である[5]。

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

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

より正確には、不完全性定理とは次の2つの定理（それぞれ第一/第二不完全性定理と呼ばれる）の総称である[5]。

第一不完全性定理 ― "初等的な自然数論"を含むω無矛盾な公理的理論 T {\displaystyle T} は不完全である。つまり T {\displaystyle T} 内で証明も反証もされない命題（決定不能命題(undecidable proposition)、あるいは独立命題）が存在する。

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

なお「有限の立場」とは、数学の形式主義における「記号の有限的な操作のみから構成される」立場を指す[12]。

注意

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

「初等的な自然数論」について、ゲーデル自身はペアノの公理と原始帰納法による関数の定義を前提に自然数論の体系を構築した (Godel 1931)。この体系は、加法・乗法・べき乗・階乗・順序関係などを帰納的に定義する十分な表現力を持っている。それぞれの定理の前提条件は、ロビンソン算術を含む半決定可能な理論（第一）、 I Σ 1 {\textstyle \mathbf {I} \Sigma _{1}} を含む半決定可能な理論（第二）に置き換えても証明することができる[14]。