Craigの補間定理

$\operatorname{var}(\varphi)$ のうち $\operatorname{var}(\psi)$ に属さない命題変数を $q_1,\dots,q_k$ とする（$k=0$ なら $\theta:=\varphi$ でよい）。$e=(e_1,\dots,e_k)\in\{\top,\bot\}^k$ ごとに、$\varphi$ の $q_i$ に $e_i$ を代入した論理式を $\varphi[e/\bar q]$ とし、
$$ \theta:=\bigvee_{e\in\{\top,\bot\}^k}\varphi[e/\bar q] $$
とおく。$\varphi[e/\bar q]$ には $q_1,\dots,q_k$ が現れないので、$\operatorname{var}(\theta)\subset\operatorname{var}(\varphi)\cap\operatorname{var}(\psi)$ である。以下、付値 $v$ と $e$ について、$v_e$ を「$q_i$ では $e_i$ の真理値をとり、ほかの命題変数では $v$ と同じ値をとる付値」とする。恒真式 の記事の補題「代入と付値」により $v(\varphi[e/\bar q])=v_e(\varphi)$ である（同補題は、定数 $\top,\bot$ を含む論理式でも、論理式の組み立てについての同じ帰納法で成り立つ）。
$\varphi\to\theta$ が恒真式であること． $v(\varphi)=\mathrm{T}$ とし、$e_i$ を $v(q_i)$ が $\mathrm{T}$ なら $\top$、$\mathrm{F}$ なら $\bot$ とおく。このとき $v_e=v$ なので $v(\varphi[e/\bar q])=v(\varphi)=\mathrm{T}$ となり、$v(\theta)=\mathrm{T}$ である。
$\theta\to\psi$ が恒真式であること． $v(\theta)=\mathrm{T}$ とすると、ある $e$ で $v_e(\varphi)=v(\varphi[e/\bar q])=\mathrm{T}$ である。$\varphi\to\psi$ は恒真式なので $v_e(\psi)=\mathrm{T}$ である。$v_e$ と $v$ は $q_1,\dots,q_k$ でしか違わず、それらは $\psi$ に現れないので、$v(\psi)=v_e(\psi)=\mathrm{T}$ である。$\square$

$\varphi\models\theta$ となる $L_0$ の文 $\theta$ の全体を $\Gamma$ とする。
段 1（$\Gamma\cup\{\lnot\psi\}$ はモデルをもつ）． もたないとすると $\Gamma\models\psi$ であり、コンパクト性定理(一階論理) の系「帰結の有限性」により有限個の $\theta_1,\dots,\theta_k\in\Gamma$ で $\{\theta_1,\dots,\theta_k\}\models\psi$ となるものがある。$\theta:=\theta_1\land\cdots\land\theta_k$（$k=0$ なら $\forall x\,(x=x)$）は $L_0$ の文で、$\varphi\models\theta$、$\theta\models\psi$ を満たす補間式になり、仮定に反する。そこで $\Gamma\cup\{\lnot\psi\}$ の $L_2$ 構造のモデル $\mathcal N$ をとる。
段 2（$\varphi$ と $\mathcal N$ の $L_0$ の理論は両立する）． $\mathcal N|_{L_0}$ で真な $L_0$ の文の全体を $T_0$ とする。$T_0\cup\{\varphi\}$ がモデルをもたないとすると、段 1 と同じく有限個の $\chi_1,\dots,\chi_m\in T_0$ で、$\chi:=\chi_1\land\cdots\land\chi_m$（$m=0$ なら $\forall x\,(x=x)$）が $\varphi\models\lnot\chi$ を満たすものがある。$\lnot\chi$ は $L_0$ の文なので $\lnot\chi\in\Gamma$ であり、$\mathcal N\models\lnot\chi$ となるが、$\chi\in T_0$ なので $\mathcal N\models\chi$ であり矛盾する。よって $T_0\cup\{\varphi\}$ の $L_1$ 構造のモデル $\mathcal M$ がある。$\mathcal M|_{L_0}$ は $T_0$ のすべての文を満たし、$T_0$ はどの $L_0$ の文についてもそれ自身か否定を含むので、$\mathcal M|_{L_0}$ と $\mathcal N|_{L_0}$ は同じ $L_0$ の文を満たす。$\square$

