Skinerrian's blog

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

EFQ

タブローで、矛盾からは何でも言えるということを証明するにはどうするのか、という質問を見かけて、それは考えたことなかったなと思った。言語が⊥を含むかどうかで場合分けすればよいのだろうか。

  • ⊥を論理記号に含む言語の場合:⊥に関する推論規則として、すぐに枝を閉じるという規則を加える。EFQの証明図では、根にいきなり⊥が現れるので、速攻で枝を閉じて終了。
  • ⊥を含まない言語なら、¬(P∧¬P→Q) から出発して枝が閉じることを証明する。¬→の規則を適用するとすぐにP∧¬Pが出てくるから、枝が閉じて終了。

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