正規様相論理の完全性定理
参考文献
Lem 1.3.6
正規様相論理$ \Lambdaがフレームクラス$ \mathbb{F}に対して強完全である
$ \iff任意の$ \Lambda無矛盾な論理式の集合$ \Gammaが$ \mathbb{F}で充足可能である．
Lem 1.3.8
正規様相論理$ \Lambdaと任意の極大$ \Lambda無矛盾集合$ \Gamma^+について 1. $ \Lambda \sube \Gamma^+
2. $ \Gamma^+ \vdash_\Lambda \varphi \iff \varphi \in \Gamma^+
3. $ \varphi \in \Gamma^+かつ$ \vdash_\Lambda \varphi \to \psi$ \implies$ \psi \in \Gamma^+
4. $ \lnot \varphi \in \Gamma \iff \varphi \not\in \Gamma
5. $ \varphi \to \psi \in \Gamma^+$ \iff$ \varphi \notin \Gamma^+または$ \psi \in \Gamma^+
任意の$ \Lambda無矛盾な集合$ \Gammaに対して，ある極大$ \Lambda無矛盾$ \Gamma^+が存在し，$ \Gamma \sube \Gamma^+．
Def 1.3.11: $ \Lambdaカノニカルモデル$ \mathcal{M}^\Lambda
正規様相論理$ \Lambdaの$ \Lambdaカノニカルモデル$ \mathcal{M}^\Lambda \coloneqq \lang W^\Lambda, R^\Lambda, V^\Lambda \rang
$ W^\Lambda \coloneqq \{ \Gamma^+ \mid \text{$\Gamma^+$ is maximally $\Lambda$ consistent set}\}
$ \Gamma^+ R^\Lambda \Delta^+$ \iff任意の論理式$ \varphiに対し$ \Box \varphi \in \Gamma^+ \implies \varphi \in \Delta^+
$ \Gamma^+ \in V^\Lambda(p) \iff p \in \Gamma^+
Lem 1.3.10
任意の$ \Box \psi，任意の極大$ \Lambda無矛盾集合$ \Gamma^+に対し，
$ \Box \psi \notin \Gamma^+ \implies \{\lnot \psi\} \cup \{\gamma \mid \Box \gamma \in \Gamma^+ \}は$ \Lambda無矛盾
証明
Lem 1.3.13: 真理補題
任意の論理式$ \varphi，任意の極大$ \Lambda無矛盾集合$ \Gamma^+に対し
$ \mathcal{M}^\Lambda, \Gamma^+ \models \varphi \iff \varphi \in \Gamma^+
証明
論理式$ \varphiの構成方法による帰納法で．
1, $ \varphi \equiv p（$ pは命題記号）は$ V^\Lambdaの定義より明らか
2. $ \varphi \equiv \botは$ \bot \not\in \Gamma^+と$ \mathcal{M},\Gamma^+ \not\models \botより同値．
3. $ \varphi \equiv \psi \to \chi
$ \mathcal{M}^\Lambda,\Gamma^+ \models \psi \to \chi
$ \iff$ \mathcal{M}^\Lambda,\Gamma^+ \not\models \psiまたは$ \mathcal{M}^\Lambda,\Gamma^+ \models \chi
$ \iff$ \psi \notin \Gamma^+または$ \chi \in \Gamma^+（帰納法の仮定）
$ \iff$ \psi \to \chi \in \Gamma^+（補題1.3.8.5）❏．
4. $ \varphi \equiv \Box \psi
$ \implies
1. $ \Box \psi \in \Gamma^+を仮定する．
2. $ \mathcal{M}^\Lambda,\Gamma^+ \models \Box\psiを示す
$ \iff任意な$ \Gamma^+R^\Lambda\Delta^+な$ \Delta^+で$ \mathcal{M}^\Lambda,\Delta^+ \models \psiを示す
$ \iff任意な$ \Gamma^+R^\Lambda\Delta^+な$ \Delta^+で$ \psi \in \Delta^+を示す（帰納法の仮定）
3. $ R^\Lambdaの定義より明らか．❏．
$ \impliedby
1. 対偶$ \Box\psi \notin \Gamma^+ \implies \mathcal{M}^\Lambda,\Gamma^+ \not\models \Box\psiを示す．
2. $ \Box\psi \notin \Gamma^+を仮定する
3. $ \{\lnot \psi\} \cup \{\gamma \mid \Box \gamma \in \Gamma^+ \}が$ \Lambda無矛盾．(Lem 2.1)
4. $ \{\lnot \psi\} \cup \{\gamma \mid \Box \gamma \in \Gamma^+ \} \sube \Delta^+となる極大$ \Lambda無矛盾集合$ \Delta^+が存在する．(Lindemaumm補題)
5. 明らかに，$ \Gamma^+ R^\Lambda \Delta^+．
6. $ \psi \notin \Delta^+（補題1.3.8.5）
7. $ \mathcal{M}^\Lambda,\Delta^+ \not\models \psi（6と帰納法の仮定）
8. $ \mathcal{M}^\Lambda,\Gamma^+ \not\models \Box\psi（5と$ \modelsの定義より）．❏．
Thm1.3.14&1.3.15: 到達可能性の制約 論理式$ \alpha \in \{\mathsf{T,B,4,5,D,.2}\}とし，正規様相論理$ \Lambda_\alphaは$ \alpha \in \Lambda_\alphaを満たすとする．
1. $ R^{\Lambda_\mathsf{T}}は反射律を満たす． 2. $ R^{\Lambda_\mathsf{B}}は対称律を満たす． 3. $ R^{\Lambda_\mathsf{4}}は推移律を満たす． 5. $ R^{\Lambda_\mathsf{D}}は継起的となる． 6. $ R^{\Lambda_\mathsf{.2}}は有向的となる． proof 1.
1. $ \mathsf{T} \in R^{\Lambda_\mathsf{T}}．ただし$ \mathsf{T} \equiv \Box\Phi \to \Phi
2. 極大$ R^{\Lambda_\mathsf{T}}無矛盾集合$ \Gamma^+
3. 目標: $ \Gamma^+ R^{\Lambda_\mathsf{T}} \Gamma^+を示す．
任意の$ \varphiに対し$ \Box\varphi \in \Gamma^+とする．このとき$ \varphi \in \Gamma^+か？
4. 1より$ \vdash_{\Lambda_\mathsf{T}} \Box\varphi \to \varphi
5. 4,Lem1.3.6.1より$ \varphi \in \Gamma^+．❏． その他は省略．
任意の$ \Sigma \sube \{\mathsf{T,B,4,5,D,.2}\}について
論理$ \mathbf{K}\Sigmaは$ \Sigmaが定義するフレームクラス$ \mathbb{F}_\Sigmaに対して強完全．
すなわち，$ \mathbb{F}_\Sigma \models \varphi \implies \varphi \in \mathbf{K}\Sigma．
証明
1. $ \Sigmaを含む最小の正規様相論理を$ \Lambda_\Sigmaとする．
2. 任意の$ \Lambda_\Sigma無矛盾な集合$ \Gammaが$ \mathbb{F}_\Sigmaで充足可能であることを示せば十分である．（補題1.3.6）
3. $ \Gammaには極大$ \Lambda_\Sigma無矛盾集合$ \Gamma^+が存在して$ \Gamma \sube \Gamma^+．（Lindebaum補題）
4. $ \mathcal{M}^{\Lambda_\Sigma}, \Gamma^+ \models \Gamma．
任意の論理式$ \varphiに対し，$ \varphi \in \Gamma^+ \iff \mathcal{M}^{\Lambda_\Sigma}, \Gamma^+ \models \varphi（補題1.3.13）
$ \Gamma \sube \Gamma^+より当然$ \varphi \in \Gamma \iff \mathcal{M}^{\Lambda_\Sigma}, \Gamma^+ \models \varphi
よって$ \mathcal{M}^{\Lambda_\Sigma}, \Gamma^+ \models \Gamma
5. 4よりすなわち，$ \lang W^{\Lambda_\Sigma}, R^{\Lambda_\Sigma}, V^{\Lambda_\Sigma} \rang, \Gamma^+ \models \Gammaとなる$ V^{\Lambda_\Sigma}と$ \Gamma^+の存在は示された．
残る問題は$ \mathcal{F}^{\Lambda_\Sigma} \coloneqq \lang W^{\Lambda_\Sigma}, R^{\Lambda_\Sigma} \rang \in \mathbb{F}_\Sigmaであるかどうかである．
$ \mathcal{F}^{\Lambda_\Sigma} \in \mathbb{F}_\Sigmaであることを示せば，$ \Gammaは$ \mathbb{F}_\Sigmaで充足可能である．
6. $ \mathcal{F}^{\Lambda_\Sigma} \models \Sigma \iff \mathcal{F}^{\Lambda_\Sigma} \in \mathbb{F}_\Sigmaであるので，$ \mathcal{F}^{\Lambda_\Sigma} \models \Sigmaを示す．
フレームクラスの定義より．
7. Lem 1.3.14, Lem 1.3.15より$ \mathcal{F}^{\Lambda_\Sigma} \models \Sigmaは示される．❏．