Linear Logic - Sequent Calculus Presentation

Sequent Calculus Presentation

One way of defining linear logic is as a sequent calculus. We use the letters Γ and Δ to range over list of propositions A₁, ..., A_n, also called contexts. A sequent places a context to the left and the right of the turnstile, written Γ Δ. Intuitively, the sequent asserts that the conjunction of Γ entails the disjunction of Δ (though we mean the "multiplicative" conjunction and disjunction, as explained below). Girard describes classical linear logic using only one-sided sequents (where the left-hand context is empty), and we follow here that more economical presentation.

We now give inference rules describing how to build proofs of sequents.

First, to formalize the fact that we do not care about the order of propositions inside a context, we add the structural rule of exchange:

(Alternatively we could accomplish the same thing by defining contexts to be multisets rather than lists.) Note that we do not add the structural rules of weakening and contraction, because we do care about the absence of propositions in a sequent, and the number of copies present.

Next we add initial sequents and cuts:

The cut rule can be seen as a way of composing proofs, and initial sequents serve as the units for composition. In a certain sense these rules are redundant: as we introduce additional rules for building proofs below, we will maintain the property that arbitrary initial sequents can be derived from atomic initial sequents, and that whenever a sequent is provable it can be given a cut-free proof. Ultimately, this canonical form property (which can be divided into the completeness of atomic initial sequents and the cut-elimination theorem, inducing a notion of analytic proof) lies behind the applications of linear logic in computer science, since it allows the logic to be used in proof search and as a resource-aware lambda-calculus.

Now, we explain the connectives by giving logical rules. Typically in sequent calculus one gives both "right-rules" and "left-rules" for each connective, essentially describing two modes of reasoning about propositions involving that connective (e.g., verification and falsification). In a one-sided presentation, one instead makes use of negation: the right-rules for a connective (say ⅋) effectively play the role of left-rules for its dual (⊗). So, we should expect a certain "harmony" between the rule(s) for a connective and the rule(s) for its dual.