ゲーデルの完全性定理

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

概要

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

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

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

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

背景

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

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

定理とその帰結

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

ゲーデルの完全性定理をより一般化した版もある。すなわち、任意の一階の理論 T とその理論での言語における任意の命題 S について、T における S の形式的演繹が存在することと、S が T のあらゆるモデルで成り立つことは同値である。この一般化された定理は暗黙のうちに使われており、例えば、命題を群論の公理系で証明可能であることを示すとき、任意の群についてその命題が成り立つことを示すことで証明とする。

異なるモデルでも真となることを扱う数理論理学の一分野をモデル理論と呼ぶ。証明論という一分野では形式体系の証明そのものの構造を研究する。完全性定理は意味論と統語論の間を繋ぐことでこれら2つの分野の基本的な繋がりを確立している。しかし、完全性定理はこれら2つの概念の差異をなくすものではない。実際、もう1つの成果であるゲーデルの不完全性定理によれば、数学における形式的証明で達成できることには本質的な限界がある。不完全性定理でいう「完全」は別の意味で使われている。完全性定理は一階の理論の論理的帰結である論理式を扱い、不完全性定理は特定の理論の論理的帰結にはならない論理式を構築する。

完全性定理の重要な帰結の1つとして、一階の理論での論理的帰結の集合が帰納的可算集合であるという事実がある。論理的帰結の定義は特定の言語でのあらゆる構造上で全称化するもので、論理式が論理的に妥当かどうかをアルゴリズム的に検証する直接の手段とはならない。さらに言えば、ゲーデルの不完全性定理の帰結により、論理的に妥当な論理式の集合は決定可能ではない。しかし完全性定理は、実効的な理論の帰結の集合が枚挙可能であることを示している。そのアルゴリズムは、まずその理論から全ての形式的演繹を枚挙する方法を構成し、それを使って帰結の枚挙を生み出すことになる。形式的演繹の有限かつ統語的性質により、それらを枚挙することが可能になっている。

コンパクト性定理との関係

完全性定理とコンパクト性定理は、一階論理の2つの基礎である。これら定理はどちらも実効的な方法で証明できないのに対して、一方からもう一方を実効的に得ることが可能である。

コンパクト性定理は、論理式 φ が一連の論理式の（無限もありうる）集合 Γ の論理的帰結であるとき、φ は Γ の有限な部分集合の論理的帰結でもある、というものである。φ の形式的推論で言及される Γ の公理は有限個であるため、これは完全性定理から直接得られる帰結である。演繹系の健全性から、φ がこの有限集合の論理的帰結となる。このコンパクト性定理の証明は本来ゲーデルに帰されるものである。

逆に多くの演繹系では、コンパクト性定理の実効的な帰結として完全性定理を証明可能である。

完全性定理の非実効性は、集合論と逆数学で測られる。集合論では、ツェルメロ＝フレンケルの集合論 (ZF) では証明できない選択公理の弱い形のウルトラフィルターの補題がある。ZF では完全性定理とコンパクト性定理は等価であり、ウルトラフィルターの補題とも等しい。従って、ZFを拡張した理論は、ウルトラフィルターの補題を証明せずに完全性定理またはコンパクト性定理のどちらかを証明することができない。逆数学では、可算性の構造と可算性の理論だけが考慮される。この場合、RCA₀ 上で完全性定理とコンパクト性定理は等価であり、それは公理系 WKL₀ とも等価である。特に、全ての無矛盾な一階理論は完全性定理とレーヴェンハイム＝スコーレムの定理から有限モデルか可算モデルを持つが、計算可能モデルを持たない無矛盾な一階理論も知られている。

他の論理の完全性

完全性定理は一階述語論理の中心的属性だが、あらゆる論理で成り立つわけではない。例えば二階述語論理では、standard semantics の場合に完全性定理を持たず（Henkin semantics の場合は完全性を有する）、全ての高階論理でも同様である。高階論理の健全な演繹系を生成することは可能だが、そのような系は完全ではない。二階論理における論理的に妥当な論理式の集合は枚挙可能ではない。

完全性定理は、クリプキ意味論を使った様相論理についても証明可能である。

証明

ゲーデルのオリジナルの証明(en)は、問題を論理式の特殊ケースを表すある統語論的な形式に還元し、以後はその形式を場当たり的な方法で扱った。

最近の論理学の文献では、 ヘンキンの証明の方がよく紹介されている。ヘンキンの証明では、任意の無矛盾な一階理論に適用できるような項モデル(en)を直接構築する。他の証明方法も存在する。

参考文献

• Kurt Gödel, "Über die Vollständigkeit des Logikkalküls", doctoral dissertation, University Of Vienna, 1929. - 完全性定理の証明のオリジナル
• Kurt Gödel, "Die Vollständigkeit der Axiome des logischen Funktionen-kalküls", Monatshefte für Mathematik und Physik 37 (1930), 349-360. - 上の論文の証明を簡略化したものが含まれている。
• 菊池誠 「On Godel′s Incompleteness Theorems(Godelの不完全性定理について)」。
• 廣瀬健、横田一正 『ゲーデルの世界--完全性定理と不完全性定理--』 海鳴社、1985年。 -付録に完全性定理の論文「論理学における述語計算の公理の完全性」の翻訳が収録されている。
• D.ヒルベルト、W.アッケルマン 『記号論理学の基礎（第三版）』 伊藤誠（訳）、大阪教育図書社、1954年。
• D.ヒルベルト、W.アッケルマン 『記号論理学の基礎（第六版）』 石本新、竹尾治一郎（訳）、大阪教育図書社、1974年、改訂最新版。

関連項目

• レーヴェンハイム-スコーレムの定理
• エルブランの定理
• ゲーデルの不完全性定理

外部リンク

• スタンフォード哲学百科事典: "Kurt Gödel" -- by Juliette Kennedy.
• MacTutor biography: Kurt Gödel.
• Detlovs, Vilnis, and Podnieks, Karlis, "Introduction to mathematical logic."