Sequent Calculus for Linear Logic

Notes for CS 358, Spring 1995

April 19 Lecture

1 Intuitive Explanation of Connectives

The central concept of linear logic is illustrated by linear implication, written A−∘B. Negation is written as a post-fix operation, A^{⊥}. The four remaining propositional connectives are two forms of conjunction, ⊗ and & , and two forms of disjunction, ℘ and ⊕.

A−∘B Using A exactly once, we can obtain B:

A process that consumes one A, then produces one B then halts.

A^{⊥}  A negative resource (or debt) that cancels A:

A process that can consume exactly one A and then halt.

A ⊗ B Presence of resources A and B:

A process that can produce exactly one A and one B and then halt.

A & B Choice between resources A and B:

A process with two push-buttons, one labeled A, the other B. If we push A, exactly one A will be produced before halting, similarly for B

A ⊕ B One of A and B

A process that will produce A or B and then halt. (A black box that might contain either a process that produces an A or a process that produces a B.)

A℘B Resources A or B, in the situation that if not one then the other:

A process that outputs A if the negation of B is given, otherwise B if the negation of A.

Using this process intuition, we can anticipate the provability or non-provability of various sequents:

(A ⊗ (A−∘B))−∘B. If we are given A ⊗ (A−∘B), then we can wire the A process so that it’s output goes into the A−∘B, resulting in the consumption of A and final output of B.

(A⊗(A−∘B)⊗(A−∘C))−∘B ⊗C should not be provable, by conservation of resources. If we are given A, A−∘B and A−∘C processes, then we can either feed the output of the A process into A−∘B or into A−∘C, but not both.

(A ⊗ A ⊗ A ⊗ (A−∘B) ⊗ (A−∘C))−∘B ⊗ C also fails. We can convert one A to B, one A to C, but this leaves one extra A left over. (A ⊗ (A−∘B))−∘B.

A^{⊥} ℘A. This specifies a process that is able to output A or A^{⊥}, but need not decide which until it interacts with its environment. If presented with A, which is the negation of A^{⊥}, then the possibility of outputing A^{⊥} is disabled and the output must be A. Conversely, if presented with A^{⊥}, the output must be A^{⊥}. We can easily construct such a process as simply a “wire” or “channel” that outputs its input.

According to standard terminology, the forms of conjunction and disjunction can be divided into two categories, as shown in this table.

Multiplicative Additive
Conjunction  ⊗  &
Disjunction  ℘  ⊕

Intuitively, “multiplicative” connectives have the flavor of “partitioning of resources,” i.e., both conjuncts or disjuncts may be obtained, by a process that divides available resources into those needed for each result. On the other hand, “additive” connectives intuitively involve some “choice between resources,” so that either or both results may be obtained, by some process that chooses which to produce. This informal explanation is probably very hard to make sense of in the abstract; it is best to look carefully at each of the rules and form your own intuition from the definition of the logic itself.

We may treat implication as a derived form

A−∘B {def \atop =} A^{⊥} ℘B

and restrict negation as discussed below.

The remaining propositional operators are modalities ! and ?, with the following intuitive explanations.

!A As much A as we want:

A process that will produce A as many times as required to satisfy other processes that take A as input.

?A dual to !A:

A process that will input A^{⊥} as many times as required to satisfy other processes that output A^{⊥}.

2 Negation

Some analysis of the proof system will be simpler if we treat negation as a derived form, allowing negation only on propositional symbols or, in the first-order case, atomic formulas. This approach makes termination of the cut-elimination procedure easier to establish by restricting the use of the negation rule.

(p_{i})^{⊥} =^{Δ} p_{i}^{⊥}  (p_{i}^{⊥})^{⊥} =^{Δ} p_{i}
(A ⊗ B)^{⊥} =^{Δ} B^{⊥}℘A^{⊥}  (A℘B)^{⊥} =^{Δ} B^{⊥} ⊗ A^{⊥}
(A ⊕ B)^{⊥} =^{Δ} A^{⊥} & B^{⊥}  (A & B)^{⊥} =^{Δ} A^{⊥} ⊕ B^{⊥}
(!A)^{⊥} =^{Δ} ?A^{⊥}  (?A)^{⊥} =^{Δ} !A^{⊥}
(1)^{⊥} =^{Δ} ⊥  (⊥)^{⊥} =^{Δ} 1
(0)^{⊥} =^{Δ} ⊤  (⊤)^{⊥} =^{Δ} 0

