First-order Modal Logic, Section 8. Completeness, incompleteness, and non-axiomatizability

間がちょっと飛んで part 2 の途中、Section 8 から。Section 5 は参考文献リストがメインだし 6 は Part 2 への導入なので飛ばしたのは 7 だけですが。

この節は first-order modal logic の Kripke-completeness について……なのですが、どうやら constant domain semantics で Kripke-complete になるやつはあまりないようです。何が効いてそういう結果になるんだろう。

面白そうだったのが van Bethem の functional frame 。可能世界を index にした domain の族 D_w を考えて、到達可能関係の代わりに domain の間の写像の族をとるというもの。別の言葉でいうと、普通の Kripke frame がグラフであるのに対して functional frame は集合の圏の部分グラフです (実際には S4 を含む論理に対する意味論を考えて small subcategory になっているようです)。

で、w で □を解釈するときには assignment の後ろに任意にとってきた を合成して v で解釈することになります。高階論理の topos semantics に似てるような気がします*1。

より強力な意味論として presheaf を用いたものがあとの章で出てくるようです。少し覗いてみたところ、S4 の拡張しか扱っていないように見えます。Kripke frame を圏に変えて presheaf へ拡張するとそうなるのでしょうが、identity と composition がないとうまくいかないんでしょうか。圏の代わりにグラフを使えばいいような気がしないでもありませんが。個人的には S4 だけでなく K ぐらいまでできてほしいので、後の節を読むときにはそのあたりも意識してみたいと思います。

*1:うろ覚えなので曖昧な言い方をする