完全性定理 は、一階述語論理において「正しい（すべてのモデルで成り立つ）ものは、必ず証明できる」ことを保証する定理です。意味（モデル）と構文（証明）という、まったく別の方法で定義された2つの「正しさ」が一致することを示しています。

この定理には、歴史的に重要な2つの証明があります。

  • ゲーデル流：1929年の博士論文と1930年の論文による、元の証明（文献 [1]、[9]）。
  • ヘンキン流：1949年にヘンキンが与えた証明（文献 [3]）。今日の教科書ではこちらが標準です。

この記事では、2つの証明の道筋を、細部を省きつつも骨組みが分かるように追いかけます。

2つの証明の流れ。ゲーデル流は命題論理への帰着、ヘンキン流は極大無矛盾集合を足場にする

1. 準備：意味と証明

1.1 意味：モデルと充足

一階の言語 L\mathcal{L}（述語記号、関数記号、定数記号の集まり）を固定します。L\mathcal{L} の 構造 M\mathcal{M} は、空でない領域 MM と、各記号の解釈からなります。

文 σ\sigma が M\mathcal{M} で成り立つことを M⊨σ\mathcal{M} \models \sigma と書きます。この「成り立つ」の定義は、タルスキによる帰納的な定義です。

1.2 証明：形式的な導出

一方、証明 は、公理と推論規則だけを使って、記号列を機械的に書き換えていく操作です。ここでは、命題論理の公理図式、量化子の公理、モーダスポネンス、汎化の規則からなる、ヒルベルト流の体系を考えます。

Γ\Gamma から φ\varphi が導出できることを Γ⊢φ\Gamma \vdash \varphi と書きます。また、ある φ\varphi について Γ⊢φ\Gamma \vdash \varphi と Γ⊢¬φ\Gamma \vdash \neg\varphi がどちらも成り立つとき、Γ\Gamma は 矛盾している といい、そうでないとき 無矛盾 であるといいます。

この体系について、次の2つの性質は比較的簡単に示せます。証明の中で何度も使います。

  • 健全性：Γ⊢φ\Gamma \vdash \varphi ならば Γ⊨φ\Gamma \models \varphi（証明できるものは正しい）。
  • 演繹定理：Γ∪{ψ}⊢φ\Gamma \cup \{\psi\} \vdash \varphi ならば Γ⊢ψ→φ\Gamma \vdash \psi \to \varphi。

1.3 完全性定理の2つの形

Γ=∅\Gamma = \varnothing の場合、つまり「妥当な文は証明できる」が 弱い形 です。ゲーデルが1929年に証明したのは主にこちらです。

強い形は、次の モデル存在定理 と同値です。ヘンキンの証明はこの形を直接示します。

2. ゲーデル流の証明

ゲーデルの証明の核心は、一階述語論理の問題を、無限個の命題論理の問題に帰着する ことです。ゲーデルが扱った言語は、関数記号を含まない（述語記号と等号のみの）言語でした。以下でも、まず等号のない場合を考えます。

ゲーデルが実際に示したのは、次の形の定理です。

以下の証明で作るモデルの領域は自然数（変数全体）なので、充足可能な場合は 可算な領域で 充足できることも同時に分かります（文献 [10]）。

この定理を ¬φ\neg\varphi に当てはめると、弱い形の完全性定理が出ます。φ\varphi が妥当なら ¬φ\neg\varphi は充足不可能なので、¬φ\neg\varphi は反駁可能、つまり ⊢¬¬φ\vdash \neg\neg\varphi です。したがって ⊢φ\vdash \varphi となります。

2.1 ステップ1：標準形への帰着

まず、論理式を 冠頭標準形（量化子をすべて先頭に出した形）にします。ゲーデルは、スコーレムがレーヴェンハイム＝スコーレムの定理の証明で使った方法を応用し、新しい述語記号を導入することで、さらに次の形の論理式だけを考えれば十分であることを示しました（文献 [10]）。

φ  =  ∀x1⋯∀xk  ∃y1⋯∃ym  ψ(x1,…,xk,y1,…,ym)\varphi \;=\; \forall x_1 \cdots \forall x_k \; \exists y_1 \cdots \exists y_m \; \psi(x_1, \dots, x_k, y_1, \dots, y_m)

