"A simplified embedding of E into K", Rohan French

ちょっと前に読んだ論文で、様相論理 E から K への変換の話。

E は congruence

$A \leftrightarrow B \Longleftrightarrow \picture(11,13){\put(0,3){\line(0,10){10}} \put(0,2){\line(10,0){10}} \put(1,12){\line(10,0){10}} \put(10,2){\line(0,10){10}}} A \leftrightarrow \picture(11,13){\put(0,3){\line(0,10){10}} \put(0,2){\line(10,0){10}} \put(1,12){\line(10,0){10}} \put(10,2){\line(0,10){10}}} B$

を満たす最小の様相論理。K は normality

$\picture(11,13){\put(0,3){\line(0,10){10}} \put(0,2){\line(10,0){10}} \put(1,12){\line(10,0){10}} \put(10,2){\line(0,10){10}}}(A \rightarrow B) \rightarrow \picture(11,13){\put(0,3){\line(0,10){10}} \put(0,2){\line(10,0){10}} \put(1,12){\line(10,0){10}} \put(10,2){\line(0,10){10}}} A \rightarrow \picture(11,13){\put(0,3){\line(0,10){10}} \put(0,2){\line(10,0){10}} \put(1,12){\line(10,0){10}} \put(10,2){\line(0,10){10}}} B$

を満たす最小の様相論理。

で E から bimodal K (K2) への埋め込みは存在が知られていた。また K2 から monomodal K への埋め込みも知られていた。それらを合わせれば E から monomodal K への埋め込みが作れるのだが、この変換よりも簡単なものがあるということで、それを示している論文。

結論を書くと、新しい様相を

$\picture(11,13){\put(0,3){\line(0,10){10}} \put(0,2){\line(10,0){10}} \put(1,12){\line(10,0){10}} \put(10,2){\line(0,10){10}}}' A = \diamond (\diamond(\picture(11,13){\put(0,3){\line(0,10){10}} \put(0,2){\line(10,0){10}} \put(1,12){\line(10,0){10}} \put(10,2){\line(0,10){10}}} A \wedge \picture(11,13){\put(0,3){\line(0,10){10}} \put(0,2){\line(10,0){10}} \put(1,12){\line(10,0){10}} \put(10,2){\line(0,10){10}}} \picture(11,13){\put(0,3){\line(0,10){10}} \put(0,2){\line(10,0){10}} \put(1,12){\line(10,0){10}} \put(10,2){\line(0,10){10}}} \diamond \top) \wedge \diamond(\diamond \neg A \wedge \picture(11,13){\put(0,3){\line(0,10){10}} \put(0,2){\line(10,0){10}} \put(1,12){\line(10,0){10}} \put(10,2){\line(0,10){10}}} \picture(11,13){\put(0,3){\line(0,10){10}} \put(0,2){\line(10,0){10}} \put(1,12){\line(10,0){10}} \put(10,2){\line(0,10){10}}} \diamond \top) \wedge \diamond \diamond \picture(11,13){\put(0,3){\line(0,10){10}} \put(0,2){\line(10,0){10}} \put(1,12){\line(10,0){10}} \put(10,2){\line(0,10){10}}} \top)$

で定義すると E の様相に対応する monomodal K での様相ができるらしい。

証明は、たぶん neighborhood frame を Kripke frame で模倣してるんだと思う。E は (non-empty) neighborhood frame 全体のクラスに対応することを使う。

簡単になったといってもずいぶん複雑に見えるが、基本的なアイデアは元になっている K3 (trimodal K) への埋め込み

$(\picture(11,13){\put(0,3){\line(0,10){10}} \put(0,2){\line(10,0){10}} \put(1,12){\line(10,0){10}} \put(10,2){\line(0,10){10}}} A)^F = \diamond_1 (\picture(11,13){\put(0,3){\line(0,10){10}} \put(0,2){\line(10,0){10}} \put(1,12){\line(10,0){10}} \put(10,2){\line(0,10){10}}}_2 A^F \wedge \picture(11,13){\put(0,3){\line(0,10){10}} \put(0,2){\line(10,0){10}} \put(1,12){\line(10,0){10}} \put(10,2){\line(0,10){10}}}_3 \neg A^F)$

と同じであるように思える。これは neighborhood frame での必然様相の解釈

ある neighborhood があって
その中では A が成り立ち
その外では A が成り立たない

に対応しているそうだ。言われてみれば確かにきれいに対応しそう。

bimodal への埋め込みは、実は上の埋め込みの定義で 1 と 2 の様相が同じものとしてもよいという事実の帰結らしい。

細かいところまでは追いかける気にならず。