FOL 完全性 (Henkin構築法)
Σ ⊨ A ⇒ Σ ⊢ A
対偶: Σ ⊢/ A ⇒ Σ ⊨/ A
{ Σ, ¬A }のタブローは閉じていない枝が存在 ⇒ { Σ, ¬A }が充足可能
無限枝の極限 (Hintikka集合) から項モデルを構成します。
一階述語論理式：半決定可能性（Semi-decidability）
① 恒真 (Valid)
$\Sigma \vDash A$
- 判定可能 (Decidable)
- タブロー{ Σ, ¬A }：有限ステップで必ず停止（すべての枝が閉じる）。
機械は必ず「YES」と答える。
② 恒真でない (Invalid) / 反モデルあり
$\Sigma \not\vDash A$
- 判定 不能の場合あり (Undecidable)
- タブロー{ Σ, ¬A }: 閉じない枝が存在する。
-
A. 有限で停止 (単純な反例)
-
B. 無限ループ (停止しない)
機械は「NO」と言うか、沈黙し続ける。
ここの「無限」を扱うのがHenkin証明！ ↓
1. 極限集合の構成 (The Limit Set)
タブローが閉じない場合、ケーニヒの補題より無限に続く枝 $\mathcal{B}$ が存在します。
展開戦略が公平 (Fair) である（すべての公式がいつかは処理される）と仮定し、この枝上のすべての論理式の和集合を $H$ と定義します。
$$ H = \bigcup_{n=0}^{\infty} \text{formulas}(Node_n) $$
この集合 $H$ は、以下の「ヒンティッカ集合」の性質を満たします。
2. ヒンティッカ集合 (Hintikka Set) の性質
集合 $H$ は以下の飽和条件を満たします（公平な戦略により保証されます）：
- 無矛盾性: 原子論理式 $P$ について、$P$ と $\neg P$ の両方が $H$ に含まれることはない。
- 下法飽和 (命題): $A \land B \in H \Rightarrow A, B \in H$ など、命題論理の分解規則がすべて適用済みであること。
- $\exists$ の飽和 (Witness):
もし $\exists x \phi(x) \in H$ ならば、ある定数 $c \in Term(H)$ が存在し、$\phi(c) \in H$。
（コード解説: これはプログラムが `newConst` を生成し続ける動作に対応します）
- $\forall$ の飽和 (Universality):
もし $\forall x \phi(x) \in H$ ならば、全ての定数 $t \in Term(H)$ について、$\phi(t) \in H$。
（コード解説: 無限に増える定数すべてに対し、ループ処理で $\forall$ を適用し続ける動作の極限です）
3. 項モデル (Canonical/Term Model)
集合 $H$ 自身を使って、モデル $M = (D, I)$ を構成します（Henkin Construction）。
定義域 D: $H$ に現れるすべての閉じた項（定数）の集合。
$$ D = \{ c_0, c_1, c_2, \dots \} $$
解釈 I: 原子論理式の真偽を $H$ への所属で決定する。
$$ (c_1, \dots, c_n) \in P^M \iff P(c_1, \dots, c_n) \in H $$
直観的解釈：なぜ記号をモデルにして良いのか？
通常、モデルとは現実の物体（例：リンゴや数字）の集まりですが、Henkinの方法では「名前（定数記号）そのものを実体とみなす」という大胆な発想をとります。
タブロー法が無限に新しい定数 $c_1, c_2, \dots$ を生成するとき、プログラム上は終わりのないプロセス（潜勢的無限）に見えます。しかし、数学的証明ではそのプロセスの極限としての全体（実無限）を捉えます。
「無限に生成される記号たち」全体を一つの定義域 $D$ として固定することで、無限の連鎖を断ち切ることなく、論理的に完結したモデルを構成できるのです。
4. 真理値補題 (Model Existence Lemma)
「任意の論理式 $\phi$ について、$\phi \in H \iff M \vDash \phi$」を、論理式の構成に関する構造的帰納法で証明します。
【基礎段階】原子論理式 $P(t_1, \dots, t_n)$
解釈 $I$ の定義により直接的に成立します。
$P(\vec{t}) \in H \iff \vec{t} \in P^M \iff M \vDash P(\vec{t})$。
【帰納段階：命題論理】
論理式 $\psi, \chi$ について補題が成立すると仮定します（帰納法の仮定 IH）。
-
否定 ($\phi = \neg \psi$):
$\neg \psi \in H \iff \psi \notin H$ （ヒンティッカ集合の極大無矛盾性より）
$\iff M \not\vDash \psi$ （IHより）
$\iff M \vDash \neg \psi$ （モデルの定義より）。
-
連言 ($\phi = \psi \land \chi$):
$\psi \land \chi \in H \iff \psi \in H \text{ かつ } \chi \in H$ （下法飽和性より）
$\iff M \vDash \psi \text{ かつ } M \vDash \chi$ （IHより）
$\iff M \vDash \psi \land \chi$。
-
含意 ($\phi = \psi \to \chi$):
$\psi \to \chi$ は $\neg \psi \lor \chi$ と等価です。
$\in H \iff \neg \psi \in H \text{ または } \chi \in H$ （飽和性より）
$\iff M \vDash \neg \psi \text{ または } M \vDash \chi$ （IHより）
$\iff M \vDash \psi \to \chi$。
【帰納段階：量子化】
-
存在量化 ($\phi = \exists x \psi(x)$):
$\exists x \psi(x) \in H \implies$ ある $c \in D$ について $\psi(c) \in H$ （Witness条件）。
$\implies$ IHより $M \vDash \psi(c)$。
$\implies$ 定義域 $D$ 内に $\psi$ を満たす要素 $c$ が存在するため、$M \vDash \exists x \psi(x)$。
-
全称量化 ($\phi = \forall x \psi(x)$):
$\forall x \psi(x) \in H \implies$ 全ての $t \in D$ について $\psi(t) \in H$ （Universality条件）。
$\implies$ IHより、全ての $t \in D$ について $M \vDash \psi(t)$。
$\implies$ $D$ はモデルの全要素であるため、$M \vDash \forall x \psi(x)$。
5. 結論
帰納法により、根ノード $S_0 = \{\Sigma, \neg A\}$ に含まれる全ての論理式はモデル $M$ で真となります。
すなわち、タブローが閉じない（証明できない）ならば、反例モデル $M$（無限モデルの可能性あり）が存在します。
対偶をとれば、$\Sigma \vDash A \Rightarrow \Sigma \vdash A$ となり、完全性が証明されました。
Q.E.D.
6. 派生する驚くべき帰結：モデルのサイズ
完全性定理の証明の中で構成した「項モデル $M$」をもう一度よく見てみましょう。
このモデルの定義域 $D$ は、タブローの枝に出現する定数（および閉項）の集合でした。
定義域 $D$ の濃度（Cardinality）は？
我々が扱う論理式の言語が可算（記号の数が有限、あるいは自然数と同じ程度）である限り、そこから生成される項の集合 $D$ もまた高々可算無限（Countable）です。
つまり、この証明は副産物として以下の定理を導き出しています。
下方レーヴェンハイム・スコーレムの定理
(Downward Löwenheim-Skolem Theorem)
定理：
「もし、ある第一階の理論 $T$ がモデルを持つ（無矛盾である）ならば、
$T$ は必ず可算なモデル（有限または可算無限）を持つ。」
証明の骨子：
ヘンキン構成で作ったモデル $M$ こそが、その「可算モデル」の実例である。
（どんなに巨大な無限を扱う理論であっても、閉項の集合 $D$ に押し込めることができる）
7. スコーレムのパラドックス (Skolem's Paradox)
ここで直観に反する事態が生じます。例えば「実数論（Real Analysis）」のような、非可算無限（数えきれない無限）を扱う公理系であっても、一階述語論理で記述されている限り、「可算なモデル（数えきれてしまう世界）」が存在してしまいます。
公理系の主張 (内部)
$\exists x (\text{uncountable})$
公理系の中では「実数は非可算である（自然数と1対1対応しない）」という定理 $\phi$ が証明可能です。
モデル $M$ も当然 $M \vDash \phi$ を満たします。
モデルの実体 (外部)
$\text{Domain } D \cong \mathbb{N}$
しかし、モデル $M$ 全体の要素数は可算です。
「非可算である」という事実さえも、可算な要素の上でシミュレートされていることになります。
解説：なぜ矛盾しないのか？
「非可算である」とは「全単射関数が存在しない」ことを意味します。
モデル $M$ の中では、実数と自然数を結ぶ全単射関数という「要素」が欠落しているため、モデル内部の住人にとっては「数え上げ不能（非可算）」に見えているだけなのです。
これを「概念の相対性」と呼びます。