Henkin構成

要点：置き換えは記号を 1 つずつ取り替えるだけなので、論理公理は論理公理に、前件肯定は前件肯定に移る。$\Gamma$ の元は $c$ を含まないので変わらない。

要点：矛盾を示す導出に現れる新しい定数は有限個なので、lem-henkin-constant-replacement でそれらを 1 つずつ新しい変数に替えると、$L$ での矛盾が得られる。

要点：$c$ を導出に現れない変数 $y$ に替えると $\Gamma_0\vdash\varphi[y/x]$（$\Gamma_0$ は使った前提）となり、汎化定理で $\forall y\,\varphi[y/x]$ を得てから、(A4) と汎化定理で束縛変数を $x$ に戻す。

$W:=W(\varphi,x,c)$ とおき、$T\cup\{W\}$ が矛盾すると仮定する。論理式の集合 $\Delta$ が $\Delta\vdash W$ を満たすなら、$T\cup\{W\}$ から導出できる論理式は $T\cup\Delta$ からも導出できる（推移性）ので、$T\cup\Delta$ も矛盾する。この $\Delta$ を 2 通りにとる。

1. (A1) の実例 $\lnot\varphi[c/x]\to(\lnot\forall x\,\varphi\to\lnot\varphi[c/x])$ と MP から $\{\lnot\varphi[c/x]\}\vdash W$ である。よって $T\cup\{\lnot\varphi[c/x]\}$ は矛盾し、$T\vdash\varphi[c/x]$ である。$c$ は $T$ にも $\varphi$ にも現れないので、$L\setminus\{c\}$ を cor-henkin-generalization-on-constants の $L$ として、$T\vdash\forall x\,\varphi$ である。
2. 爆発律により $\{\forall x\,\varphi,\lnot\forall x\,\varphi\}\vdash\lnot\varphi[c/x]$ であり、演繹定理（一階論理の証明体系 の定理「一階論理の演繹定理」）により $\{\forall x\,\varphi\}\vdash W$ である。よって $T\cup\{\forall x\,\varphi\}$ は矛盾し、$T\vdash\lnot\forall x\,\varphi$ である。
   1 と 2 から $T$ は矛盾し、仮定に反する。$\square$

$L_0:=L$ とする。$L_n$ が定まったとき、自由変数が $x$ 以外にない $L_n$ の論理式 $\varphi$ と変数 $x$ の組 $(\varphi,x)$ ごとに、相異なる新しい定数記号 $c_{\varphi,x}$ を用意し、それらを $L_n$ に加えた言語を $L_{n+1}$ とする。$L_H:=\bigcup_nL_n$ とし、
$$ T_0:=T,\qquad T_{n+1}:=T_n\cup\bigl\{W(\varphi,x,c_{\varphi,x})\bigm|(\varphi,x)\text{ は }L_n\text{ の上の組}\bigr\},\qquad T_H:=\bigcup_nT_n $$
とおく。
証人をもつ。 $L_H$ の論理式は有限個の記号しか含まないので、ある $L_n$ の論理式であり、$W(\varphi,x,c_{\varphi,x})\in T_{n+1}\subset T_H$ である。
無矛盾である。 cor-henkin-new-constants により $T_0=T$ は $L_H$ で無矛盾である。$T_n$ が $L_H$ で無矛盾として $T_{n+1}$ も無矛盾であることを示す。矛盾するなら、有限個の相異なる組 $(\varphi_1,x_1),\dots,(\varphi_k,x_k)$ で $T_n\cup\{W_1,\dots,W_k\}$（$W_i:=W(\varphi_i,x_i,c_{\varphi_i,x_i})$）が矛盾するものがある（無矛盾性 の命題「矛盾の言い換え」の 3）。$W_1,\dots,W_{k-1}$ と $T_n$ は $L_n$ の記号と $c_{\varphi_1,x_1},\dots,c_{\varphi_{k-1},x_{k-1}}$ しか含まず、$\varphi_k$ は $L_n$ の論理式なので、$c_{\varphi_k,x_k}$ はそのどれにも現れない。prop-henkin-witness-consistent の対偶により $T_n\cup\{W_1,\dots,W_{k-1}\}$ が矛盾する。これを $k$ 回繰り返すと $T_n$ が矛盾することになり、帰納法の仮定に反する。$T_H$ が矛盾すれば、矛盾を示す有限個の文はある $T_n$ に含まれるので、$T_H$ も無矛盾である。
濃度。 $L_n$ の論理式と変数の組の個数は $\kappa_L$ 以下なので、$n$ に関する帰納法で $|L_n|\le\kappa_L$ であり、$|C|\le\aleph_0\cdot\kappa_L=\kappa_L$ である（濃度）。$\square$

