First-order Modal Logic, Section 10. Mathematical models for modalities

このあたりから数学的にハードに感じるようになってきました。基礎体力が足りませんね。しかしここで頑張らなければいつまで経っても成長しないことがこれまでの幾多の経験から実証されているので頑張る。

10.1 Geometric morphisms and modal logic

とりあえず証明はある程度自分で補いながら読み進めましたが、まだあまり身についてる感じがありません。

普通の Kripke semantics をこの章に出てくる言葉を使って自分で再構成してみると理解の助けになるのではないかと思います (が、まだやってません)。

elementary toposes

圏 E が elementary topos とは、E が subobject classifier をもつ lex CCC であること。この E 上には subobject functor により hyperdoctrine の構造が入る。これにより、(直観主義の)一階述語論理のモデルを E 上に考えることができる。

問題は、様相をどう入れるか。この章では geometric morphism による方法を紹介しています。

geometric morphisms

geometric morphism $(F_*, F^*) : E_1 {\;\rightarrow\;} E_2$ は、次のようなデータからなる。

a functor $F_* : E_1 {\;\rightarrow\;} E_2$
a lex functor $F^* : E_2 {\;\rightarrow\;} E_1$
adjunction $F^* \dashv F_*$

前層や層の引き戻しはこの条件を満たすので geometric morphism になる。

余談ですが、引き戻しには右随伴と左随伴が両方とも存在して、その構成法を YouTube で見たことがあるような気がします。どれだったか思い出せませんが TheCatsters の動画のどこかにあったと思います。

modality from geometric morphisms

$(F_*, F^*) : E_1 {\;\rightarrow\;} E_2$ が geometric morphism のとき、様相を次のようにして入れると $E_2 \ni D \mapsto Sub(F^* D) \in Int^{op}$ が modal hyperdoctrine になる。

subobject $A {\;\rightarrow\;} F^* D$ が与えられたとき、これを使ってできる diagram $F_* A {\;\rightarrow\;} F_* F^* D {\;\leftarrow\;} D$ (右側は adjoint の unit) から pullback $F_* A {\;\leftarrow\;} \flat A {\;\rightarrow\;} D$ を作る。 $A {\;\rightarrow\;} F^* D$ が mono で $F_*$ が右随伴であることから $\flat A$ は D の subobject となる。さらに left exactness から $F^* \flat A {\;\rightarrow\;} F^* D$ も mono である。このとき ${\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^* \flat A$ と定義する。

この様相は S4 necessity となる。その証明は「定義を展開すればできるよ」とだけ書いてありますが、慣れていないせいか、わりと大変でした。