パースの法則：((A→B)→A)→A
直観主義論理NJに、パースの法則を公理図式として加えると古典論理になるという話を聞いたので少し考えた。たしかに、((A→⊥)→A)→A を前提することで、((A→⊥)→⊥)→A が導出できるっぽい。つまり、二重否定除去が導出できるから、これで古典になる。
個人的には、二重否定除去を経由しないで排中律を導くのには、ちょっと苦労した。Av￢AをLEMと表すと、((LEM→⊥)→LEM)→LEM を前提すれば、LEM が出せるかな、と。
しかし、この結果はいったい何を意味しているんだろうか…。
Postscript (2014/11/6)
最近出版された菊池誠『不完全性定理』p.39によると、パースの法則は、否定を使っていないのに、直観主義論理では証明できないトートロジーという点に価値がある、のだとか。なるほど～。
