式と推論

シーケント（シークエント）計算と自然演繹の関係を考えるとき、次の対応を想定するとよい。

＼	式	推論
自然演繹	対象	射
片側シーケント	点射	射から導かれるオペレータ
シーケント	射	オペレータ

点射（あるいは点、element）とは、1→A という形の射、オペレータは主にホムセットに対して定義される集合論的な操作で、対象や対象の組でindexされたもの。自然変換はオペレータの特殊なもの。結合、トレース、部分トレースなどもオペレータ。射からオペレータが導かれるとは、反変／共変のホム関手がいい例。

片側シーケント計算は、実は田中一之「数の体系と超準モデル」の65ページに出てくる。Gentzen-Tait System GT というのがそれだ。両側シーケントがいつでも片側に変換できるわけではないが、古典論理やコンパクト論理のような対称性が高い論理なら、片側にできる。

あーそれと、あまり脈絡もなく書いておくが、証明図はツリーだと思う必要はないな。別に分岐してもいい。ステファネスクが言うところのフローダイアグラムあたりか。ツルのように多少は絡まってもいい林みたいな図形。