件の二つの公理を分離する話

やったからといって特に何があるわけでもないけど、気になるので重箱の隅に残ったごはん粒をつつくお仕事。

問題

直観主義様相論理の Kripke semantics では、定式化によっては次の公理が必ずしも真になりません。

$A_1 = \Diamond (p \vee q) \supset (\Diamond p \vee \Diamond q)$
$A_2 = (\Diamond p \supset {\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}}} } q) \supset {\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}}} } (p \supset q)$

で、この二つの公理のうち一方だけが真になる birelational なモデルがあるかという問題。そんなに自明じゃありません。

これが、前からことあるごとに思い出して気になってました。

settings

モデルのクラスを決めないと話が始まらないのでとりあえず定義を並べます。だいたい普通なので、こんな記事を真面目に読もうとするような人なら最後の解釈の定義だけ見れば済むかもしれません。

birelational frame とは、集合、その上の二項関係、その上の順序の三つ組み $\langle W, R, \leq \rangle$ のことをいう。W の要素を世界という。また R を modal accessibility といい ≦ を intuitionistic accessibility という。ここでは、両者のとり方には何も制約を課さないものとする。

birelational frame $F = \langle W, R, \leq \rangle$ が与えられたとき、その admissible set とは W の部分集合であって ≦ に関して upward-closed なもののことである。admissible set 全体を $A_F$ と書く。

F 上の付値とは、あらかじめ固定された命題変数の集合から admissible set の集合への写像 $V : PV {\;\rightarrow\;} A_F$ のことである。

論理式の satisfaction relation $F, w, V {\picture(20,18){\put(4,0){\line(0,18){18}} \put(4,7){\line(12,0){12}} \put(4,11){\line(12,0){12}}} A$ を次のように定義する。

$F, w, V {\picture(20,18){\put(4,0){\line(0,18){18}} \put(4,7){\line(12,0){12}} \put(4,11){\line(12,0){12}}} A \supset B {\;\Longleftrightarrow\;} \forall w' \geq w, (F, w', V {\picture(20,18){\put(4,0){\line(0,18){18}} \put(4,7){\line(12,0){12}} \put(4,11){\line(12,0){12}}} A {\;\Longrightarrow\;} F, w' V {\picture(20,18){\put(4,0){\line(0,18){18}} \put(4,7){\line(12,0){12}} \put(4,11){\line(12,0){12}}} B)$
$F, w, V {\picture(20,18){\put(4,0){\line(0,18){18}} \put(4,7){\line(12,0){12}} \put(4,11){\line(12,0){12}}} {\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 {\;\Longleftrightarrow\;} \forall w' \geq w, \forall v \in R[w'], F, v, V {\picture(20,18){\put(4,0){\line(0,18){18}} \put(4,7){\line(12,0){12}} \put(4,11){\line(12,0){12}}} A$
$F, w, V {\picture(20,18){\put(4,0){\line(0,18){18}} \put(4,7){\line(12,0){12}} \put(4,11){\line(12,0){12}}} \Diamond A {\;\Longleftrightarrow\;} \forall w' \geq w, \exists v \in R[w'], F, v, V {\picture(20,18){\put(4,0){\line(0,18){18}} \put(4,7){\line(12,0){12}} \put(4,11){\line(12,0){12}}} A$

要するに古典と同じような演算をしたあと upward closure をとって辻褄を合わせなさいということですね。

それで、上述の二つの公理を global validity の意味で分離する例を作りました。つまり一方が任意の世界と付値で真 (globally valid ) だがもう一方は適当な付値を与えればある世界で偽になる、という例を作りました。

A1 を満たすが A2 を満たさない例

図を描いたほうがわかりやすいけど面倒なので集合で書き下しますごめんなさい。

$W = \{ a, b, c \}$
$a R c$
$a \leq b$ (で生成される順序)

とする。

A1 を満たす

a で ◇(何か) の形の論理式はどうやっても成り立たないから明らか。

A2 を満たさない

$V(p) = \{ c \}, V(q) = \emptyset$ とすれば a で不成立。

A1 を満たさないが A2 を満たす例

$W = \{ a, a_1, a_2, b, c \}$
$a R b, a_1 R b, a_2 R c$
$a \leq a_1, a \leq a_2$ (で生成される順序)

A1 を満たさない

$V(p) = \{ b \}, V(q) = \{ c \}$ とすれば a で不成立。

A2 を満たす

a 以外からは intuitionistic accessibility で行ける世界が自分自身しかないので、そこでの validity は古典と同じになるから成り立つ。

a で A2 が成り立つことを確かめるには $F, a, V {\picture(20,18){\put(4,0){\line(0,18){18}} \put(4,7){\line(12,0){12}} \put(4,11){\line(12,0){12}}} \Diamond p \supset {\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}}} } q$ を仮定して

$F, b, V {\picture(20,18){\put(4,0){\line(0,18){18}} \put(4,7){\line(12,0){12}} \put(4,11){\line(12,0){12}}} p {\;\Longrightarrow\;} F, b, V {\picture(20,18){\put(4,0){\line(0,18){18}} \put(4,7){\line(12,0){12}} \put(4,11){\line(12,0){12}}} q$
$F, c, V {\picture(20,18){\put(4,0){\line(0,18){18}} \put(4,7){\line(12,0){12}} \put(4,11){\line(12,0){12}}} p {\;\Longrightarrow\;} F, b, V {\picture(20,18){\put(4,0){\line(0,18){18}} \put(4,7){\line(12,0){12}} \put(4,11){\line(12,0){12}}} q$

をいえばよい。これはそれぞれ

$F, b, V {\picture(20,18){\put(4,0){\line(0,18){18}} \put(4,7){\line(12,0){12}} \put(4,11){\line(12,0){12}}} p {\;\Longrightarrow\;} F, a_1, V {\picture(20,18){\put(4,0){\line(0,18){18}} \put(4,7){\line(12,0){12}} \put(4,11){\line(12,0){12}}} \Diamond p$
$F, c, V {\picture(20,18){\put(4,0){\line(0,18){18}} \put(4,7){\line(12,0){12}} \put(4,11){\line(12,0){12}}} p {\;\Longrightarrow\;} F, a_2, V {\picture(20,18){\put(4,0){\line(0,18){18}} \put(4,7){\line(12,0){12}} \put(4,11){\line(12,0){12}}} \Diamond p$

から出る。