⟐ 数学の作り方 How to make Mathematics

↑ ↓ 移動 Enter 開く Esc 閉じる

第7章 ゲーデルの完全性定理

「正しい」は、必ず「導ける」

命題論理では ⊢\vdash と ⊨\models が一致しました（第3章）。一階述語論理でも同じことが成り立つ—— これがゲーデルの完全性定理（1929年、博士論文）です。量化子・関数・無限の領域という複雑さが 加わってなお、「すべての構造で真な式（妥当な式）は、有限の記号操作で必ず導ける」。

Γ⊨φ  ⟺  Γ⊢φ.\Gamma\models\varphi \iff \Gamma\vdash\varphi.

⇐\Leftarrow（健全性）は前章で示しました。この章は ⇒\Rightarrow（完全性）を、ヘンキンの方法で完全に証明します。 戦略は第3章と同じ骨格——「無矛盾なら充足可能（モデルをもつ）」を示せば完全性が出る——ですが、 一階では致命的な難所があります。命題論理では極大無矛盾集合から付値を「読む」だけでモデルができました。 しかし一階では、∃x φ\exists x\,\varphi が理論に属していても、それを満たす具体的な対象が言語の中に無いかもしれない。 ヘンキンの発想は「無ければ、証人となる新しい定数を言語に足してしまえ」。この一手で、 理論そのものから領域（対象の集合）を作り出します。

完全性の本体は「無矛盾 ⇒ モデルが存在」。難所は ∃\exists の証人不足で、ヘンキンは証人定数を足して解決する。

目標の言い換え

定理 モデル存在定理（一階）

文の集合 Γ\Gamma が無矛盾ならば、Γ\Gamma はモデルをもつ（充足可能）。

これが示せれば完全性は第3章とまったく同じ論法で従います：Γ⊬φ\Gamma\not\vdash\varphi なら Γ∪{¬φ}\Gamma\cup\{\lnot\varphi\} は無矛盾、 モデル存在定理より Γ\Gamma を満たし φ\varphi を偽にする構造があり、Γ⊭φ\Gamma\not\models\varphi。以下、言語 L\mathcal L は 可算とする（非可算でもツォルンの補題を使えば同様。この選択公理への依存も完全性の重要な側面）。

段階1：ヘンキン証人の添加

まず「∃x φ\exists x\,\varphi が言えるなら、それを満たす名前がある」という状態を、言語ごと作ります。

定義 ヘンキン理論・証人性

理論 TT が証人性（Henkin property）をもつとは、任意の論理式 φ(x)\varphi(x)（自由変数 xx のみ）について、 ある定数 cc で「∃x φ(x)→φ(c)\exists x\,\varphi(x)\to\varphi(c)」が TT に属すること。この cc を ∃x φ\exists x\,\varphi の証人という。

補題 証人1個の添加は無矛盾性を保つ

TT を言語 L\mathcal L の無矛盾な理論、φ(x)\varphi(x) を論理式、cc を L\mathcal L に現れない新しい定数とする。 このとき T′=T∪{∃x φ(x)→φ(c)}T'=T\cup\{\exists x\,\varphi(x)\to\varphi(c)\} も無矛盾。

証明

T′T' が矛盾すると仮定する。演繹定理より T⊢¬(∃x φ(x)→φ(c))T\vdash\lnot(\exists x\,\varphi(x)\to\varphi(c))、命題論理で整理すると T⊢∃x φ(x)T\vdash\exists x\,\varphi(x) かつ T⊢¬φ(c)T\vdash\lnot\varphi(c)。cc は TT に現れないので、T⊢¬φ(c)T\vdash\lnot\varphi(c) の証明中の cc を新変数 yy で一斉に置換しても正しい証明であり T⊢¬φ(y)T\vdash\lnot\varphi(y)、yy は TT に自由に現れないから 一般化して T⊢∀y ¬φ(y)T\vdash\forall y\,\lnot\varphi(y)、すなわち T⊢¬∃x φ(x)T\vdash\lnot\exists x\,\varphi(x)。これは T⊢∃x φ(x)T\vdash\exists x\,\varphi(x) と 矛盾し、TT の無矛盾性に反する。∎

「新しい定数だから、それについて導けたことは実は任意の変数について導けたはず」という置換の議論が心臓です。 これをすべての論理式について同時に行い、さらに新定数が生む新しい論理式にも証人を、と繰り返します。

補題 ヘンキン拡大

可算無矛盾理論 TT（言語 L\mathcal L）に対し、可算言語 L∗⊇L\mathcal L^*\supseteq\mathcal L と無矛盾理論 T∗⊇TT^*\supseteq T で、 T∗T^* が証人性をもつものが存在する。

証明

