Left Rule

In Sequent Calculus, a left rule corresponds to an Elimination Rule for a connective. However, such rules need to be flipped "upside down" from their usual presentation in Natural Deduction.

For instances, the normal elimination rules for Conjunction as a Negative Connective are

Γ⊢A∧BΓ⊢AprovesΓ𝐴𝐵provesΓ𝐴\displaystyle\frac{\Gamma\vdash A\land B}{\Gamma\vdash A}
Γ⊢A∧BΓ⊢BprovesΓ𝐴𝐵provesΓ𝐵\displaystyle\frac{\Gamma\vdash A\land B}{\Gamma\vdash B}

The corresponding left rules are

Γ,A∧B,A⊢ΔΓ,A∧B⊢ΔprovesΓ𝐴𝐵𝐴ΔprovesΓ𝐴𝐵Δ\displaystyle\frac{\Gamma,A\land B,A\vdash\Delta}{\Gamma,A\land B\vdash\Delta}
Γ,A∧B,B⊢ΔΓ,A∧B⊢ΔprovesΓ𝐴𝐵𝐵ΔprovesΓ𝐴𝐵Δ\displaystyle\frac{\Gamma,A\land B,B\vdash\Delta}{\Gamma,A\land B\vdash\Delta}