タブローはシークエント計算の特殊例にすぎない、という話を昔聞いたことがある。一体どういうことだろう、と長いこと理解できないでいたのだが、最近になって、こういうことかな、と勝手に自己解決したのでちょっとメモしてみる。
古典論理のシークエント計算にも色々な流儀があるが、ここで考えたいのはG3cと呼ばれる証明体系である。
よくよく考えてみると、G3cの推論規則はタブローで枝を伸ばす規則と似ている。類似性に気づくためには、まず、シークエントに出現する式をすべて左側に寄せる必要がある。右辺から左辺に寄せるには、否定を付ければよい。任意の結合子〇について、A〇Bから枝を伸ばす規則は、〇の左規則を下から上に読むことに対応する。￢（A〇B）から枝を伸ばす規則は、〇の右規則を下から上に読むことに対応する。枝が閉じることは、シークエント計算の公理である同一律のシークエントに出現する式をすべて左辺に寄せたもの、つまり矛盾律に対応する。
二重否定文から枝を伸ばす規則に対応するのは…。うーん、古典論理だから二重否定除去は許される、ということでシークエントの右辺から左辺に動かすときに二重否定は取り払ってしまうことにしておこう…。
∀の左規則は結論だけでなく前提にも全称文が含まれるが、タブローでは全称文から枝を伸ばす場合には、この式にチェックを入れることは許されず、何度でも利用可能であることに対応しているのだろう。
対応関係はメタ的な性質にも及ぶ。タブローの証明は部分式性質subformula propertyを満たし、カットフリーのG3cも部分式性質を満たす。対応関係が崩れるとすれば、構造規則かな…。まぁでもG3は構造規則がadmissibleなので、なくても証明能力はまったく落ちないわけだ。
素人考えだが、この先も考えてみたくなる。例えば、様相論理Kのシークエント計算。これを上のようなやり方で左側だけのシークエント計算に翻訳すれば、prefixなしの様相論理タブローが得られそうだ。
