ゲーデルの完全性定理

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

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

完全性定理は、さまざまなモデルで何が真実であるかを扱うモデル理論と、特定の形式体系で何が形式的に証明できるかを研究する証明理論とを密接に結び付けます。

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

第一階述語論理には、自然演繹システムやヒルベルトスタイルのシステムなど、多数の演繹システムがあります。すべての演繹システムに共通するのは、形式的演繹の概念です。これは、特別に指定された結論を伴う式のシーケンス（または、場合によっては有限ツリー）です。演繹の定義は、それが有限であり、特定の式のシーケンス（またはツリー）が実際に演繹であることをアルゴリズム的に（たとえば、 コンピューターまたは手作業で）検証できるというものです。

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

第一階論理の特定の演繹体系が健全かつ完全である場合、それは「完全」であり（式は論理的に有効である場合にのみ証明可能）、したがって同じ品質の他の演繹体系と同等である（1 つの体系の証明は他の体系に変換できる）。

まず、よく知られている同等のシステムのいずれかを選択して、一階述語計算の演繹システムを固定します。ゲーデルの元の証明では、ヒルベルト-アッカーマン証明システムを前提としていました。

完全性定理は、式が論理的に有効である場合、その式の有限演繹（正式な証明）が存在することを述べています。

したがって、演繹システムは、すべての論理的に有効な式を証明するために追加の推論規則が必要ないという意味で「完全」です。完全性の逆は健全性であり、演繹システムでは論理的に有効な式のみが証明可能であるという事実です。健全性（検証が容易）とともに、この定理は、式が正式な演繹の結論である 場合に限り、その式が論理的に有効であることを意味します。

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

ならば、。${\displaystyle T\models s}$${\displaystyle T\vdash s}$

逆（健全性）も成り立つため、の場合に限りとなり、したがってその構文的および意味的結果は一階述語論理では同等となります。 ${\displaystyle T\models s}$ ${\displaystyle T\vdash s}$

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

ゲーデルのオリジナルの定式化は、公理のない理論の特定のケースを取り上げることで導き出されます。

完全性定理は、ヘンキンのモデル存在定理の結果として、一貫性の観点からも理解できます。演繹システムでTからsとその否定 ¬ sの両方が証明可能な文sが存在しない場合に、理論Tは統語的に一貫していると言えます。モデル存在定理は、整列可能な言語を持つ 任意の一階理論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}$

モデル存在定理とその証明は、ペアノ算術の枠組みで形式化できます。正確には、Tの各記号を、その記号の引数を自由変数とする算術式で解釈することにより、ペアノ算術における任意の無矛盾な有効一階理論Tのモデルを体系的に定義できます。(多くの場合、構築の仮説として、 T が無矛盾であると仮定する必要があります。ペアノ算術ではその事実を証明できない可能性があるためです。) ただし、この式で表される定義は再帰的ではありません (ただし、一般にはΔ ₂です)。

完全性定理の重要な帰結は、理論の公理から可能な形式的演繹をすべて列挙することによって、任意の有効な一階理論の意味論的帰結を再帰的に列挙し、これを使用して結論の列挙を生成することが可能であるということです。

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

また、これにより、「証明可能性」の概念、つまり「定理」の概念が、証明システムの選択ではなく、理論の公理の選択されたシステムのみに依存する明確な概念になります。

ゲーデルの不完全性定理は、数学のあらゆる第一階理論内で証明できる内容には固有の限界があることを示しています。その名前の「不完全性」は、完全性の別の意味を指します(モデル理論 - コンパクト性定理と完全性定理の使用を参照)。の言語のすべての文が証明可能 ( ) または反証可能 ( )である場合、理論は完全 (または決定可能) です。 ${\displaystyle T}$${\displaystyle S}$${\displaystyle T}$${\displaystyle T\vdash S}$${\displaystyle T\vdash \neg S}$

最初の不完全性定理は、内で証明も反証も不可能な文を明示的に構築することにより、 が無矛盾で有効であり、ロビンソン算術 (" Q ") を含む任意の がこの意味で不完全でなければならないことを述べています。2番目の不完全性定理は、 が自身 の無矛盾性を表現するように選択できることを示すことにより、この結果を拡張します。${\displaystyle T}$${\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 を含むあらゆる理論のモデルは、非同等の証明述語と、それ自身の構築を解釈する非同等の方法を持つ非標準であり、そのためこの構築は非再帰的です (再帰的な定義は明確であるため)。

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

完全性定理とコンパクト性定理は、一階述語論理の 2 つの基礎です。これらの定理はどちらも完全に効果的な方法で証明することはできませんが、一方から他方を効果的に導くことができます。

コンパクト性定理は、式 φ が（おそらく無限の）式集合 Γ の論理的帰結である場合、それは Γ の有限部分集合の論理的帰結である、というものです。これは完全性定理の直接的な帰結です。なぜなら、Γ からの公理のうち、φ の形式的な演繹で言及できるのは有限個だけであり、演繹システムの健全性は、φ がこの有限集合の論理的帰結であることを意味するからです。コンパクト性定理のこの証明は、もともとゲーデルによるものです。

逆に、多くの演繹システムでは、コンパクト性定理の有効な結果として完全性定理を証明することが可能です。

完全性定理の無効性は、逆数学の線に沿って測定することができます。可算言語で考えると、完全性定理とコンパクト性定理は互いに同値であり、弱いケーニッヒの補題として知られる選択公理の弱い形式と同値であり、同値性は RCA _{0 (Σ} ⁰ ₁の式での帰納法に制限されたペアノ算術の 2 次変形) で証明可能です。弱いケーニッヒの補題は、選択公理を持たないツェルメロ–フレンケル集合論のシステムである ZF で証明可能であり、したがって可算言語の完全性定理とコンパクト性定理は ZF で証明可能です。ただし、言語の基数が任意の大きさの場合は状況が異なり、その場合、完全性定理とコンパクト性定理は ZF で互いに同値であることが証明されますが、超フィルタ補題として知られる選択公理の弱い形式とも同値であることが証明されます。特に、ZF を拡張する理論は、同じ濃度の集合上の超フィルタ補題を証明せずに、任意の (おそらくは無数な) 言語上の完全性定理またはコンパクト性定理を証明することはできません。

完全性定理は、すべての論理に当てはまるわけではない、一階論理の中心的な性質です。たとえば、二階論理には、その標準的な意味論に対する完全性定理はありません (ただし、ヘンキン意味論に対する完全性の性質はあります)。また、二階論理の論理的に有効な式の集合は、再帰的に列挙できません。同じことは、すべての高階論理にも当てはまります。高階論理に対して健全な演繹システムを作成することは可能ですが、そのようなシステムは完全ではありません。

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

完全性定理は、クリプキ意味論に関して様相論理または直観論理に対して証明できます。

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

現代の論理学の教科書では、ゲーデルの完全性定理は、ゲーデルのオリジナルの証明ではなく、ヘンキンの証明で証明されることが多い。ヘンキンの証明は、あらゆる一貫した一階理論の項モデルを直接構築する。ジェームズ・マーゲットソン（2004）は、イザベル定理証明器を使用してコンピューターによる形式的証明を開発した。^[4]他の証明も知られている。

• ゲーデルの不完全性定理
• ゲーデルの完全性定理のオリジナル証明

• ゲーデル、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年）。『数学論理学入門』。Hochschultext（Springer-Verlag）。ロンドン：Springer。ISBN 3540058192. ISSN  1431-4657.第5章：「ゲーデルの完全性定理」。

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