Left Sequent

sequent-calculus

Definition

Left Sequent

In sequent calculus, a left sequent rule explains how to use/deconstruct this connective when it’s available as an assumption (on the left of $⊢$).

Example: (from Multiplicative Conjunction)

$$\frac{\Gamma ,A,B⊢C}{\Gamma ,A\otimes B⊢C}(\otimes L)$$