Kripke意味論

$\Gamma$ からの導出 $\chi_1,\dots,\chi_m$ の各 $\chi_k$ について、$\Gamma$ の元をすべて強制する世界 $w$ が $\chi_k$ を強制することを $k$ に関する帰納法で示す。$\chi_k$ が公理なら、直観主義論理 の定理「Heyting 代数に関する健全性」を $\operatorname{Up}(W)$ に当てると値は $W$ なので、prop-ks-upsets によりすべての世界で強制される。$\chi_k\in\Gamma$ なら仮定による。$\chi_k$ が $\chi_i$ と $\chi_i\to\chi_k$ から前件肯定で得られたなら、帰納法の仮定から $w\Vdash\chi_i$、$w\Vdash\chi_i\to\chi_k$ であり、$w\le w$ なので $w\Vdash\chi_k$ である。$\square$

論理式は可算個なので $\chi_0,\chi_1,\dots$ と並べる。$\Gamma_0=\Gamma$ とし、$\Gamma_n\cup\{\chi_n\}\not\vdash_{\mathrm I}\varphi$ なら $\Gamma_{n+1}=\Gamma_n\cup\{\chi_n\}$、そうでなければ $\Gamma_{n+1}=\Gamma_n$ とする。各 $\Gamma_n$ について $\Gamma_n\not\vdash_{\mathrm I}\varphi$ であり、導出は有限個の仮定しか使わないので、$\Delta=\bigcup_n\Gamma_n$ も $\Delta\not\vdash_{\mathrm I}\varphi$ をみたす。とくに $\varphi\notin\Delta$ である。
鍵は次の観察である：$\chi=\chi_n\notin\Delta$ なら、$\chi$ は第 $n$ 段で加えられなかったので $\Gamma_n\cup\{\chi\}\vdash_{\mathrm I}\varphi$、したがって 直観主義論理 の命題「演繹定理」により $\Delta\vdash_{\mathrm I}\chi\to\varphi$ である（$(\ast)$）。
1：$\Delta\vdash_{\mathrm I}\chi$ で $\chi\notin\Delta$ なら、$(\ast)$ と前件肯定で $\Delta\vdash_{\mathrm I}\varphi$ となり矛盾する。2：$\bot\in\Delta$ なら公理 7（$\bot\to\varphi$）で $\Delta\vdash_{\mathrm I}\varphi$ となる。3：$\chi\lor\theta\in\Delta$ で $\chi,\theta\notin\Delta$ なら、$(\ast)$ から $\Delta\vdash_{\mathrm I}\chi\to\varphi$、$\Delta\vdash_{\mathrm I}\theta\to\varphi$ であり、公理 6 の $(\chi\to\varphi)\to((\theta\to\varphi)\to(\chi\lor\theta\to\varphi))$ と前件肯定 3 回で $\Delta\vdash_{\mathrm I}\varphi$ となる。$\square$

$\varphi$ の組み立てに関する帰納法による。要は含意の場合で、そこで lem-ks-prime-extension を使う。
$\varphi=\psi\to\chi$ とする。$\psi\to\chi\in\Delta$ で、$\Delta\subset\Delta'$、$\Delta'\Vdash\psi$ なら、帰納法の仮定から $\psi\in\Delta'$、$\psi\to\chi\in\Delta'$ であり、$\Delta'$ は導出で閉じているので $\chi\in\Delta'$、すなわち $\Delta'\Vdash\chi$。よって $\Delta\Vdash\psi\to\chi$。逆に $\psi\to\chi\notin\Delta$ なら $\Delta\cup\{\psi\}\not\vdash_{\mathrm I}\chi$ である（そうでなければ演繹定理で $\Delta\vdash_{\mathrm I}\psi\to\chi$ となり、閉じているので $\psi\to\chi\in\Delta$）。lem-ks-prime-extension で $\Delta\cup\{\psi\}\subset\Delta'$、$\chi\notin\Delta'$ となる素な理論 $\Delta'$ をとれば、$\Delta\subset\Delta'$ で、帰納法の仮定から $\Delta'\Vdash\psi$、$\Delta'\not\Vdash\chi$ なので $\Delta\not\Vdash\psi\to\chi$。

$\Gamma\not\vdash_{\mathrm I}\varphi$ とする。lem-ks-prime-extension で $\Gamma\subset\Delta$、$\varphi\notin\Delta$ となる素な理論 $\Delta$ をとると、lem-ks-truth により標準モデルの世界 $\Delta$ は $\Gamma$ の元をすべて強制し、$\varphi$ を強制しない。よって $\Gamma\not\Vdash\varphi$。$\square$

$\mathcal M=(W,\le,V)$、$w_*\not\Vdash\varphi$ とし、$\Sigma=\operatorname{Sub}(\varphi)$ とおく。$u\in W$ に $\tau(u)=\{\psi\in\Sigma\mid u\Vdash\psi\}$ を対応させ、$W^*=\{\tau(u)\mid u\in W\}$ に包含を順序として入れる。$W^*$ は $\Sigma$ の部分集合からなるので $2^{|\Sigma|}$ 個以下である。$V^*(p)=\{X\in W^*\mid p\in X\}$（$p\in\Sigma$ のとき。それ以外は $\emptyset$）は上に閉じている。$\mathcal M^*=(W^*,\subset,V^*)$ について、すべての $\psi\in\Sigma$ と $u\in W$ で
$$ \mathcal M,u\Vdash\psi\iff\mathcal M^*,\tau(u)\Vdash\psi $$
を $\psi$ の組み立てに関する帰納法で示す（$\Sigma$ は部分論理式で閉じているので、帰納法の仮定が使える）。命題変数は $V^*$ の定義から、$\bot,\land,\lor$ は帰納法の仮定から従う。含意 $\psi=\theta\to\chi$ の場合は、⇒ で $\theta\to\chi\in\tau(u)\subset\tau(v)$ を、⇐ で lem-ks-persistence を使う。

⇒：$(W,R)$ を反射的かつ推移的なフレーム、$V$ を付値とする。$\vdash_{\mathrm I}\varphi$ なので、thm-ks-soundness（前順序でも成り立つ）により前順序上のモデル $(W,R,V')$ のすべての世界で $\varphi$ が強制され、lem-ks-translation から $(W,R,V)\Vdash T(\varphi)$ である。よって $T(\varphi)$ は反射的かつ推移的なすべてのフレームで妥当であり、様相論理 の定理「標準モデルの性質と完全性定理」の 3 により $\mathbf{S4}\vdash T(\varphi)$。
⇐：同じ定理の 3 により、$T(\varphi)$ は反射的かつ推移的なすべてのフレームで妥当である。Kripke モデル $(W,\le,V)$ を様相論理のモデルとみると、$\le$ は反射的で $V(p)$ は上に閉じているので $w\Vdash\Box p\iff w\in V(p)$、すなわち $V'=V$ である。lem-ks-translation から $(W,\le,V)$ のすべての世界で $\varphi$ が強制される。よって $\varphi$ は Kripke 妥当であり、thm-ks-completeness により $\vdash_{\mathrm I}\varphi$。$\square$