様相論理の強さ分析
Def
言語$ \mathscr{L}_\Box上の論理$ \Lambda_1,\Lambda_2とその証明体系$ \vdashとする.
任意の論理式$ \varphiで$ \vdash_{\Lambda_1} \varphi \implies \vdash_{\Lambda_2} \varphiであることを$ \Lambda_1 \leq \Lambda_2と書くことにする.
$ \Lambda_1 \leq \Lambda_2かつ$ \Lambda_1 \not\leq \Lambda_2であることを$ \Lambda_1 < \Lambda_2と書く.
すなわち$ \vdash_{\Lambda_2} \varphiで$ \nvdash_{\Lambda_1} \varphiな$ \varphiが存在することとする.
$ \Lambda_1 \leq \Lambda_2かつ$ \Lambda_2 \leq \Lambda_1であることを$ \Lambda_1 = \Lambda_2と書く.
Remark
当たり前だが,論理$ \Lambda_1,\Lambda_2を公理集合$ \Sigma_1,\Sigma_2(または公理図式としても良いが)によって特徴づけるのなら自明に$ \Sigma_1 \sube \Sigma_2 \implies \Lambda_1 \leq \Lambda_2である.
例えば$ \bf K \cup T \sube K \cup T \cup 4だから,$ \bf KT \leq KT4である.(すなわち$ \bf KT \leq S4)
重要なのは$ \Sigma_1 \not\sube \Sigma_2などのケースで,$ \bf K \cup Dと$ \bf K \cup Tは集合としては比較不能だが,実際には$ \bf KD \leq KTが成り立つ.
これは$ \vdash_\mathbf{KT} \Box \varphi \to \Diamond \varphiを示せば良い.
のだが,この証明が統語論的に面倒という問題もある.
健全性/完全性を使って$ \mathbb{F}(\Lambda_1) \sube \mathbb{F}(\Lambda_2) \implies \Lambda_1 \leq \Lambda_2.
更にフレーム定義性$ F \in \mathbb{F}(\Lambda) \iff P_\Lambda(F)が存在するなら $ P_\Lambdaは$ P_\Lambdaはフレームの性質:推移律など $ \lbrack P_{\Lambda_2}(F) \implies P_{\Lambda_1}(F) \rbrack \implies \Lambda_1 \leq \Lambda_2
今後論理は完全性と健全性を適当に満たすものとする.