コンパクト性定理(命題論理)

$\Sigma_0\subset\Sigma$ で $\Sigma_0\models\varphi$ なら、$\Sigma$ を充足する付値は $\Sigma_0$ も充足するので $\varphi$ を $\mathrm{T}$ にし、$\Sigma\models\varphi$ である。
逆に $\Sigma\models\varphi$ とする。定義の直後に述べたことから $\Sigma\cup\{\lnot\varphi\}$ は充足可能でない。thm-propositional-compactness により、充足可能でない有限部分集合 $F\subset\Sigma\cup\{\lnot\varphi\}$ がある。$\Sigma_0:=F\cap\Sigma$ は $\Sigma$ の有限部分集合で、$F\subset\Sigma_0\cup\{\lnot\varphi\}$ なので $\Sigma_0\cup\{\lnot\varphi\}$ も充足可能でない。よって $\Sigma_0\models\varphi$ である。$\square$

どちらも有限充足可能でないと仮定する。$\Delta$ 自身は有限充足可能なので、$\Delta\cup\{\psi\}$ の充足可能でない有限部分集合は $\psi$ を含み、$F\cup\{\psi\}$（$F\subset\Delta$ は有限）の形に書ける。同様に、有限集合 $G\subset\Delta$ で $G\cup\{\lnot\psi\}$ が充足可能でないものがある。$F\cup G$ は $\Delta$ の有限部分集合なので、これを充足する付値 $v$ がある。$v(\psi)=\mathrm{T}$ なら $v$ は $F\cup\{\psi\}$ を充足し、$v(\psi)=\mathrm{F}$ なら $v(\lnot\psi)=\mathrm{T}$ なので $v$ は $G\cup\{\lnot\psi\}$ を充足する。どちらも仮定に反する。$\square$

$\Sigma$ を含む有限充足可能な論理式の集合全体を $\mathcal P$ とし、包含関係で順序づける。$\Sigma\in\mathcal P$ なので $\mathcal P$ は空でない。
$\mathcal C\subset\mathcal P$ を鎖（どの 2 元も包含で比べられる部分集合）とする。$\mathcal C$ が空なら $\Sigma$ が上界である。$\mathcal C$ が空でないとき $U:=\bigcup\mathcal C$ とおく。$U$ の有限部分集合 $F=\{\theta_1,\dots,\theta_m\}$ をとると、各 $\theta_i$ はある $\Delta_i\in\mathcal C$ に属する。$\Delta_1,\dots,\Delta_m$ は包含で比べられるので、その中に最大のもの $\Delta_j$ があり、$F\subset\Delta_j$ である（$m=0$ なら $F=\emptyset$ は充足可能）。$\Delta_j$ は有限充足可能なので $F$ は充足可能である。よって $U$ は有限充足可能で $\Sigma\subset U$ を満たし、$U\in\mathcal P$ は $\mathcal C$ の上界である。
Zornの補題 により $\mathcal P$ は極大元 $\Delta$ をもつ。$\Delta$ より真に大きい有限充足可能集合 $\Delta'$ があれば、$\Delta'\supset\Sigma$ なので $\Delta'\in\mathcal P$ となり、$\Delta$ の極大性に反する。よって $\Delta$ は極大有限充足可能集合である。$\square$

1：両方が属すると、有限部分集合 $\{\psi,\lnot\psi\}$ が充足可能でない。lem-propositional-compactness-dichotomy により $\Delta\cup\{\psi\}$ か $\Delta\cup\{\lnot\psi\}$ は有限充足可能であり、$\Delta$ の極大性からその集合は $\Delta$ に等しいので、$\psi\in\Delta$ または $\lnot\psi\in\Delta$ である。
2：$\theta\notin\Delta$ なら 1 により $\lnot\theta\in\Delta$ である。$F\cup\{\lnot\theta\}$ は $\Delta$ の有限部分集合なので、これを充足する付値 $v$ がある。$v$ は $F$ を充足するので仮定から $v(\theta)=\mathrm{T}$ だが、$v(\lnot\theta)=\mathrm{T}$ と両立しない。
3：$\psi\land\chi\in\Delta$ なら、$F=\{\psi\land\chi\}$ を充足する付値は $\psi$ も $\chi$ も $\mathrm{T}$ にするので、2 により $\psi,\chi\in\Delta$ である。逆に $\psi,\chi\in\Delta$ なら $F=\{\psi,\chi\}$ に 2 を使えばよい。
4：$\psi\in\Delta$ なら $F=\{\psi\}$、$\chi\in\Delta$ なら $F=\{\chi\}$ に 2 を使えば $\psi\lor\chi\in\Delta$ である。逆に $\psi\lor\chi\in\Delta$ で $\psi,\chi$ がともに $\Delta$ に属さないとすると、1 により $\lnot\psi,\lnot\chi\in\Delta$ となり、有限部分集合 $\{\psi\lor\chi,\lnot\psi,\lnot\chi\}$ は充足可能でないので矛盾する。
5：$\psi\notin\Delta$ なら 1 により $\lnot\psi\in\Delta$ で、$F=\{\lnot\psi\}$ を充足する付値は $\psi\to\chi$ を $\mathrm{T}$ にする。$\chi\in\Delta$ なら $F=\{\chi\}$ で同様である。いずれも 2 により $\psi\to\chi\in\Delta$ である。逆に $\psi\to\chi\in\Delta$ かつ $\psi\in\Delta$ なら、$F=\{\psi,\psi\to\chi\}$ を充足する付値は $\chi$ を $\mathrm{T}$ にするので、2 により $\chi\in\Delta$ である。$\square$

