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

Definition

Right Sequent

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

Example: (from Multiplicative Conjunction)

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

Link to original

Left Rule

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)$$

Link to original