シーケント計算の再解釈 2

ド・モルガン双対

ド・モルガン双対をリスト〈バンチ〉に対して定義する。双対化演算は、

• *(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, Γ, Π → Δ, Π)

リーズニング

1. 連言の濃縮・希釈 バンチ演算
2. 選言の濃縮・希釈 バンチ演算
3. 全称命題の濃縮・希釈 拡大バンチ演算
4. 存在命題の濃縮・希釈 拡大バンチ演算
5. マージ バンチ演算
6. ド・モルガン双対移動
7. プレ結合 知識ベース使用
8. ポスト結合 知識ベース使用
9. 同値置換 プレポスト結合 知識ベース使用
10. カリー化