ここで ψ\psi は量化子を含まない論理式です。「すべての xˉ\bar{x} に対して、ある yˉ\bar{y} が存在して、ψ\psi が成り立つ」という形です。

2.2 ステップ2：命題論理式の列を作る

変数を v0,v1,v2,…v_0, v_1, v_2, \dots と並べます。ψ\psi の xˉ\bar{x} と yˉ\bar{y} に、次の規則で変数を代入していきます。

  • xˉ\bar{x} には、それまでに登場した変数の kk 個組 を、もれなく順番に代入する。
  • yˉ\bar{y} には、毎回 まだ使っていない新しい変数 を mm 個代入する。

最初は xˉ=(v0,…,v0)\bar{x} = (v_0, \dots, v_0)、yˉ=(v1,…,vm)\bar{y} = (v_1, \dots, v_m) とします。こうして得られる nn 番目の代入例を ψn\psi_n とし、最初の nn 個の連言を

Bn  =  ψ1∧ψ2∧⋯∧ψnB_n \;=\; \psi_1 \wedge \psi_2 \wedge \cdots \wedge \psi_n

とおきます。BnB_n は量化子を含まないので、R(v2,v5)R(v_2, v_5) のような原子論理式の1つ1つを命題変数とみなせば、命題論理の論理式 として扱えます。

2.3 ステップ3：二者択一

ここで、次の2つの場合に分かれます。

(a) どれかの BnB_n が、命題論理の論理式として充足不可能な場合

¬Bn\neg B_n は命題論理のトートロジーなので、述語論理でも証明でき、汎化により ⊢¬∃vˉ Bn\vdash \neg \exists \bar{v}\, B_n が得られます（∃vˉ\exists \bar{v} は BnB_n に現れる変数すべてについての存在量化）。

一方、φ\varphi から BnB_n の存在閉包が証明できることが、代入例の作り方から帰納法で示せます。

⊢φ→∃vˉ Bn\vdash \varphi \to \exists \bar{v}\, B_n

この2つを合わせると ⊢¬φ\vdash \neg\varphi、つまり φ\varphi は 反駁可能 です。

(b) すべての BnB_n が、命題論理の論理式として充足可能な場合

各 BnB_n には、それを真にする真理値の割り当てがあります。ただし、nn ごとに割り当てがばらばらでは困ります。欲しいのは、すべての BnB_n を同時に真にする1つの割り当て です。

BnB_n に現れる原子論理式は有限個なので、「BnB_n を真にする割り当て」を nn の順に延長していく木は、各段で枝分かれが有限個の無限の木になります。今日の言葉でいえば ケーニヒの補題 により、この木には無限に続く枝があります。その枝が、すべての BnB_n を同時に真にする割り当て VV を与えます。

2.4 ステップ4：変数からモデルを作る

割り当て VV から、次のように構造 M\mathcal{M} を作ります。

  • 領域：変数全体 {v0,v1,v2,… }\{v_0, v_1, v_2, \dots\}（自然数と同一視できる可算集合）。
  • 述語の解釈：RM(vi1,…,vir)R^{\mathcal{M}}(v_{i_1}, \dots, v_{i_r}) が成り立つ   ⟺  \iff VV が原子論理式 R(vi1,…,vir)R(v_{i_1}, \dots, v_{i_r}) を真とする。

すべての ψn\psi_n が M\mathcal{M} で成り立ちます。領域の任意の kk 個組は、いつか xˉ\bar{x} に代入されています。そのとき yˉ\bar{y} に代入された新しい変数が、ψ\psi を満たす「証人」になっています。したがって

M⊨∀xˉ ∃yˉ ψ\mathcal{M} \models \forall \bar{x}\, \exists \bar{y}\, \psi

となり、φ\varphi は 可算な領域で充足可能 です。これで二者択一が示されました。

