Logical formulas are expressions constructed from predicate symbols and variables as their arguments with using connectives & (and), ∨ (or), ⊃ (implication), ¬ (negation), and quantifiers ∀ (universal), ∃ (existential). Yet another connective ∼ (equivalence) is defined via others as A ∼ B = (A ⊃ B) & (B ⊃ A). Click here to read about negation dependency. Optionally, terms constructed with using object functions and constants may be allowed as arguments of predicate symbols.

Sequents are expressions of the form Γ |- Δ, where Γ and Δ are (possibly empty) sequences of logical formulas. Γ is called the antecedent and Δ is called the consequent. A formal theory in which axioms and inference rules are formulated in terms of sequents is called sequent calculus. In fact, there are several sequent calculi; these variants will be discussed later in section Formulations. The informal understanding of sequents is that the sequent A₁, ..., A_m |- B₁, ..., B_n corresponds to the formula: A₁& ... &A_m |- B₁∨ ... ∨B_n

The only axiom schema of sequent calculus is A |- A, where A is any logical formula. There are two sorts of inference rules in sequent calculus: structural and logical. Every logical rule corresponds to a connective or quantifier. There are at least two logical rules for every propositional connective and every quantifier. One of them applies to the antecedent, whereas the other applies to the consequent. Further on, Greek letters denote sequences of formulas, and English letters denote individual logical formulas.

S t r u c t u r a l	Thinning (Weakening)	Γ |- Δ --------- A, Γ |- Δ				Γ |- Δ --------- Γ |- Δ, A
	Contraction	A, A, Γ |- Δ ----------- A, Γ |- Δ				Γ |- Δ, A, A ----------- Γ |- Δ, A
	Exchange	Π, A, B, Γ |- Δ -------------- Π, B, A, Γ |- Δ				Γ |- Σ, A, B, Δ -------------- Γ |- Σ, B, A, Δ
	Cut		Γ |- Δ, C C, Σ |- Π ---------------------- Γ, Σ |- Δ, Π
L o g i c a l	Conjunction	A, Γ |- Δ B, Γ |- Δ --------- --------- A&B, Γ |- Δ A&B, Γ |- Δ				Γ |- Δ, A Γ |- Δ, B ---------------------- Γ |- Δ, A&B
	Disjunction	A, Γ |- Δ B, Γ |- Δ ---------------------- A∨B, Γ |- Δ				Γ |- Δ, A Γ |- Δ, B --------- --------- Γ |- Δ, A∨B Γ |- Δ, A∨B
	Implication	Γ |- Δ, A B, Σ |- Π ---------------------- A⊃B, Γ, Σ |- Δ, Π				A, Γ |- Δ, B ----------------- Γ |- Δ, A⊃B
	Negation	A, Γ |- Δ ---------------- Γ |- Δ, ¬A				Γ |- Δ, A ---------------- ¬A, Γ |- Δ
	Universal Quantifier	A(t), Γ |- Δ ---------------- ∀x A(x), Γ |- Δ				Γ |- Δ, A(a) ---------------- Γ |- Δ, ∀x A(x)
	Existential Quantifier	A(a), Γ |- Δ ---------------- ∃x A(x), Γ |- Δ				Γ |- Δ, A(t) ---------------- Γ |- Δ, ∃x A(x)

In these inference rules, Γ, Δ, Σ, Π are finite lists of formulas, A and B are any formulas, x, a, t are any variables. If terms are allowed, then t is any term. A(a) and A(t) are obtained from A(x) by replacing all free occurrences of x by a and t, respectively. The variables a and t are free in A(a) and A(t), respectively. If t is a term, then all variable occurrences in it are free in A(t). The variable a, which occurs in the ∀-succedent rule and the ∃-antecedent rule, is called eigenvariable. It may not occur free in the lower sequents of the respective rules.

Derivations (or proofs) in sequent calculus consist of sequents arranged in tree form. The bottommost sequent of a derivation is called endsequent. Formula F is derivable in sequent calculus if sequent |- F is derivable. The formulas in the lower sequents of the inference rules containing a logical symbol (connective or quantifier) are called principal formulas. The formulas in the upper sequent(s) that are constituents of the respective principal formula are called side formulas.

