Why use sequents

logicmotivationproof-theorysequent-calculus

In the sequent calculus, the building blocks of a proof are inference rules, which are rules for inferring the validity of certain sequents from other sequents, something like this:

$$\frac{\vec\varphi_1\vdash\vec\psi_1 \qquad \vec\varphi_2\vdash\vec\psi_2}{\vec\varphi_3\vdash\vec\psi_3}$$

However, why sequents, not just propositions?

$$\frac{P \qquad Q}{R}$$

What is the motivation for sequents?

Best Answer

When dealing with abstract representations of proofs, it is important to distinguish between hypotheses and conclusions. This is why the turnstile symbol $\vdash$ is used: on its left there are the hypotheses, on its right the conclusions. Note that the turnstile $\vdash$ is not a connective (it is not part of the object language), and the intuitive meaning of a sequent $A_1, \dots, A_n \vdash B_1, \dots, B_m$ is "there is a derivation from the hypothesis $A_1 \land \dots \land A_n$ to the conclusion $B_1 \lor \dots \lor B_m$". A sequent talks about derivability of something from something else.

Technically, this distinction between hypotheses and conclusions is needed by inference rules such one the one to introduce the connective $\to$ (implication), which changes not only the conclusions but also the hypotheses. Indeed, the "direct" way to prove a sentence of the form $A \to B$ is to have a derivation $\pi$ with hypothesis $A$ and conclusion $B$; from this derivation $\pi$ you can discharge the hypothesis $A$ (i.e. $A$ is not an hypothesis any more) and conclude $A \to B$.

Formally, in the sequent calculus, this is represented by the inference rule $\to_\mathrm{R}$ (right introduction of the implication)
\begin{align} \frac{\Gamma, A \vdash B, \Delta}{\Gamma \vdash A \to B, \Delta}\to_R \end{align}


It is clear that on the left of the turnstile a finite set of formulas is required (technically, it can be a finite multiset or a finite sequence): these formulas represent the hypotheses, which can be several.

For technical reasons, at least in classical logic, it is crucial$^*$ that there is a finite set (or more precisely, a finite multiset or a finite sequence) of formulas also on the right of the turnstile, for the conclusions. Indeed, inference rules such as \begin{align} \frac{\Gamma \vdash A, B, \Delta}{\Gamma \vdash A \lor B, \Delta}\lor_R \qquad \frac{\Gamma\vdash A, A, \Delta}{\Gamma \vdash A, \Delta}\mathrm{ctr}_R \end{align} (where it is important to have more than one formula on the right of the turnstile) distinguish the sequent calculus for classical logic from the one for weaker logics such as intuitionistic.


${}^*$ More precisely, it is crucial if you don't want to lose good structural properties of your proof system, such as symmetry between left and right, analiticity with the subformula property and cut-elimination.

Related Question