直観主義論理の¬
$ \lnotの定義
$ \lnot\varphi:=\varphi\to\bot
到達可能なすべての世界で成り立たなければ、$ \lnot\varphiが成り立つ
$ wRw'を満たす任意の$ w'\in Wに対して、
$ S,w'\models \varphiが成り立たいない時、また、その時に限り
$ S,w\models\lnot\varphiが成り立つ
「$ \lnot Pが真である」というのは
「$ Pが偽であることが証明されている」という意味であって、
「$ Pが真ではない」だけでは不十分
ということに注意が必要