from 命題直観主義論理

\lnotの定義

\lnot\varphi:=\varphi\to\bot

ref 直観主義論理の→

到達可能なすべての世界で成り立たなければ、\lnot\varphiが成り立つ

上記の定義を直観主義論理の→の解釈で読み替えると、

wRw'を満たす任意のw'\in Wに対して、

S,w'\models \varphiが成り立たいない時、また、その時に限り

S,w\models\lnot\varphiが成り立つ

「\lnot Pが真である」というのは

「Pが偽であることが証明されている」という意味であって、

「Pが真ではない」だけでは不十分

ということに注意が必要

ref 直観主義論理では排中律は一般に成り立たない