証明と主張: 一覧表
語源、由来、謂れ、いわく、物語、逸話 とかを要求されると困るのだが、人々はそれを求めるので、書いておく。
記号 | 由来 |
---|---|
! | たぶん唯一性から ∃! と同じ由来 |
π | 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 |
Prod, Conj | |
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 | Δ
同値関係
可逆性とかベータ変換{による同値}、イータ変換{による同値}、マックレーンの一貫性法則、分配法則など。めんどくさいから今日は省略。