Boxdot特性
References
貰った資料を参考にしている
Def
標準的な言語における正規様相論理に対して，boxdot変換$ \cdot^bを$ (\Box\varphi)^b \equiv \boxdot \varphi \equiv \varphi \land \Box \varphiと定める．（その他は構造を保存する） 直感的に言えば，全ての$ \Boxを$ \boxdotに置き換えたものとすれば良い．
正規様相論理$ \Lambdaに対して，$ \Lambda^{-b} := \{ \varphi \mid \vdash_\Lambda \varphi^b \}と定める．
Prop 1
1. $ \vdash_\mathbf{K} \boxdot(A \to B) \to (\boxdot A \to \boxdot B)
2. $ \vdash_\mathbf{K} \boxdot A \to A
3. $ \vdash_\Lambda A \implies \vdash_\Lambda \boxdot A
Prop 2
$ \Lambda^{-b}は正規様相論理かつ，特に$ \mathbf{KT} \sube \Lambda^{-b}
proof
古典命題論理のトートロジー
$ \Boxを含まない論理式$ \varphiに対して$ \varphi^b \equiv \varphiだからOK
$ \vdash_{\Lambda^{-b}} A \to Bかつ$ \vdash_{\Lambda^{-b} } Aだったとして$ \vdash_{\Lambda^b} Bを示す．
このとき
$ \vdash_\Lambda (A \to B)^bすなわち$ \vdash_\Lambda A^b \to B^b
$ \vdash_\Lambda A^b
より直ちに$ \vdash_\Lambda B^bが成り立つので$ \vdash_{\Lambda^{-b}} B．OK
$ \vdash_{\Lambda^{-b}} Aだったとして$ \vdash_{\Lambda^{-b}} \Box Aを示す．
$ \vdash_{\Lambda} A^bだからProp1.3より$ \vdash_\Lambda \boxdot A^b．
括って$ \vdash_\Lambda (\Box A)^b．よって$ \vdash_{\Lambda^{-b}} \boxdot A．OK
$ (\Box (A \to B) \to (\Box A \to \Box B))^b \equiv \boxdot(A \to B) \to (\boxdot A \to \boxdot B)．
Prop1.1より後者は$ \bf Kで証明可能だからOK．
同様に，Prop1.3よりOK．
Prop 3
$ \vdash_\mathbf{KT} A \leftrightarrow A^b
proof論理式に関する帰納法
Cor 4
$ \Lambda \sube \mathbf{KT}とすると$ \Lambda^{-b} = \mathbf{KT}．
proof
$ \Lambda \sube \mathbf{KT}とする
$ \vdash_{\Lambda^{-b}} \varphi \implies \vdash_\mathbf{KT} \varphi
$ \vdash_{\Lambda^{-b}} \varphiとする．
$ \vdash_\Lambda \varphi^b
論理の強さより$ \vdash_\mathbf{KT} \varphi^bでProp 3より$ \vdash_\mathbf{KT} \varphi．OK
$ \vdash_\mathbf{KT} \varphi \implies \vdash_{\Lambda^{-b}} \varphi
Prop2より直ちに明らか
何らかの性質を満たす任意の$ \Lambdaに対し，$ \Lambda^{-b} = \mathbf{KT} \iff \Lambda \sube \mathbf{KT}
Fact.1
次数1以下の公理による$ \bf K拡張$ \Lambdaに対して$ \Lambda^{-b} = \mathbf{KT} \iff \Lambda \sube \mathbf{KT}
references
Fact.2
Geach論理$ \Lambdaに対して$ \Lambda^{-b} = \mathbf{KT} \iff \Lambda \sube \mathbf{KT} references
Prop 5
$ \mathbf{KT} \sub \Lambda \implies \Lambda^{-b} \neq \mathbf{KT}
proof
$ \mathbf{KT} \sub \Lambdaなら$ \vdash_\Lambda Aかつ$ \nvdash_\mathbf{KT} Aな$ Aが存在する．
今$ \mathbf{KT} \sube \Lambdaではあるので，Prop3より$ \vdash_\Lambda A^bが言えるので，$ \vdash_{\Lambda^{-b}} Aとなる．よって$ \Lambda^{-b} \neq \mathbf{KT}．
Def
$ \mathbf{KT} \sube \Lambdaとする．$ \Lambda_0 := \{ \varphi^b \mid \Lambda \vdash \varphi \}と定める．
Prop 6
$ \mathbf{KT} \sube \Lambdaなら$ \Lambda_0 \sube \Lambda．
proof
$ \vdash_\Lambda AならProp3より$ \vdash_\Lambda A^bであるので．
$ \mathbf{KT} \sube \Lambdaとする．$ \Lambdaがboxdot特性を持つとは， 任意の$ \Xiに対し，$ \Xi^{-b} = \Lambda \implies \Xi \sube \Lambdaとなることとする．
remark
$ \Lambda = \mathbf{KT}のとき，これはBoxdot予想そのものである．（しかも従来のFact,1/Fact2より強い：任意の$ \Xiだから） Main Thm.1
references