シークエント計算における「論理式の集まり」
一般に
シークエント計算
における
シークエント
とは
論理式の集まり
$ \Gamma,\Delta
を用いて
$ \Gamma \Rightarrow \Delta
として定義される.
論理式の集まりという構造に対して何を採用するかによって微妙に違う体系が得られる.
有限/無限性は一旦無視する.
普通は
集合
として採用する.これは
古典論理
や
直観主義論理
などで普通に仮定して良い.
他方,もっと制約を課すことも出来る.
多重集合
を採用した際,
縮約規則
を認めなければ
線形論理
といった個数センシティヴな体系が得られる
資源としての命題
リスト
を採用した際,
交換規則
を認めなければ
Lambek計算
といった順序センシティヴな体系が得られる(?)
ツリー
を採用した際,
結合規則
を認めなければ…何になるの?
参考文献
大西琢朗; "論理学上級Ⅱ, 様相論理のシークエント計算"