First-order Modal Logic, Section 11. Counterpart models

細かいところはだんだん書くのが面倒になってきたので気になった部分だけ informal に。

わりと技術的なところからくる動機づけがあって、実はそれが counterpart theory という古くから考えられてきた話と関係がありそうだという展開。*1

代入の問題

前節でみたように、bundle model のようなモデルを考えると

$f^{-1} \circ {\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}}} } = {\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}}} } \circ f^{-1}$

が必ずしも成立しない。しかし syntax の側でこれに対応するのは代入の定義

$({\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}}} } \phi)[t/x] = {\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}}} }(\phi[t/x])$

なので、まず構文をいじらなければ bundle model の振る舞いを論理としてとらえることはできない。

構文をいじる

$({\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}}} } \phi)[t/x]$ と ${\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}}} }(\phi[t/x])$ を区別するために様相の構文を変えて、様相には $({\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}}} } \phi) (t_1, \dots, t_k)$ のように必ず引数が付くようにする。引数の個数は φ の中に現れる自由変数の個数。正確には φ が k-formula のとき k 個の引数をつけ、それらの引数が n-term なら全体は n-formula になる。

その結果

$({\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}}} } \phi)[t/x] = ({\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}}} } \phi)(t) \neq {\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}}} }(\phi[t/x])$

となるので目的が達成されるという話。

意味論の作り方

もちろん、構文的に違うものになったからといってそれだけで終わりではなく。異なっているであろう右の二つの式が本当に違う意味に解釈されなければ、結局二つを区別したことにはならないでしょう。

直感的にはどうするかというと。箱が付いてるので遷移先を任意にとってきてそっちで φ を解釈するのですが、変数 x の解釈のしかたが違います。

$({\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}}} } \phi) (t)$ のほうは、まず今の世界 w での t の解釈 $\llbracket t \rrbracket_w$ をとって、x は遷移先での $\llbracket t \rrbracket_w$ の(任意の)対応物で解釈。

一方で ${\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}}} }(\phi[t/x])$ のときには、まず遷移先 v を任意に与えて、その先での t の解釈 $\llbracket t \rrbracket_v$ として x を解釈する。

すると両者は必ずしも一致しないので、区別可能ですよ、という話。

「遷移先での対応物」という言葉を何の説明もなしに使いましたが、これがこの節のタイトルに入っている counterpart と呼ばれるものです。一般には counterpart は複数あったり一つもなかったりすることが許されています。

*1:counterpart theory が何物なのかは知りません