Sequent calculus

Definition

Fix a language of predicate logic. A sequent is an expression $\Gamma \vdash \Delta$, where $\Gamma$ and $\Delta$ are finite lists of formulas. The sequent calculus LK has the following parts.

1. Axioms: $A \vdash A$ for each formula $A$.
2. Structural rules: weakening, contraction and exchange on each side, and the cut rule. The cut rule infers $\Gamma, \Pi \vdash \Delta, \Lambda$ from $\Gamma \vdash \Delta, A$ and $A, \Pi \vdash \Lambda$.
3. Logical rules: for each connective and quantifier, rules that introduce it on the left and on the right.

The logical rules for conjunction, disjunction, implication, negation and the quantifiers are these.

• $\wedge$R: from $\Gamma \vdash \Delta, A$ and $\Gamma \vdash \Delta, B$ infer $\Gamma \vdash \Delta, A \wedge B$.
• $\wedge$L: from $A, \Gamma \vdash \Delta$ infer $A \wedge B, \Gamma \vdash \Delta$ and $B \wedge A, \Gamma \vdash \Delta$.
• $\vee$L: from $A, \Gamma \vdash \Delta$ and $B, \Gamma \vdash \Delta$ infer $A \vee B, \Gamma \vdash \Delta$.
• $\vee$R: from $\Gamma \vdash \Delta, A$ infer $\Gamma \vdash \Delta, A \vee B$ and $\Gamma \vdash \Delta, B \vee A$.
• $\to$R: from $A, \Gamma \vdash \Delta, B$ infer $\Gamma \vdash \Delta, A \to B$.
• $\to$L: from $\Gamma \vdash \Delta, A$ and $B, \Pi \vdash \Lambda$ infer $A \to B, \Gamma, \Pi \vdash \Delta, \Lambda$.
• $\neg$R: from $A, \Gamma \vdash \Delta$ infer $\Gamma \vdash \Delta, \neg A$.
• $\neg$L: from $\Gamma \vdash \Delta, A$ infer $\neg A, \Gamma \vdash \Delta$.
• $\forall$R: from $\Gamma \vdash \Delta, A(y)$ infer $\Gamma \vdash \Delta, \forall x\, A(x)$, where the variable $y$ is not free in $\Gamma, \Delta, \forall x\, A(x)$.
• $\forall$L: from $A(t), \Gamma \vdash \Delta$ infer $\forall x\, A(x), \Gamma \vdash \Delta$, where $t$ is a term.
• $\exists$L: from $A(y), \Gamma \vdash \Delta$ infer $\exists x\, A(x), \Gamma \vdash \Delta$, where $y$ is not free in $\Gamma, \Delta, \exists x\, A(x)$.
• $\exists$R: from $\Gamma \vdash \Delta, A(t)$ infer $\Gamma \vdash \Delta, \exists x\, A(x)$, where $t$ is a term.

A derivation is a finite tree of sequents. Each leaf is an axiom, and each other node follows from its children by a rule. The calculus LJ for intuitionistic logic is LK with the restriction that each right side has at most one formula.