圏的オペレータとシーケント

圏的オペレータを考えるといいことのひとつが、シーケントの（とりあえずの）意味論ができることだ。

シーケントを射と思うと、基本推論は、0個、1個、2個のホムセットの直積から1個のホムセットへの写像と考えることができる。ホムセットを(a, b)のように書くことにすると、推論は、|- (a, a) とか (a, b),(b, c) |- (a, c) のように書ける。

この方針で、有限個のホムセットの並び（ストリング）を対象とする圏（むしろ多圏）を作れる。この圏のモノイド積は連列で非対称。モノイド単位は空な並び。基本推論（に対応するオペレータ）が生成射になる。生成射から生成された自由圏が証明の圏ということになる。証明の圏の射＝証明が、もとの圏上にうまく2-射を定義できる保証はない。が、いずれにしも証明の圏はもとの圏と強い関係がある。

問題意識としては、命題＝対象、自然演繹＝射である圏があるとき、自然演繹＝シーケント＝対象、ゲンツェン証明＝射である圏をどう構成するのか、もとの圏＝自然演繹の圏と、構成された証明の圏はどう関係するのか？ さらには証明の変形／書き換えを2-射とするとき、2-射をどう構成するのか？ などだろう。

ジラール（Girard）がいうように、証明図が「式」で、証明図の変形が「計算」、それ以上変形できない証明図が「値」である計算論も構成できるのだろう、おそらく。