Sequent calculus Glossary
Definition
The sequent calculus is a deductive system in which sequents are derived directly from other sequents. In these notes, we consider the standard such presentation of classical logic, which uses a notion of sequent with a set of premises on the left and a set of conclusions (rather than a single conclusion) on the right. In contrast with natural deduction, the sequent calculus gives each connective or quantifier an introduction rule on the left of the sequent as well as one on the right. The left-side introduction rules replace the right-side elimination rules found in natural deduction.
Comments
The sequent calculus can be seen as little more than a notational variant of the semantic tableau method, though it is normally associated with the ideas of derivation and proof rather than with reasoning about interpretations. It therefore constitutes a unified theory, drawing together the deduction-theoretic and semantic approaches to logic.
In order to be sure that the sequent calculus delivers a consequence relation, it is necessary to establish that an appropriate version of the rule of extended transitivity, known as "cut", holds for it. This is a non-trivial result, generally requiring a detailed and case-ridden proof.
Examples
-
Proof of a sequent in propositional logic:
p ⊢ q, p ⊢ IMP ⊢ p IMP q, p p ⊢ p IMP ⊢ (p IMP q) IMP p ⊢ p -
Proof of a sequent in first order predicate logic: