TETRA'S MATH

数学と数学教育
<< 直観主義論理の公理系 | main | 亀井喜久男さんの「約数集合構造」 >>

直観主義論理では成り立たない定理

 直観主義論理が出てくる前の従来の命題論理、つまり古典論理の公理系で「二重否定」がなくなったことで、なぜ、「排中律」の証明ができなくなるのか。それを考えるために、まず、古典論理での排中律の証明を勉強することにしました。

 これがね、なんかね、スゴイのよ。

 野矢茂樹さんも「初心者には難しいかも、ここでくじけないでね〜」とおっしゃっています。

 何はともあれ、見てみます。



 閉塞しているんだか大胆なんだかよくわからない世界です。ゆっくり見ていくと、なるほどねぇと感心することしきり。でも、1行間違いが入っていてもだまされそう(!?)な気分ではあります。

 [1]も[2]も否定の形をした背理法の仮定なので、(5)と(8)は否定除去型の背理法()となり、直観主義論理ではアウトになるのだと思います。

 次に、直観主義論理ではド・モルガンの法則のうちの1つ

        ¬(A∧B)⊃(¬A∨¬B)

が成り立たないわけを考えます。古典論理では次のような証明になっています。



 (3)で使っている定理は証明済みのド・モルガンの法則の1つです。途中で二重否定を2回使っているし、否定除去型の背理法もあるし、どう考えてもアウトかな。じゃあ、他のド・モルガンの法則はどうなのかというと、あとの3つはみんな二重否定も否定除去型背理法も使っていないのです。不思議なことに。ちなみに、(¬A∨¬B)⊃¬(A∧B)は二重否定導入A⊃¬¬Aは使ってあります。上のド・モルガンの法則も二重否定なしで証明できないのか?と気になりますが、トライする気力はなく……。

 こうやって証明をながめてみると、背理法って便利だなぁとしみじみ思います。背理法なしじゃなんにもできないな。

論理学 | permalink
  

サイト内検索