直観主義論理で二重否定除去は一般に成り立たない
ただし、maximal worldsでは成り立つ
以下のような構造を考える
W=\{0,1\}
R = \{(0,1),(0,0),(1,1)\}
V(0,P)=\bot
V(1,P)=\top
この時、二重否定除去S,0\models \lnot\lnot P \to Pが成り立たないことを見る
まず、S,0\models PとS,1\models\lnot Pは成り立たない
∵ V(0,P)=\bot
∵ V(1,P)=\top
また、S,0\models\lnot Pは成り立たない
∵ V(1,P)=\topかつ0R1
↑この時点で、世界0ではPは真でも偽でも無いということがわかったということ
S,0\models\lnot\lnot Pが成り立つ
∵ S,0\models\lnot Pが成り立たないので
さらにS,1\models\lnot Pも成り立たないので
従って、S,0\models\lnot\lnot P\to Pは成り立たない
∵ S,0\models\lnot\lnot Pが成り立ち、S,0\models Pは成り立たないので