Sequent Calculus - Introduction

Introduction

One way to classify different styles of deduction systems is to look at the form of judgments in the system, i.e., which things may appear as the conclusion of a (sub)proof. The simplest judgment form is used in Hilbert-style deduction systems, where a judgment has the form

where is any formula of first-order-logic (or whatever logic the deduction system applies to, e.g., propositional calculus or a higher-order logic or a modal logic). The theorems are those formulae that appear as the concluding judgment in a valid proof. A Hilbert-style system needs no distinction between formulae and judgments; we make one here solely for comparison with the cases that follow.

The price paid for the simple syntax of a Hilbert-style system is that complete formal proofs tend to get extremely long. Concrete arguments about proofs in such a system almost always appeal to the deduction theorem. This leads to the idea of including the deduction theorem as a formal rule in the system, which happens in natural deduction. In natural deduction, judgments have the shape

where the 's and are again formulae and . In words, a judgment consists of a list (possibly empty) of formulae on the left-hand side of a turnstile symbol "", with a single formula on the right-hand side. The theorems are those formulae such that (with an empty left-hand side) is the conclusion of a valid proof. (In some presentations of natural deduction, the s and the turnstile are not written down explicitly; instead a two-dimensional notation from which they can be inferred is used).

The standard semantics of a judgment in natural deduction is that it asserts that whenever, etc., are all true, will also be true. The judgments

are equivalent in the strong sense that a proof of either one may be extended to a proof of the other.

Finally, sequent calculus generalizes the form of a natural deduction judgment to

a syntactic object called a sequent. The formulas on left-hand side of the turnstile are called the antecedent, and the formulas on right-hand side are called the succedent; together they are called cedents. Again, and are formulae, and and are nonnegative integers, that is, the left-hand-side or the right-hand-side (or neither or both) may be empty. As in natural deduction, theorems are those where is the conclusion of a valid proof. The empty sequent, having both cedents empty, is defined to be false.

The standard semantics of a sequent is an assertion that whenever every is true, at least one will also be true. One way to express this is that a comma to the left of the turnstile should be thought of as an "and", and a comma to the right of the turnstile should be thought of as an (inclusive) "or". The sequents

are equivalent in the strong sense that a proof of either one may be extended to a proof of the other.

At first sight, this extension of the judgment form may appear to be a strange complication — it is not motivated by an obvious shortcoming of natural deduction, and it is initially confusing that the comma seems to mean entirely different things on the two sides of the turnstile. However, in a classical context the semantics of the sequent can also (by propositional tautology) be expressed either as

(at least one of the As is false, or one of the Bs is true) or as

(it cannot be the case that all of the As are true and all of the Bs are false). In these formulations, the only difference between formulae on either side of the turnstile is that one side is negated. Thus, swapping left for right in a sequent corresponds to negating all of the constituent formulae. This means that a symmetry such as De Morgan's laws, which manifests itself as logical negation on the semantic level, translates directly into a left-right symmetry of sequents — and indeed, the inference rules in sequent calculus for dealing with conjunction (∧) are mirror images of those dealing with disjunction (∨).

Many logicians feel that this symmetric presentation offers a deeper insight in the structure of the logic than other styles of proof system, where the classical duality of negation is not as apparent in the rules.