ゲーデルの完全性定理

ゲーデルの完全性定理は、一階述語論理における意味論的真理と構文論的証明可能性との間の対応関係を確立する、数理論理学における基本定理である。

完全性定理は、あらゆる一階理論に適用されます。Tがそのような理論であり、φ が（同じ言語の）文であり、Tのすべてのモデルがφのモデルである場合、 Tの命題を公理として用いるφの（一階）証明が存在します。これは、「すべてのモデルで真であるものは何でも証明可能である」と表現されることがあります。（これは、ある理論Tでは証明不可能だが自然数の「標準」モデルでは真である式φ _uに関するゲーデルの不完全性定理とは矛盾しません。φ _{u は}、Tの他の「非標準」モデルでは偽です。^{[ 1 ]}）

完全性定理は、異なるモデルにおいて何が真であるかを扱うモデル理論と、特定の形式体系において何が形式的に証明できるかを研究する証明理論との間に密接な関連性を持たせるものである。

これは1929年にクルト・ゲーデルによって初めて証明されました。その後、レオン・ヘンキンが博士論文で証明の難しい部分をモデル存在定理として提示できることに気づき、証明が簡略化されました（1949年に発表）。^{[ 2 ]}ヘンキンの証明は1953年にギスベルト・ハーゼンイェーガーによって簡略化されました。^{[ 3 ]}

一階述語論理には、自然演繹体系やヒルベルト型体系など、数多くの演繹体系が存在する。すべての演繹体系に共通するのは、形式的演繹という概念である。これは、特別な結論を持つ一連の式（あるいは場合によっては有限ツリー）である。演繹の定義は、それが有限であり、与えられた一連の式（あるいはツリー）が実際に演繹であることをアルゴリズム的に（例えばコンピュータによって、あるいは手作業によって）検証できるというものである。

一階述語論理式は、その論理式の言語のすべての構造（つまり、論理式の変数に値を割り当てる場合）において真である場合に、論理的に妥当であると呼ばれます。完全性定理を正式に述べ、証明するためには、演繹体系も定義する必要があります。演繹体系は、すべての論理的に妥当な論理式が何らかの形式的演繹の結論である場合に完全であると呼ばれ、特定の演繹体系の完全性定理は、この意味でその体系が完全であるという定理です。したがって、ある意味では、各演繹体系ごとに異なる完全性定理が存在します。完全性の逆は健全性であり、演繹体系において証明可能なのは論理的に妥当な論理式のみであるという事実です。

ある特定の一階述語論理の演繹体系が健全かつ完全であれば、それは「完全」である（論理式は、論理的に妥当である場合に限り証明可能である）。したがって、同じ性質を持つ他の演繹体系と等価である（一方の体系における証明は、他方の体系に変換できる）。

まず、よく知られている同値なシステムの中からいずれかを選び、一階述語論理の演繹体系を固定する。ゲーデルの元の証明は、ヒルベルト＝アッカーマン証明体系を前提としていた。

より一般的な形式

この定理は、論理的帰結という観点からより一般的に表現できる。文s は理論Tの構文的帰結であると言い、次のように表される。${\displaystyle T\vdash s}$s が我々の演繹システムにおいてTから証明可能である場合、sはTの意味論的帰結であると言い、次のように表記する。${\displaystyle T\models s}$s がTのすべてのモデルで成り立つ場合、完全性定理は、整列可能な言語を持つ任意の一階理論Tと、Tの言語の任意の文sに対して、

もし${\displaystyle T\models s}$、 それから${\displaystyle T\vdash s}$。

逆（健全性）も成り立つので、${\displaystyle T\models s}$かつその場合に限り${\displaystyle T\vdash s}$したがって、一階述語論理においては、構文的帰結と意味的帰結は等価である。

このより一般的な定理は、例えば、任意の群を考察し、その群によって文が満たされることを示すことによって、群論の公理から文が証明可能であることを示す場合などに、暗黙のうちに用いられます。

ゲーデルの本来の定式化は、公理を持たない理論という特殊なケースを取り上げることによって導き出される。

モデル存在定理

