- 483 名前：470 mailto:sage [2005/06/01(水) 00:00:25 ]
- >>482
(¬ 導入)
Ｐ ├ Ｑ
Ｐ ├ ¬Ｑ
------------
¬Ｐ
(¬ 消去)
¬¬Ｐ
--------
Ｐ
のペアのこと。他の論理記号については、（導入）規則は、当該論理記号が
陽に出てくるのが横線の下に一箇所だけだし、（消去）規則は当該論理記号
が陽に出てくるのが横線の上に一箇所だけであるのに、古典論理の ¬ に関
する推論規則は、（導入）規則には ¬ が横線の上段にも出てくるし、（消
去）規則には ¬ が横線の下段に２個出てくる。これでは「導入して直ちに
消去」した場合でも、そもそも当該論理記号を消し去ることができない。
なお、直観主義論理では、¬ を基本的な論理記号とみなすと古典論理と
同じことになるが、直観主義論理では ¬ のかわりに ⊥ を基本的な論理記
号とみなせば、他の論理記号と同じ性質を持つ（古典論理ではそうはいかな
い）。
