D e f i n i t i o n
e f i n i t i o n
↓
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_{1} , ..., A_{m} |- B_{1} , ..., B_{n} corresponds to the formula:
A_{1} & ... &A_{m} |- B_{1} ∨ ... ∨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.

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 ⊃ ⊥
P r o o f T h e o r y
r o o f T h e o r y
↑
↓
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.

S a m p l e D e r i v a t i o n s
a m p l e D e r i v a t i o n s
↑
↓
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 |- 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

F o r m u l a t i o n s
o r m u l a t i o n s
↑
↓
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.