檜山正幸のキマイラ飼育記 メモ編

ドウセンの論文、これはサイコー：命題論理とタングル

圏一般論, 論理, からみ系 | 11:18

コスタ・ドウセンとゾラン・ペトリック（Kosta Dos^ven 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

ドウセン／ペトリック論文では、⊃に矢印を使っている。γ（対称、またはブレイディング）は僕が付け足した。その他の記号はママ採用。少し注意：

1. 射影がπじゃなくてkなのは、Kコンビネータからだろう。
2. 対角がwなのはdoubleだからだろう。weakeningのwかもしれない。
3. ηとεは、単位／余単位の記号。余単位εがモダスポネンスなのは面白い。

以上の推論図から次のような、タングルもどきを作る。

(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) がモダスポネンスの“ある種の双対”となるのはまったく知らなかった。絵図を使わないと気が付きにくいだろう。