様相論理

$\mathsf C$ で妥当な論理式の集合が正規様相論理であり、$\Lambda$ の図式の形の論理式を含むことを示せばよい（$\mathbf K\Lambda$ はそのような最小のものだから）。

(a) ⇒ (b) は明らかである。
(c) ⇒ (a)． $\mathcal F$ 上のモデルと世界 $w$ を任意にとり、図式の前件が $w$ で真なら後件も真であることを確かめる。4 で代表させる。$w\Vdash\Box\varphi$ とし、$wRv$、$vRu$ とする。推移性から $wRu$ なので $u\Vdash\varphi$。よって $v\Vdash\Box\varphi$ であり、$w\Vdash\Box\Box\varphi$。

1 は、論理式を $\varphi_0,\varphi_1,\dots$ と並べ、$\varphi_k$ か $\lnot\varphi_k$ の無矛盾に保てるほうを順に加えていけば得られる。2 と 3 は $\Sigma$ が恒真式の代入例を含みモーダスポネンスで閉じていることから従う。

$\Box^{-1}\Delta\cup\{\lnot\varphi\}$ が $\Sigma$ 無矛盾であることを示せば、lem-ml-mcs の 1 でそれを含む極大無矛盾集合 $\Delta'$ がとれ、$\Box^{-1}\Delta\subset\Delta'$、$\lnot\varphi\in\Delta'$ となる。無矛盾性は lem-ml-rk から従う。

$\varphi$ の組み立てに関する帰納法による。$\Box\psi$ の場合が要で、$\Box\psi\notin\Delta$ のとき lem-ml-existence を使う。

1. $\Sigma\vdash\varphi$ なら lem-ml-mcs の 2 と lem-ml-truth から $\mathcal M^\Sigma\Vdash\varphi$。$\Sigma\not\vdash\varphi$ なら $\{\lnot\varphi\}$ は $\Sigma$ 無矛盾（矛盾すれば $\Sigma\vdash\lnot\varphi\to\bot$ から $\Sigma\vdash\varphi$）なので、それを含む $\Delta$ がとれ、$\Delta\not\Vdash\varphi$ である。$\Sigma=\mathbf K$ とし、$\varphi$ が妥当なら $\mathcal M^{\mathbf K}\Vdash\varphi$ なので $\mathbf K\vdash\varphi$。
2. $\mathrm T$：$\Box\psi\in\Delta$ なら $\Box\psi\to\psi\in\Sigma\subset\Delta$ から $\psi\in\Delta$。よって $\Delta R^\Sigma\Delta$。$4$：$\Delta_1R^\Sigma\Delta_2R^\Sigma\Delta_3$ とし、$\Box\psi\in\Delta_1$ とする。$4$ から $\Box\Box\psi\in\Delta_1$、よって $\Box\psi\in\Delta_2$、$\psi\in\Delta_3$。よって $\Delta_1R^\Sigma\Delta_3$。
   D・B・5 を開く

   $\mathrm D$：$\Box^{-1}\Delta$ が無矛盾なら、それを含む $\Delta'$ が $\Delta R^\Sigma\Delta'$ を満たす。矛盾するとすると $\psi_i\in\Box^{-1}\Delta$ で $\Sigma\vdash\psi_1\land\dots\land\psi_n\to\bot$、lem-ml-rk から $\Box\bot\in\Delta$ となる。$\mathrm D$ から $\Diamond\bot=\lnot\Box\lnot\bot\in\Delta$ だが、$\lnot\bot$ は恒真式なので必然化で $\Box\lnot\bot\in\Sigma\subset\Delta$ となり矛盾する。

   $\mathrm B$：$\Delta R^\Sigma\Delta'$ とし、$\Box\psi\in\Delta'$ なのに $\psi\notin\Delta$ とする。$\lnot\psi\in\Delta$ と $\mathrm B$ から $\Box\Diamond\lnot\psi\in\Delta$、よって $\Diamond\lnot\psi=\lnot\Box\lnot\lnot\psi\in\Delta'$。一方 $\psi\to\lnot\lnot\psi$ に lem-ml-rk を使うと $\Box\lnot\lnot\psi\in\Delta'$ となり矛盾する。よって $\Delta'R^\Sigma\Delta$。

   $5$：$\Delta_1R^\Sigma\Delta_2$、$\Delta_1R^\Sigma\Delta_3$ とし、$\Box\psi\in\Delta_2$ なのに $\psi\notin\Delta_3$ とする。$\lnot\psi\in\Delta_3$ なので lem-ml-mcs の 3 から $\Diamond\lnot\psi\in\Delta_1$、$5$ から $\Box\Diamond\lnot\psi\in\Delta_1$、よって $\lnot\Box\lnot\lnot\psi\in\Delta_2$。$\mathrm B$ の場合と同じく $\Box\lnot\lnot\psi\in\Delta_2$ なので矛盾する。よって $\Delta_2R^\Sigma\Delta_3$。

