証明と主張：一覧表 - (保存用) 檜山正幸のキマイラ飼育記メモ編

語源、由来、謂れ、いわく、物語、逸話とかを要求されると困るのだが、人々はそれを求めるので、書いておく。

記号	由来
!	たぶん唯一性から ∃! と同じ由来
π	projectionのp
ι	injectionのi
Δ	diagonalのd、それと形状の類似
λ	leftのl
ρ	rightのr（rh）
α	associativeのa
σ	symmetryのs, symmetriy = permutation
γ	conjunctionとconstructorのc、だが注記参照
ε	evalのe
δ	distributiveのd

※注記： γはcには対応しない。gに対応。だが、三番目に登場するのでcの代わりに使われることがある。

基本スパイダー

双対の作り方は：

矢印の向きは逆にする。
T と ⊥ を取り替える。
, と | を取り替える。
∧ と ∨ を取り替える。

この双対は圏論的双対で、否定や含意は絡んでないからド・モルガン双対ではない。

圏論的背景は：

論理式は圏の対象
論理式のリストは双対性を持つ多圏の多対象
推論図（証明図と同義）は多圏の多射
基本リーズニングは圏・多圏の構造写像
推論図の同値性（可逆性やベータ同値など）は、圏・多圏の一貫性法則

基本スパイダーの一覧、'↔'は可逆であることを示す。

id:A ↔ A
!:A → T
π[1]:A, B → A
π[2]:A, B → B
Δ:A ↔ A, A
α:A, B, C ↔ A, B, C （注記参照）
λ:T, A ↔ A
ρ:A, T ↔ A
σ:A, B ↔ B, A
γ:A, B ↔ A∧B

これらはすべて双対がある。

*id:A ↔ A
*!:⊥ → A
*π[1]:A → A | B
*π[2]:B → A | B
*Δ:A | A ↔ A
*α:A | B | C ↔ A | B | C
*λ:A ↔ ⊥ | A
*ρ:A ↔ A | ⊥
*σ:A | B ↔ B | A
*γ:A∨B ↔ A | B

モーダスポネンスに相当するεは、

ε:A, A⇒B → B

分配法則は、

δ:A, B∨C ↔ A∧B | A∧C
*δ:A∨B, A∨C ↔ A | B∧C

双対は同じことだから、星なしの推論図を横棒図で表す。

id:A → A
    A
  ----↑[id]
    A

!:A → T
    A
   ----[!]
    T

π[1]:A, B → A
    A  B
   ------[π[1]]
     A

π[2]:A, B → B
    A  B
   ------[π[2]]
     B

Δ:A → A, A
    A
   -----↑[Δ]
   A  A

α:A, B, C → A, B, C
   A  B  C
  ---------↑[α]
   A  B  C

λ:T, A → A
    T  A
   ------↑[λ]
      A

ρ:A, T → A
   A  T
  ------↑[ρ]
    A

σ:A, B → B, A
    A   B
   -------↑[σ]
    B   A

γ:A, B → A∧B
    A   B
   -------↑[γ]
     A∧B

ε:A, A⇒B → B
    A  A⇒B
   ---------[ε]
       B

δ:A, B∨C → A∧B | A∧C
    A   B∧C
   --------------↑[δ]
    A∧B | A∧C

絵図コンビネータ

次の6種類

記号	綴り
;	Comp
$\otimes$	Prod, Conj
$\oplus$	Sum, Disj
◇	Diam
□	Squa
Λ	Lamb

ダイアモンドとスクエアには項数として集合Xが入る。<X>, [X] で書く。X = {1, 2, ..., n}のときは <n>, [n] と略記する。

  Γ→Δ   Δ→Σ
 =================[Comp]
   Γ→Σ

  Γ→Δ   Σ→Π
 =================[Conj]
  Γ,Σ → Δ,Π

  Γ→Δ   Σ→Π
 =================[Disj]
  Γ|Σ → Δ|Π


  Γ, (x∈X) A → B[x]
 ==========================[Diam X]
    Γ, A → ∀x∈X.B[x]


  Γ, (x∈X) A[x] → B
 ==========================[Squa X]
    Γ, ∃x∈X.A[x] → B


   A, Γ → B | Δ
 =====================[Lamb]
   Γ → A⇒B | Δ

あるいは、

   Γ     Δ
  ----   ----
   Δ     Σ
 =============[Comp]
    Γ
    ---
    Σ


   Γ      Σ
   ----   ----
   Δ      Π
 ================[Conj]
     Γ Σ
   ---------
     Δ  Π


   Γ      Σ
  -----   ----
   Δ      Π
 ===============[Disj]
    Γ | Σ
    --------
    Δ | Π



  Γ
  ---+-(x∈X)--
         A
        ---
         B[x]
     +---------
 ====================[Diam X]
    Γ     A
   ----------------
      ∀x∈X.B[x]



  Γ
  --+-(x∈X)---
       A[x]
       -----
         B
    +----------
 =====================[Squa X]
    Γ  ∃x∈X.A[x]
    ---------------
            B


     A  Γ
   --------
     B | Δ
 =============[Lamb]
        Γ
   ----------
   A⇒B | Δ

同値関係

可逆性とかベータ変換{による同値}、イータ変換{による同値}、マックレーンの一貫性法則、分配法則など。めんどくさいから今日は省略。