出典は列挙するだけでなく、脚注などを用いてどの記述の情報源であるかを明記してください。記事の信頼性向上にご協力をお願いいたします。（2017年8月）

数理論理学においてゲーデルの完全性定理（ゲーデルのかんぜんせいていり、英: Godel's completeness theorem、独: Godelscher Vollstandigkeitssatz）とは、一階述語論理の恒真な論理式はその公理系からすべて導出可能であることを示した定理を言う[1]。1929年にクルト・ゲーデルが証明した。
概要

1928年に、D. ヒルベルトとW. アッケルマンの共著書であり、一階述語論理（狭義の述語論理）を独立した論理体系として形式化した最初の本である『記号論理学の基礎』[2]の初版が出版されたが、この初版本において一階述語論理の完全性は一つの未解決問題であった[3]。この本を読み、この問題の解決に取り掛かったクルト・ゲーデルは、学位論文として1929年の秋にその結果を発表した。これがいわゆるゲーデルの完全性定理である[4]。

一階述語論理の論理式が恒真あるいは普遍妥当であるとは、個体領域の選び方のいかんにかかわらず、その変項に代入を行っても恒にその論理式が真となることを意味する。完全性定理は、論理式が論理的に妥当ならば、その論理式の有限な演繹（形式的証明）が存在することを示した。その演繹は有限であり、人間またはコンピュータによって検証可能である。この真理値と証明可能性の関係により、数理論理学におけるモデル理論と証明論の密接な関係が確立された。

完全性定理の重要な帰結の1つとして、任意の一階の理論について、その理論の公理を使った正しい演繹を全て数え上げることで、論理的帰結を数え上げることが可能であると示された。すなわち完全性定理は論理的帰結関係 Γ ⊨ φ {\displaystyle \Gamma \models \varphi } と証明可能性関係 Γ ⊢ φ {\displaystyle \Gamma \vdash \varphi } とが一致することを述べているが、後者は帰納的可算であるので前者も帰納的可算であるということである。

ゲーデルの不完全性定理（この場合の「完全性」の意味は異なる）は、ある程度の初等算術を含む帰納的可算理論が無矛盾なら、その理論体系内で証明も反証もできない閉論理式が存在することを示した。その場合も、そのような理論体系に完全性定理を適用でき、その理論体系における任意の論理的帰結はその理論体系内で証明可能である。
背景

一階論理の演繹系としては、自然演繹やヒルベルト系など様々なものがある。演繹系は一般に形式的演繹の記法である。それは論理式の並び（あるいは場合によっては木構造）であり、末尾に特別な帰結がある。演繹とは、有限でアルゴリズム的に（コンピュータや人間の手で）検証可能な論理式の集まりである。

論理式が論理的に妥当であるとは、その論理式の言語におけるあらゆる構造に照らして真であることを言う。完全性定理を形式的に定義し証明するには、演繹系を定義する必要もある。演繹系が完全であるとは、論理的に妥当な全ての論理式が何らかの形式的演繹の帰結であることを意味し、特定の演繹系についての完全性定理は、そういった意味で完全であることを示す定理である。したがって、それぞれの演繹系ごとにそれぞれの完全性定理が存在する。
定理とその帰結

ゲーデルの完全性定理は、一階述語計算の演繹系が、全ての論理的に妥当な論理式の証明に追加の推論規則を必要としないという意味で「完全」であるとしている。完全性の逆は健全性であり、演繹系において論理的に妥当な論理式のみが証明可能だということを意味する。