With implication treated as an abbreviation, A−∘B = A^{⊥} ℘B, we have this derived property of implication:

(A−∘B)^{⊥} = (A^{⊥} ℘B)^{⊥} = A ⊗ B^{⊥}

3 Sequent rules (two-sided)

Identity  \overline{A ⊢ A}  \frac{Γ_{1} ⊢ A, Σ_{1}  Γ_{2}, A ⊢ Σ_{2}}{Γ_{1}, Γ_{2} ⊢ Σ_{1}, Σ_{2}}  Cut

Exch. Left  \frac{Γ_{1}, A, B, Γ_{2} ⊢ Σ}{Γ_{1}, B, A, Γ_{2} ⊢ Σ}  \frac{Γ ⊢ Σ_{1}, A, B, Σ_{2}}{Γ ⊢ Σ_{1}, B, A, Σ_{2}}  Exch. Right

⊗ Left  \frac{Γ, A, B ⊢ Σ}{Γ, (A ⊗ B) ⊢ Σ}  \frac{Γ_{1} ⊢ A, Σ_{1}  Γ_{2} ⊢ B, Σ_{2}}{Γ_{1}, Γ_{2} ⊢ (A ⊗ B), Σ_{1}, Σ_{2}}  ⊗ Right

−∘ Left  \frac{Γ_{1} ⊢ A, Σ_{1}  Γ_{2}, B ⊢ Σ_{2}}{Γ_{1}, Γ_{2}, (A−∘B) ⊢ Σ_{1}, Σ_{2}}  \frac{Γ, A ⊢ B, Σ}{Γ ⊢ (A−∘B), Σ}  −∘ Right

℘ Left  \frac{Γ_{1}, A ⊢ Σ_{1}  Γ_{2}, B ⊢ Σ_{2}}{Γ_{1}, Γ_{2}, (A℘B) ⊢ Σ_{1}, Σ_{2}}  \frac{Γ ⊢ A, B, Σ}{Γ ⊢ (A℘B), Σ}  ℘ Right

& Left

Γ, A ⊢ Σ  Γ, B ⊢ Σ
Γ, (A&B) ⊢ Σ  Γ, (A&B) ⊢ Σ

\frac{Γ ⊢ A, Σ Γ ⊢ B, Σ}{Γ ⊢ (A&B), Σ}

& Right

⊕ Left \frac{Γ, A ⊢ Σ Γ, B ⊢ Σ}{Γ, (A ⊕ B) ⊢ Σ} Γ ⊢ A, Σ  Γ ⊢ B, Σ Γ ⊢ (A ⊕ B), Σ  Γ ⊢ (A ⊕ B), Σ ⊕ Right

! W  \frac{Γ ⊢ Σ}{Γ,!A ⊢ Σ}  \frac{Γ,!A,!A ⊢ Σ}{Γ,!A ⊢ Σ}  ! C

! D  \frac{Γ, A ⊢ Σ}{Γ,!A ⊢ Σ}  \frac{!Γ ⊢ A,?Σ}{!Γ ⊢!A,?Σ}  ! S

? W  \frac{Γ ⊢ Σ}{Γ ⊢?A, Σ}  \frac{Γ ⊢?A,?A, Σ}{Γ ⊢?A, Σ}  ? C

? D  \frac{Γ ⊢ A, Σ}{Γ ⊢?A, Σ}  \frac{!Γ, A ⊢?Σ}{!Γ,?A ⊢?Σ}  ? S

⊥ Left  \frac{Γ ⊢ A, Σ}{Γ, A^{⊥} ⊢ Σ}  \frac{Γ, A ⊢ Σ}{Γ ⊢ A^{⊥}, Σ}  ^{⊥} Right
0 Left  Γ, 0 ⊢ Σ  Γ ⊢ ⊤, Σ  ⊤ Right

⊥ Left  ⊥ ⊢  \frac{Γ ⊢ Σ}{Γ ⊢ ⊥, Σ}  ⊥ Right

