昨日書いた記事「対称モノイド多圏（簡約版）」に関連しての雑多なお話。
過去の記事で何度か触れたように、多圏〈polycategory〉は難しくて閉口します。そんな難しい多圏を何で必要とするのか？ というと、僕の主たる動機は“シーケント計算のモデル”としてです。シーケント計算はナニカを指示〈denote〉してるだろう、シーケント計算はナニカの計算手段だろうと考えたときのナニカが「シーケント計算のモデル」です。
そもそも、シーケント計算が、意味不明で謎な計算体系です。「ゲンツェンは、何でこんなものを考えついたのだろう？」は、誰でもが抱く疑問でしょう。しかし、シーケント計算を実際に使ってみると、驚くほどうまく機能します。使えば使うほどに、ゲンツェンの、時代を超越した天才っぷりに驚愕します。2020年の現時点においても、ゲンツェンのシーケント計算は、完全には解明されてないように思えます。
ゲンツェンのオリジナルの（古典論理）シーケント計算は難しすぎるので、単純化して二項論理演算はひとつだけにします。そのように単純化した論理を総称してコンパクト論理と呼びます（ジラーは「コンパクト論理」と呼んでたと思うけど、一般的な言葉ではないです）。コンパクト論理の意味論は、唯一の二項論理演算を圏のモノイド積と解釈して遂行できるのではないか？ と期待できます。
コンパクト論理のシーケント計算 -- コンパクトシーケント計算であっても、意味論構成には多圏が必要そうです。やっぱり難しい！ はぁ(ため息)。目論見はあっても、手が出ない期間が長く続きました。
ところが、コンパクトシーケント計算のために“本物の多圏”が必要か？ と問うてみると、どうも「要らない」ようです。我々は多圏の一般論をしたいわけではなくて、“特定目的のための特定状況下において”多圏概念（の一部）を利用したいだけです（「多圏の必要性、煩雑さ、そして単純化 // 何とかなりそう」）。そこで、多圏概念を極端に単純化した簡約多圏〈reduced polycategory〉を定義したわけです（「対称モノイド多圏（簡約版）」）。
“特定目的のための特定状況下”を具体的に言えば、モノイド圏と多圏が相互に強く結びついている状況です。大雑把にまとめれば：
| 計算 | モデル |
|---|---|
| シーケント計算 | 多圏 |
| 自然演繹 | モノイド圏 |
シーケント計算〈コンパクトシーケント計算〉で出てくる多圏は置換の作用と挿入を持ちます。この置換作用／挿入は、ゲンツェンの言葉で言えば、構造規則「換〈exchange〉」に相当します。モノイド圏（自然演繹のモデル）では通常の対称性で、二項論理演算の可換性になります。
「換」以外の構造規則も、圏の構造射〈律子〉やモダリティ（装備、「マルコフ圏の一族 // 様々な装備圏」参照）からの射に対応するようです。また、通常は、（自然演繹の）モデルであるモノイド圏は対称モノイド圏以上の構造を持ちます。それは：
- デカルト閉圏
- コンパクト閉圏〈コンパクト圏〉
モデル側の指数〈内部ホム〉や双対が、計算側の含意や否定に対応します。
一般的なモノイド圏は厳密とは限りません。むしろ、たいていのモノイド圏は厳密ではありません。しかし、コンパクトシーケント計算に対応する簡約多圏は厳密モノイド圏です。つまり、コンパクトシーケント計算は、自然演繹のモデルであるモノイド圏の厳密化〈strictification〉を与えます。コンパクトシーケント計算が、自然演繹のモデルの厳密化を与える構図は、デカルト閉圏／コンパクト閉圏の場合も同様です。
厳密化は、一貫性定理〈coherence theorem〉として表現できます。となると、ゲンツェンがやったことは、一貫性の議論を先取りしていたように思えます。一貫性は、概念的にも技術的にも難しい事項です。
100年近く前のゲンツェンのシーケント計算が、多圏や一貫性の概念を潜在的に含んでいたとすれば、そりゃ難しいわなー。謎だわな－。そしてやっぱり、ゲンツェンが偉大すぎる。
