First-order Modal Logic, Section 9. Towards more powerful semantics

少し時間ができたので "Handbook of Modal Logic" 再開。

9.1 は言葉の準備。なんか de Bruijn level っぽい表記を導入している様子。で自由変数が高々 n 個の term/formula を n-term/n-formula と呼ぶ、と。簡単に言ってしまうとそれだけのことのような。

9.2 Cartesian and lex categories

技術的には以下の三つの定義が並んでるだけみたいな印象。

finite product をもつ圏を cartesian category という
finite limit をもつ圏を lex category という
subobject functor Sub
- on objects: Sub(A) = A の subobjects の同型類全体
- on arrows: Sub(f) = pullback

それ以外で目に付いたのは、言葉を適切に選ぶことで諸々の概念の定義の見通しがよくなるということ。 $x : U \rightarrow X$ を U-element of X ということにすると、例えば射 $f : X \rightarrow Y$ が単射であるのは $f(x)=f(y) \;\Longrightarrow\; x = y$ が任意の U-element x, y について成り立つこと、となります (ただし $f(x) = f \circ x$ )。これは普通の写像の単射性と同じ形をしています。直積の定義も集合の直積と同じように書けたりして、技術的には新しいことではないけど面白いと思いました。

9.3 Hyperdoctrine

実はこれまでに何度か勉強しようとして結局理解してない hyperdoctrine がここで登場。やっぱり掴みどころがない感じでよくわからない。

後できちんとまとめるかも。

9.4 Metaframes

なんか最初に preordered set の open map とか定義されてて "f is open iff f is monotone and $f(x) = y \;\Longrightarrow\; \exists x' \geq x, y = f(x')$ " みたいなことが書いてあるんですけど、それって p-morphism のことなんじゃないのかなあとか思ったりしました。

その次に、順序集合 X に対してその冪集合の上に interior algebra の構造をかくかくしかじかの方法で入れるとか書いてあって、それって complex algebra じゃなかったっけとか思いました。

そういえば、もしかしたらこの章ではそういう言葉が出てきてなかったから self-contained にするためにきっちり書いてあったのかもしれません。

で T を cartesian category とするとき T-metaframe というのは functor M : T -> F (F は frame の圏、本文では S4 に限定しているので preordered set の圏) であって、complex algebra functor との合成が hyperdoctrine になっているもののこと。

で、これくらい広い枠組の中でモデルを考えると完全性が証明できるのだそうです。