2.5 ゲーデル流の特徴

  • 命題論理の完全性を足場にしている：述語論理の問題を、無限個の命題論理の問題と、それらを貼り合わせる「コンパクト性」の議論に分解しています。
  • 副産物が多い：同じ論文で、ゲーデルは可算個の論理式の集合にも議論を広げ、コンパクト性定理（可算個の論理式の集合は、その有限部分集合がすべて充足可能なら、全体も充足可能）にあたる結果も得ています（文献 [10]）。モデルが可算になることから、レーヴェンハイム＝スコーレムの定理 も同時に得られます。
  • スコーレムとの関係：一階述語論理の完全性は、スコーレムが1920年代前半に証明し1928年の論文で論じた結果から、系として導けるものでした。しかしスコーレム自身は、それを完全性定理として述べてはいません（文献 [11]）。ゲーデルは後年、スコーレムの研究に暗に解答が含まれていたことを、当時は知らなかったと認めています（1964年のファン・ハイエノールト宛ての手紙。文献 [12]）。ゲーデルの貢献は、モデルの構成を 形式的な証明可能性 と結びつけ、完全性という形で明確に述べた点にあります。

3. ヘンキン流の証明

ヘンキンは、標準形への変換を使わずに、無矛盾な理論から直接モデルを作る 方法を与えました（文献 [3]）。モデルの要素は、閉項（変数を含まない項）そのものです。ヘンキンは論文の冒頭で、それまでに発表された一階述語論理の完全性の証明は、ゲーデルの元の証明と、ヒルベルトとベルナイスによるその変形だけだったと述べています。

方針は次の3段階です。

ヘンキンの証明の3段階

  1. 証人の追加：「∃x φ(x)\exists x\, \varphi(x) ならば φ(c)\varphi(c)」という公理を加え、存在文ごとに証人となる定数 cc を用意する。
  2. 極大化：理論を、どの文についてもそれ自身か否定のどちらかを含む 極大無矛盾集合 Δ\Delta に拡大する。
  3. 項モデル：閉項を要素とする構造 M\mathcal{M} を作り、M⊨σ  ⟺  σ∈Δ\mathcal{M} \models \sigma \iff \sigma \in \Delta を示す。

以下、言語 L\mathcal{L} は可算であるとし、Γ\Gamma を無矛盾な文の集合とします。

3.1 ステップ1：証人を追加する

存在文 ∃x φ(x)\exists x\, \varphi(x) ごとに新しい定数 cφc_\varphi を用意し、次の ヘンキン公理 を加えます。

∃x φ(x)  →  φ(cφ)\exists x\, \varphi(x) \;\to\; \varphi(c_\varphi)

「何かが φ\varphi を満たすなら、cφc_\varphi がその1つだ」という意味です。

新しく加えた定数を含む存在文にも、また証人が必要です。そこで、言語の拡大を ω\omega 回繰り返します。

L=L0⊆L1⊆L2⊆⋯ ,L∗=⋃kLk\mathcal{L} = \mathcal{L}_0 \subseteq \mathcal{L}_1 \subseteq \mathcal{L}_2 \subseteq \cdots, \qquad \mathcal{L}^* = \bigcup_{k} \mathcal{L}_k

Lk+1\mathcal{L}_{k+1} は、Lk\mathcal{L}_k の存在文ごとに新しい定数を加えた言語です。加えたヘンキン公理全体を HH とします。Γ∪H\Gamma \cup H の有限部分には有限個のヘンキン公理しか含まれないので、補題1を1つずつ（定数が導入された順に）適用すれば、Γ∪H\Gamma \cup H は無矛盾です。

3.2 ステップ2：極大無矛盾集合に拡大する

こうして得た Δ\Delta は、次の性質を持ちます。

  • 演繹で閉じている：Δ⊢σ\Delta \vdash \sigma ならば σ∈Δ\sigma \in \Delta。
  • 否定：¬σ∈Δ  ⟺  σ∉Δ\neg\sigma \in \Delta \iff \sigma \notin \Delta。
  • 含意：(σ→τ)∈Δ  ⟺  σ∉Δ(\sigma \to \tau) \in \Delta \iff \sigma \notin \Delta または τ∈Δ\tau \in \Delta。
  • 証人の性質：∃x φ(x)∈Δ\exists x\, \varphi(x) \in \Delta ならば、ある定数 cc について φ(c)∈Δ\varphi(c) \in \Delta。

最後の性質は、Δ\Delta がヘンキン公理を含み、演繹で閉じていることから従います。

3.3 ステップ3：閉項からモデルを作る

