読者です 読者をやめる 読者になる 読者になる

Skinerrian's blog

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

EFQ

論理学

タブローで、矛盾からは何でも言えるということを証明するにはどうするのか、という質問を見かけて、それは考えたことなかったなと思った。もっとも、大して難しいことではないだろうけど。⊥を論理記号に含む言語だったら、⊥に関する推論規則として、すぐに枝を閉じるという規則を加えればいいのかな。⊥を含まない言語なら、¬(P∧¬P→Q) から出発して枝が閉じることを証明すればよさそう。

⊥を含むかどうかで、二通りに分岐するってのは何か意味があるのかもなぁ。例えば、シークエント計算の場合、EFQを示すには右の弱化規則が本質的な役割を果たしそう、ということは前に述べたことがあるが、これは⊥を含まない言語の話で。⊥を含む言語だったら、EFQは公理に加えるんだと思う。ここでも⊥を含むかどうかで分岐がある。