3.2 Sequent Calculus

The sequent calculus is a proof system in which reasoning is expressed in terms of sequents, and it makes the structure of logical arguments explicit by separating assumptions from conclusions and by allowing multiple formulas to appear on both sides of a derivation.

A sequent has the form:

where $\Gamma$ and $\Delta$ are finite collections of formulas, and it is understood that $\Gamma$ represents assumptions while $\Delta$ represents possible conclusions.

The intended meaning of a sequent is that whenever all formulas in $\Gamma$ are true under a valuation, at least one formula in $\Delta$ is true under that valuation, so the sequent expresses a form of generalized implication.

Interpretation of Sequents

A sequent:

is interpreted as the statement that:

is valid.

Thus the left side represents a conjunction of assumptions, while the right side represents a disjunction of possible conclusions.

In particular, a sequent of the form:

with a single formula on the right corresponds to the usual notion of entailment.

Axioms

The basic axioms of the sequent calculus are identity sequents of the form:

These express that any formula implies itself, and they serve as the starting point for all derivations.

Structural Rules

The sequent calculus includes rules that manipulate the structure of sequents without involving specific logical connectives.

The weakening rule allows additional formulas to be added:

This rule expresses that adding extra assumptions or extra possible conclusions does not invalidate a valid argument.

The contraction rule allows duplicate formulas to be removed:

This reflects that repeating the same formula does not change its logical effect.

The exchange rule allows formulas to be reordered, reflecting that the order of formulas in $\Gamma$ and $\Delta$ is not significant.

Logical Rules

Each logical connective is governed by rules that describe how it behaves on the left side and on the right side of a sequent.

For conjunction, the right rule states that to prove:

it is enough to prove both:

and:

The left rule states that from:

one may infer:

These rules reflect that a conjunction on the right behaves like a pair of obligations, while a conjunction on the left behaves like two available assumptions.

For disjunction, the right rule states that from:

one may infer:

and similarly from:

The left rule states that if:

and:

then:

This reflects that a disjunction on the left requires reasoning by cases.

For implication, the right rule states that if:

then:

The left rule states that from:

and:

one may infer:

These rules capture the behavior of implication in terms of how assumptions and conclusions interact.

For negation, the rules are derived from implication and falsity, but they can be expressed directly.

The right rule states that if:

then:

The left rule states that if:

then:

These rules express that negation moves formulas from one side of the sequent to the other.

Example 3.5

We derive:

First we use the identity axiom:

Then we apply the implication left rule to use the formula $p \to q$, and we combine this with the assumption $p$.

The structure of the derivation reflects that from $p$ and $p \to q$, the formula $q$ follows.

Cut Rule

The cut rule allows intermediate formulas to be introduced and then eliminated:

This rule expresses that if a formula $A$ can be derived and can also be used to derive the final conclusion, then it can be removed from the proof.

The cut rule is powerful, but one of the central results about the sequent calculus is that it is not necessary.

Theorem 3.6 (Cut Elimination)

Every proof that uses the cut rule can be transformed into a proof that does not use the cut rule.

This result is fundamental because it shows that all derivations can be carried out using only the basic rules, and it leads to important consequences such as consistency and normalization.

Proof Idea

The proof proceeds by transforming a derivation step by step, eliminating occurrences of the cut rule by pushing them upward in the proof tree until they can be removed.

At each stage, the structure of the proof is simplified, and eventually all cuts are eliminated.

The process is finite because formulas have finite structure, and each transformation reduces the complexity of the proof in a well defined sense.

Properties of the System

The sequent calculus has a clear symmetry between the left and right sides of sequents, and this symmetry reflects the dual roles of assumptions and conclusions.

It also makes structural properties explicit, such as weakening and contraction, which are often implicit in other proof systems.

Because of its explicit structure, the sequent calculus is well suited for studying meta theoretical properties of logic, including consistency, completeness, and normalization, and it plays a central role in proof theory.