どうでもいいのだが、書き方決める

命題、証明、規則をそれぞれ0-射、1-射、2-射の意味で使う。

公理

公理証明

ax_A : * -> A


  *
 ----[ax A]
  A

Ax⊆|C| なので、Axは命題の集合として与えられるが、それはデカルト閉圏の特殊事情で、一般には、

a : X -> A


  X
 ---[a]
  A

つまり、Ax⊆Mor(C)。Axはどんな部分集合でもよい。

基本証明＝原子証明も公理の一種である。基本証明は推論規則ではない！ 命題としての公理は、証明としての公理のエンコード形式のひとつに過ぎない。

恒等

恒等証明

id_A : A->A


  A
 ---[id A]
  A

定義

定義は可逆1-射である。展開（expand）方向と縮約（contraction）方向が決まっている。

expn_d : A -> B, cont_d : B -> A


  A
 ---[expn d]
  B

  B
 ---[cont d]
  A

推論規則

構造規則は、圏の対角、射影、対称に由来する。

 Γ| A, B ->C
 --------------[exch] 対称の存在
     B, A ->C

 Γ| ->B
 --------------[weak] 終射（特殊な射影）の存在
    A ->B

 Γ| ->⊥
 --------------[weak] 始射（特殊な入射）の存在
     ->B

  Γ| A, A ->C
 --------------[cont] 対角の存在
        A ->C

左規則をL、右規則をRとする。

  Γ| Ai ->C
 ----------------[∧Li] 第i射影の存在
     A1∧A2 ->C

  Γ| ->A1  ->A2
 ----------------[∧R] デカルトペアリングの存在
     -> A1∧A2

  Γ| A ->C   B ->C
 --------------------[∨L] デカルトコペアリングの存在
      A∨B ->C

 Γ | ->Ai
--------------------[∨Ri] 第i入射の存在
      ->A1∨A2

 Γ| B->C  ->A
 ----------------[⊃L] ？
    A⊃C ->B

 Γ| A ->B
 ----------------[⊃R] カリー化
     -> A⊃B

 Γ| ->A
 ------------[¬L] 否定双対性
    ¬A ->⊥

 Γ| A ->⊥
 ------------[¬R] 否定双対性
      ->¬A

 Γ|   A[t] ->B
 -----------------------[∀L] 脱具体化
    ∀x.A[x/t] ->B

 Γ| ->A[y]
 ----------------------[∀R]
     ->∀x.A[x/y]

 Γ|   A[y] ->B
 -----------------------[∃L]
    ∃x.A[x/y] ->B

 Γ| ->A[t]
 ----------------------[∃R] 実例
     ->∃x.A[x/t]

とりあえず列挙した。分析は後日。