直観主義論理では排中律は一般に成り立たない
従って、背理法を認めない
ただし、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
直観主義論理の¬の定義をしっかり思い出すと良い
命題Pが偽であるためには、その命題が全ての到達可能な世界で偽である必要がある
直観主義論理の¬#6563520b1982700000f138adの説明を具体的に適用すると、
0Rw'を満たす任意のw'\in Wに対して、
S,w'\models Pが成り立たない時、また、その時に限り
S,0\models \lnot Pが成り立つ
となる
ここで、w'=1と考えれば、S,1\models Pが成り立っちゃてるので、S,0\models\lnot Pが成り立たない事がわかる
従って、S,0\models P\lor \lnot Pは成り立たない