一階述語様相論理の sheaf semantics とか

ひさしぶりに様相論理の論文を読みました。なんとなくまとめ。

最初のは first-order S4 の意味論を sheaf を使って与えるという内容。関数記号とか定数記号とかをどう解釈するかはこれまであんまり考えられてなかったらしい。sheaf だったら関数記号は sheaf の射だし定数記号は global section ということで自然に決まる。あと完全性の証明,詳細は書いてなかったけど力技でモデルを作るらしい。Löwenheim-Skolem の定理を使うとか書いてあった。

次のは first-order MC (K から necessitation を除いたもの) の意味論。Kripke sheaf と topological sheaf (普通の意味での集合の層) を統合する形で neighborhood sheaf というものを定義して,その上での意味論 (neighborhood sheaf semantics, NSS) を与える。細かい計算をまったく追いかけてないので MC より弱いところではなんでできないのかよくわかってない。

最後のは NSS を使って first-order public announcement logic の意味論も作ったよという話で,これは NSS の定義ができていればそんなに難しくなさそうに見えるけどどうなのだろう。

どれも sheaf を使っているのだけど,なんで sheaf でないといけないかというとたぶん,ある世界 w に個体 a があったとして,世界 v が w から到達可能なとき v において a に対応する個体 b が一意に定まってほしい,ということなのだと思う。それがうまく定まるということが locally isomorphic という条件で表されているように見える。

こういう意味論だと,世界が変わったときに存在していたものが存在しなくなったり二つに分裂したりすることはない(NSS では「近傍を適切に選べば」という前提付きになる,のかな)。昔そういうことの起きる意味論である counterpart semantics を少し触ったことがあるのだけど,あれは理論的に扱いづらい印象があった。とにかく話がきれいにならない。sheaf であればそれよりは大人しいので扱いやすくて公理化もできるのだろう。