2 から 1 を示す。$\Sigma$ を有限充足可能とし、lem-propositional-compactness-extension により $\Sigma\subset\Delta$ となる極大有限充足可能集合 $\Delta$ をとる。付値 $v_\Delta$ を
$$ v_\Delta(p)=\mathrm{T}\iff p\in\Delta\qquad(p\in\mathrm{Var}) $$
で定める。すべての論理式 $\varphi$ について
$$ v_\Delta(\varphi)=\mathrm{T}\iff\varphi\in\Delta $$
であることを、論理式の組み立てに沿った帰納法で示す。命題変数では $v_\Delta$ の定義そのものである。$\varphi=\lnot\psi$ なら、$v_\Delta(\lnot\psi)=\mathrm{T}\iff v_\Delta(\psi)=\mathrm{F}\iff\psi\notin\Delta\iff\lnot\psi\in\Delta$ である（2 つ目は帰納法の仮定、3 つ目は lem-propositional-compactness-maximal-properties の 1）。$\varphi=\psi\land\chi$ なら
$$ v_\Delta(\psi\land\chi)=\mathrm{T}\iff v_\Delta(\psi)=v_\Delta(\chi)=\mathrm{T}\iff\psi\in\Delta\text{ かつ }\chi\in\Delta\iff\psi\land\chi\in\Delta $$
であり、最後は同じ補題の 3 による。$\lor$ と $\to$ も、付値の規則と補題の 4・5 から同様である。
$\Sigma\subset\Delta$ なので、$\Sigma$ の元はすべて $v_\Delta$ で $\mathrm{T}$ になる。よって $\Sigma$ は充足可能である。1 から 2 は定理の直後に述べた。最後の主張は 2 から 1 の対偶である。$\square$

段 1（各層は空でない有限集合）。$T_0=\{()\}$ であり、$T_{n+1}$ は $T_n$ の各元の子の集合の和集合なので、$T_n$ が有限なら有限分岐の仮定から $T_{n+1}$ も有限である。よって帰納法ですべての $T_n$ は有限である。ある $N$ で $T_N=\emptyset$ なら、$m\ge N$ の $\sigma\in T_m$ について $\sigma|N\in T_N$ となるので $T_m=\emptyset$ であり、$T=T_0\cup\cdots\cup T_{N-1}$ は有限集合になって仮定に反する。よってすべての $T_n$ は空でない。
段 2（論理式の集合）。$\sigma\in T$ ごとに命題変数 $q_\sigma$ を用意する（「$\sigma$ が求める枝の上にある」と読む）。$\Sigma$ を次の論理式全体とする。

