"Topological duality for intuitionistic modal algebras"

B. P. Hilken の論文。見た*1のでメモ。

概要

二項関係の入った位相空間 (relational spaces) と、様相演算子 □, ◇ の入った frame (modal frame) *2 の間の双対性についての論文。

要するに Stone duality の直観主義様相論理版を考えましょうということ。直観主義様相論理にはいろいろなバージョンがありうるが、この論文で扱われているものは比較的弱い論理になっている。特に ◇ が disjunction (join) を保存しない (bottom は保存する)。

section 2 前半

最初に気になったのが、morphism の定義が普通と違うところ。

relational space の p-morphism の back-condition で、合流する先はぴったり一致していなくても modally indistinguishable (二点の近傍系が一致する) ならよいことになっています。

それに対応して(?)、modal frame morphism は □, ◇ を完全に保存する必要がなくて、様相を後に施したほうが大きくなっていてもよいということになっています。

この条件、どういうことなのか最初はよくわかりませんでしたが、そういえば birelational Kripke semantics でも似たような事情があることをいま思い出しました。p-morphism は homomorphism を導きますが、homomorphism を導くものが p-morphism だとは限らないのです。そのあたりの事情と関係があるのでしょう。

ここをうまく対応させる条件としてあまり自然なものを知らなかったのですが、この論文の定義が一つの答えを与えているのかもしれません。ただ、論理の意味論とみたときにこういう morphism が自然なのかどうかよくわからないのですが。

section 2 後半

duality を与えるところで面白そうだったのが、modal frame から relational space を作るやり方。普通は point *3 の全体を考えて Spec(X) を定義するとうまくいくのですが、様相が入ると point だけでは関係の部分が復元できなくなります。そこで point に何らかの情報を追加する必要があり、そのために "the set of unrelated points" (形式的には frame の適当な条件を満たす元) を使っています。

birelational semantics でも ◇ が入ると prime theory だけでは完全性がうまくいえないのですが、それを解決するために "negative information" を追加するというアイデアが考えられています。おそらく "unrelated points" も本質的には同じようなことをやっているのではないかと思います。

section 3

残りの部分は直観主義様相論理の完全性で、普通の直観主義論理の場合のアナロジーだと書いてあるのですが、元になった話をよく知らないのでどうしたものか。

途中で集中力が切れたので、今日はここまで。

*1:話の流れには目を通したつもりだけど、技術的な詳細は全くフォローできていないので「読んだ」とは怖くて言えないの意

*2:ここでの "frame" は Kripke frame ではなく complete Heyting algebra のこと

*3:{0, 1} への frame-homomorphism