Sequent calculus was introduced by G. Gentzen. Sequent calculus with the above inference rules specifies classical first-order logic. The same framework can also be used to specify intuitionistic logic. In order to limit derivations to intuitionistic ones, one constraint is added: every succedent may have not more than one formula. The classical (multi-succedent) variant of sequent calculus is called LK. The intuitionistic (single-succedent) variant is called LJ.

It is actually sufficient to have the axiom schema applicable to atoms only. Given that, it can be proved that it would be applicable to all formulas then. The proof is by induction on the size of formulas. Induction base: it is satisfied by the premise. Iduction step: We have to prove that if the axiom schema holds for formulas A and B, then it holds for ¬A, A&B, A∨B, A⊃B, and if the axiom schema holds for formula A(x) then it does for ∀x A(x) and ∃x A(x).   to see derivations confirming this.

A |- A          B |- B                     A |- A          B |- B
-------         -------                    -------         -------
A&B |- A        A&B |- B                   A |- A∨B        B |- A∨B
-----------------------                    -----------------------
      A&B |- A&B                                A∨B |- A∨B

        *           *           *           *           *

A |- A                                     A |- A          B |- B
------                                     ----------------------
¬A, A |-                                        A, A⊃B |- B
-------                                         ----------
¬A |- ¬A                                        A⊃B |- A⊃B

        *           *           *           *           *

A(a) |- A(a)                               A(a) |- A(a)
------------                               ------------
∀x A(x) |- A(a)                            A(a) |- ∃x A(x)
-----------------                          -----------------
∀x A(x) |- ∀x A(x)                         ∃x A(x) |- ∃x A(x)

Derivations in sequent calculus are normally very concise and economical. They are built out of components of the resulting formula. It especially applies to derivations without the cut rule. See next section Proof Theory for more information on this. This compactness of proofs in sequent calculus is in a sharp contrast with Hilbert-style proofs. In sequent calculus, every inference rule relates to one connective or quantifier only. In the Hilbert-style formulation of first-order logic, the choice of axiom schemas is not quite intuitive. Especially, axiom schemas releated to implication are obscure. Single Hilbert-style axiom schemas contain multiple occurrences of connectives. As a result, proofs of even very simple facts require detours or use of previously derived facts.

Section Sample Derivations below contains multiple examples conforming the claim of compatness of Gentzen-style proofs. Due to the orderly set of inference rules and thus direct proofs, sequent calculus is a favorite tool for proof theorists and an excellent framework for automatic theorem proving. In our examples, the cut rule will not be used at all. Also, multi-formula succedents will appear only in the derivations that do not hold intuitionistically.

Derivation of the Law of Excluded Middle (A∨¬A) is given on the right. Since it is classical-only law and does not hold intuitionistically, presence of mutiple formulas in succedents is unavoidable.		>	A |- A -------- |- A, ¬A --------- -------------- |- A∨¬A, A∨¬A ------------- |- A∨¬A
A(a,b) |- A(a,b) -------- ∀y A(a,y) |- A(a,b) --------- ∀y A(a,y) |- A(a,b) --------- ∀x ∀y A(x,y) |- A(a,b) --------- -------------- ∀x ∀y A(x,y) |- ∀y ∀x A(x,y)
	<	Here is another sample derivation on the left: alteration of universal quantifiers. Of course, a similar property holds for the existential quantifier too, and its proof is symmetrical to this one.

In order to define sequent calculus with logical constants ⊤ (true) and ⊥ (false), the two following axioms should be added:

|- ⊤

⊥ |-

In presence of logical constants, negation can be defined as the following: ¬A = A ⊃ ⊥

Cut Elimination (Hauptsatz): Perhaps the most most important feature of sequent calculus is the fact that the cut rule is admissible, i.e. it can be eliminated from derivations without affecting the set of derivable formulas. Note that cut elimination works for both classical and intuitionistic variants of sequent calculus. The cut elimination theorem, also called the 'Hauptsatz', states that every sequent calculus derivation can be transformed into another derivation with the same endsequent and in which the cut rule does not occur. This theorem basically gives an algorithm for turning derivations into equivalent derivations without cut.

