Sequent

logic sequent-calculus

Definition

Sequent

A sequent is a very general kind of conditional assertion of form

$$A_1,A_2,\dots A_m⊢B_1,B_2,\dots ,B_n$$

A sequent may have any number $m$ of condition formulas $A_i$, the antecedents, and any number $n$ of asserted formulas $B_j$, called consequents. A sequent is understood to mean that if all of the antecedent conditions are true, then at least one of the consequent formulas is true.

General form: $\Gamma ⊢\Sigma$

Left vs. Right

Sequent rules are often split into two categories “left” and “right”.

Right Rule

A right rule explains how to build this connective when it’s your goal (on the right of $⊢$).

$$\frac{\Gamma ⊢A\Delta ⊢B}{\Gamma ,\Delta ⊢A\otimes B}(\otimes R)$$

From Multiplicative Conjunction.

Left Rule

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

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

From Multiplicative Conjunction.