Sequent calculus
In proof theory and mathematical logic, the sequent calculus is a widely known deduction system for firstorder logic (and propositional logic as a special case of it). The system is also known under the name LK, distinguishing it from various other systems of similar fashion that have been created later and that are sometimes also called sequent calculi. Another term for such systems in general is Gentzen systems.Since sequent calculi and the general concepts relating to them are of major importance to the whole field of proof theory and mathematical logic, the system LK will be explained in greater detail below. Some familarity with the basic notions of predicate logic (especially its syntactic structure) is assumed.
Table of contents 

The System LK
A (formal) proof in this calculus is a sequence of sequents, where each of the elements is derivable from a number of sequents, that appear earlier in the sequence, by using one of the below rules. An intuitive explanation of these rules is given thereafter. Please do also refer to sequent and rule of inference if you are not familiar with these concepts.
History
The Sequent calculus LK has been introduced by Gerhard Gentzen as a tool for studying natural deduction (which has been around before, although not quite as formal). It has subsequently turned out to be a much more easy to handle calculus when constructing logical derivations. The name itself is derived from the German term Logischer Kalkül, meaning logical calculus. Sequent calculi are the method of choice for many investigations on the subject.
The InferenceRules for LK
The following notation will be used:
 A and B denote formulae of firstorder predicate logic (one may also restrict this to propositional logic),
 Γ, Δ, Σ, and Π are finite (possibly empty) sequences of formulae, called contexts,
 t denotes an arbitrary term,
 A[t] denotes a formula A, in which some occurrences of a term t are of interest
 A[s/t] denotes the formula that is obtained by substituting the term s for the specified occurrences of t in A[t],
 x and y denote variables,
 a variable is said to occur free within a formula if its only occurrences in the formula are not within the scope of quantifiers ∀ or ∃.
Axiom:  Cut:  

(I) 
Γ  A, Δ Σ, A Π 
(Cut) 

Left logical rules:  Right logical rules:  
Γ, A  Δ 
(∧L_{1}) 

Γ, B  Δ 
(∧L_{2}) 
Γ  A, Δ Σ  B, Π 
(∧R) 

Γ, A  Δ Σ, B  Π 
(∨L) 
Γ  A, Δ 
(∨R_{1}) 

Γ  B, Δ 
(∨R_{2}) 

Γ  A, Δ Σ, B  Π 
(→L) 
Γ, A  B, Δ 
(→R) 

Γ  A, Δ 
(¬L) 
Γ, A  Δ 
(¬R) 

Γ, A[t]  Δ 
(∀L) 
Γ  A[y], Δ 
(∀R) 

Γ, A[y]  Δ 
(∃L) 
Γ  A[t], Δ 
(∃R) 

Left structural rules:  Right structural rules:  
Γ  Δ 
(WL) 
Γ  Δ 
(WR) 

Γ, A, A  Δ 
(CL) 
Γ  A, A, Δ 
(CR) 

Γ1, A, B, Γ2  Δ 
(PL) 
Γ  Δ1, A, B, Δ2 
(PR) 
Note: In the rules (∀R) and (∃L), the variable y must not be free within Γ, A[x/y], or Δ.
An Intuitive Explanation
An Example Derivation
As for an example, this is the sequential derivation of (A¬A), known as the Law of excluded middle (tertium non datur in Latin).
 (I) 
AA  
 (¬R) 
¬A, A  
 (R_{2}) 
A¬A, A  
 (PR) 
A, A¬A  
 (R_{1}) 
A¬A, A¬A  
 (CR) 
A¬A 
This derivation also emphasizes the strictly formal structure of a syntactic calculus. For example, the right logical rules as defined above do always act on the first formula of the right sequent, such that the application of (PR) is formally required. This very rigid reaonsing may at first be difficult to understand, but it forms the very core of the difference between syntax and semantics in formal logics. Although we know that we mean the same with the formulae A¬A and ¬AA, a derivation of the latter would not be equivalent to the one that is given above. However, one can make syntactic reasoing more convenient by introducing lemmas, i.e. predefined schemes for achieving certain standard derivations. As an example one could show that the following is a legal transformation:
Γ AB, Δ 

Γ BA, Δ 
Once a general sequence of rules if known for establishing this derivation, one can use it as an abbreviation within proofs. However, while proofs become more readable when using good lemmas, it can also make the process of derivation more complicated, since there are more possible choices to be taken into account. This is especially important when using proof theory (as often desired) for automated deduction.
Structural Rules
The structural rules deserve some additional discussion. The names of the rules are Weakening (W), Contraction (C), and Permutation (P). Contraction and Permutation assure that neither the order (P) nor the multiplicity of occurrences (C) of elements of the sequences do matter. Thus, one could instead of sequences also consider sets.
The extra effort of using sequences, however, is justified since part or all of the structural rules may be omitted. Doing so, one obtains the so called substructural logics.
Properties of the System LK
This system of rules can be shown to be both sound and complete with respect to firstorder logic, i.e. a statement A follows semantically from a set of premisses Γ (Γ = A) iff the sequent Γ  A can be derived by the above rules.
In Sequent calculus, the rule of cut is admissible. This result is also referred to as Gentzen's Hauptsatz ("Main Theorem").
Modifications of the System
The System LJ
Surprisingly, some small changes in the rules of LK suffice in order to turn it into a proof system for intuitionistic logic. To this end, one has to restrict to intuitionistic sequents (i.e. the right contexts are eliminated) and modify the rule (∨L) as follows:
Γ, A  C Σ, B C 
(∨Li) 
The resulting system is called LJ. It is sound and complete with respect to intuitionistic logic and admits a similar cutelimination proof.