Proof of the Hauptsatz is quite complicated. It is carried out by double induction. A variant of the cut rule called mix is introduced for the sake of this proof. The main idea of the proof is to swap the mix rule with its predecessor rules. The mix rules whose one upper sequent is an axiom can be eliminated. If you are interested to read the complete proof, click here. Availability of the cut rule makes shorter proofs possible. The cut elimination process defined in the proof may lead to a very significant increase in the size of derivations.

Subformula Property: The most important corollary of the cut elimination theorem is so-called subformula property: all derivations without cuts posses the sub-formula property that all formulas occurring in a derivation are sub-formulas of the formulas from the endsequent. Note that if formula F contains ∀x A(x) or ∃x A(x), then A(t) is also considered a subformula for any term t such that all its variables are free in A(t).

Sharpened Hauptsatz: Another important theorem about sequent calculus is called sharpened Hauptsatz. Sharpened Hauptsatz applies to the classical variant of sequent calculus only. This theorem states that any derivation can be transformed into another derivation with the same endsequent and having the following properties.
- it has no cuts.
- it contains a so-called midsequent whose derivation contains no quantifiers, and the only inference rules occurring in the derivation below the midsequent are the ∀, ∃ rules and structural rules.

Sign Property: The notion of positive and negative subformulas can generalized to define positive and negative parts of sequents. For sequent Γ |- Δ, if A is a formula from Δ, then its positive (negative) subformulas are considered positive (negative) in this sequent. If formula B is from Γ, then the signs of its subformulas are reversed. Another, much lesser known property of sequent calculus is so-called sign property. It states that each ancestor of any positive (negative) part of sequent Γ |- Δ in its derivation is also positive (negative). One interesting corollary of the sign property is that any atom P has only positive or only negative occurrences in derivable formula F, then axioms P |- P can never appear in any derivation of F.

Constructing derivations in sequent calculus may be somewhat confusing at first. But many agree that once you master derivation search skills, it is actually easier to find a sequent-based derivations than a Hilbert-type proofs. A number of sample derivations are collected and presented in here in order to help with this process of mastering derivation search skills. Actually, presentation of examples of sequent calculus derivations was a primary motivation for creating this page because such examples are hard to find anywhere including monographs in proof theory.

Deliberately, the cut rule is not used in the examples; neither are multi-formula succedents in the derivations holding intuitionistically. You will see that all the presented proofs are very direct and compact. And when compiling these derivations, I did not make any selection. I picked some well-known logical laws and then built their derivations - nothing was sieved out.

Note that only logical rules are shown in the sample derivations below. Thinnings, exchanges and contractions are normally combined with logical rules, or multiple structural rules are grouped as one rule.

(¬A∨B) ∼ (A⊃B)

A |- A          B |- B
--------        --------
¬A, A |- B      B, A |- B
------------------------

      ------------
      ¬A∨B |- A⊃B



A |- A      B |- B
------------------
  A⊃B, A |- B
  ------------

  --------------
  A⊃B |- ¬A∨B, B
  ----------------
  A⊃B |- ¬A∨B, ¬A∨B
  -------------
  A⊃B |- ¬A∨B

¬( A & B ) ∼ ( ¬A ∨ ¬B )

A |- A          B |- B
----------      ----------
¬A, A, B |-     ¬B, A, B |-
-------------------------
      ¬A∨¬B, A, B |-
      --------------
      ¬A∨¬B, A&B, B |-
      --------------
      ¬A∨¬B, A&B |-
      --------------
      ¬A∨¬B |- ¬(A&B)



A |- A          B |- B
----------      ----------
A, B |- A       A, B |- B
-------------------------
      A, B |- A&B
      --------------
      ¬(A&B), A, B |-
      --------------
      ¬(A&B), B |- ¬A
      --------------
      ¬(A&B) |- ¬A, ¬B
      ----------------

      ---------------------
      ¬(A&B) |- ¬A∨¬B, ¬A∨¬B
      --------------------
      ¬(A&B) |- ¬A∨¬B

¬( A ∨ B ) ∼ ( ¬A & ¬B )