L0=L, T0=T\mathcal L_0=\mathcal L,\ T_0=T から始め、各段 nn で Ln\mathcal L_n の全論理式 φ(x)\varphi(x) に対し新定数 cφc_\varphi を導入して Ln+1\mathcal L_{n+1} とし、Tn+1=Tn∪{∃x φ(x)→φ(cφ):φ∈Ln}T_{n+1}=T_n\cup\{\exists x\,\varphi(x)\to\varphi(c_\varphi):\varphi\in\mathcal L_n\} とする。上の補題 （を有限個ずつ適用；証明はどれも有限個の証人しか使わない）により各 TnT_n は無矛盾。L∗=⋃Ln\mathcal L^*=\bigcup\mathcal L_n、 T∗=⋃TnT^*=\bigcup T_n とおくと、T∗T^* の矛盾は有限個の公理しか使わずある TnT_n で起こるはずで不合理、ゆえに無矛盾。 L∗\mathcal L^* の任意の論理式は既にどこかの Ln\mathcal L_n に現れるので、その証人が Tn+1⊆T∗T_{n+1}\subseteq T^* にある。∎

段階2：極大無矛盾へ拡大（リンデンバウム）

第3章とまったく同じ手続きで、T∗T^* を極大無矛盾集合 Δ\Delta（言語 L∗\mathcal L^*）へ拡大します。

補題 証人性は極大化で保たれる

T∗⊆ΔT^*\subseteq\Delta、Δ\Delta を L∗\mathcal L^* 上の極大無矛盾集合とすると、Δ\Delta は次を満たす： （第3章の (a)(b)(c) に加えて）∀x φ∈Δ  ⟺  \forall x\,\varphi\in\Delta \iff すべての閉項 tt で φ[x:=t]∈Δ\varphi[x:=t]\in\Delta、 かつ ∃x φ∈Δ  ⟺  \exists x\,\varphi\in\Delta \iff ある定数 cc で φ[x:=c]∈Δ\varphi[x:=c]\in\Delta。

証明

第3章の (a)–(c)（演繹閉包・否定完全性・→\to の規則）はそのまま成り立つ。∃\exists：∃x φ∈Δ\exists x\,\varphi\in\Delta なら、 証人性の公理 ∃x φ→φ(cφ)∈T∗⊆Δ\exists x\,\varphi\to\varphi(c_\varphi)\in T^*\subseteq\Delta と MP・演繹閉包で φ(cφ)∈Δ\varphi(c_\varphi)\in\Delta。逆に φ[x:=c]∈Δ\varphi[x:=c]\in\Delta なら (A4) 系（φ(c)→∃x φ\varphi(c)\to\exists x\,\varphi）で ∃x φ∈Δ\exists x\,\varphi\in\Delta。∀\forall は ∀x φ≡¬∃x ¬φ\forall x\,\varphi\equiv\lnot\exists x\,\lnot\varphi と否定完全性から従う。∎

証人性のおかげで、Δ\Delta の中の「∃\exists」は必ず具体的な名前つきの証人をもちます。これが次のモデル構成で決定的です。

段階3：項モデルの構成

いよいよモデルを作ります。領域を外から用意するのではなく、言語の閉項そのものを対象とみなすのがヘンキンの妙技です。

定義 項モデル（正準モデル）

L∗\mathcal L^* の閉項（変数を含まない項）全体を CT\mathrm{CT} とする。CT\mathrm{CT} 上の関係 t∼t′  ⟺  (t=t′)∈Δt\sim t' \iff (t=t')\in\Delta は同値関係（Δ\Delta が等号公理を含み演繹で閉じているので反射・対称・推移）。商 M=CT/∼M=\mathrm{CT}/{\sim} を領域とし、 cM=[c],fM([t1],…,[tn])=[f(t1,…,tn)],([t1],…,[tn])∈RM  ⟺  R(t1,…,tn)∈Δc^{\mathcal M}=[c],\quad f^{\mathcal M}([t_1],\dots,[t_n])=[f(t_1,\dots,t_n)],\quad ([t_1],\dots,[t_n])\in R^{\mathcal M}\iff R(t_1,\dots,t_n)\in\Delta と解釈する。等号公理が ∼\sim との両立（well-defined 性・合同性）を保証する。

対象とは「名前（閉項）を、Δ\Delta が等しいと言うものどうしで同一視したもの」。証人性があるおかげで MM は空でなく（少なくとも証人定数がある）、しかも「∃\exists の対象」が必ず領域に居ます。関数・関係の解釈が 代表元 tit_i の取り方によらないこと（well-defined）は、等号公理 x=y→(… )x=y\to(\dots) が Δ\Delta にあることから従います。

段階4：真理補題

補題 真理補題

M\mathcal M を上の項モデルとする。L∗\mathcal L^* の任意の文 σ\sigma について M⊨σ  ⟺  σ∈Δ.\mathcal M\models\sigma \iff \sigma\in\Delta.

