LK改の説明：ハイパードクトリン的な解釈
オリジナルのゲンツェンLKでは、
- 公理は一種類（1パターン）
- 推論規則は左右それぞれ10種で合計20種
- Cutが一種
- 合計で21種の推論規則
LK改では、
- 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
αは何もしないので除外。π[1], π[2]はまとめてπとカウント、可逆な場合は2つとしてカウント、idとσは逆にしても変わらないので1つとカウント。このカウント法で12種。
双対、
- *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
idは既に勘定した。先と同じカウント法で11種。
- ε:A, A⇒B → B
- δ:A, B∨C ↔ A∧B | A∧C
- *δ:A∨B, A∨C ↔ A | B∧C
これで5種。すべての合わせて (12 + 11 + 5) = 28種、ρと*ρは除くなら26種。
数は多いが解釈が簡単なメリットがある。Aの真理集合を同じくAで書いて、コンテキストの領域をXとすると：
- id:A = A 自明
- !:A ⊆ X 全体集合が最大
- π[1]:A∩B ⊆ A 共通部分の減少性
- π[2]:A∩B ⊆ B 共通部分の減少性
- Δ:A = A∩A 共通部分のベキ等性
- α:(A∩B)∩C = A∩(B∩C) 共通部分の結合性
- λ:X∩A = A 全体集合は左単位
- ρ:A∩X = 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) 合併の右分配法則
自明冗長を除くと：
- A ⊆ X 最大元
- A∩B ⊆ A ミートの減少性
- A = A∩A ミートのベキ等性
- (A∩B)∩C = A∩(B∩C) ミートの結合性
- X∩A = A 最大元は左単位
- A∩B = B∩A ミートの可換性
- ∅ ⊆ A 最小元
- A ⊆ A∪B ジョインの増加性
- A∪A = A ジョインのベキ等性
- (A∪B)∪C = A∪(B∪C) ジョインの結合性
- A = ∅∪A 最小元は左単位
- A∪B = B∪A ジョインの可換性
- A∩(A⇒B) ⊆ B 指数
- A∩(B ∪ C) = (A∩B) ∪ (A∩C) ミートの右分配法則
- (A∪B) ∩ (A∪C) = A∪(B ∩ C) ジョインの右分配法則
ミートとジョインという可換ベキ等二項演算を持ち、それらが最大元と最小元を中立元としてモノイドであり、お互いに分配的。そして、指数演算を持つ（ハイティング束）。指数演算と最小限から補演算を作れてブール束になる。
今書いたような代数構造を、コンテキスト領域（議論の領域）ごとに持っているので、総体としてハイパードクトリンになる。項の代入がコンテキストのあいだの射になり、それによりハイパードクトリンの構造（引き戻しと随伴）が定義される。
