直観主義論理で二重否定除去は一般に成り立たない

古典論理では二重否定除去はトートロジーだが、直観主義論理では一般に成り立たない

ただし、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は真でも偽でも無いということがわかったということmrsekut.icon

$ 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は成り立たないので