証明

まず閉項 tt について tM=[t]t^{\mathcal M}=[t] が項の構造に関する帰納法で従う（解釈の定義そのもの）。次に文 σ\sigma について 構造的帰納法。

原子文 R(t1,…,tn)R(t_1,\dots,t_n)：M⊨R(t1,…,tn)  ⟺  ([t1],…,[tn])∈RM  ⟺  R(t1,…,tn)∈Δ\mathcal M\models R(t_1,\dots,t_n)\iff([t_1],\dots,[t_n])\in R^{\mathcal M}\iff R(t_1,\dots,t_n)\in\Delta （解釈の定義）。等式 t1=t2t_1=t_2 も ∼\sim の定義より同様。

¬,→\lnot,\to：否定完全性 (b) と →\to の規則 (c)（極大無矛盾集合の性質）が、¬,→\lnot,\to の充足の定義とちょうど対応する （第3章の真理補題と同型の議論）。

∃x φ\exists x\,\varphi（∀\forall はその否定）： (⇒)(\Rightarrow) M⊨∃x φ\mathcal M\models\exists x\,\varphi なら、ある対象 [t]∈M[t]\in M で M⊨φ[x:=t]\mathcal M\models\varphi[x:=t]。φ[x:=t]\varphi[x:=t] は φ\varphi より簡単な文なので帰納法の仮定より φ[x:=t]∈Δ\varphi[x:=t]\in\Delta、よって（φ(t)→∃x φ\varphi(t)\to\exists x\,\varphi が導けるので）∃x φ∈Δ\exists x\,\varphi\in\Delta。 (⇐)(\Leftarrow) ∃x φ∈Δ\exists x\,\varphi\in\Delta なら、証人性（段階2の補題）よりある定数 cc で φ[x:=c]∈Δ\varphi[x:=c]\in\Delta。帰納法の仮定で M⊨φ[x:=c]\mathcal M\models\varphi[x:=c]、すなわち対象 [c][c] が φ\varphi を満たすので M⊨∃x φ\mathcal M\models\exists x\,\varphi。∎

証明の全行程で、(⇐)(\Leftarrow) の ∃\exists の場合だけが証人性を本質的に使います。ここがヘンキン構成の要で、 「Δ\Delta が ∃x φ\exists x\,\varphi を認めるなら、その証人 cc が領域に居て実際に φ\varphi を満たす」——だから 「Δ\Delta に属する ＝ モデルで真」が量化子を越えて成立するのです。

完成

証明

真理補題より M⊨Δ\mathcal M\models\Delta、特に M⊨T⊆Δ\mathcal M\models T\subseteq\Delta。M\mathcal M は言語 L∗\mathcal L^* の構造だが、 非論理記号を L\mathcal L に制限（reduct）すれば元の Γ⊆T\Gamma\subseteq T のモデルになる。よって Γ\Gamma は充足可能—— モデル存在定理が示せた。ゆえに完全性 Γ⊨φ⇒Γ⊢φ\Gamma\models\varphi\Rightarrow\Gamma\vdash\varphi が成り立つ。∎

定理 ゲーデルの完全性定理

一階述語論理において Γ⊨φ  ⟺  Γ⊢φ\Gamma\models\varphi \iff \Gamma\vdash\varphi。 （健全性は前章、完全性は本章。）

つまずきポイント

注意 よくある誤解

  • 完全性 ≠ 完全な理論。 「完全性定理」は論理の証明体系が妥当な式を全部導けること。特定の理論 TT が「完全（すべての文の真偽を決める）」かは別問題で、第13章の不完全性はまさにそこを否定する。
  • モデルは言語から作られる。 領域は外から与えるのでなく、閉項の同値類。証人性が「∃\exists の対象」を言語内に用意する。
  • 可算言語では帰納的、非可算では選択公理。 ヘンキン拡大とリンデンバウムは、非可算だとツォルンの補題を要する。完全性は選択公理に（弱く）依存する。

この章のまとめ

  • 完全性の本体はモデル存在定理「無矛盾 ⇒ 充足可能」。命題論理と同じ骨格だが、∃\exists の証人不足という難所がある。
  • ヘンキンの構成：(1) 証人定数を添加して証人性をもつ無矛盾拡大を作る、(2) 極大無矛盾集合へ拡大、(3) 閉項の同値類を領域とする項モデルを作る、(4) 真理補題（∃\exists の場合に証人性が効く）で締める。
  • 結論、一階述語論理で ⊢\vdash と ⊨\models は一致する。証明は可算なら帰納的、非可算なら選択公理に依存する。

次章は、完全性の“ご褒美”——コンパクト性定理とレーヴェンハイム–スコーレムの定理、そして超準モデルへ進みます。