|
|
| 1行目: |
1行目: |
| − | {{参照方法|date=2017年8月}}
| + | __NOINDEX__ |
| − | [[数理論理学]]において'''ゲーデルの完全性定理'''（ゲーデルのかんぜんせいていり、{{lang-en-short|Gödel's completeness theorem}}、{{lang-de-short|Gödelscher Vollständigkeitssatz}}）とは、[[第一階述語論理]]の恒真な論理式はその公理系からすべて導出可能であることを示した定理を言う<ref>[[#廣瀬,横田(1985)|廣瀬,横田(1985)]] p.147、[[#HA(第三版) |ヒルベルト、アッケルマン(第三版)]] p.107、[[#HA(第六版) |ヒルベルト、アッケルマン(第六版)]] pp.139-145</ref>。[[1929年]]に[[クルト・ゲーデル]]が証明した。
| + | {{テンプレート:20180815sk}} |
| − | | |
| − | == 概要 ==
| |
| − | 1928年に、[[ダフィット・ヒルベルト|D. ヒルベルト]]と[[ヴィルヘルム・アッカーマン|W. アッケルマン]]の共著書であり、[[第一階述語論理]]（狭義の述語論理）を独立した論理体系として形式化した最初の本である『記号論理学の基礎』<ref>国内では第三版と第六版の邦訳が出版されている。[[#HA(第三版) |ヒルベルト、アッケルマン(第三版)]]、[[#HA(第六版) |ヒルベルト、アッケルマン(第六版)]]</ref>の初版が出版されたが、この初版本において第一階述語論理の[[完全性]]は一つの未解決問題であった<ref>制限された形では証明されていた。さらにこの初版本は「この公理系が、すべての正しい論理式を導き出すことができるという意味で、完全であるか否かは依然として未解決の問題である。この公理系がどんな場合にも十分であるというのは、まったく経験的なものである」と述べていた。[[#廣瀬,横田(1985)|廣瀬,横田(1985)]] pp.5-6</ref>。この本を読み、この問題の解決に取り掛かった[[クルト・ゲーデル]]は、学位論文として1929年の秋にその結果を発表した。これがいわゆるゲーデルの完全性定理である<ref>[[#廣瀬,横田(1985)|廣瀬,横田(1985)]] pp.5-6</ref>。
| |
| − | | |
| − | 第一階述語論理の論理式が恒真あるいは普遍妥当であるとは、個体領域の選び方のいかんにかかわらず、その変項に代入を行っても恒にその論理式が真となることを意味する。完全性定理は、論理式が論理的に妥当ならば、その論理式の有限な演繹（形式的証明）が存在することを示した。その演繹は有限であり、人間またはコンピュータによって検証可能である。この真理値と証明可能性の関係により、数理論理学における[[モデル理論]]と[[証明論]]の密接な関係が確立された。
| |
| − | | |
| − | 完全性定理の重要な帰結の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<sub>0</sub> 上で完全性定理とコンパクト性定理は等価であり、それは公理系 WKL<sub>0</sub> とも等価である。特に、全ての無矛盾な一階理論は完全性定理と[[レーヴェンハイム＝スコーレムの定理]]から有限モデルか可算モデルを持つが、計算可能モデルを持たない無矛盾な一階理論も知られている。
| |
| − | | |
| − | == 他の論理の完全性 ==
| |
| − | 完全性定理は[[一階述語論理]]の中心的属性だが、あらゆる論理で成り立つわけではない。例えば[[二階述語論理]]では、standard semantics の場合に完全性定理を持たず（Henkin semantics の場合は完全性を有する）、全ての高階論理でも同様である。高階論理の健全な演繹系を生成することは可能だが、そのような系は完全ではない。二階論理における論理的に妥当な論理式の集合は枚挙可能ではない。
| |
| − | | |
| − | 完全性定理は、[[クリプキ意味論]]を使った[[様相論理学|様相論理]]についても証明可能である。
| |
| − | | |
| − | == 証明 ==
| |
| − | [[ゲーデルの完全性定理の原証明|ゲーデルのオリジナルの証明]]([[:en:Original proof of Gödel's completeness theorem|en]])は、問題を論理式の特殊ケースを表すある[[統語論]]的な形式に還元し、以後はその形式を場当たり的な方法で扱った。
| |
| − | | |
| − | 最近の論理学の文献では、[[レオン・ヘンキン | ヘンキン]]の証明の方がよく紹介されている。ヘンキンの証明では、任意の無矛盾な一階理論に適用できるような[[項モデル]]([[:en:term model|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の不完全性定理について)」<ref>博士論文書誌データベース</ref>。
| |
| − | * {{cite book | 和書 | author=廣瀬健、横田一正 | title=ゲーデルの世界--完全性定理と不完全性定理-- | publisher=[[海鳴社]] | year=1985 | ISBN=4875251068 | ref=廣瀬,横田(1985)}} <small>-付録に完全性定理の論文「論理学における述語計算の公理の完全性」の翻訳が収録されている。</small>
| |
| − | * {{cite book | 和書 | author=D.ヒルベルト、W.アッケルマン | editor=伊藤誠（訳） | title=記号論理学の基礎（第三版） | year=1954 | publisher=大阪教育図書社 | ref=HA(第三版) }}
| |
| − | * {{cite book | 和書 | author=D.ヒルベルト、W.アッケルマン | editor=石本新、竹尾治一郎（訳） | title=記号論理学の基礎（第六版） | edition=改訂最新版 | year=1974 | publisher=大阪教育図書社 | ref=HA(第六版) }}
| |
| − | | |
| − | ==脚注==
| |
| − | <references/>
| |
| − | | |
| − | == 関連項目 ==
| |
| − | * [[レーヴェンハイム-スコーレムの定理]]
| |
| − | * [[エルブランの定理]]
| |
| − | * [[ゲーデルの不完全性定理]]
| |
| − | | |
| − | == 外部リンク ==
| |
| − | *[[スタンフォード哲学百科事典]]: "[http://plato.stanford.edu/entries/goedel/ Kurt Gödel]" -- by Juliette Kennedy.
| |
| − | *MacTutor biography: [http://www-groups.dcs.st-and.ac.uk/~history/Mathematicians/Godel.html Kurt Gödel.]
| |
| − | * Detlovs, Vilnis, and Podnieks, Karlis, "[http://www.ltn.lv/~podnieks/ Introduction to mathematical logic.]"
| |
| − | | |
| − | {{Metalogic}}
| |
| − | {{DEFAULTSORT:けえてるのかんせんせいていり}}
| |
| − | [[Category:数理論理学]]
| |
| − | [[Category:数学基礎論の定理]]
| |
| − | [[Category:数学に関する記事]]
| |