Skinerrian's blog

論理学・哲学・科学史・社会学などに興味があるので、その方面のことを書きます。更新は不定期。

排中律の反例

排中律についてのメモ。

直観主義論理では排中律(P v not-P)が成り立たないと言われる。しかし、これは排中律の否定が成り立つということではない。排中律の否定を仮定すると直観主義論理の範囲でも矛盾が導かれるので、排中律の二重否定が成立する*1

そういうわけで、排中律が成り立たないからといって、それを端的に否定することはできない。一般によく言及されるのは排中律への「弱い反例」というものだ。例えば、「aのb乗が有理数となるような、無理数a, bは存在するか」という問題を解こうとして、√2の√2乗は有理数有理数でないかのどちらかである、という形で排中律が使われることがある。しかし、直観主義者にとっては選言文を主張できるのは、どちらか一方の選言肢を証明したときに限られるので、仮定ではなしにこの選言を主張することは許されない。とはいえ、このことは「√2の√2乗は有理数有理数でないかのどちらかである」の否定を主張するのとは違う。だから「弱い」反例。

量化が言語に含まれる場合、事情はもう少しややこしくなるようだ。古典論理では

  • ∀x(Fx v not-Fx)

が成り立つ。QLEMとでも呼んでおこう。先ほどの命題論理からの類推でいけば、直観主義でも、QLEMの二重否定

  • not-not-∀x(Fx v not-Fx)

は成り立ちそうに思える。しかし、どうもそうではないらしい。一階論理では、 not-∀x(Fx v not-Fx) という主張が成り立つ余地があるらしい。直観主義数学、例えば実数論では、実際にそういう例があるようだ。もちろん一階論理は命題論理を包摂しているので、not-(P v not-P) などと主張するのが不合理であるのは変わらないのだが。

排中律の否定が矛盾であるにも関わらず、モデルによってはQLEMの否定が成り立つということがどうして起きるのか、以前は理解できなかった。今思うと、いくつかの混乱があった気がしている。情けない話だが、戒めとして記しておく。

直観主義では二重否定除去(not-not-P ⇒ P)が成り立たないが、二重否定導入(P ⇒ not-not-P)は成り立つ。でも当たり前だが、二重否定導入が成り立つこととnot-not-Pが成り立つことは別である。Pが成り立たなければnot-not-Pを結論づけることなどできない。

でも、古典論理直観主義論理に埋め込めるという話もある。雑にいえば、ある式が古典論理トートロジーなら、それの二重否定が直観主義論理でトートロジーとされる、のではないのか(二重否定翻訳)。たしかに、それはそう。でもそのことから、QLEMが古典論理の妥当式ならQLEMの二重否定が直観主義論理の妥当式であるはずだ、というのは飛躍がある。二重否定翻訳が成り立つのは命題論理の範囲に限られており、一階論理では成り立たない、とすればどうか。そのときには、直観主義論理では排中律の否定は矛盾だが、QLEMの否定は成り立ちうる、と言っても問題は生じない。

関連記事

*1:多値論理、例えば、三値論理では排中律の否定も整合的であり、成り立つ余地が残されている。