超丁寧に解説するゲーデルの完全性定理（後編）
後編について
前編
では命題論理の完全性定理を証明した。骨格はこうだった。
$$
\text{無矛盾な } T \ \xrightarrow{\ \text{Lindenbaum}\ } \ \text{極大無矛盾な } T \subseteq U \ \xrightarrow{\ \text{真理補題}\ } \ T \text{ のモデル}$$
後編では、この骨格をそのまま維持したまま述語論理の完全性定理を証明する。維持したまま、というのは文字どおりで、Lindenbaumの補題も真理補題も、名前も役割もそっくり同じものが出てくる。
違いはただ一点である。命題論理のモデルは真理値割り当て、すなわち「どの命題変数を真とするか」を決めるだけの対象だった。述語論理のモデルは構造であり、台集合の元、すなわち登場人物を用意しなければならない。材料は構文しかないのだから、登場人物も構文から調達するほかない。その調達がうまくいくように言語をあらかじめ整備しておく、というのが後編で追加される唯一の作業である。
なお前編の議論のうち、背理法の補題・片方無矛盾の補題・有限性補題・極大無矛盾集合まわりの補題・Lindenbaumの補題は、述語論理でもそのまま成り立つ。これらの証明が使っているのは演繹定理と$\mathbf{P1}$〜$\mathbf{P3}$、および「証明は有限列である」という性質だけであり、公理と推論規則が増えても壊れないからである。以下では、これらを前編の名前で呼んで自由に使う。
舞台設定
言語
言語$L$は定数記号・関数記号・関係記号からなる集合とする。等号$=$は論理記号として常に含める。項、論理式は通常どおり定義する。自由変数を持たない項を閉項、自由変数を持たない論理式を文という。
論理記号は$\neg, \to, \forall$を原始的とし、$\lor, \land$は前編と同じ略記、$\exists$は次の略記とする。
$$
\exists x \varphi \equiv \neg\forall x \neg\varphi$$
$\varphi(x)$と書いたら「$x$以外に自由変数を持たない論理式」を、$\varphi(t)$で$x$に項$t$を代入したものを表す。代入可能性（$t$の変数が代入先で束縛されないこと）は常に仮定する。
また、この記事では「等しい」が二つの意味で出てくるので記号を分けておく。$t_1 = t_2$は対象言語の等号であり、論理式の一部として理論に属したり属さなかったりする。$s \equiv t$は記号列として同一であるというメタな主張である。$c$と$d$が別の定数記号なら$c \not\equiv d$だが、$(c = d)$という論理式がある理論に属することはありうる。この区別が後半の要点になる。
名前による意味論
$L$-構造$\mathfrak{M}$は空でない台集合$|\mathfrak{M}|$と、$L$の各記号の解釈からなる。
さて、$\mathfrak{M}$において文の真偽を定めたい。$\neg$と$\to$は前編と同じでよいが、$\forall x \varphi(x)$が問題になる。「$|\mathfrak{M}|$のすべての元$a$について$\varphi$が成り立つ」と言いたいが、$a$は台集合の元であって言語の記号ではないので、そのままでは$\varphi$に代入できない。そこで、台集合の元それぞれに名前を与えて、言語のほうを拡大してしまう。
$\mathfrak{M}$を$L$-構造とする。$|\mathfrak{M}|$の各元$a$に対して新しい定数記号$c_a$を用意し、
$$
L(\mathfrak{M}) = L \cup \lbrace c_a : a \in |\mathfrak{M}| \rbrace $$
とおく。$c_a$を$a$の名前と呼ぶ。相異なる元には相異なる名前を与える。$\mathfrak{M}$は$L(\mathfrak{M})$-構造とみなす。すなわち台集合と$L$の記号の解釈はそのままで、$c_a$の解釈を$a$とする。
$L(\mathfrak{M})$の閉項$t$の値$t^{\mathfrak{M}} \in |\mathfrak{M}|$を、$t$の構成に関する帰納法で定める。定数記号$d$については$d^{\mathfrak{M}}$（とくに$c_a^{\mathfrak{M}} = a$）、$t \equiv f(t_1,\dots,t_n)$については$f^{\mathfrak{M}}(t_1^{\mathfrak{M}},\dots,t_n^{\mathfrak{M}})$。
$L(\mathfrak{M})$の文$\varphi$に対し、$\mathfrak{M} \models \varphi$を$\varphi$の論理記号$\neg, \to, \forall$の個数に関する帰納法で定める。
・$\mathfrak{M} \models R(t_1,\dots,t_n) \iff (t_1^{\mathfrak{M}},\dots,t_n^{\mathfrak{M}}) \in R^{\mathfrak{M}}$
・$\mathfrak{M} \models t_1 = t_2 \iff t_1^{\mathfrak{M}} = t_2^{\mathfrak{M}}$
・$\mathfrak{M} \models \neg\varphi \iff \mathfrak{M} \not\models \varphi$
・$\mathfrak{M} \models \varphi \to \psi \iff \mathfrak{M} \not\models \varphi$ または $\mathfrak{M} \models \psi$
・$\mathfrak{M} \models \forall x \varphi(x) \iff$ すべての$a \in |\mathfrak{M}|$について$\mathfrak{M} \models \varphi(c_a)$
自由変数を持つ論理式$\varphi$については、自由変数すべてに名前を代入して得られる文を$\varphi$の名前代入例と呼び、名前代入例がすべて真であるとき$\mathfrak{M} \models \varphi$と書く。
$T$のすべての要素について$\mathfrak{M} \models \varphi$となるとき$\mathfrak{M} \models T$と書き、$\mathfrak{M}$を$T$のモデルという。$T$のすべてのモデルが$\varphi$のモデルであるとき$T \models \varphi$と書く。
$\forall$の条項で、$\varphi(c_a)$は$\forall x \varphi(x)$の部分論理式ではない。だから部分論理式に関する帰納法では定義が回らない。回っているのは複雑さを論理記号の個数で測っているからで、定数の代入は論理記号の個数を変えないので
$$
\# (\varphi(c_a)) = \# (\varphi(x)) = \# (\forall x \varphi(x)) - 1 < \# (\forall x \varphi(x))$$
となる。記号列の長さで測ると（$c_a$のほうが$x$より長いかもしれないので）この議論は崩れる。この測度は真理補題でもそのまま効いてくる。意味論の定義と真理補題の証明が同じ形の帰納法になるというのが、名前による定義の利点である。
自由変数を持つ論理式の真偽を「名前代入例がすべて真」と定めたことは、自由変数を暗黙に全称量化として読むという約束にほかならない。実際、定義から直ちに
$$
\mathfrak{M} \models \varphi(x) \iff \mathfrak{M} \models \forall x \varphi(x)
$$
が成り立つ。この約束は$\mathrm{Gen}$のところで効いてくる。
名前の使い方について補題を一つ用意しておく。「同じ元を指す閉項どうしは交換してよい」という当たり前の主張である。
$s, t$を$L(\mathfrak{M})$の閉項で$s^{\mathfrak{M}} = t^{\mathfrak{M}}$を満たすものとし、$\varphi(x)$を$x$のみを自由変数に持つ$L(\mathfrak{M})$の論理式とする。このとき
$$
\mathfrak{M} \models \varphi(s) \iff \mathfrak{M} \models \varphi(t)$$
とくに$a = t^{\mathfrak{M}}$とすれば$\mathfrak{M} \models \varphi(t) \iff \mathfrak{M} \models \varphi(c_a)$。
まず、$x$以外の変数を含まない項$u(x)$について$u(s)^{\mathfrak{M}} = u(t)^{\mathfrak{M}}$が、項の構成に関する帰納法で従う（$u$が$x$のときが仮定そのもの）。
次に$\varphi$の論理記号の個数に関する帰納法。原子文のときは上の結果と充足の定義から、$\neg$と$\to$のときは帰納法の仮定から直ちに従う。$\varphi(x) \equiv \forall y \psi(y,x)$のときは、各$a$について$\psi(c_a,x)$（$x$のみを自由変数に持ち、論理記号が一つ少ない）に帰納法の仮定を使えばよい。なお$s,t$は閉項なので、代入で変数が束縛される心配はない。$\square$
証明体系と一般化規則
前編の$\mathbf{P1}$〜$\mathbf{P3}$に次を追加する。
$\mathbf{P4}$ $\forall x \varphi(x) \to \varphi(t)$ （$t$は$x$に代入可能）
$\mathbf{P5}$ $\forall x(\varphi \to \psi) \to (\varphi \to \forall x \psi)$ （$x$は$\varphi$に自由に現れない）
$\mathbf{E1}$ $x = x$
$\mathbf{E2}$ $x = y \to (\varphi(x) \to \varphi(y))$
推論規則は$\mathrm{MP}$と、$\varphi$から$\forall x \varphi$を導く$\mathrm{Gen}$の二つ。証明の定義は前編に
$4.$ ある$i < k$と変数$x$が存在して、$\varphi_k$は$\forall x \varphi_i$という形をしている$(\mathrm{Gen})$
という条項を足したものとする。
前編と同様、単調性は定義から直ちに従う。矛盾・無矛盾の定義も前編と同じである。
$\mathrm{Gen}$は初めて見るとおかしな規則である。「$x$について$\varphi$が成り立つ」から「すべての$x$について$\varphi$が成り立つ」を導くというのだから、実際$P(x)$から$\forall x P(x)$が一行で出てしまう。
しかしこれは$\varphi(x)$の読み方を誤解している。自由変数を持つ論理式は、この体系では最初から全称的に読まれている。意味論の側で$\mathfrak{M} \models \varphi(x) \iff \mathfrak{M} \models \forall x \varphi(x)$だったことを思い出そう。$\varphi(x)$と$\forall x \varphi(x)$は最初から同じことを主張しており、$\mathrm{Gen}$はそれを構文の側でも認めるというだけの規則である。「新しい情報を生む規則」ではなく「同じ主張を書き換える規則」だと思えばよい。
そもそもこの規則が要るのは、$\forall$を含む定理を証明する手段がほかにないからである。$\mathbf{P4}$は$\forall$を外す公理、$\mathbf{P5}$は$\forall$を動かす公理であって、$\forall$を新たに付けることはできない。$\vdash \forall x(x=x)$を$\mathbf{E1}$から出すには$\mathrm{Gen}$を使うしかない。数学の実践に照らしても、「$x$を任意にとる。…よって$P(x)$」の最後の一歩がこれである。
とはいえ、ただでは済まない。次の二つが成り立つ。
$$
\lbrace \varphi(x) \rbrace \vdash \forall x \varphi(x) \qquad \text{しかし} \qquad \nvdash \varphi(x) \to \forall x \varphi(x)$$
左は$\mathrm{Gen}$そのもの。右が成り立たないことは健全性から分かる（$|\mathfrak{M}| = \lbrace 0,1 \rbrace $、$P^{\mathfrak{M}} = \lbrace 0 \rbrace $とすれば名前代入例$P(c_0) \to \forall x P(x)$は偽）。つまり「仮定に置く」ことと「含意の前件に置く」ことが一致しない。左では$\varphi(x)$が単独の主張として全称的に読まれるのに対し、右では一つの論理式の中で$x$が共有されるからである。
この食い違いが演繹定理に制限として現れる。なお規則としての$\mathrm{Gen}$自体には制限がない。制限が出るのは演繹定理のほうだけであり、しかも本稿で扱う$T$も$\varphi$もすべて文なので、実際には自動的に満たされる。
健全性
前編と同じく、健全性は完全性定理の$(\Rightarrow)$の向きと、コンパクト性定理を導くときの「モデルを持つ理論は無矛盾である」という一歩にだけ使う。証明は要点のみを述べる。
$T \vdash \varphi$ならば$T \models \varphi$。とくに、モデルを持つ理論は無矛盾である。
まず公理の実例がすべての構造で真であること。自由変数には名前を代入して考える。$\mathbf{P1}$〜$\mathbf{P3}$は前編と同じ計算。$\mathbf{P4}$は、$\mathfrak{M} \models \forall x \varphi(x)$のとき$a = t^{\mathfrak{M}}$として$\mathfrak{M} \models \varphi(c_a)$、名前の交換より$\mathfrak{M} \models \varphi(t)$。$\mathbf{P5}$は、$x$が$\varphi$に自由に現れないので$x$に$c_a$を代入しても$\varphi$の側が変わらないことから。$\mathbf{E1}$は明らか。$\mathbf{E2}$は、前件が真なら$a = b$、すなわち$c_a \equiv c_b$なので後件が$\varphi(c_a) \to \varphi(c_a)$の形になることから（相異なる元に相異なる名前を与えるという約束がここで効く）。
次に推論規則。$\mathrm{MP}$は$\to$の充足条件から。$\mathrm{Gen}$は、$\forall x \varphi$の名前代入例が真であることが「すべての$a$について$\varphi$の名前代入例が真」と同値であることから従う。自由変数を全称的に読むと約束したことが、そのまま$\mathrm{Gen}$の健全性になっている。
あとは前編と同様、証明列の添字に関する累積帰納法。後半も前編と同様、$\chi$と$\neg\chi$が同時に真になりえないことによる。$\square$
道具箱：演繹定理と量化子
前編の演繹定理は、そのままの形では成り立たない。$\mathrm{Gen}$の代償がここに制限として現れる。
$T \cup \lbrace \varphi \rbrace \vdash \psi$であって、その証明の中で$\varphi$に自由に現れる変数に対する$\mathrm{Gen}$が使われていないならば、$T \vdash \varphi \to \psi$。とくに$\varphi$が文ならば無条件に成り立つ。
$T \cup \lbrace \varphi \rbrace $からの証明$\psi_0, \dots, \psi_n = \psi$を固定し、添字$k$に関する累積帰納法で$T \vdash \varphi \to \psi_k$を示す。条項$1$〜$3$の場合は前編の演繹定理の証明と一字一句同じである（$\mathbf{P1}$と$\mathbf{P2}$しか使っていないので、公理が増えても影響しない）。新しいのは次の場合だけである。
$(\text{iv})$ ある$i < k$と変数$x$について$\psi_k \equiv \forall x \psi_i$のとき：
帰納法の仮定より$T \vdash \varphi \to \psi_i$。この論理式に$\mathrm{Gen}$を適用して
$$
T \vdash \forall x(\varphi \to \psi_i)$$
いま仮定より、もとの証明でのこの$\mathrm{Gen}$は$\varphi$に自由に現れる変数に対するものではない。つまり$x$は$\varphi$に自由に現れない。よって$\mathbf{P5}$の実例
$$
\forall x(\varphi \to \psi_i) \to (\varphi \to \forall x \psi_i)$$
が使えて、$\mathrm{MP}$より$T \vdash \varphi \to \forall x \psi_i$、すなわち$T \vdash \varphi \to \psi_k$。$\square$
前編で「$\mathbf{P1}$と$\mathbf{P2}$は演繹定理を成立させるために置かれた公理である」と述べた。$\mathbf{P5}$もまったく同じ役割で、$\mathrm{Gen}$を足したせいで生じた新しい場合を処理するためだけに要る。そして$\mathbf{P5}$の側条件がそのまま演繹定理の制限になっている。前節で見た食い違いは、証明のこの一点に集約されているのである。
以下の導出は機械的な演習なので省略する。前編の道具箱と同様、これらはすべて演繹定理を使ってよいので循環はしない。
次はすべて導出可能である。
$(1)$ $\vdash \varphi(t) \to \exists x \varphi(x)$
$(2)$ $\vdash \forall x(\theta(x) \to \psi) \to (\exists x \theta(x) \to \psi)$ （$x$は$\psi$に自由に現れない）
$(3)$ $\vdash \exists x(\theta \to \varphi(x)) \leftrightarrow (\theta \to \exists x \varphi(x))$ （$x$は$\theta$に自由に現れない）
$(4)$ $\vdash \exists x \varphi(x) \leftrightarrow \exists y \varphi(y)$ （束縛変数の付け替え。$y$は$\varphi$に現れない）
$(5)$ $\vdash t = t$ , $\vdash t_1 = t_2 \to t_2 = t_1$ , $\vdash (t_1 = t_2 \land t_2 = t_3) \to t_1 = t_3$
$(6)$ $\vdash \bigwedge_i (s_i = t_i) \to f(s_1,\dots,s_n) = f(t_1,\dots,t_n)$
$(7)$ $\vdash \bigwedge_i (s_i = t_i) \to (R(s_1,\dots,s_n) \to R(t_1,\dots,t_n))$
$(8)$ 前編の道具箱の各項目
一つだけ、証明列の形が本質的に使われるものがあるので、これは書いておく。
$c$を$T$にも$\theta$にも現れない定数記号、$y$を$\theta$にも証明列にも現れない変数とする。このとき
$$
T \vdash \theta(c) \ \Longrightarrow \ T \vdash \forall y \theta(y)$$
$T$から$\theta(c)$への証明列に現れる$c$をすべて$y$に一斉に置き換える。$c$は$T$に現れないので条項$2$は保たれ、公理の実例は公理の実例に、$\mathrm{MP}$は$\mathrm{MP}$に、$\mathrm{Gen}$は$\mathrm{Gen}$に移る。こうして$T \vdash \theta(y)$を得るので、$\mathrm{Gen}$を適用すればよい。$\square$
「新しい定数記号$c$について何かが証明できたなら、$c$は具体的な何ものでもないのだから、それは『任意の$y$について』の主張にすぎない」。この補題はその直観の形式化であり、新しい定数を変数に置き換えるというこの一手が後で決定的に効く。
何が難しくなったのか
前編の骨格をそのまま持ち込もう。$T$が無矛盾なら、Lindenbaumの補題で極大無矛盾な$T \subseteq U$がとれる。あとは真理補題を証明したい。
しかし、ここで壁にぶつかる。そもそもモデルの台集合が存在しない。
命題論理では、モデルとは真理値割り当てという写像にすぎず、$\in U$という関係がそのまま写像を定めてくれた。述語論理では、構造を作るためにまず元の集まりが要る。何を元にすればよいのか。
ここで意味論の定義を思い出そう。我々は台集合の元それぞれに名前をつけ、$\forall$の真偽を名前を通じて定めたのだった。つまり構造とは、実質的には「名前をつけた元の集まり」である。ならば話は早い。材料は構文しかないのだから、名前のほうを先に用意して、それ自体を元とみなす。すなわち定数記号（より一般には閉項）を台集合にする。これを項モデルという。
しかし、これだけでは真理補題が回らない。$\forall$のケースを考えてみよう。示したいのは
$$
\mathfrak{M} \models \forall x \psi(x) \iff \forall x \psi(x) \in U$$
$(\Leftarrow)$は問題ない。$\forall x \psi(x) \in U$なら、$\mathbf{P4}$と演繹的閉包より任意の閉項$t$について$\psi(t) \in U$で、帰納法の仮定より$\mathfrak{M} \models \psi(t)$。台集合の元はすべて閉項が指すものなので、すべての元について$\psi$が成り立つ。
問題は$(\Rightarrow)$である。対偶をとろう。$\forall x \psi(x) \notin U$なら$\neg\forall x \psi(x) \in U$、すなわち$U$は「$\psi$を満たさないものがある」と言っている。ここから$\mathfrak{M} \not\models \forall x \psi(x)$を言うには、$\neg\psi(t) \in U$となる閉項$t$が実際に存在しなければならない。
そんな保証はどこにもない。
・そもそも$L$に定数記号が一つもなければ、閉項が存在せず台集合が空になる。
・定数記号があっても、たとえば$L = \lbrace c \rbrace $、$\exists x(x \neq c) \in U$という状況では、$U$は「$c$でない何かがある」と主張しているのに、その何かを名指しする閉項が言語にない。
つまり、$U$が「$\exists x \varphi(x)$」と主張しているとき、それを目撃（witness）する名前が言語の中にあるとは限らない。これが述語論理特有の困難であり、そして唯一の困難である。
対処法も、こうして問題が特定されれば自明である。
$$
\textbf{名前が足りないなら、足せばよい。}$$
問題は、どう足すかである。次の章では素朴な足し方を試し、それがうまくいくこと、しかし段取りが込み入ることを見る。その込み入り方を分析すると、もっと機械的な足し方が見つかる。残りの道のりを示しておく。
$$
① \text{ Henkin定数と公理を足す} \ \longrightarrow \ ② \text{ 極大化して } U \text{ を得る} \ \longrightarrow \ ③ \text{ 項モデル } \mathfrak{M}' \text{ を作る} \ \longrightarrow \ ④ \text{ 真理補題}$$
Henkin拡大
この章でやることは①、目撃者を用意することである。欲しいのは極大無矛盾であり、かつ目撃者性質
$$
\exists x \varphi(x) \in U \ \Longrightarrow \ \text{ある定数 } c \text{ について } \varphi(c) \in U$$
を持つ集合$U$である。
素朴な方針と、その行き詰まり
一つずつなら簡単である。極大無矛盾にするだけならLindenbaumの補題でよい。目撃者を用意するだけなら、$\exists x \varphi(x)$が入っているごとに新しい定数$c$を持ってきて$\varphi(c)$を足せばよく、この操作が無矛盾性を壊さないことも保証できる（後述の「一個剥がす」補題と同じ議論による）。
では順にやればよい。まず極大化し、次に目撃者を足す。ところが、これでは終わらない。
$$
\textbf{定数を足した瞬間に、極大性が壊れる。}$$
新しい定数を含む文が大量に生まれ、それらについて$U$は何も言っていないからである。ならばもう一度極大化する。すると新しい存在文が$U$に入りうる。それらの目撃者がまた要る。目撃者を足すと、また極大性が壊れる。二つの性質が互いを壊し合っている。結局、極大化と目撃者追加を交互に$\omega$回繰り返し、極限で両方の性質が成り立つことを確認することになる。これは完成させられる方針であり、実際そうしている教科書も多いが、もう少し楽な道がないか考えてみたい。
原因は一点に絞れる。
$$
\textbf{目撃者を足す作業が、その時点の理論に依存している。}$$
どの$\varphi$に目撃者を用意すべきかは、$\exists x \varphi(x)$が$U$に入るかどうかで決まる。それを知るには極大化しなければならない。しかし極大化の後に定数を足すと極大性が壊れる。この循環が交互反復の正体である。逆に言えば、目撃者の準備を理論と無関係に済ませられれば循環は切れる。準備を全部先にやってしまい、極大化は最後に一度だけ行えばよい。極大化は言語を増やさないので、一度用意した目撃者性質は壊れない。
含意の形で足す
そのための工夫は一つだけである。追加するものを$\varphi(c)$そのものではなく
$$
\exists x \varphi(x) \to \varphi(c)$$
という含意の形にする。こうすると、$\exists x \varphi(x)$が$U$に入らなかった場合は前件が偽なので自動的に真になり、何も主張しない。つまり無害である。したがって「$\exists x \varphi(x)$が$U$に入るかどうか」を事前に知る必要がなくなり、すべての$\varphi$について無差別に足してしまってよい。手順は次の三段階になる。
$1.$ すべての$\varphi$に対して新しい定数$c_\varphi$を用意する（言語だけを見る操作）。
$2.$ すべての$\varphi$について$\exists x \varphi(x) \to \varphi(c_\varphi)$を$T$に足す（これも$\varphi$から機械的に決まる）。
$3.$ Lindenbaumの補題で一度だけ極大化する。
$1$と$2$には理論が登場しないので、$3$まで走り切ってから理論の話を始められる。$3$の後に言語は増えないので、目撃者性質はそのまま残る。交互反復は消えた。
代償は二つある。一つは定数記号を大量に用意すること（ただし濃度は増えない。すぐ下で確認する）。もう一つは無矛盾性を別途示さなければならないことで、無限個を一度に足す以上、一個ずつ確認するわけにいかない。ここにこの記事で唯一の技巧的な議論が現れる。
Henkin定数とHenkin公理
「全部足す」といっても一回では終わらない。定数を足すと言語が大きくなり、新しい定数を含む論理式が生まれ、そいつらのための定数がまた必要になる。$\omega$回繰り返して閉じさせる。ただしこの反復は言語だけを見た反復であって、交互反復とは違い理論とは無関係である。
$L_0 = L$とする。
$L_i$が定まったとき、$C_i$を、$x$のみを自由変数に持つ$L_i$の論理式$\varphi(x)$であってまだ定数が用意されていないもののそれぞれに対して用意した新しい定数記号$c_\varphi$の全体とし、$L_{i+1} = L_i \cup C_i$とおく。
$C = \bigcup_{i \in \mathbb{N}} C_i$、$L' = L \cup C$とし、$C$の要素をHenkin定数と呼ぶ。
$x$のみを自由変数に持つ$L'$の論理式$\varphi(x)$に対し、文$\exists x \varphi(x) \to \varphi(c_\varphi)$をHenkin公理と呼び、その全体を$H$とおく。$L'$の理論$T \cup H$を$T$のHenkin拡大という。
「まだ定数が用意されていないもの」に限ったのは、同じ論理式に二つ以上の定数が割り当てられるのを防ぐためである。これにより各$\varphi$に対して$c_\varphi$がただ一つ定まり、しかもそれがどの段階で作られたかが確定する。この事実は保存性の証明で効く。
$\kappa = |L| + \aleph_0$とおく。論理式は記号の有限列だから、濃度$\kappa$の言語の論理式は高々$\kappa$個しかない。よって$|L_i| \le \kappa$ならば$|C_i| \le \kappa$、したがって$|L_{i+1}| \le \kappa + \kappa = \kappa$。帰納的にすべての$i$で$|L_i| \le \kappa$であり、$C$は可算個の$C_i$の和なので
$$
|C| \le \aleph_0 \cdot \kappa = \kappa = |L| + \aleph_0$$
とくに$L$が可算なら$C$も可算である。無差別に足したように見えて、濃度は増えていない。この見積もりは後で下方Löwenheim–Skolemの定理も与える。
上では$x$のみを自由変数に持つ論理式にだけ定数を用意した。$y$のみを自由変数に持つ$\psi(y)$についてはどうするか。$y$を$x$に付け替えた論理式を$\psi'(x)$と書けば、道具箱$(4)$より$\vdash \exists y \psi(y) \leftrightarrow \exists x \psi'(x)$なので、$\psi'$のために用意した定数をそのまま使えばよい。実質的に同じ論理式それぞれに別の定数を用意しないための約束である。
保存性
$H$は無限集合だが、証明は有限列なので、一つの証明で実際に使われるHenkin公理は有限個しかない。だからそれらを一つずつ剥がしていけばよい。まず道具を作る。
$S$を理論、$\psi$を論理式、$\varphi(x)$を$x$のみを自由変数に持つ論理式、$c$を定数記号とする。$c$が$S$にも$\psi$にも$\varphi$にも現れないならば
$$
S \cup \lbrace \exists x \varphi(x) \to \varphi(c) \rbrace \vdash \psi \ \Longrightarrow \ S \vdash \psi$$
Henkin公理は文だから演繹定理が使えて
$$
S \vdash (\exists x \varphi(x) \to \varphi(c)) \to \psi
$$
$y$を、この証明にも$S$にも$\psi$にも$\varphi$にも現れない新しい変数とすると、定数の一般化の補題より
$$
S \vdash \forall y \big((\exists x \varphi(x) \to \varphi(y)) \to \psi\big)$$
$y$は$\psi$に自由に現れないから道具箱$(2)$と$\mathrm{MP}$で
$$
S \vdash \exists y(\exists x \varphi(x) \to \varphi(y)) \to \psi
$$
$y$は$\exists x \varphi(x)$に自由に現れないから道具箱$(3)$で
$$
S \vdash \big(\exists x \varphi(x) \to \exists y \varphi(y)\big) \to \psi$$
前件は束縛変数の付け替え（道具箱$(4)$）なので導出可能。$\mathrm{MP}$より$S \vdash \psi$。$\square$
この補題を使うときに確認すべきことは一点だけ、剥がす公理の定数$c$が残りのどこにも現れないことである。証明が「$c$は何も意味していない新しい記号だから、証明中の$c$を変数に置き換えても証明のままである」という一手に依っている以上、$c$が他の場所にも現れていたら巻き添えで書き換わってしまう。
ところがHenkin定数どうしは入れ子になりうるので、この条件は剥がす順番に依存する。例えば、$R$を$L$の$1$項関係記号として$\varphi_1(x) \equiv R(x)$とおくと、その定数$c_1$は段階$0$で作られる。次に$\varphi_2(x) \equiv (x = c_1)$とおくと、これは$L_1$の論理式なので、その定数$c_2$は段階$1$で作られる。この二つのHenkin公理$\theta_1, \theta_2$が使われているとしよう。$\theta_1$から剥がそうとすると、残っている$\theta_2$が$c_1$を含むので失敗する。$\theta_2$からなら、$c_2$は$T$にも$\psi$にも$\theta_1$にも$\varphi_2$にも現れないので剥がせる。
後から作られた定数から先に剥がす。これが答えであり、理由はたった一つの事実に尽きる。
$c \in C_n$ならば、$c$は$L_n$のどの論理式にも現れない。
$L_n = L \cup C_0 \cup \cdots \cup C_{n-1}$であり、$C_n$の定数はこの中に含まれていない。各段階で用意するのは、それまでになかった新しい定数記号だからである。$\square$
$\varphi$が$L_n$の論理式となる最小の$n$を$\varphi$の、そして$c_\varphi \in C_n$の世代と呼ぶ。$ \varphi_i $の世代を$n_i $と書く。世代の補題から、$n_j \le n_i$ならば$\varphi_j$は$L_{n_i}$の論理式なので$c_{\varphi_i}$を含まない。すなわち世代の遅い定数は、世代の早い論理式には現れない。
$T \cup H$は$T$の保存的拡大である。すなわち、$L$の論理式$\psi$について$T \cup H \vdash \psi$ならば$T \vdash \psi$。
使われる$H$の要素を
$$
\theta_i \equiv \exists x \varphi_i(x) \to \varphi_i(c_i) \quad\text{（$1 \le i \le k$ , $c_i$は$c_{\varphi_i}$の略記）}$$
とすれば$T \cup \lbrace \theta_1,\dots,\theta_k \rbrace \vdash \psi$。$\theta_i$たちは相異なるので$\varphi_i$も$c_i$も相異なる。世代$n_i$の小さい順に番号を振り直しておき、$k$に関する帰納法で示す。$k = 0$なら結論そのもの。
$k \ge 1$のとき、$c_k$が残りのどこにも現れないことを確かめる。$T$と$\psi$は$L = L_0$の対象なので世代の補題から。$\varphi_k$は$L_{n_k}$の論理式なので世代の補題そのもの。$j < k$なる$\theta_j$については、$\varphi_j$が$L_{n_j} \subseteq L_{n_k}$の論理式なので世代の補題から、また$c_j \not\equiv c_k$である。よって「一個剥がす」補題が$S = T \cup \lbrace \theta_1,\dots,\theta_{k-1} \rbrace $として適用でき、残りは$k-1$個になるので帰納法の仮定から$T \vdash \psi$。$\square$
$T$が無矛盾ならば$T \cup H$も無矛盾である。
$T \cup H$が矛盾するなら$L$の論理式$\psi$について$T \cup H \vdash \psi$かつ$T \cup H \vdash \neg\psi$。保存性より$T \vdash \psi$かつ$T \vdash \neg\psi$となり、$T$が矛盾する。$\square$
技巧的なのはこの一箇所だけで、しかも中身は「世代の遅いものから片づける」というそれだけのことである。以降の議論はこの結果を使うだけで、順序の話は二度と出てこない。
目撃者性質を持つ極大無矛盾集合
②の極大化である。前章の準備のおかげで、Lindenbaumの補題を一度だけ使えば終わる。
$T$を$L$の無矛盾な理論とする。このとき$L'$の理論$U$で、次の三条件を満たすものが存在する。
$(1)$ $T \subseteq U$
$(2)$ $U$は極大無矛盾である
$(3)$ $x$のみを自由変数に持つ$L'$の論理式$\varphi(x)$について、$\exists x \varphi(x) \in U$ならば$\varphi(c_\varphi) \in U$ （目撃者性質）
前章より$T \cup H$は無矛盾なので、Lindenbaumの補題（言語$L'$で適用する）より極大無矛盾な$T \cup H \subseteq U$がとれる。$(1)(2)$はこれでよい。$(3)$は、$\exists x \varphi(x) \in U$のとき対応するHenkin公理も$U$に属するので$\mathrm{MP}$より$U \vdash \varphi(c_\varphi)$、演繹的閉包より$\varphi(c_\varphi) \in U$。$\square$
この$U$が完全性定理の証明の全材料である。命題論理では「極大無矛盾」だけで足りたところに、「目撃者性質」が一つ加わっただけだということを確認してほしい。
なお以降で実際に使うのは次の形である。
$\neg\forall x \varphi(x) \in U$ならば、ある$c \in C$について$\neg\varphi(c) \in U$
$\exists x \neg\varphi(x)$とは$\neg\forall x \neg\neg\varphi(x)$のことである。前編の道具箱（二重否定）より$\vdash \neg\forall x \varphi(x) \to \exists x \neg\varphi(x)$が導けるので、演繹的閉包より$\exists x \neg\varphi(x) \in U$。目撃者性質を$\neg\varphi$に適用すればよい。$\square$
項モデルの構成
③である。台集合の候補は$L'$の閉項全体だが、実は$C$だけで足りる。
$L'$の任意の閉項$t$に対し、ある$c \in C$が存在して$(c = t) \in U$
$\varphi(x) \equiv (x = t)$とおく。道具箱$(5)$より$\vdash t = t$、道具箱$(1)$より$\vdash \exists x(x = t)$なので$\exists x \varphi(x) \in U$。目撃者性質より$(c_\varphi = t) \in U$。$\square$
なぜ商をとるのか
構造を作るとき、台集合も各記号の解釈も我々の自由である。しかし論理記号の真偽条件だけは選べない。意味論の定義で
$$
\mathfrak{M}' \models t_1 = t_2 \iff t_1^{\mathfrak{M}'} = t_2^{\mathfrak{M}'}$$
と定めた右辺は、台集合の元としての同一性である。$R(\vec c)$の真偽は$R^{\mathfrak{M}'}$の定め方で$U$に合わせられるが、等号の真偽は、どの定数がどの元を指すかを決めた瞬間に自動的に決まってしまう。
真理補題の等号のケースは$(c_1 = c_2) \in U \iff c_1^{\mathfrak{M}'} = c_2^{\mathfrak{M}'}$だから、これは解釈の選び方への強い制約になる。$$
\textbf{$U$が等しいと言う名前には同じ元を、そうでない名前には異なる元を割り当てよ}$$
つまり、割り当て$c \mapsto c^{\mathfrak{M}'}$は好き勝手には決められない。$U$がすでに答えを指定しているのである。
いちばん素朴なのは、記号をそのまま元として使う選び方である。すなわち
$$
|\mathfrak{M}'| = C, \qquad c^{\mathfrak{M}'} = c$$
（各定数記号が自分自身を指す）とすると、集合$C$の元は定数記号そのものであり、相異なる記号は$C$の相異なる元であるので$c_1^{\mathfrak{M}'} = c_2^{\mathfrak{M}'}$は$c_1 \equiv c_2$と同値になってしまう。そしてこれは実際に破れる。$e \in C$に対し$\varphi(x) \equiv (x = e)$とおくと、閉項の補題の証明と同じく$(c_\varphi = e) \in U$である。一方$e$は$\varphi$に現れるので$e \in L_{n_\varphi}$、$c_\varphi \in C_{n_\varphi}$は世代の補題より$L_{n_\varphi}$に属さないので$c_\varphi \not\equiv e$。これは事故ではない。$\exists x(x = e)$の目撃者として新しい記号を用意した以上、それは$e$と同じものを指すに決まっている。同じものに二つ目の名前を与えたのだから避けようがない。
要するに$C$は名前の集合であって登場人物の集合ではない。$U$を読むと、同じ人物に複数の名前がついていることが分かる。ならばやることは決まっている。同じ人物を指す名前どうしを、まとめて一つの元と数える。同じ人物かどうかを教えてくれるのは$U$だけなので、$U$が$(c_1 = c_2)$を含むかどうかで判断する。群を正規部分群で割るのと同じ発想である。
これで、$c$の同値類を$[c]$、$c^{\mathfrak{M}'} = [c]$とすれば
$$
\mathfrak{M}' \models (c_1 = c_2) \iff [c_1] = [c_2] \iff (c_1 = c_2) \in U$$
となり、上の制約が過不足なく実現される。商をとるとは、真理補題の等号のケースを成り立たせるための最小限の細工である。あとは$(1)$同値関係になること、$(2)$解釈が代表元によらないことを確かめればよく、それを保証するのが等号公理$\mathbf{E1}, \mathbf{E2}$（道具箱$(5)$〜$(7)$）である。等号公理を置いた理由がここで回収される。
構成
$C$上の二項関係$\sim$を$c_1 \sim c_2 \iff (c_1 = c_2) \in U$と定める。道具箱$(5)$と演繹的閉包より、これは同値関係である。$c$の同値類を$[c]$と書き、$L'$-構造$\mathfrak{M}'$を次で定める。
・台集合：$|\mathfrak{M}'| = C/{\sim}$（$C \neq \emptyset$だから空でない）
・定数記号$d$の解釈：$(c = d) \in U$なる$c \in C$をとり$d^{\mathfrak{M}'} = [c]$
・関数記号$f$の解釈：$f^{\mathfrak{M}'}([c_1],\dots,[c_n]) = [c]$、ただし$c$は$(c = f(c_1,\dots,c_n)) \in U$なるもの
・関係記号$R$の解釈：$R^{\mathfrak{M}'} = \lbrace ([c_1],\dots,[c_n]) : R(c_1,\dots,c_n) \in U \rbrace $
このままでは構造が定まったとは言えない。定数記号と関数記号については「〜なる$c$をとり」という言い方が、そんな$c$が存在しなければ意味をなさず、複数あれば値が定まらない。また関数記号と関係記号については、左辺が同値類なのに右辺で代表元を使っている。この二つを潰す。
$t$を$L'$の閉項とする。$(c = t) \in U$なる$c \in C$が存在し、そのような$c$の同値類$[c]$は一つに定まる。
存在は閉項の補題。一意性は、$(c = t) \in U$かつ$(c' = t) \in U$なら道具箱$(5)$の対称律と推移律から$(c = c') \in U$、すなわち$[c] = [c']$。$\square$
項モデルの定義は、選んだ$c$にも代表元の取り方にもよらない。
定数記号については、$t \equiv d$として上の補題を使えばよい（代表元の問題はない）。
関数記号については、代表元を固定したときの値が一意であることが$t \equiv f(\vec c)$として上の補題から従う。代表元の取り方については、$c_i \sim d_i$のとき道具箱$(6)$と演繹的閉包より$(f(\vec c) = f(\vec d)) \in U$なので、$(c = f(\vec c)) \in U$と推移律から$(c = f(\vec d)) \in U$。すると$c$も、$f(\vec d)$に対して選んだ$c'$も「$f(\vec d)$と等しい$C$の元」なので、上の補題の一意性より$[c] = [c']$。
関係記号については、$c_i \sim d_i$のとき道具箱$(7)$と$\mathrm{MP}$、演繹的閉包より$R(\vec c) \in U$から$R(\vec d) \in U$が従う。$\sim$は対称なので逆も同様。$\square$
Henkin定数は名前として働く
台集合の元$[c]$を指す$L'$の定数記号はあるだろうか。$c$自身がそうなっている。
任意の$c \in C$について$c^{\mathfrak{M}'} = [c]$。したがって、$x$のみを自由変数に持つ$L'$の論理式$\psi(x)$について$\mathfrak{M}' \models \psi(c) \iff \mathfrak{M}' \models \psi(c_{[c]})$。
定数記号$d$の解釈は$(c' = d) \in U$なる$c'$をとって$[c']$と定めたのだった。$d$として$c$自身をとると、$(c = c) \in U$なので$c' \equiv c$と選ぶことが許され、well-defined性より選び方によらないから$c^{\mathfrak{M}'} = [c]$。
後半は、名前の定義より$c_{[c]}^{\mathfrak{M}'} = [c]$でもあるので、名前の交換の補題を$s \equiv c$、$t \equiv c_{[c]}$として適用すればよい。$\square$
意味論を定義したとき、我々は構造の各元$a$に名前$c_a$を外から補った。$c_a$は$L'$の記号ではなく、充足を定義するためだけの補助的な記号であり、一般の構造では元に言語内の名前がついている保証などない。項モデルはその点が特別で、$C$の元$c$自身がすでに$[c]$を指す$L'$の定数記号になっている。上の補題は、二重についた名前がいつでも交換できると言っている。おかげで$\forall$の充足条件を
$$
\big(\text{すべての } a \in |\mathfrak{M}'| \text{ について } \mathfrak{M}' \models \psi(c_a)\big) \iff \big(\text{すべての } c \in C \text{ について } \mathfrak{M}' \models \psi(c)\big)$$
と書き直せる。右辺は$L'$の記号だけで書かれている。「台集合のすべての元が言語内の定数記号で名指しされている」とは、正確にはこのことである。
最後に、閉項一般についても同じことが成り立つ。真理補題の原子文のケースで使う。
$L'$の任意の閉項$t$と$c \in C$について$t^{\mathfrak{M}'} = [c] \iff (c = t) \in U$
$(\Leftarrow)$を$t$の構成に関する帰納法で示す。$t$が定数記号のときは定義とwell-defined性から。$t \equiv f(t_1,\dots,t_n)$のときは、閉項の補題で$(c_i = t_i) \in U$なる$c_i$をとると帰納法の仮定より$t_i^{\mathfrak{M}'} = [c_i]$なので$t^{\mathfrak{M}'} = [c']$（ただし$(c' = f(\vec c)) \in U$）。道具箱$(6)$と推移律から$(c' = t) \in U$であり、仮定$(c = t) \in U$と併せて$[c'] = [c]$。よって$t^{\mathfrak{M}'} = [c']$。
$(\Rightarrow)$はここから従う。$t^{\mathfrak{M}'} = [c]$のとき、閉項の補題で$(c'' = t) \in U$なる$c''$をとれば$(\Leftarrow)$より$t^{\mathfrak{M}'} = [c'']$、よって$(c = c'') \in U$、推移律で$(c = t) \in U$。$\square$
真理補題
④、山場である。とはいえ骨格は前編と同じで、$\forall$のケースが増えるだけである。
$L'$の任意の文$\varphi$について
$$
\mathfrak{M}' \models \varphi \iff \varphi \in U$$
$(\text{i})$ 原子文のとき：$\varphi \equiv R(t_1,\dots,t_n)$とする。閉項の補題で$(c_i = t_i) \in U$なる$c_i$をとると、項の解釈の補題より$t_i^{\mathfrak{M}'} = [c_i]$。よって
$$
\mathfrak{M}' \models R(\vec t) \iff ([c_1],\dots,[c_n]) \in R^{\mathfrak{M}'} \iff R(\vec c) \in U \iff R(\vec t) \in U$$
最初は充足の定義、次は$R^{\mathfrak{M}'}$の定義、最後は道具箱$(7)$と演繹的閉包による。$\varphi \equiv (t_1 = t_2)$のときも同様に
$$
\mathfrak{M}' \models t_1 = t_2 \iff [c_1] = [c_2] \iff (c_1 = c_2) \in U \iff (t_1 = t_2) \in U$$
$(\text{ii})$ $\varphi \equiv \neg\psi$のとき：
$$
\mathfrak{M}' \models \neg\psi \iff \mathfrak{M}' \not\models \psi \iff \psi \notin U \iff \neg\psi \in U$$
前編とまったく同じで、二つ目は帰納法の仮定、三つ目は$U$の極大無矛盾性による。
$(\text{iii})$ $\varphi \equiv \psi \to \chi$のとき：前編の真理補題の$(\text{iii})$と一字一句同じである。$U$の極大無矛盾性、$\mathrm{MP}$、$\mathbf{P1}$、前編の道具箱しか使っていない。
$(\text{iv})$ $\varphi \equiv \forall x \psi(x)$のとき：ここが述語論理固有の部分である。充足の定義と、名前としてのHenkin定数の補題による書き直しから、示すべきは
$$
\big(\text{すべての } c \in C \text{ について } \mathfrak{M}' \models \psi(c)\big) \iff \forall x \psi(x) \in U$$
$(\Leftarrow)$：$\forall x \psi(x) \in U$なら、任意の$c \in C$について$\mathbf{P4}$と演繹的閉包より$\psi(c) \in U$。$\psi(c)$は$\forall x \psi(x)$より論理記号が一つ少ない文だから、帰納法の仮定より$\mathfrak{M}' \models \psi(c)$。
$(\Rightarrow)$：対偶を示す。$\forall x \psi(x) \notin U$なら極大性より$\neg\forall x \psi(x) \in U$なので、目撃者性質（の言い換え）よりある$c$について$\neg\psi(c) \in U$。すると$\psi(c) \notin U$だから、帰納法の仮定より$\mathfrak{M}' \not\models \psi(c)$。$\square$
$(\text{iv})$で使ったのは、台集合のすべての元がHenkin定数で名指しされていること（これで「すべての元について」を「すべての$c \in C$について」に書き換えた）と、$U$の存在主張には必ず言語内の目撃者がいること（これで$(\Rightarrow)$が通った）の二つである。Henkin定数はこの二つを同時に実現するために導入されたのである。
また、帰納法の測度が論理記号の個数であることは充足の定義のところで述べたとおりで、ここでも同じ理由で必要になっている。意味論の定義の帰納法と真理補題の帰納法が同じ形をしているのは偶然ではない。真理補題とは要するに、構文の側の「$\in U$」という関係が、意味論の定義とまったく同じ再帰を満たすことの確認だからである。
完全性定理の証明
真理補題より$\mathfrak{M}' \models U$であり、$T \subseteq U$なので$\mathfrak{M}' \models T$。最後に、$\mathfrak{M}'$は$L'$-構造なので余計な記号を落とす。
$\mathfrak{M}$を、$\mathfrak{M}'$の$L$への制限とする。すなわち$|\mathfrak{M}| = |\mathfrak{M}'|$、$L$の記号の解釈は$\mathfrak{M}'$と同じ、$C$の定数記号の解釈は忘れる。
忘れても$L$の文の真偽が変わらないことは当たり前に見えるが、名前による意味論では構造ごとに言語が変わるので、一度確認しておく。台集合が同じだから名前の集合は共通であり、$L(\mathfrak{M}) \subseteq L'(\mathfrak{M}')$。この範囲の文については$\mathfrak{M}$と$\mathfrak{M}'$の両方で真偽が定義されていて、比べることに意味がある。
$L(\mathfrak{M})$の任意の文$\varphi$について$\mathfrak{M} \models \varphi \iff \mathfrak{M}' \models \varphi$
まず$L(\mathfrak{M})$の閉項$t$について$t^{\mathfrak{M}} = t^{\mathfrak{M}'}$が項の構成に関する帰納法で従う（$C$の記号は現れないので、忘れた解釈が使われる場面がない）。
次に論理記号の個数に関する帰納法。原子文のときは上の結果と$R^{\mathfrak{M}} = R^{\mathfrak{M}'}$から、$\neg$と$\to$のときは帰納法の仮定から従う。$\varphi \equiv \forall x \psi(x)$のときは、台集合が同じなので$a$の動く範囲が両者で一致し、$\psi(c_a)$に帰納法の仮定が使える。$\square$
この補題を「$L$の文について」と述べると証明が回らない。$\forall$のケースで帰納法の仮定を使う相手$\psi(c_a)$は名前を含むので、$L$の文ではないからである。名前を含む文まで込めて述べる必要がある。
$L$の文は$L(\mathfrak{M})$の文でもあるから、とくに$\mathfrak{M} \models T$。以上で目標に到達した。
$L$の理論$T$について、$T$が無矛盾であることと$T$がモデルを持つことは同値である。
$(\Rightarrow)$：Henkin拡大$T \cup H$を極大無矛盾な$U$に拡大し、項モデル$\mathfrak{M}'$を作り、真理補題から$\mathfrak{M}' \models T$、$L$に制限して$\mathfrak{M} \models T$。$(\Leftarrow)$：健全性定理の後半そのもの。$\square$
$L$の理論$T$と$L$の文$\varphi$について$T \vdash \varphi \iff T \models \varphi$
$(\Rightarrow)$は健全性そのもの。$(\Leftarrow)$は対偶を示す。$T \nvdash \varphi$なら背理法の補題の対偶より$T \cup \lbrace \neg\varphi \rbrace $は無矛盾。モデル存在定理よりそのモデル$\mathfrak{M}$が存在し、$\mathfrak{M} \models T$かつ$\mathfrak{M} \not\models \varphi$だから$T \not\models \varphi$。$\square$
自由変数を持つ論理式については全称閉包を考えればよい。$\mathrm{Gen}$と$\mathbf{P4}$により$T \vdash \varphi \iff T \vdash \forall \vec x \varphi$であり、意味論の側でも$\mathfrak{M} \models \varphi \iff \mathfrak{M} \models \forall \vec x \varphi$が名前代入例の定義から従うからである。ここでも$\mathrm{Gen}$と自由変数の全称的な読みが対応している。
副産物
完全性定理そのものより、その系のほうが実際にはよく使われる。
$L$における無矛盾な理論は、濃度が高々$|L| + \aleph_0$のモデルを持つ。とくに$L$が可算なら高々可算なモデルを持つ。
構成したモデルは$|\mathfrak{M}| = C/{\sim}$だから$|\mathfrak{M}| \le |C| \le |L| + \aleph_0$。$\square$
証明を追ったからこそ意味が分かるタイプの系である。モデルを外から与えられていたら濃度の制御などできないが、我々は自分で作ったのだから材料の個数が分かっている。
集合論の言語$L_S = \lbrace \in \rbrace $は有限なので、$\mathrm{ZFC}$が無矛盾ならば$\mathrm{ZFC}$は可算なモデルを持つ。しかし$\mathrm{ZFC}$は「非可算集合が存在する」を証明する。可算なモデルの中に非可算集合が住んでいることになる。
矛盾ではない。「$A$は非可算である」とは「$A$から$\omega$への全単射が存在しない」という主張であり、その「存在しない」はモデルの内部で解釈される。モデルの外から見れば全単射は存在するが、それがモデルの元として入っていないだけである。濃度という概念のモデル相対性を示す例であり、パラドックスと呼ばれるが実際には完全性定理の証明の直接の帰結にすぎない。
$T$がモデルを持つための必要十分条件は、$T$の任意の有限部分集合がモデルを持つことである。
必要性は明らか。十分性：健全性定理の後半より$T$の各有限部分集合は無矛盾なので、有限性補題の対偶より$T$は無矛盾。モデル存在定理よりモデルを持つ。$\square$
前編と同じく、「証明は有限列である」という性質だけが効いている。応用を一つ挙げておく。
「$\mathfrak{M} \models T \iff |\mathfrak{M}|$が有限」となるような$L$の理論$T$は存在しない。
そのような$T$があるとする。新しい定数記号$c_0, c_1, \dots$を用意し$S = \lbrace c_i \neq c_j : i \neq j \rbrace $とおくと、$T \cup S$の任意の有限部分集合には有限個の$c_i$しか現れないので、$T$の十分大きな有限モデルの相異なる元を割り当てればモデルになる。コンパクト性より$T \cup S$はモデル$\mathfrak{M}$を持ち、$c_i^{\mathfrak{M}}$は互いに相異なるから$\mathfrak{M}$は無限。$L$に制限すれば$T$の無限モデルが得られ、矛盾。$\square$
各$n$について「濃度が$n$以上である」を表す文$\mu_n \equiv \exists x_1 \cdots \exists x_n \bigwedge_{i< j} x_i \neq x_j$は書けるので、$\lbrace \neg\mu_n : n \in \mathbb{N} \rbrace $のどれか一つが成り立つと言えれば有限性を表現できる。しかし理論とは公理の集合であり、その要素は「かつ」で結ばれる。無限個の「または」は書けない。一階述語論理の表現力の限界がどこにあるかを、この例はきれいに示している。
まとめ
前編と後編を並べて眺めておく。
| 出発点 | 準備 | 極大化（Lindenbaumの補題） | モデルの材料 | 核心 | 結論 | |
|---|---|---|---|---|---|---|
| 前編： | 無矛盾な$T$ | 不要 | 極大無矛盾な$U$ | $\in U$という関係そのもの | 真理補題 | $T$のモデル |
| 後編： | 無矛盾な$T$ | Henkin拡大$T \cup H$ | 極大無矛盾かつ目撃者性質を持つ$U$ | $C/{\sim}$（Henkin定数の同値類） | 真理補題 | $T$のモデル |
それぞれの部品が何のためにあったのかを再確認する。
・有限性（証明は有限列）：Lindenbaumの補題で鎖の和の無矛盾性を保証し、Henkin拡大の保存性を有限個の議論に帰着させ、コンパクト性定理を生む。
・極大無矛盾性：真理補題の$\neg$と$\to$のケースを回すため。
・Henkin定数と目撃者性質：真理補題の$\forall$のケースを回すため。意味論の側で台集合の元に名前を与えたのと同じことを、構文の側で先回りして用意したものである。
・Henkin公理という含意の形：目撃者を「選ばずに」用意するため。これによって構成が二段階に収まり、前編の補題をそのまま流用できた。
・等号公理と商：構文から作った構造で、等号を真の等号として解釈するため。
・$\mathrm{Gen}$と$\mathbf{P5}$：自由変数を全称的に読むという約束を構文の側でも認めるため。その代償が演繹定理の制限である。
・真理補題：構文的な関係$\in U$が、意味論の定義とまったく同じ再帰を満たすことの確認。ここに全部が集約される。
こう並べてしまえば、完全性定理の証明に天下りな部分は一つもない。材料は構文しかないのだから、構文からモデルを作る。作ったモデルが期待どおり動くために足りないものを、順番に補う。それだけである。
（完）