3. ⇒ は thm-ml-correspondence の (c) ⇒ (a) と thm-ml-soundness による。⇐：$\mathbf K\Lambda\not\vdash\varphi$ なら 1 により $\mathcal M^{\mathbf K\Lambda}\not\Vdash\varphi$ であり、2 によりそのフレーム $(W^{\mathbf K\Lambda},R^{\mathbf K\Lambda})$ は $\mathsf C_\Lambda$ に属するので、$\mathsf C_\Lambda\not\models\varphi$。$\mathbf{S5}$ は、反射的かつ Euclid 的な関係が同値関係であること（対応定理の後）とその逆による。$\square$

1. $\psi$ の組み立てに関する帰納法による。$\Gamma$ が部分論理式で閉じているので、帰納法の仮定は $\psi$ の部分論理式に使える。要の $\psi=\Box\chi$ の場合を示す。
   命題変数の場合と □ の場合を開く

   $\psi=p\in\Gamma$ のとき、$[w]\in V^*(p)$ なら $w\equiv u$ となる $u\in V(p)$ があり、$p\in\Gamma$ なので $w\Vdash p$ である。逆は定義から。結合子の場合は帰納法の仮定と真理値表による。$\psi=\Box\chi$ とする。$w\Vdash\Box\chi$ で $[w]R^*[v]$ なら、$u'Rv'$ となる $u'\equiv w$、$v'\equiv v$ がある。$\Box\chi\in\Gamma$ なので $u'\Vdash\Box\chi$、よって $v'\Vdash\chi$、$\chi\in\Gamma$ なので $v\Vdash\chi$、帰納法の仮定から $[v]\Vdash\chi$。よって $[w]\Vdash\Box\chi$。逆に $[w]\Vdash\Box\chi$ で $wRv$ なら $[w]R^*[v]$ なので $[v]\Vdash\chi$、帰納法の仮定から $v\Vdash\chi$。よって $w\Vdash\Box\chi$。

2. $[u]$ に $\{\psi\in\Gamma\mid u\Vdash\psi\}$ を対応させる写像は、$\equiv$ の定義から well-defined かつ単射で、値は $\Gamma$ の部分集合である。
3. $\mathbf K\not\vdash\varphi$ なら thm-ml-completeness の 1 により、あるモデル $\mathcal M$ の世界 $w$ で $\varphi$ は偽である。$\Gamma=\operatorname{Sub}(\varphi)$ による最小のフィルトレーションをとれば、1 と 2 から求めるモデルが得られる。
   決定の手続きを開く

   世界が $\{1,\dots,m\}$（$m\le2^{|\operatorname{Sub}(\varphi)|}$）のモデルで、付値を $\varphi$ に現れる命題変数だけについて決めたものは有限個しかない（ほかの変数の付値は $\varphi$ の真偽に影響しない）。そのすべてで $\varphi$ の真偽を計算し、偽になる世界がなければ、上の議論により $\mathbf K\vdash\varphi$ であり、あれば thm-ml-soundness により $\mathbf K\not\vdash\varphi$ である。$\square$