normality of diamond in birelational semantics

興味のある人は滅多にいないでしょうが、真面目に調べたので自分用にメモ。

直観主義様相論理の birelational Kripke semantics では ◇ の解釈のしかたに何通りかのバリエーションがあります。これまでに見たことがあってすぐに思い出せるのは

$w, V {\hspace{1}||\hspace{-5}-\hspace{1}} \diamond A {\;\Longleftrightarrow\;} \forall w' \geq w. \exists v \in R[w']. v, V {\hspace{1}||\hspace{-5}-\hspace{1}} A$
$w, V {\hspace{1}||\hspace{-5}-\hspace{1}} \diamond A {\;\Longleftrightarrow\;} \exists v \in R[w]. v, V {\hspace{1}||\hspace{-5}-\hspace{1}} A$
$w, V {\hspace{1}||\hspace{-5}-\hspace{1}} \diamond A {\;\Longleftrightarrow\;} \forall w' \leq w. \exists v \in R[w']. v, V {\hspace{1}||\hspace{-5}-\hspace{1}} A$

の三つ。下の二つは必ず $\diamond(p \vee q) \rightarrow \diamond p \vee \diamond q$ が成立しますが、一番上のだとそうとは限りません。

じゃあどういう条件で成り立つかということで、半時間ぐらい計算してみたら必要十分条件が出てきました。次の二つが同値。

$w {\hspace{1}||\hspace{-5}-\hspace{1}} \diamond(p \vee q) \rightarrow \diamond p \vee \diamond q$
- where $X \downarrow = \{ y | \exists x \in X. y \leq x\}$

ただし ${\hspace{1}||\hspace{-5}-\hspace{1}}$ と書いたのは、付値をどのようにとっても真になる (locally valid) ということ。

上から下

結論が成り立たないとして、その反例 $w \leq w' \leq w_1, w_2$ を考える。

$x, V {\hspace{1}||\hspace{-5}-\hspace{1}} p {\;\Longleftrightarrow\;} x \notin R[w_1]\downarrow$
$x, V {\hspace{1}||\hspace{-5}-\hspace{1}} q {\;\Longleftrightarrow\;} x \notin R[w_2]\downarrow$

となるように付値 V をとることができる。そのような V について

$w', V {\hspace{1}||\hspace{-5}-\hspace{1}} \diamond(p \vee q)$
$w', V \not {\hspace{1}||\hspace{-5}-\hspace{1}} \diamond p \vee \diamond q$

となる。

下から上

$w' \geq w$ とする。

$w', V \not {\hspace{1}||\hspace{-5}-\hspace{1}} \diamond p \vee \diamond q$ だとすると、適当に $w_1, w_2 \geq w$ をとって $w_1 \cap V(p) = w_2 \cap V(q) = \emptyset$ となるようにできる。

このとき仮定から $w'' \geq w$ を $R[w''] \subseteq R[w_1]\downarrow \cap R[w_2]\downarrow$ となるようにとれて、そのとき $w'' \not {\hspace{1}||\hspace{-5}-\hspace{1}} \diamond (p \vee q)$ である。したがって $w' \not {\hspace{1}||\hspace{-5}-\hspace{1}} \diamond (p \vee q)$ となる。