ド・モルガン双対
ド・モルガン双対をリスト〈バンチ〉に対して定義する。双対化演算は、
- *(A1, ..., An) = (¬A1| ...| ¬An)
- *(,) = (|)
- *(A1| ...| An) = (¬A1, ..., ¬An)
- *(|) = (,)
- ** = id
と定義する。推論規則は
¬ 左 (Γ → Δ| Φ) ⇒ (*Φ, Γ → Δ) ¬ 右 (Ψ, Γ → Δ) ⇒ (Γ → Δ| *Ψ)
特別な場合として
¬ 左 (Γ → Φ) ⇒ (*Φ, Γ → (|)) ¬ 右 (Ψ → Δ) ⇒ ((,) → Δ| *Ψ)
∧ 右 と ∨ 左 と限量子
まず、そのまま書く。
∧ 右 (Γ → Δ| A And, Π → Λ| B) ⇒ (Γ, Π ⇒Δ| Λ| A∧B) ∨ 左 (A, Γ → Δ And, B, Π → Λ) ⇒ (A∨B, Γ, Π → Δ| Λ)
構造規則を使って、Γ, Π を新たに Γ、Δ| Λ 新たに Δ と置いて:
∧ 右 (Γ → Δ| A And, Γ → Δ| B) ⇒ (Γ ⇒Δ| A∧B) ∨ 左 (A, Γ → Δ And, B, Γ → Δ) ⇒ (A∨B, Γ → Δ)
限量子
∀ 右 (Γ → Δ| A(a) ) ⇒ (Γ ⇒Δ| ∀x.A(x)) ∨ 左 (A(a), Γ → Δ) ⇒ (∃x.A(x), Γ → Δ)
Σ とΠ を使うと:
Π 右 (Γ → Δ| A(i) ) ⇒ (Γ ⇒Δ| Πi.A(x)) Σ 左 (A(i), Γ → Δ) ⇒ (Σi.A(x), Γ → Δ)
⊃ 左
→ と ⇒ を使ってしまったので、含意を ⊃ にする。
⊃ 左 (Γ → Δ, A And, B,Π → Λ) ⇒ (A⊃B, Γ, Π → Δ, Π)
これは、マージとド・モルガン双対で解釈するのがいいかな。
マージ (Γ → Δ, A And, B,Π → Λ) ⇒ (B, Γ, Π → Δ, Π, A) ド・モルガン双対 (B, Γ, Π → Δ, Π, A) ⇒ (¬A, B, Γ, Π → Δ, Π) 連言濃縮 (¬A, B, Γ, Π → Δ, Π) ⇒ (¬A∧B, Γ, Π → Δ, Π) 同値置換 ¬A∧B ≡ A⊃B (¬A∧B, Γ, Π → Δ, Π) (A⊃B, Γ, Π → Δ, Π)
リーズニング
- 連言の濃縮・希釈 バンチ演算
- 選言の濃縮・希釈 バンチ演算
- 全称命題の濃縮・希釈 拡大バンチ演算
- 存在命題の濃縮・希釈 拡大バンチ演算
- マージ バンチ演算
- ド・モルガン双対移動
- プレ結合 知識ベース使用
- ポスト結合 知識ベース使用
- 同値置換 プレポスト結合 知識ベース使用
- カリー化