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

古典論理では排中律はトートロジーだが、直観主義論理では一般に成り立たない

従って、背理法を認めない

ただし、maximal worldsでは成り立つ

以下のような構造を考える

$ W=\{0,1\}

$ R = \{(0,1),(0,0),(1,1)\}

$ V(0,P)=\bot

$ V(1,P)=\top

この時、排中律$ S,0\models P\lor\lnot Pが成り立たないことを見る

まず、$ S,0\models Pは成り立たない

∵ $ V(0,P)=\bot

また、$ S,0\models\lnot Pも成り立たない

∵ $ V(1,P)=\topかつ$ 0R1

直観主義論理の¬の定義をしっかり思い出すと良いmrsekut.icon

命題Pが偽であるためには、その命題が全ての到達可能な世界で偽である必要がある

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

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

$ S,0\models \lnot Pが成り立つ

となる

ここで、$ w'=1と考えれば、$ S,1\models Pが成り立っちゃてるので、$ S,0\models\lnot Pが成り立たない事がわかるmrsekut.icon

従って、$ S,0\models P\lor \lnot Pは成り立たない