1. 各 $n$ について、$T_n$ の元を $\sigma_1,\dots,\sigma_k$ と並べた選言 $q_{\sigma_1}\lor\cdots\lor q_{\sigma_k}$。
2. 各 $n$ と $T_n$ の相異なる元 $\sigma,\tau$ について、$\lnot(q_\sigma\land q_\tau)$。
3. 各 $n$ と $\sigma\in T_{n+1}$ について、$q_\sigma\to q_{\sigma|n}$。
   段 1 により 1 は有限の選言であり、正しい論理式である。1 と 2 で「各層でちょうど 1 つ」、3 で「選んだ頂点の親も選ぶ」ことを表す。
   段 3（有限充足可能）。$F\subset\Sigma$ を有限部分集合とし、$F$ の論理式に現れる $q_\sigma$ の $\lvert\sigma\rvert$ の最大値を $N$ とする。段 1 により $\tau\in T_N$ がとれる。付値 $v$ を「$v(q_\sigma)=\mathrm{T}\iff\lvert\sigma\rvert\le N$ かつ $\sigma=\tau|\lvert\sigma\rvert$」で定める。$n\le N$ の層では $\tau|n\in T_n$ がちょうど 1 つの $\mathrm{T}$ の変数なので、1 と 2 の形の論理式は $\mathrm{T}$ である。3 の形の論理式で $v(q_\sigma)=\mathrm{T}$ なら $\sigma=\tau|(n+1)$ なので $\sigma|n=\tau|n$ となり、$v(q_{\sigma|n})=\mathrm{T}$ である。$F$ の論理式はすべて $N$ 以下の層の変数だけを使うので、$v$ は $F$ を充足する。
   段 4（枝を読み取る）。thm-propositional-compactness により $\Sigma$ を充足する付値 $v$ がある。1 と 2 により、各 $n$ について $v(q_{\sigma_n})=\mathrm{T}$ となる $\sigma_n\in T_n$ がちょうど 1 つある。3 により $v(q_{\sigma_{n+1}|n})=\mathrm{T}$ で $\sigma_{n+1}|n\in T_n$ なので、一意性から $\sigma_{n+1}|n=\sigma_n$ である。帰納法で $n\le m$ なら $\sigma_m|n=\sigma_n$ となる。$a_n$ を $\sigma_{n+1}$ の最後の項とすると $(a_0,\dots,a_{n-1})=\sigma_n\in T$ であり、$(a_0,a_1,\dots)$ は $T$ の無限の枝である。$\square$

$\lambda\in\Lambda$ と $u\in U_\lambda$ の組ごとに命題変数 $r_{\lambda,u}$ を用意する（「$f(\lambda)=u$」と読む）。$I=\{\lambda\}$ に仮定を使えば $U_\lambda\ne\emptyset$ である。$\Sigma$ を次の論理式全体とする。

1. 各 $\lambda$ について、$U_\lambda$ の元を $u_1,\dots,u_k$ と並べた選言 $r_{\lambda,u_1}\lor\cdots\lor r_{\lambda,u_k}$。
2. 各 $\lambda$ と $U_\lambda$ の相異なる元 $u,u'$ について、$\lnot(r_{\lambda,u}\land r_{\lambda,u'})$。
3. 相異なる $\lambda,\mu\in\Lambda$ と $u\in U_\lambda\cap U_\mu$ について、$\lnot(r_{\lambda,u}\land r_{\mu,u})$。
   $U_\lambda$ が有限なので 1 は有限の選言である。1 と 2 で「$f(\lambda)$ が $U_\lambda$ の元としてちょうど 1 つに決まる」こと、3 で「$f$ が単射」であることを表す。
   有限部分集合 $F\subset\Sigma$ をとり、$F$ の論理式に添字として現れる $\lambda$ の全体を $I$ とする。$I$ は有限集合であり、仮定から有限族 $(U_\lambda)_{\lambda\in I}$ は Hall の条件を満たす。有限の場合の定理（Hallの結婚定理 の記事の定理「Hall の結婚定理」。添字を $1,\dots,\lvert I\rvert$ に付け替えて使う）により、単射 $g\colon I\to Y$ で $g(\lambda)\in U_\lambda$ となるものがある。付値 $v$ を「$v(r_{\lambda,u})=\mathrm{T}\iff\lambda\in I$ かつ $g(\lambda)=u$」で定める。$F$ の 1・2 の形の論理式は $\lambda\in I$ についてのものなので、$g(\lambda)$ だけが $\mathrm{T}$ であることから $\mathrm{T}$ になる。3 の形の論理式は $\lambda,\mu\in I$ についてのもので、$g$ が単射なので $r_{\lambda,u}$ と $r_{\mu,u}$ が同時に $\mathrm{T}$ になることはない。よって $v$ は $F$ を充足し、$\Sigma$ は有限充足可能である。
   thm-propositional-compactness により $\Sigma$ を充足する付値 $v$ がある。1 と 2 により、各 $\lambda$ について $v(r_{\lambda,u})=\mathrm{T}$ となる $u\in U_\lambda$ がちょうど 1 つあるので、それを $f(\lambda)$ とおく。$\lambda\ne\mu$ で $f(\lambda)=f(\mu)=u$ なら $u\in U_\lambda\cap U_\mu$ で、3 の論理式 $\lnot(r_{\lambda,u}\land r_{\mu,u})$ が $\mathrm{F}$ になり矛盾する。よって $f$ は単射である。$\square$