A |- A            B |- B
----------        ----------
A |- A∨B          B |- A∨B
----------        -----------
¬(A∨B), A |-      ¬(A∨B), B |-
------------      -------------
¬(A∨B) |- ¬A      ¬(A∨B) |- ¬B
    -------------------------
      ¬(A∨B) |- ¬A&¬B



A |- A            B |- B
--------          -------
¬A, A |-          ¬B, B |-
--------          --------
¬A&¬B, A |-       ¬A&¬B, B |-
--------------------------
   A∨B, ¬A&¬B |-
   -------------
   ¬A&¬B |- ¬(A∨B)

( (A⊃B) & (B⊃C) ) ⊃ (A⊃C)

A |- A       B |- B
------------------
A⊃B, A |- B         C |- C
--------------------------

      ---------------
      A⊃B, B⊃C |- A⊃C
      ---------------
      (A⊃B)&(B⊃C), B⊃C |- A⊃C
      -----------------------------
      (A⊃B)&(B⊃C), (A⊃B)&(B⊃C) |- A⊃C
      ---------------------------
      (A⊃B)&(B⊃C) |- A⊃C

(A⊃B) ⊃ ((A⊃¬B) ⊃ ¬A)

              A |- A      B |- B
              -----------------
                A⊃B, A |- B
                ------------
A |- A          ¬B, A⊃B, A |-
----------------------------

   ---------------
   A⊃¬B, A⊃B |- ¬A
   ----------------
   A⊃B |- (A⊃¬B) ⊃ ¬A

∃x (A(x)⊃B) ∼ (∀x A(x) ⊃ B)

A(a) |- A(a)
-----------
∀x A(x) |- A(a)        B |- B
----------------------------
A(a)⊃B, ∀x A(x) |- B
----------------------

-------------------------
∃x (A(x)⊃B) |- ∀x A(x) ⊃ B



A(a) |- A(a)
-----------
A(a) |- A(a), B
--------------
 |- A(a), A(a)⊃B
---------------
 |- A(a), ∃x (A(x)⊃B)
----------------
 |- ∀x A(x), ∃x (A(x)⊃B)     B |- B
----------------------------------
∀x A(x)⊃B |- ∃x (A(x)⊃B), B
----------------------------------

------------------------------------
∀x A(x)⊃B |- ∃x (A(x)⊃B), ∃x (A(x)⊃B)
-----------------------------------
∀x A(x)⊃B |- ∃x (A(x)⊃B)