Δ\Delta から、構造 M\mathcal{M} を次のように作ります。

  • 領域：L∗\mathcal{L}^* の閉項全体。
  • 関数記号：fM(t1,…,tn)=f(t1,…,tn)f^{\mathcal{M}}(t_1, \dots, t_n) = f(t_1, \dots, t_n)（項をそのまま組み立てる）。
  • 述語記号：RM(t1,…,tn)R^{\mathcal{M}}(t_1, \dots, t_n) が成り立つ   ⟺  \iff R(t1,…,tn)∈ΔR(t_1, \dots, t_n) \in \Delta。

等号を含む言語では、「(t=s)∈Δ(t = s) \in \Delta」で定まる同値関係で閉項を割った商を領域にします。等号の公理により、この同値関係は関数や述語と両立します。

Γ⊆Δ\Gamma \subseteq \Delta なので、M\mathcal{M}（を言語 L\mathcal{L} に制限したもの）は Γ\Gamma のモデルです。これでモデル存在定理、したがって強い形の完全性定理が示されました。

3.4 ヘンキン流の特徴

  • 標準形が不要：論理式の形を変換せずに、理論全体を一度に扱えます。
  • 強い形を直接示す：無限個の文からなる理論 Γ\Gamma を最初から扱えるので、コンパクト性定理も直ちに得られます。Γ\Gamma の有限部分がすべてモデルを持てば、Γ\Gamma は無矛盾だからです（導出は有限個の前提しか使わない）。
  • 非可算の言語にも拡張しやすい：ヘンキン自身が論文で、この方法が非可算個の記号を持つ体系にも一般化できることを指摘しています（文献 [3]）。文を並べる部分を、ツォルンの補題（または超限帰納法）に置き換えるだけです。モデルの大きさは言語の大きさで抑えられ、レーヴェンハイム＝スコーレムの定理の一般形も得られます。
  • 他の論理にも応用できる：同じ考え方で、ヘンキンは1950年に高階論理（型理論）の一般モデルに対する完全性を示しました（文献 [4]）。様相論理の 正準モデル による完全性証明も、極大無矛盾集合を「世界」とする、同じ系統の方法です。

4. 2つの証明の比較

観点ゲーデル流（1929–1930）ヘンキン流（1949）
直接示す形各論理式は反駁可能か充足可能か（弱い形）無矛盾な集合はモデルを持つ（強い形）
出発点1つの論理式文の集合（理論）全体
前処理標準形 ∀xˉ∃yˉψ\forall \bar{x} \exists \bar{y} \psi への変換証人となる定数とヘンキン公理の追加
中心となる道具命題論理への帰着とケーニヒの補題リンデンバウムの補題（極大無矛盾集合）
モデルの要素変数閉項（の同値類）
鍵となる事実代入例の連言 BnB_n がすべて充足可能真理補題 M⊨σ  ⟺  σ∈Δ\mathcal{M} \models \sigma \iff \sigma \in \Delta
一般化のしやすさ可算の言語が前提非可算の言語、高階論理、様相論理へ拡張しやすい

一見まったく違う証明ですが、どちらも 記号そのもの（変数や閉項）を要素とする構造を作る という点では共通しています。「構文から意味を作る」ことこそが、完全性定理の証明の本質だといえます。

5. その後の展開

ヘンキンの後も、完全性定理にはさまざまな証明が与えられました。

  • ラショーヴァとシコルスキ（1950年）：論理式の同値類がなすブール代数を考え、その上の極大フィルター（超フィルター）からモデルを作る、代数的な証明（文献 [5]）。可算個の上限・下限だけを保てばよいことに注目し、ベールのカテゴリー定理という位相的な道具を使っています（文献 [8]）。なお、この論文は Fundamenta Mathematicae の1950年の巻に収められていますが、実際の刊行は1951年です。
  • ベートとヒンティッカ（1955年）：証明を探す手続きそのものから、失敗した探索の跡としてモデルを読み取る、タブロー（意味論的タブロー、モデル集合）による方法（文献 [6]、[7]）。ベートは同じ方法を1954年にはすでに考えていたとされます（文献 [14]）。

特にタブローの方法は、「証明を探す」ことと「反例となるモデルを探す」ことが表裏一体であることを示しており、自動定理証明でも使われています（文献 [15]）。

