ゲーデルの完全性定理
出典: フリー百科事典『ウィキペディア（Wikipedia）』
ゲーデルの完全性定理（独：Gödelscher Vollständigkeitssatz）とは、一階述語論理における意味論的真理と統語論的立証性の対応を確立した数理論理学の基礎を成す定理である。1929年、クルト・ゲーデルが証明した。
一階述語論理の論理式が妥当であるとは、その言語のあらゆる構造についてそれが真であることを指す。完全性定理は、論理式が論理的に妥当ならば、その論理式の有限な演繹（形式的証明）が存在することを示した。その演繹は有限であり、人間またはコンピュータによって検証可能である。この真理値と立証可能性の関係により、数理論理学におけるモデル理論と証明論の密接な関係が確立された。
完全性定理の重要な帰結の1つとして、任意の一階の理論について、その理論の公理を使った正しい演繹を全て数え上げることで、論理的帰結を数え上げることが可能であると示された。
ゲーデルの不完全性定理（この場合の「完全性」の意味は異なる）は、十分に強力な算術理論が無矛盾なら、その理論体系内で真偽を証明できない論理式が存在することを示した。その場合も、そのような理論体系に完全性定理を適用でき、その理論体系における任意の論理的帰結はその理論体系内で証明可能である。
目次 |
[編集] 背景
一階論理の演繹系としては、自然演繹やヒルベルト系など様々なものがある。演繹系は一般に形式的演繹の記法である。それは論理式の並び（あるいは場合によっては木構造）であり、末尾に特別な帰結がある。演繹とは、有限でアルゴリズム的に（コンピュータや人間の手で）検証可能な論理式の集まりである。
論理式が論理的に妥当であるとは、その論理式の言語におけるあらゆる構造に照らして真でることを言う。完全性定理を形式的に定義し証明するには、演繹系を定義する必要もある。演繹系が完全であるとは、論理的に妥当な全ての論理式が何らかの形式的演繹の帰結であることを意味し、特定の演繹系についての完全性定理は、そういった意味で完全であることを示す定理である。したがって、それぞれの演繹系ごとにそれぞれの完全性定理が存在する。
[編集] 定理とその帰結
ゲーデルの完全性定理は、一階述語計算の演繹系が、全ての論理的に妥当な論理式の証明に追加の推論規則を必要としないという意味で「完全」であるとしている。完全性の逆は健全性であり、演繹系において論理的に妥当な論理式のみが証明可能だということを意味する。これらから、論理式が論理的に妥当であることと、それが形式的演繹の帰結であることは同値である。
ゲーデルの完全性定理をより一般化した版もある。すなわち、任意の一階の理論 T とその理論での言語における任意の命題 S について、T における S の形式的演繹が存在することと、S が T のあらゆるモデルで成り立つことは同値である。この一般化された定理は暗黙のうちに使われており、例えば、命題を群論の公理系で証明可能であることを示すとき、任意の群についてその命題が成り立つことを示すことで証明とする。
異なるモデルでも真となることを扱う数理論理学の一分野をモデル理論と呼ぶ。証明論という一分野では特定の形式体系で形式的に証明可能なことを研究する。完全性定理は意味論と統語論の間を繋ぐことでこれら2つの分野の基本的な繋がりを確立している。しかし、完全性定理はこれら2つの概念の差異をなくすものではない。実際、もう1つの成果であるゲーデルの不完全性定理によれば、数学における形式的証明で達成できることには本質的な限界がある。不完全性定理でいう「完全」は別の意味で使われている。完全性定理は一階の理論の論理的帰結である論理式を扱い、不完全性定理は特定の理論の論理的帰結にはならない論理式を構築する。
完全性定理の重要な帰結の1つとして、一階の理論での論理的帰結の集合が帰納的可算集合であるという事実がある。論理的帰結の定義は特定の言語でのあらゆる構造上で定量化するもので、論理式が論理的に妥当かどうかをアルゴリズム的に検証する直接の手段とはならない。さらに言えば、ゲーデルの完全性定理の帰結により、論理的に妥当な論理式の集合は決定可能ではない。しかし完全性定理は、ある理論の帰結の集合が可算であることを暗に示している。そのアルゴリズムは、まずその理論から全ての形式的演繹を枚挙する方法を構成し、それを使って帰結の枚挙を生み出すことになる。形式的演繹の有限かつ統語的性質により、それらを枚挙することが可能になる。
[編集] コンパクト性定理との関係
完全性定理とコンパクト性定理は、一階論理の2つの基礎である。これら定理をどちらも完全な方法で証明できないのに対して、一方からもう一方を得ることが可能である。
コンパクト性定理は、論理式 φ が一連の論理式の（無限もありうる）集合 Γ の論理的帰結であるとき、φ は Γ の有限な部分集合の論理的帰結でもある、というものである。φ の形式的推論で言及される Γ の公理は有限個であるため、これは完全性定理から直接得られる帰結である。演繹系の健全性から、φ がこの有限集合の論理的帰結となる。このコンパクト性定理の証明は本来ゲーデルに帰されるものである。
逆に多くの演繹系では、コンパクト性定理の帰結として完全性定理を証明可能である。
完全性定理の無効性は、集合論と逆数学で測られる。集合論では、ツェルメロ＝フレンケルの集合論 (ZF) では証明できない選択公理の弱い形のウルトラフィルターの補題がある。ZF では完全性定理とコンパクト性定理は等価であり、ウルトラフィルターの補題とも等しい。従って、ZFを拡張した理論は、ウルトラフィルターの補題を証明せずに完全性定理またはコンパクト性定理のどちらかを証明することができない。逆数学では、可算性の構造と可算性の理論だけが考慮される。この場合、RCA0 によって証明可能な等価性により、完全性定理とコンパクト性定理は等価であり、それは公理系 WKL0 とも等価である。特に、全ての無矛盾な一階理論は完全性定理とレーヴェンハイム＝スコーレムの定理から有限モデルか可算モデルを持つが、計算可能モデルを持たない無矛盾な一階理論も知られている。
[編集] 他の論理の完全性
完全性定理は一階述語論理の中心的属性だが、あらゆる論理で成り立つわけではない。例えば二階述語論理では、standard semantics の場合に完全性定理を持たず（Henkin semantics の場合は完全性を有する）、全ての高階論理でも同様である。高階論理の健全な演繹系を生成することは可能だが、そのような系は完全ではない。二階論理における論理的に妥当な論理式の集合は可算ではない。
完全性定理は、クリプキ意味論を使った様相論理についても証明可能である。
[編集] 証明
ゲーデルのオリジナルの証明は、問題をある特定の文法形式における論理式に還元し、その形式を場当たり的なものとして扱った。
最近の論理学の書籍では、Leon Henkin の証明の方がよく紹介されている。Henkin の証明では、任意の無矛盾な一階理論から項モデルを直接構築する。他の証明方法も存在する。
[編集] 関連項目
[編集] 参考文献
- 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. 上の論文の証明を簡略化したものが含まれている。
[編集] 外部リンク
- スタンフォード哲学百科事典: "Kurt Gödel" -- by Juliette Kennedy.
- MacTutor biography: Kurt Gödel.
- Detlovs, Vilnis, and Podnieks, Karlis, "Introduction to mathematical logic."
