S, w\models A

クリプキ構造S、世界w\in Wの元で、論理式Aが成り立つ

Aが\Boxを含まなければ、通常の命題論理と同じ

各世界の真偽は独立に成り立つ

Aが必然性演算子▢を含むと、世界間の真偽が絡み合うことになる

\Box Aが、wで真になるためには、

wから到達できる任意の世界w'で、Aが真になるということ

つまり、以下2つは同値

S,w\models\Box A

wRw'を満たす任意のw'\in Wに対してS,w'\models A

w\models Aのように書いた場合、以下のように場合分けができる

①wから到達可能な世界w'が0個である

②wから到達可能な世界w'が1個以上ある

②-1 全ての世界w'でw\models Aが成り立つ

②-2 全てではないが1つ以上の世界w'でw\models Aが成り立つ

②-3 どの世界w'でもw\models Aは成り立たない

↑のように場合分けした時、

w\models \square Aが成り立つのは、①と②-1

w\models \Diamond Aが成り立つのは、②-1と②-2

①は成り立たない、なぜなら

到達可能な世界が0個のとき、

w\models \square Aが成り立つ

この時、w\models \square \lnot Aも成り立つ

従って、w\models \lnot\square\lnot Aは成り立たない

\Diamond A:= \lnot\Box\lnot Aなので、①は成り立たない

ということは、∃x. Pxは、∀x. Pxを含意するのイメージは成り立たないのか

そもそもイメージで、\forall,\existと\square,\Diamondは全く別物なので、そらそうだろと言われればそうなのだが