ドウセンの論文、これはサイコー：命題論理とタングル
コスタ・ドウセンとゾラン・ペトリック（Kosta Dosven and Zoran petric'）の"Coherence and Confluence"（arXiv:math/0506310v3）を見つけた。僕の理解力とか好みにたまたまマッチしたということだろうが、これは面白い！ スゲー面白い。11ページしかないから読み切れる。僕にとっては示唆と刺激に富む。解説としてもポイントが押さえてあってとても分かりやすい。実に良い。
もういろいろ面白いんだが、とりあえずこのエントリーでは、例として出てくるコンパクト論理と、それが「からみ系（タングルなど）」とどう関係するかを述べる。
命題変数（命題letterとも言う）p, q, rなどから組み立てられた命題論理式を考える。使えるのは含意記号⊃と掛け算（multiplication）×。×は、∧と思ってよいが、論理結合子が1つしかないからコンパクト論理。推論は、常に1入力-1出力で、次の推論を許す。以下では、p, q, rなどは、命題変数つうよりは論理式（項といってもいいが）を表すメタ変数。
(1)
p×q
------[k1]
p(2)
p×q
------[k2]
q(3)
p×(p⊃q)
----------[ε, モダスポネンス]
q(4)
p
------[w, 増]
p×p(5)
q
----------[η]
p⊃(p×q)(6)
p×q
-------[γ, 換]
q×p
ドウセン／ペトリック論文では、⊃に矢印を使っている。γ（対称、またはブレイディング）は僕が付け足した。その他の記号はママ採用。少し注意：
- 射影がπじゃなくてkなのは、Kコンビネータからだろう。
- 対角がwなのはdoubleだからだろう。weakeningのwかもしれない。
- ηとεは、単位／余単位の記号。余単位εがモダスポネンスなのは面白い。
以上の推論図から次のような、タングルもどきを作る。
(1)
p×q
| |
|
p(2)
p×q
| |
|
q(3)
p×(p⊃q)
∪ |
|
q(4)
p
／＼
p × p(5)
q
|
∩ |
p⊃(p×q)(6)
p × q
＼／
／＼
q × p
命題変数のラベルを忘れてしまうと：
(1) k1: 2→1
* *
| |
|
*(2) k2:2→1
* *
| |
|
*(3) ε:3→1
* * *
∪ |
|
*(4) w:1→2
*
／＼
* *(5) η:1→3
*
|
∩ |
* * *(6) γ:2→2
* *
＼／
／＼
* *
となる。縦につないで結合、横に並べてモノイド積（テンソル）を入れると、Nを対象類とする対称モノイド圏（またはブレイド付きモノイド圏）となる。この圏は、対称の圏（またはブレイドの圏）を含むが、放電器や∪、∩を単独で取り出すことは出来ない（閉じ込められている）。対称性が不完全で双対もない。
以上で作られた圏では面白くなくて、縮約操作で得られる図形も全部入れた圏を考える（正確な定義はまだハッキリしない）。縮約してできる図形が証明ネットだろう。縮約は証明ネットの変形（書き換え）に対応する。基本的な書き換え規則から生成された書き換えを2-セルとして2圏を作る。この2圏（弱いかも知れない）が興味の対象だ。
ドウセンによると、問題の2圏内の2セルに3-セルを使って同値関係を入れて正規形を選び出すのが困難らしい。どうも焦点は3-構造のように思われる（僕の誤解がなければ）。
この例題は定義が簡単で、手でいくらでもいじれる。そのくせ難しい。テンパリー／リーブ圏とかカウフマン図式の圏とかと比べても面白い。トゥラエフのタングル圏（コッチも）とも似ているし。
適当なタングルを生成元とすると、面白い代数の例がいくらでも作れる気がする。q |- p⊃(p∧q) がモダスポネンスの“ある種の双対”となるのはまったく知らなかった。絵図を使わないと気が付きにくいだろう。