1 Left  \frac{Γ ⊢ Σ}{Γ, 1 ⊢ Σ}  ⊢ 1  1 Right

4 Discussion of selected rules

In is interesting to compare the two forms of conjunction in linear logic with classical conjunction.

∧ Left  \frac{Γ, A ⊢ Σ}{Γ, A ∧ B ⊢ Σ} \frac{Γ, B ⊢ Σ}{Γ, A ∧ B ⊢ Σ}  \frac{Γ_{1} ⊢ A, Σ_{1}  Γ_{2} ⊢ B, Σ_{2}}{Γ_{1}, Γ_{2} ⊢ (A ∧ B), Σ_{1}, Σ_{2}} ∧ Right

⊗ Left  \frac{Γ, A, B ⊢ Σ}{Γ, (A ⊗ B) ⊢ Σ}  \frac{Γ_{1} ⊢ A, Σ_{1}  Γ_{2} ⊢ B, Σ_{2}}{Γ_{1}, Γ_{2} ⊢ (A ⊗ B), Σ_{1}, Σ_{2}} ⊗ Right

& Left

Γ, A ⊢ Σ  Γ, B ⊢ Σ
Γ, (A&B) ⊢ Σ  Γ, (A&B) ⊢ Σ

\frac{Γ ⊢ A, Σ Γ ⊢ B, Σ}{Γ ⊢ (A&B), Σ}

& Right

Two apparent points are:

1. Each form of linear conjunction has one of the classical rules, but no the other.

2. If we look at “intuitionistic” form of the right rules for ⊗ and &, we can see that ⊗ uses independent resources to produce both conjuncts independently, while & allows the same resources to produce one conjunct or the other, but due to linearity (conservation of resources) not both.

A similar comparison may be made for linear and classical disjunction. The negation rules are the same for classical and linear logic.

5 Simplified presentation

Using the negation rule, we can push all formulas of a sequent A_{1}, …, A_{k} ⊢ B_{1}, …, B_{ℓ} to the right of the turnstile, giving us the equivalent sequent ⊢ A_{1}^{⊥}, …, A_{k}^{⊥}, B_{1}, …, B_{ℓ}. We can write all of the proof rules in one-sided form as follows, dropping the −∘ and negation rules since −∘ is considered a derived connective and negation is not needed if we keep all formulas on the right and negation only occurs on atomic formulas.

Identity  \overline{⊢ A^{⊥}, A}  \frac{⊢ Γ, A  ⊢ A^{⊥}, Σ}{⊢ Γ, Σ} Cut

Exchange  \frac{⊢ Γ, A, B, Σ}{⊢ Γ, B, A, Σ}  \frac{⊢ Γ, A, B}{⊢ Γ, A℘B}  ℘

⊗ \frac{⊢ Γ, A  ⊢ Σ, B}{⊢ Γ, Σ, A ⊗ B}  \frac{⊢ Γ, A  ⊢ Γ, B}{⊢ Γ, A & B}  &

⊕  \frac{⊢ Γ, A}{⊢ Γ, A ⊕ B}  \frac{⊢ Γ, B}{⊢ Γ, A ⊕ B}

? W  \frac{⊢ Σ}{⊢?A, Σ}  \frac{⊢?A,?A, Σ}{⊢?A, Σ}  ? C

? D  \frac{⊢ A, Σ}{⊢?A, Σ}  \frac{⊢?Σ, A}{⊢?Σ,!A}  ? S

⊥  \frac{⊢ Σ}{⊢ ⊥, Σ}
⊤  ⊢ Σ, ⊤  ⊢ 1  1

Exercises

1. Prove the formulas (A ⊗ (A−∘B))−∘B and A^{⊥} ℘A. Use the fact that Cut is eliminable to show that (A ⊗ (A−∘B) ⊗ (A−∘C))−∘B ⊗ C and (A ⊗ A ⊗ A ⊗ (A−∘B) ⊗ (A−∘C))−∘B ⊗ C are not provable. Use either one-sided or two-sided sequents, as you prefer.

2. Consider the informal “process interpretation” for the sequent A ⊗ B, A^{⊥} ⊗ B, A ⊗ B^{⊥}, A^{⊥} ⊗ B^{⊥}. Explain how you might create a process that satisfies this specification. Then show that this sequent is not derivable.