要点：論理公理 $\forall x_1\cdots\forall x_m\,\theta$ に (A4) を $m$ 回使うと、閉項を代入した $\theta$ の例が導出できる（閉項はどこにでも代入可能）。等号の公理の例を MP でつなぎ、(M1) で $T^*$ に戻す。

$\mathcal M:=\mathcal M_{T^*}$ とおき、$\sigma$ に現れる $\lnot,\to,\forall$ の個数に関する帰納法で示す。
原子文。 $\mathcal M\models s=t\iff s^{\mathcal M}=t^{\mathcal M}\iff[s]=[t]\iff(s=t)\in T^*$。$\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 T^*$。
$\lnot,\to$。 $\mathcal M\models\lnot\tau\iff\mathcal M\not\models\tau\iff\tau\notin T^*\iff\lnot\tau\in T^*$（帰納法の仮定と (M2)）。$\mathcal M\models\tau\to\chi\iff$「$\mathcal M\not\models\tau$ または $\mathcal M\models\chi$」$\iff$「$\tau\notin T^*$ または $\chi\in T^*$」$\iff(\tau\to\chi)\in T^*$（(M3)）。
$\forall$。 $\sigma=\forall x\,\varphi$ で、$\varphi$ の自由変数は $x$ 以外にないとする。閉項 $t$ について $\varphi[t/x]$ は文で、論理記号は $\sigma$ より 1 つ少ない。割り当て $s$ と $a=[t]$ について、一階述語論理 の補題「代入補題」の 2（$t$ は閉項なので代入可能で、$t^{\mathcal M}[s]=[t]$）により
$$ \mathcal M\models\varphi[s_x^{[t]}]\iff\mathcal M\models\varphi[t/x]\qquad(\ast) $$
である。台集合の元はどれも $[t]$ の形なので、$(\ast)$ から $\mathcal M\models\forall x\,\varphi\iff$ すべての $t\in\operatorname{Ter}$ で $\mathcal M\models\varphi[t/x]$ である。
$\sigma\in T^*$ とする。各 $t$ について (A4) の実例 $\forall x\,\varphi\to\varphi[t/x]$ と MP、(M1) から $\varphi[t/x]\in T^*$ であり、帰納法の仮定から $\mathcal M\models\varphi[t/x]$ である。よって $\mathcal M\models\sigma$。
$\sigma\notin T^*$ とする。(M2) により $\lnot\forall x\,\varphi\in T^*$ である。$T^*$ は証人をもつので、ある定数記号 $c$ で $W(\varphi,x,c)=(\lnot\forall x\,\varphi\to\lnot\varphi[c/x])\in T^*$ であり、(M3) から $\lnot\varphi[c/x]\in T^*$、(M2) から $\varphi[c/x]\notin T^*$ である。帰納法の仮定から $\mathcal M\not\models\varphi[c/x]$ であり、$\mathcal M\not\models\sigma$。$\square$

上のとおり $T\subset T_H\subset T^*$ と項モデル $\mathcal M_{T^*}$ を作る。thm-henkin-truth により $\mathcal M_{T^*}$ は $T^*$ の、とくに $T$ のすべての文を満たす。$C$ の記号の解釈を忘れた $L$ 構造 $\mathcal M_{T^*}|_L$ でも $L$ の文の真偽は変わらない（充足関係は論理式に現れる記号の解釈と台集合しか使わないので、論理式の組み立てに沿った帰納法で分かる。等号を含まない論理式についての同じ主張が Herbrandの定理 の補題「言語を広げても妥当性は変わらない」の前半であり、等号の原子論理式は台集合の上の等しさで解釈されるので同じ帰納法が通る）ので、$\mathcal M_{T^*}|_L$ は $T$ のモデルである。台集合は $\operatorname{Ter}$ の像で、$\operatorname{Ter}$ は $L_H$ の記号の有限列からなり $|L_H|\le\kappa_L$ なので、濃度は $\kappa_L$ 以下である（濃度）。$\square$

1：$\Gamma\not\vdash\varphi$ なら、命題「証明可能性と無矛盾性」により $\Gamma\cup\{\lnot\varphi\}$ は無矛盾で、thm-henkin-model-existence によりモデル $\mathcal M$ をもつ。$\mathcal M$ は $\Gamma$ を満たし $\varphi$ を偽にするので $\Gamma\not\models\varphi$ である。2：$\kappa_L=\aleph_0$ の場合の thm-henkin-model-existence である。$\square$