自然演繹とシーケント計算の解釈
困った時の米田頼み、ご利益ツールズ - 檜山正幸のキマイラ飼育記 で述べたこと：
自然演繹とシーケント計算の関係は、僕が長年興味を持っているテーマのひとつです。ある程度は理解しているつもりなんですが、なんかスッキリしない。説明しろと言われれば出来そうではありますが、バシッと決められないもどかしさを感じてました。
今まで米田頼みをしたことがなかったのですが、「ひょっとしたら」と思って米田埋め込みを探してみました。… ありましたね(ニコ)。これでたぶん、バシッと決められます。でも、今日この話はしません。まだ詰め切れてないので、もう少し考えてからにします。
これだけど、何の記録もないので忘れるかも、、、、ヤバイ。
Cが自然演繹のモデルとなっているデカルト閉圏だとする。これに対して、シーケント計算のモデルはどうなるかという話。端的に結論を言ってしまうと、（たぶん）自己プロ関手の圏Prof(C, C) = EndProf(C) だろう。以下、EndProf(C) を EndProf(C)と書く。
CをEndProf(C)に埋め込む方法は色々ある。H∈EndProf(C)を単位元に相当するCのホム双関手だとすると、H(-, T), H(-, ⊥), H(T, -), H(⊥, -) などが埋め込みの例。しかし、
- CをEndProf(C)に埋め込む標準的な方法はない。
この事実が、自然演繹（C）とシーケント計算（EndProf(C)）の関係を分かりにくくしている。
しかし、EndFunc(C)を自己関手圏Cat(C, C)とすると、EndFunc(C)の非対称モノイド圏構造も含めて、EndProf(C)に埋め込める。
- EndFunc(C)をEndProf(C)に埋め込む標準的な方法がある。
よって、Cの対象である命題や、Cの射である（自然演繹の）証明をそのままシーケント計算に持っていくのはうまくなくて、いったんEndFunc(C)で解釈してから、素直にEndProf(C)に入れる。例えば、命題＝対象ならば、直積によりスタンピング関手としてから、EndProf(C)で解釈する。
そもそも、自然演繹は、C内での解釈は（出来るが）不自然で、証明図は射ではなくて、自然変換の成分表示になっている、と解釈すべき。
- Cの射は、証明のインスタンスである。
- Cの自然変換は、証明のパターン＝テンプレートである。
自然演繹の推論図とは、EndFunc(C)の構成的部分圏を生成するための生成1-射〈generating 1-morphism〉である。1-射＝自然変換なので、結局、「推論図＝生成自然変換」となる。
現状の説明（僕自身の説明も含めて）だと、パターンとパターンのインスタンスの区別がついてない。
| パターン | インスタンス | |
|---|---|---|
| 対象 | 対象変数 | 実際の対象（個別具体的命題） |
| 射 | 自然変換 | 自然変換の特定成分 |
| 射の結合 | 自然変換の縦横結合 | 射の結合（横のみ） |
| 射の直積 | 自然変換の直積 | 射の直積 |
EndFunc(C)は、Cが直積を持つことから、関手の直積と自然変換の直積を持つモノイド2-圏となる。
EndProf(C)もモノイド2-圏となる。したがって、自然演繹からシーケント計算への埋め込みは、モノイド2-圏の構造を保つようなモノイド2-関手によって行われる。
EndProf(C)には、Cop×Cが両側加群として働くが、EndFunc(C)op×EndFunc(C)も働く。自己関手モノイド圏が自己プロ関手モノイド圏に左右から働くような構図。この両側加群構造があるので、自然演繹とシーケント計算を混ぜて使うことが出来る。
さらに証明図（パターン）の変形は自然変換のあいだの変更〈modification〉になるので、3-圏が必要になる。そればかりか、高次の複圏と多圏が必要になる。難しいわ。
いずれにしても、高次の構造が絶対に必要なのは確か。