要点：「$\mathcal B$ の初等図式」と「$\mathcal A$ で成り立つ $L_0$ の論理式すべて」を合わせた文の集合の有限部分は、$\mathcal A$ で存在を述べる $L_0$ の文に移して $\mathcal B$ の中で満たせる。

補間式がないとして矛盾を導く。lem-craig-separate の $\mathcal M\models\varphi$、$\mathcal N\models\lnot\psi$ をとる。
段 1（往復して初等鎖を作る）． $L_1$ 構造の列 $\mathcal M=\mathcal M_0\preccurlyeq\mathcal M_1\preccurlyeq\cdots$、$L_2$ 構造の列 $\mathcal N\preccurlyeq\mathcal N_0\preccurlyeq\mathcal N_1\preccurlyeq\cdots$ と、$L_0$ で初等的な写像 $f_n\colon\mathcal M_n\to\mathcal N_n$、$g_n\colon\mathcal N_n\to\mathcal M_{n+1}$ で
$$ g_n(f_n(a))=a\quad(a\in\mathcal M_n),\qquad f_{n+1}(g_n(b))=b\quad(b\in\mathcal N_n) $$
を満たすものを作る。まず空写像は $L_0$ で初等的なので（lem-craig-separate）、lem-craig-extend を $\mathcal A=\mathcal M$、$C=\emptyset$、$\mathcal B=\mathcal N$ に使って $\mathcal N_0$ と $f_0$ を得る。$f_n$ ができたら、逆写像 $f_n^{-1}\colon f_n(\mathcal M_n)\to\mathcal M_n$ は $\mathcal N_n$ の部分集合から $\mathcal M_n$ への $L_0$ で初等的な写像なので、lem-craig-extend を $\mathcal A=\mathcal N_n$、$\mathcal B=\mathcal M_n$ に使えば $\mathcal M_{n+1}$ と $f_n^{-1}$ を延長する $g_n$ が得られる。同様に $g_n^{-1}$ を延長して $f_{n+1}\colon\mathcal M_{n+1}\to\mathcal N_{n+1}$ を得る。$a\in\mathcal M_n$ なら $f_{n+1}(a)=f_{n+1}(g_n(f_n(a)))=f_n(a)$ なので、$f_{n+1}$ は $f_n$ の延長である。
段 2（和をとる）． $\mathcal M_\omega:=\bigcup_n\mathcal M_n$、$\mathcal N_\omega:=\bigcup_n\mathcal N_n$、$f:=\bigcup_nf_n$ とおく。初等部分モデル の記事の定理「初等鎖の和」により $\mathcal M_n\preccurlyeq\mathcal M_\omega$、$\mathcal N_n\preccurlyeq\mathcal N_\omega$ である。$\bar a\in\mathcal M_n$ と $L_0$ の論理式 $\chi$ について
$$ \mathcal M_\omega\models\chi[\bar a]\iff\mathcal M_n\models\chi[\bar a]\iff\mathcal N_n\models\chi[f_n(\bar a)]\iff\mathcal N_\omega\models\chi[f(\bar a)] $$
なので $f$ は $L_0$ で初等的で、とくに単射である。$b\in\mathcal N_n$ なら $b=f_{n+1}(g_n(b))$ なので全射でもある。原子論理式 $R(\bar x)$、$F(\bar x)=y$、$c=y$（$R,F,c\in L_0$）の真偽を保つ全単射なので、$f$ は $\mathcal M_\omega|_{L_0}$ から $\mathcal N_\omega|_{L_0}$ への同型写像である。
段 3（1 つの構造にまとめる）． $\mathcal M_\omega$ の台集合の上に $L_1\cup L_2$ 構造 $\mathcal K$ を、$L_1$ の記号は $\mathcal M_\omega$ のとおりに、$L_2\setminus L_1$ の記号は $f$ で $\mathcal N_\omega$ から写して（$R^{\mathcal K}:=f^{-1}(R^{\mathcal N_\omega})$ など）解釈する。$\mathcal K|_{L_1}=\mathcal M_\omega$ であり、$L_0$ の記号でも段 2 により $f$ が解釈を保つので、$f$ は $\mathcal K|_{L_2}$ から $\mathcal N_\omega$ への同型写像である。$\mathcal M\preccurlyeq\mathcal M_\omega$ から $\mathcal K\models\varphi$、$\mathcal N\preccurlyeq\mathcal N_\omega$ と同型写像が真偽を保つことから $\mathcal K\models\lnot\psi$ となり、$\varphi\models\psi$ に反する。$\square$

