Poly(C)の構成の方針

目的は非対称非厳密なモノイド閉圏でラムダ計算とコンパクト論理を展開すること。この目的に特化する。閉圏、弱いラムダ計算、弱い論理 - 檜山正幸のキマイラ飼育記 参照。

1. シーケントはコンパクトシーケントを使う。
2. 基本命題＝基本型はCの対象。現実には有限個の基本対象を選ぶ。
3. シーケントの左右の命題列はフラットで順序ありのリスト。
4. シーケントは、Cの射でラベルされる。
5. 推論規則は、Poly(C)の多射に働くオペレータ

CとPoly(C)に関して：

1. Cの対称性は仮定しない。
2. Cの厳密性は仮定しない。
3. Poly(C)は、いわゆる多圏ではなくて、厳密モノイド圏として定義する。
4. Poly(C)の多射は、Cの射で必ずラベレできる。
5. Cは、Poly(C)の単純対象と単純射の部分圏として埋め込める。
6. Poly(C)→Cのレトラクト関手が定義できて、埋め込みとレトラクトにより圏同値となる。
7. 単なる圏同値ではなくてモノイド圏同値である。
8. Poly(C)は圏であるが、モデル論の観点からは多圏として使える。
9. すべての存在物や操作に、絵的意味論を付けられる。