(∃x (A(x)∨B(x)) ∼ (∃x A(x) ∨ ∃x B(x))

A(a) |- A(a)                    B(a) |- B(a)
-----------                     -----------
A(a) |- ∃x A(x)                B(a) |- ∃x B(x)
-------------                   ---------------
A(a) |- ∃x A(x) ∨ ∃x B(x)     B(a) |- ∃x A(x) ∨ ∃x B(x)
-----------------------------------------------------

    ------------------------------------
    ∃x (A(x)∨B(x) |- ∃x A(x) ∨ ∃x B(x)



A(a) |- A(a)                    B(a) |- B(a)
------------                    ------------
A(a) |- A(a)∨B(a)               B(a) |- A(a)∨B(a)
----------------                -----------------
A(a) |- ∃x (A(x)∨B(x))         B(a) |- ∃x (A(x)∨B(x))
----------------------          ----------------------
∃x A(x) |- ∃x (A(x)∨B(x))     ∃x B(x) |- ∃x (A(x)∨B(x))
-----------------------------------------------------

¬∃x A(x) ∼ ∀x ¬A(a)

A(a) |- A(a)
----------
A(a) |- ∃x A(x)
----------

---------------
¬∃x A(x) |- ¬A(a)
---------------
¬∃x A(x) |- ∀x ¬A(a)



A(a) |- A(a)
----------
¬A(a), A(a) |-
-----------
∀x ¬A(x), A(a) |-
-------------------

-------------------
∀x ¬A(x) |- ¬∃x A(a)

(∃x A(x) ⊃ ∀x B(x)) ⊃ (∀x (A(x) ⊃ B(x)))

A(a) |- A(a)        B(a) |- B(a)
----------          ----------
A(a) |- ∃x A(x)    ∀x B(x) |- B(a)
--------------------------------

  --------------------------------
  ∃x A(x) ⊃ ∀x B(x) |- A(a) ⊃ B(a)
  -----------------------------------
  ∃x A(x) ⊃ ∀x B(x) |- ∀x (A(x) ⊃ B(x))

Many other logic formulations based on sequents have been introduced subsequently. First, Gentzen proved that the classical sequent calculus (LK) can alternatively be defined as single-succedent calculus augmented with the law of excluded middle as yet another axiom scheme. Again, it is sufficient to allow the law of excluded middle in application to atoms only because this law can be derived for the other formulas then. Note that Hauptsatz does not hold in this alternative calculus, i.e. the cut rule is not admissible when the additional axioms are in use.

Sequent calculus formulation G4 introduced by Kleene is perhaps the most known formulation after the Gentzen's. Kanger's system LC is similar to G4. There are only logical axioms in G4. The exchange rule is compensated for by considering unordered lists of formulas in antecedents and succedents and by the possibility to apply the inference rules to any formula in these lists. The axioms in G4 have the form: A, Γ |- Δ, A where Γ and Δ are any lists of formulas. This form of axioms eliminates the need for thinning (weakening). The contraction rule is compensated for by different logical rules.

Conjunction	A, B, Γ |- Δ ------------ A&B, Γ |- Δ			Γ |- Δ, A Γ |- Δ, B ---------------------- Γ |- Δ, A&B
Disjunction	A, Γ |- Δ B, Γ |- Δ ---------------------- A∨B, Γ |- Δ			Γ |- Δ, A, B ------------ Γ |- Δ, A∨B
Implication	Γ |- Δ, A B, Γ |- Δ ---------------------- A⊃B, Γ |- Δ			A, Γ |- Δ, B ------------ Γ |- Δ, A⊃B
Negation	A, Γ |- Δ ---------- Γ |- Δ, ¬A			Γ |- Δ, A ---------- ¬A, Γ |- Δ
Universal Quantifier	A(t), ∀x A(x), Γ |- Δ ------------------- ∀x A(x), Γ |- Δ			Γ |- Δ, A(a) -------------- Γ |- Δ, ∀x A(x)
Existential Quantifier	A(a), Γ |- Δ -------------- ∃x A(x), Γ |- Δ			Γ |- Δ, ∃x A(x), A(t) ------------------ Γ |- Δ, ∃x A(x)

The notes about x, a, t from the Gentzen's formulation apply here too. Note though that this formulation relies on usage of multiple formulas in succedents - see the ∨-succedent rule. Therefore, it is adequate for specification of classical first-order logic only.

Automated deduction or automated theorem proving greatly benefited from the invention of sequent calculus. Sequent calculus is is a convenient tool for for designing algorithms conducting proof search. Infereence rules can be used backward for this purpose. To prove a formula F, one can start from sequent |- F and proceed upward from level to level. For each sequent, the sequents of the next level above this sequents can be effectively determined.

System G4 is much more adequate as a framework for automatic proof search for a number of reasons. First, the absence of structural rules eliminates a lot of unnecessary branches in automatic search. Given that cut is admissible in all reasonable formulations, absence of contraction is most important because upward application of the contraction rule translates into loops in proof search procedures. Second, the &-antecedent and ∨-succedent rules of G4 are invertible in contrast to the Gentzen's rules, i.e. derivability of the lower sequent implies derivability of the upper sequent.

One of the most difficult problems in automatic proof search is instantiating varibles in the application of the ∀-antecedent and ∃-succedent rules. See this paper for further information on this topic.

As mentioned earlier, G4 is good for classical logic only. Nevetheless, there are other formulations for intuitionistic logic, which possess properties necessary for automated proof search. G4i is one such formulation. G4i is free of structural rules. In order to completely eliminate looping in automated proof search, G4i employs multiple variants of the ⊃-antecedent rule. Every variant corresponds to one type of the first argument of the implication. These types are defined by the top connective/quantifier.

Another remarkable but lesser known proof search technique based on sequent calculus is the inverse method by Maslov. The inverse method is a forward proof search exploiting the subformula property and dealing with so-called signed formulas. See this paper for further information on the inverse method.