完全性定理は、ヘンキンのモデル存在定理の結果として、一貫性の観点からも理解できます。理論Tが構文的に一貫しているとは、私たちの演繹システムにおいて、文sとその否定 ¬ sの両方がTから証明できるような文sが存在しないことを意味します。モデル存在定理は、整列可能な言語を持つ任意の一階理論Tに対して、

もし${\displaystyle T}$構文的に一貫しているならば、${\displaystyle T}$モデルがあります。

レーヴェンハイム＝スコレムの定理に関連する別のバージョンでは、次のように述べられています。

構文的に一貫性のある、可算な一階述語論理はすべて、有限または可算なモデルを持つ。

ヘンキンの定理が与えられれば、完全性定理は次のように証明できる。${\displaystyle T\models s}$、 それから${\displaystyle T\cup \lnot s}$モデルは存在しない。ヘンキンの定理の対偶により、${\displaystyle T\cup \lnot s}$構文的に矛盾している。したがって矛盾（${\displaystyle \bot }$) は証明可能である${\displaystyle T\cup \lnot s}$演繹体系において。したがって${\displaystyle (T\cup \lnot s)\vdash \bot }$そして演繹体系の特性により、${\displaystyle T\vdash s}$。

完全性定理の重要な帰結の一つは、計算可能列挙可能な一階述語論理の公理から可能なすべての形式的推論を列挙し、それを用いて結論を列挙することによって、計算可能列挙可能な任意の一階述語論理の意味論的帰結を計算可能列挙できるということである。

これは、特定の言語におけるすべての構造を定量化する意味的帰結という概念の直接的な意味とは対照的であり、明らかに再帰的な定義ではない。

また、これにより「証明可能性」、ひいては「定理」という概念が、理論の公理系の選択のみに依存し、証明体系の選択には依存しない明確な概念となる。

ゲーデルの不完全性定理は、数学における任意の一次理論内で証明できることには本質的な限界があることを示しています。その名称にある「不完全性」は、「完全」の別の意味を指しています（モデル理論 - コンパクト性定理と完全性定理の使用を参照）。理論${\displaystyle T}$すべての文が${\displaystyle S}$言語で${\displaystyle T}$証明可能か(${\displaystyle T\vdash S}$）または反証可能（${\displaystyle T\vdash \neg S}$)

第一不完全性定理は、いかなる${\displaystyle T}$一貫性があり、計算可能で、ロビンソン算術（「Q」）を含むものは、明示的に文を構築することによって、この意味で不完全でなければならない。${\displaystyle S_{T}}$それは明らかに証明も反証もできない${\displaystyle T}$第二不完全性定理は、以下のことを示すことでこの結果を拡張する。${\displaystyle S_{T}}$一貫性を表現するように選択できます${\displaystyle T}$自体。

以来${\displaystyle S_{T}}$証明できない${\displaystyle T}$完全性定理は、モデルの存在を意味する。${\displaystyle T}$その中で${\displaystyle S_{T}}$誤りです。実際には、${\displaystyle S_{T}}$これはΠ ₁文であり、つまり、ある有限性の性質がすべての自然数に当てはまることを述べている。したがって、モデルにおいてそれが偽であれば、モデルの自然数のいずれかが反例となる。この反例が標準自然数の中に存在すれば、それは反証となる。${\displaystyle S_{T}}$内で${\displaystyle T}$しかし、不完全性定理はこれが不可能であることを示したので、反例は標準数であってはならず、したがって、${\displaystyle T}$その中で${\displaystyle S_{T}}$偽の場合は、非標準の数値を含める必要があります。

実際、算術モデル存在定理の体系的な構築によって得られる、Qを含むあらゆる理論のモデルは、常に非標準であり、非等価な証明可能性述語と、その構築を解釈する非等価な方法を持つため、この構築は非再帰的である（再帰的な定義は曖昧さがないはずである）。

また、もし${\displaystyle T}$が少なくともQよりわずかに強い場合(例えば、有界存在式に対する帰納法を含む場合)、テネンバウムの定理は、再帰的な非標準モデルが存在しないことを示しています。

完全性定理とコンパクト性定理は、一階述語論理の二つの基礎となる定理である。これらの定理はどちらも完全に有効な方法で証明することはできないが、それぞれを他方から効果的に導き出すことができる。

