Γ ⊦ Δ 1 , 𝐴 ∧ 𝐵, Δ 2
Γ ⊦ Δ 1 , 𝐴, Δ 2 Γ ⊦ Δ 1 , 𝐵, Δ 2
Γ 1 , 𝐴 ∧ 𝐵, Γ 2 ⊦ Δ
Γ 1 , 𝐴, 𝐵, Γ 2 ⊦ Δ
Γ ⊦ Δ 1 , 𝐴 ∨ 𝐵, Δ 2
Γ ⊦ Δ 1 , 𝐴, 𝐵, Δ 2
Γ 1 , 𝐴 ∨ 𝐵, Γ 2 ⊦ Δ
Γ 1 , 𝐴, Γ 2 ⊦ Δ Γ 1 , 𝐵, Γ 2 ⊦ Δ
Γ ⊦ Δ 1 , 𝐴 → 𝐵, Δ 2
𝐴, Γ ⊦ Δ 1 , 𝐵, Δ 2
Γ 1 , 𝐴 → 𝐵, Γ 2 ⊦ Δ
Γ 1 , Γ 2 ⊦ Δ, 𝐴 Γ 1 , 𝐵, Γ 2 ⊦ Δ
Γ ⊦ Δ 1 , ￢ 𝐴, Δ 2
𝐴, Γ ⊦ Δ 1 , Δ 2 Γ 1 , ￢ 𝐴, Γ 2 ⊦ Δ
Γ 1 , Γ 2 ⊦ Δ, 𝐴
•
式の分解を次のように定義する．かつ または
ならば 否定
分解と証明の関係（かつ，後件）
Γ ⊦ Δ 1 , 𝐴 ∧ 𝐵, Δ 2
Γ ⊦ Δ 1 , 𝐴, Δ 2 Γ ⊦ Δ 1 , 𝐵, Δ 2
Γ 1 , Γ 2 ⊦ Δ 1 , Δ 2 , 𝐴 ∧ 𝐵
（∧R）Γ 1 ⊦ Δ 1 , 𝐴 Γ 2 ⊦ Δ 2 , 𝐵
Γ, Γ ⊦ Δ 1 , Δ 2 , Δ 1 , Δ 2 , 𝐴 ∧ 𝐵
（∧R）
Γ ⊦ Δ 1 , 𝐴, Δ 2 Γ ⊦ Δ 1 , 𝐵, Δ 2
（ER） （ER）
Γ ⊦ Δ 1 , Δ 2 , 𝐴 Γ ⊦ Δ 1 , Δ 2 , 𝐵
Γ ⊦ Δ 1 , Δ 2 , Δ 1 , Δ 2 , 𝐴 ∧ 𝐵
（CL）Γ ⊦ 𝐴 ∧ 𝐵, Δ 1 , Δ 1 , Δ 2 , Δ 2
（ER）Γ ⊦ 𝐴 ∧ 𝐵, Δ 1 , Δ 1 , Δ 2
（CR）（ER）
Γ ⊦ 𝐴 ∧ 𝐵, Δ 2 , Δ 1 , Δ 1
（CR）
Γ ⊦ 𝐴 ∧ 𝐵, Δ 2 , Δ 1 Γ ⊦ Δ 1 , 𝐴 ∧ 𝐵, Δ 2
（ER）分解
推論規則
分解と証明の関係（かつ，前件）
分解
推論規則
Γ 1 , 𝐴 ∧ 𝐵, Γ 2 ⊦ Δ
Γ 1 , 𝐴, 𝐵, Γ 2 ⊦ Δ
𝐴 ∧ 𝐵, Γ ⊦ Δ
（∧L1）
𝐴, Γ ⊦ Δ
𝐴 ∧ 𝐵, Γ ⊦ Δ
（∧L2）
𝐵, Γ ⊦ Δ
（∧L1）
Γ 1 , 𝐴, 𝐵, Γ 2 ⊦ Δ
（EL）
𝐴, 𝐵, Γ 1 , Γ 2 ⊦ Δ 𝐴 ∧ 𝐵, 𝐵, Γ 1 , Γ 2 ⊦ Δ
（EL）
𝐵, 𝐴 ∧ 𝐵, Γ 1 , Γ 2 ⊦ Δ
（∧L2）
𝐴 ∧ 𝐵, 𝐴 ∧ 𝐵, Γ 1 , Γ 2 ⊦ Δ 𝐴 ∧ 𝐵, Γ 1 , Γ 2 ⊦ Δ
（CL）（EL）
Γ 1 , 𝐴 ∧ 𝐵, Γ 2 ⊦ Δ
分解と証明の関係（または，後件）
分解
推論規則
（∨ R2）
Γ ⊦ Δ 1 , 𝐴, 𝐵, Δ 2
（ER）
Γ ⊦ Δ 1 , Δ 2 , 𝐴, 𝐴 ∨ 𝐵 Γ ⊦ Δ 1 , Δ 2 , 𝐴 ∨ 𝐵, 𝐴
（ER）
（∨ R1）
Γ ⊦ Δ 1 , Δ 2 , 𝐴 ∨ 𝐵, 𝐴 ∨ 𝐵 Γ ⊦ Δ 1 , Δ 2 , 𝐴 ∨ 𝐵
（CR）（ER）
Γ ⊦ Δ 1 , 𝐴 ∨ 𝐵, Δ 2 Γ ⊦ Δ 1 , 𝐴 ∨ 𝐵, Δ 2
Γ ⊦ Δ 1 , 𝐴, 𝐵, Δ 2
Γ ⊦ Δ, 𝐴 ∨ 𝐵
（∨R1）Γ ⊦ Δ, 𝐴
Γ ⊦ Δ, 𝐴 ∨ 𝐵
（∨R2）Γ ⊦ Δ, 𝐵
Γ ⊦ Δ 1 , Δ 2 , 𝐴, 𝐵
分解と証明の関係（または，前件）
𝐴 ∨ 𝐵, Γ 1 , Γ 2 , Γ 1 , Γ 2 ⊦ Δ, Δ
（∨ L）
Γ 1 , 𝐴, Γ 2 ⊦ Δ Γ 1 , 𝐵, Γ 2 ⊦ Δ
（EL） （EL）
𝐴, Γ 1 , Γ 2 ⊦ Δ 𝐵, Γ 1 , Γ 2 ⊦ Δ
𝐴 ∨ 𝐵, Γ 1 , Γ 2 , Γ 1 , Γ 2 ⊦ Δ
（CR）（EL）
Γ 1 , Γ 1 , Γ 2 , Γ 2 , 𝐴 ∨ 𝐵 ⊦ Δ Γ 1 , Γ 2 , Γ 2 , 𝐴 ∨ 𝐵 ⊦ Δ
（CL）（EL）
Γ 2 , Γ 2 , Γ 1 , 𝐴 ∨ 𝐵 ⊦ Δ
（CL）
Γ 2 , Γ 1 , 𝐴 ∨ 𝐵 ⊦ Δ Γ 1 , 𝐴 ∨ 𝐵, Γ 2 ⊦ Δ
（EL）分解
推論規則
𝐴 ∨ 𝐵, Γ
1, Γ 2 ⊦ Δ 1 , Δ 2
（∨L）
𝐴, Γ 1 ⊦ Δ 1 𝐵, Γ 2 ⊦ Δ 2 Γ 1 , 𝐴 ∨ 𝐵, Γ 2 ⊦ Δ
Γ 1 , 𝐴, Γ 2 ⊦ Δ Γ 1 , 𝐵, Γ 2 ⊦ Δ
分解と証明の関係（ならば，後件）
分解
推論規則
（→R）
𝐴, Γ ⊦ Δ 1 , 𝐵, Δ 2
（ER）
Γ ⊦ Δ 1 , Δ 2 , 𝐴 → 𝐵 Γ ⊦ Δ 1 , 𝐴 → 𝐵, Δ 2
（ER）
𝐴, Γ ⊦ Δ 1 , Δ 2 , 𝐵 Γ ⊦ Δ 1 , 𝐴 → 𝐵, Δ 2
𝐴, Γ ⊦ Δ 1 , 𝐵, Δ 2
Γ ⊦ Δ, 𝐴 → 𝐵
（→R）
𝐴, Γ ⊦ Δ, 𝐵
分解と証明の関係（ならば，前件）
𝐴 → 𝐵, Γ 1 , Γ 2 , Γ 1 , Γ 2 ⊦ Δ, Δ
（→ L）
Γ 1 , Γ 2 ⊦ Δ, 𝐴
Γ 1 , 𝐵, Γ 2 ⊦ Δ 𝐵, Γ 1 , Γ 2 ⊦ Δ
（EL）𝐴 → 𝐵, Γ 1 , Γ 2 , Γ 1 , Γ 2 ⊦ Δ
（CR）（EL）
Γ 1 , Γ 1 , Γ 2 , Γ 2 , 𝐴 → 𝐵 ⊦ Δ Γ 1 , Γ 2 , Γ 2 , 𝐴 → 𝐵 ⊦ Δ
（CL）（EL）
Γ 2 , Γ 2 , Γ 1 , 𝐴 → 𝐵 ⊦ Δ
（CL）
Γ 2 , Γ 1 , 𝐴 → 𝐵 ⊦ Δ Γ 1 , 𝐴 → 𝐵, Γ 2 ⊦ Δ
（EL）分解
推論規則
Γ 1 , 𝐴 → 𝐵, Γ 2 ⊦ Δ
Γ 1 , Γ 2 ⊦ Δ, 𝐴 Γ 1 , 𝐵, Γ 2 ⊦ Δ
𝐴 → 𝐵, Γ 1 , Γ 2 ⊦ Δ 1 , Δ 2
（→L）
Γ 1 ⊦ Δ 1 , 𝐴 𝐵, Γ 2 ⊦ Δ 2
分解と証明の関係（否定，後件）
分解
推論規則
𝐴, Γ ⊦ Δ 1 , Δ 2
（￢R）
Γ ⊦ Δ 1 , ￢ 𝐴, Δ 2 Γ ⊦ Δ 1 , Δ 2 , ￢ 𝐴
（ER）Γ ⊦ Δ 1 , ￢ 𝐴, Δ 2
𝐴, Γ ⊦ Δ 1 , Δ 2
Γ ⊦ Δ, ¬𝐴
𝐴, Γ ⊦ Δ
（￢R）分解と証明の関係（否定，前件）
分解
推論規則
Γ 1 , Γ 2 ⊦ Δ, 𝐴
（￢L）
Γ 1 , ￢ 𝐴, Γ 2 ⊦ Δ
¬𝐴, Γ 1 , Γ 2 ⊦ Δ
（EL）Γ 1 , ￢ 𝐴, Γ 2 ⊦ Δ
Γ 1 , Γ 2 ⊦ Δ, 𝐴
¬𝐴, Γ ⊦ Δ
（￢L）