もたないとすると、コンパクト性定理(一階論理) により、$T_1$ の有限個の文の連言 $\varphi$ と $T_2$ の有限個の文の連言 $\psi'$ で $\varphi\models\lnot\psi'$ となるものがある（空の連言は $\forall x\,(x=x)$ とする）。thm-craig-main の補間式 $\theta$ をとると、$\varphi\models\theta$、$\theta\models\lnot\psi'$ である。$T_0\models\theta$ なら $T_2\models\theta$ なので $T_2\models\lnot\psi'$ となるが、$T_2\models\psi'$ なので $T_2$ はモデルをもたず矛盾する。$T_0\models\lnot\theta$ なら $T_1\models\lnot\theta$ だが $T_1\models\varphi\models\theta$ なので、$T_1$ がモデルをもたず矛盾する。$\square$

$R$ の写しとして新しい関係記号 $R'$ を用意し、$U$ の文の $R$ を $R'$ に置き換えたものの全体を $U'$ とする。新しい定数記号 $c_1,\dots,c_n$ をとる。
段 1． $U\cup U'\models R(\bar c)\to R'(\bar c)$ である。実際、$U\cup U'$ のモデル $\mathcal K$ から、$R$ を $R^{\mathcal K}$ と解釈した構造と、$R$ を $R'^{\mathcal K}$ と解釈した構造を作ると、どちらも $U$ のモデルで、台集合と $L$ の部分が同じなので、陰の定義により $R^{\mathcal K}=R'^{\mathcal K}$ となる。
段 2． コンパクト性定理(一階論理) の系「帰結の有限性」により、$U$ の有限個の文の連言 $\alpha(R)$ と、その写し $\alpha(R')$ で $\alpha(R)\land\alpha(R')\models R(\bar c)\to R'(\bar c)$ となるものがある（$U$ と $U'$ から取り出した有限個の文を合わせ、両方の写しをとればよい）。これを
$$ \alpha(R)\land R(\bar c)\models\alpha(R')\to R'(\bar c) $$
と書き直す。左辺の記号は $L\cup\{R,\bar c\}$、右辺の記号は $L\cup\{R',\bar c\}$ の中にあるので、thm-craig-main により $L\cup\{\bar c\}$ の文 $\theta(\bar c)$ で $\alpha(R)\land R(\bar c)\models\theta(\bar c)$ かつ $\theta(\bar c)\models\alpha(R')\to R'(\bar c)$ となるものがある。後者の $R'$ を $R$ に書き戻すと $\theta(\bar c)\models\alpha(R)\to R(\bar c)$ である。
段 3． 2 つを合わせると $\alpha(R)\models R(\bar c)\leftrightarrow\theta(\bar c)$ であり、$\bar c$ は $\alpha$ に現れない新しい定数記号なので、$\theta(\bar c)$ の $c_i$ を $\alpha$ に現れない変数 $x_i$ に置き換えた $\delta(\bar x)$ について $U\models\forall\bar x\,(R(\bar x)\leftrightarrow\delta(\bar x))$ が成り立つ。$\square$