まとめ

  • 完全性定理は、一階述語論理で 「正しい」と「証明できる」が一致する ことを述べる。
  • ゲーデル流 は、論理式を標準形にし、命題論理式の列 BnB_n の二者択一（どれかが矛盾するか、すべて充足可能か）に帰着させた。後者の場合は、ケーニヒの補題で変数を要素とする可算モデルを作る。
  • ヘンキン流 は、証人の追加とリンデンバウムの補題で極大無矛盾集合 Δ\Delta を作り、閉項を要素とするモデルで M⊨σ  ⟺  σ∈Δ\mathcal{M} \models \sigma \iff \sigma \in \Delta を示した。
  • どちらも 構文から意味（モデル）を作る。ヘンキン流は一般化しやすく、現代の論理学の標準的な道具になっている。
  • 年表で20世紀の流れを見るなら、20世紀の数理論理学の年表 もあわせてどうぞ。

参考文献

本文中の「文献 n」は、以下の番号に対応します。書誌情報は、出版社・データベースの記録で確認しました（2026年11月14日）。

一次文献（原論文）

  1. K. Gödel, "Die Vollständigkeit der Axiome des logischen Funktionenkalküls", Monatshefte für Mathematik und Physik, 37 (1930), pp. 349–360.（ゲーデルの博士論文を書き直したもの。英訳は文献 [2] に収録）
  2. K. Gödel, Kurt Gödel: Collected Works, Volume I: Publications 1929–1936, S. Feferman ほか編, Oxford University Press, 1986. 出版社のページ
  3. L. Henkin, "The Completeness of the First-Order Functional Calculus", The Journal of Symbolic Logic, 14(3) (1949), pp. 159–166. doi:10.2307/2267044 Cambridge Core
  4. L. Henkin, "Completeness in the Theory of Types", The Journal of Symbolic Logic, 15(2) (1950), pp. 81–91. Cambridge Core
  5. H. Rasiowa, R. Sikorski, "A proof of the completeness theorem of Gödel", Fundamenta Mathematicae, 37 (1950, 刊行は1951), pp. 193–200. doi:10.4064/fm-37-1-193-200 EuDML
  6. E. W. Beth, "Semantic entailment and formal derivability", Mededelingen der Koninklijke Nederlandse Akademie van Wetenschappen, Afd. Letterkunde, N.R. 18(13) (1955), pp. 309–342.
  7. K. J. J. Hintikka, "Form and content in quantification theory", Two Papers on Symbolic Logic, Acta Philosophica Fennica 8 (1955), pp. 7–55.（巻号を23とする文献もあるが、The Journal of Symbolic Logic の書評の記載に従った）JSL の書評（Beth と Hintikka の論文をまとめて扱う）

二次文献・解説

  1. M. Fitting, ラショーヴァの業績に関する論考（PDF）. PDF
  2. "Kurt Gödel", Stanford Encyclopedia of Philosophy.（博士論文の主定理が完全性定理であること、1929年にハーンのもとで学位を取得したこと）SEP
  3. "Original proof of Gödel's completeness theorem", Wikipedia（英語版）.（ゲーデルの証明の構成、標準形への帰着、等号の扱い、可算集合への拡張）Wikipedia
  4. "Thoralf Skolem", Wikipedia（英語版）.（スコーレムの1920年代の結果と完全性定理の関係）Wikipedia
  5. J. W. Dawson, Jr., "The published work of Kurt Gödel: an annotated bibliography".（ゲーデルの完全性定理の論文と、スコーレムの研究との関係についての注釈）PDF
  6. "On consistency and existence in mathematics", arXiv:2007.10167.（完全性定理と弱ケーニヒの補題の同値性への言及）arXiv
  7. A. S. Troelstra, E. W. Beth の業績に関する論考（ILLC の記念論文集への寄稿）.（ベートが1954年に意味論的タブローを考案したこと）PDF
  8. "Method of analytic tableaux", Wikipedia（英語版）. Wikipedia

準備（1章）とヘンキン流の証明の細部（3章）の数学的な内容は、一階述語論理の標準的な教科書で扱われる事項であり、骨組みは文献 [3] に基づきます。