直観主義論理は排中律と二重否定除去則が成り立たない論理として知られる。どちらか一方を付け加えると、他方も導出できて、古典論理になる。
それでは、排中律と二重否定除去則は同値といってよいのだろうか。もちろん、直観主義論理の上では同値なのだが、これはもうちょっと奥の深い問題のようだ。
例えば、最小論理の上ではどうなるか調べてみる*1。最小論理とは直観主義論理からEFQを取り除いた論理だが、最小論理に二重否定除去則を加えるとEFQを導出できるため、一挙に古典論理となる。他方、最小論理に排中律を加えても古典論理にはならない。したがって、図式的に書くと
となる。
このことは二重否定除去則の方が排中律より強力であることを示しているのだろうか。そうも言いきれないと思う。シークエント計算で考えてみよう。二重否定除去則はシークエントの右辺がマルチセットになることを認めれば導出できるので、二重否定除去則は右辺がマルチセットであることに相当すると言えよう。しかし、排中律の証明にはそれだけでは足りず、右の縮約規則を使う必要がある。
そういうわけで、私としては
- 二重否定除去則+縮約規則=排中律+EFQ
あるいは、EFQが弱化規則に相当すると考えて
- 二重否定除去則+縮約規則=排中律+弱化規則
という風に考えてみたい。