コンパクト性定理は、論理式φが（無限集合である可能性のある）論理式の集合Γの論理的帰結であるならば、φはΓの有限部分集合の論理的帰結でもあると述べている。これは完全性定理の直接的な帰結である。なぜなら、φの形式的演繹において言及できるΓの公理は有限個に限られ、演繹体系の健全性からφはこの有限集合の論理的帰結であることが導かれるからである。このコンパクト性定理の証明は、もともとゲーデルによるものである。

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

完全性定理の無効性は、逆数学の手法で測定できます。可算言語について考えると、完全性定理とコンパクト性定理は互いに等価であり、弱いケーニッヒの補題として知られる弱い選択公理の形式と等価です。この等価性は、RCA ₀ ( Σ ⁰ _{1式に対する帰納法に制限された}ペアノ算術の 2 階変形) で証明可能です。弱いケーニッヒの補題は、選択公理のないツェルメロ・フレンケル集合論の体系である ZF で証明可能であり、したがって可算言語の完全性定理とコンパクト性定理は ZF で証明可能です。しかし、言語の濃度が任意に大きい場合は状況が異なります。その場合、完全性定理とコンパクト性定理は ZF で互いに証明可能等価のままですが、超フィルター補題として知られる弱い選択公理の形式とも証明可能等価になります。特に、ZFを拡張する理論では、同じ濃度の集合上で超フィルター補題を証明せずに、任意の（場合によっては非可算な）言語上で完全性定理またはコンパクト性定理を証明することはできない。

完全性定理は一階述語論理の中心的な性質ですが、すべての論理体系に当てはまるわけではありません。例えば、二階述語論理は標準意味論に対して完全性定理を持ちません（ただし、ヘンキン意味論に対しては完全性を持っています）。また、二階述語論理における論理的に妥当な式の集合は再帰的に列挙可能ではありません。これはすべての高階述語論理にも当てはまります。高階述語論理に対して健全な演繹体系を構築することは可能ですが、そのような体系はどれも完全ではありません。

リンドストロームの定理は、一階述語論理が（一定の制約の下で）コンパクト性と完全性の両方を満たす最も強力な論理であると述べている。

クリプキ意味論に関して、様相論理または直観主義論理の完全性定理を証明することができる。

ゲーデルによるこの定理の元の証明は、問題を特定の構文形式の論理式の特殊なケースに還元し、その形式をアドホックな議論で扱うことによって進められた。

現代の論理学の教科書では、ゲーデルの完全性定理は、ゲーデル自身の証明ではなく、ヘンキンの証明を用いて示されることが多い。ヘンキンの証明は、しばしば以下の手順で示される。

• すべての式について、理論をヘンキン化する。${\displaystyle \psi (x)}$常に${\displaystyle c_{\psi }}$そして公理$\displaystyle \exists _{x}\psi (x)\to \psi (c_{\psi })}$。
• リンデンバウムの補題を適用して、完全な拡張を得る。
• 関連項モデルを構築する。^{[ 4 ]}

ジェームズ・マーゲットソン（2004）は、イザベル定理証明器を用いたコンピュータによる形式的証明を開発した。^{[ 5 ]}他の証明も知られている。

• ゲーデルの完全性定理の原典証明
• トラクテンブロートの定理

• ゲーデル、K (1929)。Über die Vollständigkeit des Logikkalküls (論文)。博士論文。ウィーン大学。完全性定理の最初の証明。
• ゲーデル、K (1930)。 「Die Vollständigkeit der Axiome des logischen Funktionenkalküls」。Monatshefte für Mathematik (ドイツ語)。37 (1): 349–360。土井: 10.1007/BF01696781。JFM 56.0046.04。S2CID 123343522。  論文と同じ内容だが、証明をより簡潔にし、説明をより簡潔にし、長々とした序論を省略している。
• ハンス・ヘルメス（1973）。数理論理学入門。大学教科書（シュプリンガー出版）。ロンドン：シュプリンガー。ISBN 3540058192ISSN 1431-4657​​ 第5章：「ゲーデルの完全性定理」

• スタンフォード哲学百科事典：「クルト・ゲーデル」—ジュリエット・ケネディ著。
• MacTutorの略歴：クルト・ゲーデル。 2005年10月13日にWayback Machineにアーカイブされました。
• Detlovs、Vilnis、および Podnieks、Karlis、「数学的論理入門」 。