neighborhood sheaf semantics 補足 - 論理とか計算機とか数学とか

http://lkozima.hatenablog.com/entries/2013/09/30

細かい計算をまったく追いかけてないので MC より弱いところではなんでできないのかよくわかってない。

のところ，計算してみたらわかった気がした。たぶん $\exists x \varphi \to \varphi[t/x]$ の健全性のところで使うのではないかと。

もうちょっと詳しく言うと，その証明の途中で $\varphi$ に様相が含まれているときに，代入と様相の順番を入れ換えたくなるので，それができることを保証するのに MC を使うのだと思う。

t を n 変数の term として $\sigma : D^{n+1} \ni \bar a \mapsto (\bar a, \llbracket t\rrbracket (a)) \in D^n$ を考えると

$\mathrm{int} (\sigma^{-1} (A)) = \sigma^{-1} (\mathrm{int}(A))$

となってほしくて，そのためにはすべての $\bar a \in D^n$ について

$\sigma^{-1}(A) \in \mathcal N(\bar a) \Longleftrightarrow A \in \mathcal N(\sigma(\bar a))$

がいえることが必要十分。で，MC があるとこれはたぶんすぐにいえて，なぜなら σ は local iso だから適当な近傍 B をとってやれば B 上で全単射としてよい。公理 C があるから A∩B も近傍で，そうすると A のかわりに A∩B として上の同値が成り立って，M があるからそれより大きい A も近傍になる。

気がする。たぶん。