Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic

\underline{Ranald Clouston}, Jeremy Dawson, Rajeev Goré, Alwen Tiu

Logic and Computation Group Research School of Computer Science The Australian National University

22nd EACSL Annual Conference on Computer Science Logic (CSL ’13 Torino) 2 September 2013

Sequent Calculus: Classical vs Intuitionistic

Gentzen’s calculus LK for classical propositional logic has (multi-)sets of formulae to the left and right of a ‘turnstile’ ⊢.

Commas on the left are interpreted as ∧; on the right as ∨.

To restrict to intuitionistic logic we restrict the right of the turnstile to singletons; indeed we need only make this restriction to (⊃ R):

\begin{aligned}& Γ, A ⊢ B \\ (⊃ R_{1}) \\ & Γ ⊢ A ⊃ B \end{aligned}  \begin{aligned}& Γ, A ⊢ B, Δ \\ (⊃ R_{2}) \\ & Γ ⊢ A ⊃ B, Δ \end{aligned}

If we make the same restriction with respect to (⊸ R) to a two-sided sequent calculus for (multiplicative) linear logic, where comma on the left is ⊗ and right is ⊕, do we get a sensible logic?

The Schellinx calculus

[Schellinx 1991] posed this question and answered it in the negative – such a calculus is not cut-free:

\begin{matrix}\begin{matrix}⋮ ; p ⊸ q ⊢ p ⊸ q & ⋮ ; r ⊕ s ⊢ r, s \\ (p ⊸ q) ⊕ (r ⊕ s) ⊢ (p ⊸ q) ⊕ r, s \end{matrix} & \begin{matrix}⋮ ; p ⊸ q, p ⊢ q & ⋮ ; r ⊢ r \\ (p ⊸ q) ⊕ r, p ⊢ q ⊕ r \end{matrix} ; (p ⊸ q) ⊕ r ⊢ p ⊸ (q ⊕ r) \\ (p ⊸ q) ⊕ (r ⊕ s) ⊢ p ⊸ (q ⊕ r), s \end{matrix}

This sequent cannot be proved without cut in the ‘Schellinx calculus’.

Perhaps this argues for the usual absence of ⊕ in intuitionistic linear logic - when we go classical, we get it ‘for free’ via de Morgan duality.

But is hope really lost for this logic?

Full Intuitionistic Linear Logic – Semantics

[Hyland & de Paiva 1993] coined the name Full Intuitionistic Linear Logic (FILL) for the logic specified by the Schellinx calculus with cut, and gave its semantics in the category theoretic style:

• (⊗, I, ⊸) is a symmetric monoidal closed structure (as usual);

• (⊕, ⊥) is a symmetric monoidal structure;

• Interaction between these structures is entirely described by weak distributivity:

A ⊗ (B ⊕ C) → (A ⊗ B) ⊕ C

Semantics are great, but what we really want is a cut-free calculus...

Full Intuitionistic Linear Logic – Sequent Calculus

We need a ‘compromise’ between the too-weak (⊸ R_{1}) and toostrong (⊸ R_{2}):

\begin{aligned}& Γ, A ⊢ B \\ (⊸ R_{1}) \\ & Γ ⊢ A ⊸ B \end{aligned}  \begin{aligned}& Γ, A ⊢ B, Δ \\ (⊸ R_{2}) \\ & Γ ⊢ A ⊸ B, Δ \end{aligned}

[Hyland & de Paiva 1993] found this compromise by annotating their proofs via a term calculus, and then blocking (⊸ R_{2}) unless the variable for A is not free for the terms for Δ.

The development is fiddly and, it turns out, wrong - [Bierman 1996] showed some cuts were still essential and offered two possible fixes (one due to Bellin). [Bräuner and de Paiva 1997] suggested another.

All three fixes use the same strategy of using annotations to block invalid use of (⊸ R_{2}).

Our Example Again

\begin{matrix}⋮ ; p ⊸ q, p ⊢ q & ⋮ ; r ⊕ s ⊢ r, s \\ (p ⊸ q) ⊕ (r ⊕ s), p ⊢ q, r, s \end{matrix} ; (p ⊸ q) ⊕ (r ⊕ s), p ⊢ q ⊕ r, s ; (p ⊸ q) ⊕ (r ⊕ s) ⊢ p ⊸ (q ⊕ r), s

The bottom step is legal because our annotations confirm that p is ‘independent’ from s.

It has been generally asserted in the literature that FILL requires annotations for cut-free sequent calculus. This has seen it described as “curious”, and even that it “does not have a satisfactory proof theory”

Our contribution is to show that such annotations are not necessary.

Our Strategy

• Give a display calculus for FILL.

✓ Easily shown to be complete. ✓ Easily shown to support a cut-elimination procedure. X Embeds FILL into a bigger logic – conservativity, and hence

soundness, not clear. X Not well suited to proof search.

• Refine display calculus to a nested sequent calculus with deep inference. ✓ Conservativity, and hence soundness, now clear. ✓ Supports proof search, shows that tautology problem for FILL

is NP-complete.

Annotation-Free Sequent Calculi for FILL 7

Display calculus

Display calculus [Belnap 1982] is an organising principle for sequent calculus that offers a generic cut-elimination procedure ‘for free’.

Every logical connective has a structural counterpart: just as ⊗ and ⊕ correlate to comma (depending on their position), ⊸ correlates to >:

\begin{aligned}X ⊢ A & B ⊢ Y \\ (⊸⊢) \\ & A ⊸ B ⊢ X > Y \end{aligned}  \begin{aligned}& X ⊢ A > B \\ (⊢⊸) \\ & X ⊢ A ⊸ B \end{aligned}

Any substructure can be displayed by applying residuation rules e.g.

\begin{aligned}& X, Y ⊢ Z \\ (rp) \\ & X ⊢ Y > Z \end{aligned}  \begin{aligned}& X, Y ⊢ Z \\ (rp) \\ & Y ⊢ X > Z \end{aligned}

This display property is the heart of the cut-elimination theorem.

Display property - Comma on the right

We have seen how we deconstruct comma on the left (⊗ in disguise) with (rp). What about comma on the right (⊕ in disguise)?

Solution: a new structural connective, <, and dual residuation rules:

\begin{aligned}& X ⊢ Y, Z \\ (drp) \\ & X < Y ⊢ Z \end{aligned}  \begin{aligned}& X ⊢ Y, Z \\ (drp) \\ & X < Z ⊢ Y \end{aligned}

What is this new structural connective?

For now, view it as a meaningless syntactic tool, but observe that it raises immediate questions about soundness, as X < Y ⊢ Z has no obvious meaning in FILL’s semantics.

From Weak Distributivity to Grishin (b)

FILL’s signature property, weak distributivity

p ⊗ (q ⊕ r) → (p ⊗ q) ⊕ r

turns out to be equivalent to (either of) the Grishin (b) rules

\begin{aligned}& W, (X < Y) ⊢ Z \\ (Grnb ⊢) \\ & (W, X) < Y ⊢ Z \end{aligned}  \begin{aligned}& W ⊢ (X > Y), Z \\ (⊢ Grnb) \\ & W ⊢ X > (Y, Z) \end{aligned}

If we had the converse of these rules (Grishin (a)), we could ‘gather up’ Z with Y to make > (structural ⊸) the main connective.

We would hence effectively have an unrestrained (⊸ R) rule, regaining classical linear logic exactly.

An Example Proof

\begin{matrix}⋮ ; p ⊸ q ⊢ p > q & ⋮ ; r ⊕ s ⊢ r, s \\ (p ⊸ q) ⊕ (r ⊕ s) ⊢ (p > q), r, s \end{matrix} ; (p ⊸ q) ⊕ (r ⊕ s) < s ⊢ (p > q), r ; (p ⊸ q) ⊕ (r ⊕ s) < s ⊢ p > (q, r) ; ((p ⊸ q) ⊕ (r ⊕ s) < s), p ⊢ q, r ; ((p ⊸ q) ⊕ (r ⊕ s) < s), p ⊢ q ⊕ r ; (p ⊸ q) ⊕ (r ⊕ s) < s ⊢ p > q ⊕ r ; (p ⊸ q) ⊕ (r ⊕ s) < s ⊢ p ⊸ (q ⊕ r) ; (p ⊸ q) ⊕ (r ⊕ s) ⊢ p ⊸ (q ⊕ r), s

Annotation-Free Sequent Calculi for FILL 11

\begin{matrix}⋮ ; p ⊸ q ⊢ p > q & ⋮ ; r ⊕ s ⊢ r, s \\ (p ⊸ q) ⊕ (r ⊕ s) ⊢ (p > q), r, s \end{matrix} ; (p ⊸ q) ⊕ (r ⊕ s) < s ⊢ (p > q), r ; (p ⊸ q) ⊕ (r ⊕ s) < s ⊢ p > (q, r) ; ((p ⊸ q) ⊕ (r ⊕ s) < s), p ⊢ q, r ; ((p ⊸ q) ⊕ (r ⊕ s) < s), p ⊢ q ⊕ r ; (p ⊸ q) ⊕ (r ⊕ s) < s ⊢ p > q ⊕ r ; (p ⊸ q) ⊕ (r ⊕ s) < s ⊢ p ⊸ (q ⊕ r) ; (p ⊸ q) ⊕ (r ⊕ s) ⊢ p ⊸ (q ⊕ r), s

Annotation-Free Sequent Calculi for FILL 12

\begin{matrix}⋮ ; p ⊸ q ⊢ p > q & ⋮ ; r ⊕ s ⊢ r, s \\ (p ⊸ q) ⊕ (r ⊕ s) ⊢ (p > q), r, s \end{matrix} ; (p ⊸ q) ⊕ (r ⊕ s) < s ⊢ (p > q), r ; (p ⊸ q) ⊕ (r ⊕ s) < s ⊢ p > (q, r) ; ((p ⊸ q) ⊕ (r ⊕ s) < s), p ⊢ q, r ; ((p ⊸ q) ⊕ (r ⊕ s) < s), p ⊢ q ⊕ r ; (p ⊸ q) ⊕ (r ⊕ s) < s ⊢ p > q ⊕ r ; (p ⊸ q) ⊕ (r ⊕ s) < s ⊢ p ⊸ (q ⊕ r) ; (p ⊸ q) ⊕ (r ⊕ s) ⊢ p ⊸ (q ⊕ r), s

Note how < was useful to ‘move s out the way’. We will return to this theme of ‘deep inference’...

Annotation-Free Sequent Calculi for FILL 13

The Meaning of < – Exclusion

We may view < as the structural version of a new logical connective −<, called exclusion (sometimes subtraction):

\begin{aligned}& A < B ⊢ X \\ (−< ⊢) \\ & A−<B ⊢ X \end{aligned}  \begin{aligned}X ⊢ A & B ⊢ Y \\ (⊢ −<) \\ & X < Y ⊢ A−<B \end{aligned}

A categorical semantics for FILL with this connective equips ⊕ with a co-closure: a (natural) isomorphism between arrows

A → B ⊕ C and A−<B → C

Call the corresponding logic Bi-Intuitionistic Linear Logic (BiILL).

Our display calculus is easily cut-free complete for FILL and BiILL, and sound for BiILL. FILL-soundness then reduces to the question of the conservativity of BiILL over FILL.

Nested sequents

We will refine our display calculus to a deep inference calculus with no structural rules (and hence no need for the troublesome (drp)).

A convenient notation for this are nested sequents:

S T ::= S_{1}, …, S_{k}, A_{1}, …, A_{m} ⇒ B_{1}, …, B_{n}, T_{1}, …, T_{l}

where A_{i} and B_{j} are formulae.

This is a trivial variation on display calculus notation – merely replace all ⊢, <, > with ⇒.

(To go back, we need to pay attention to whether a given ⇒ appears on the left or right, and replace it with < or > as appropriate.)

Deep Inference and Merging

All proof rules can be applied deeply (in context). Many rules involve merging sequents – nested sequents with the same tree structure merge by combining their formulae. Examples:

\begin{matrix}X_{1}[S_{1}, A ⇒ T_{1}] & X_{2}[S_{2}, B ⇒ T_{2}] \\ X[S, A ⊕ B ⇒ T ] \end{matrix} ⊕_{l}^{d}  {X[S ⇒ A, B, T ] \atop X[S ⇒ A ⊕ B, T ]} ⊕_{r}^{d}

On the left S is a merge of S_{1}, S_{2}; T of T_{1}, T_{2}; X[ ] of X_{1}[ ], X_{2}[ ]. ⊕_{l}^{d} is valid by weak distributivity.

Annotation-Free Sequent Calculi for FILL 16

Propagation

Along with rules for logical connectives and identity, propagation rules allow formulae to be moved levels in the nested sequents:

{X[S ⇒ (A, S′ ⇒ T′), T ] \atop X[S, A ⇒ (S′ ⇒ T′), T ]} pl_{1}  {X[(S ⇒ T , A), S′ ⇒ T′] \atop X[(S ⇒ T ), S′ ⇒ A, T′]} pr_{1}
{X[S, A, (S′ ⇒ T′) ⇒ T ] \atop X[S, (S′, A ⇒ T′) ⇒ T ]} pl_{2}  {X[S ⇒ T , A, (S′ ⇒ T′)] \atop X[S ⇒ T , (S′ ⇒ T′, A)]} pr_{2}

Again weak distributivity is the key to the validity of these rules.

Annotation-Free Sequent Calculi for FILL 17

Deep Inference: An Example

\begin{matrix}\begin{matrix}· ⇒ (p ⇒ p) & · ⇒ (q ⇒ q) \\ · ⇒ (p ⊸ q, p ⇒ q) \end{matrix} ; p ⊸ q ⇒ (p ⇒ q) & \begin{matrix}\begin{matrix}r ⇒ r, (· ⇒ ·) \\ r ⇒ (· ⇒ r) \end{matrix} & s ⇒ (· ⇒ ·), s \\ r ⊕ s ⇒ (· ⇒ r), s \end{matrix} \\ (p ⊸ q) ⊕ (r ⊕ s) ⇒ (p ⇒ q, r), s \end{matrix} ; (p ⊸ q) ⊕ (r ⊕ s) ⇒ (p ⇒ q ⊕ r), s ; (p ⊸ q) ⊕ (r ⊕ s) ⇒ p ⊸ (q ⊕ r), s

Annotation-Free Sequent Calculi for FILL 18

Deep Inference: An Example

\begin{matrix}\begin{matrix}· ⇒ (p ⇒ p) & · ⇒ (q ⇒ q) \\ · ⇒ (p ⊸ q, p ⇒ q) \end{matrix} ; p ⊸ q ⇒ (p ⇒ q) & \begin{matrix}\begin{matrix}r ⇒ r, (· ⇒ ·) \\ r ⇒ (· ⇒ r) \end{matrix} & s ⇒ (· ⇒ ·), s \\ r ⊕ s ⇒ (· ⇒ r), s \end{matrix} \\ (p ⊸ q) ⊕ (r ⊕ s) ⇒ (p ⇒ q, r), s \end{matrix} ; (p ⊸ q) ⊕ (r ⊕ s) ⇒ (p ⇒ q ⊕ r), s ; (p ⊸ q) ⊕ (r ⊕ s) ⇒ p ⊸ (q ⊕ r), s

Annotation-Free Sequent Calculi for FILL 19

Deep Inference: An Example

\begin{matrix}\begin{matrix}· ⇒ (p ⇒ p) & · ⇒ (q ⇒ q) \\ · ⇒ (p ⊸ q, p ⇒ q) \end{matrix} ; p ⊸ q ⇒ (p ⇒ q) & \begin{matrix}\begin{matrix}r ⇒ r, (· ⇒ ·) \\ r ⇒ (· ⇒ r) \end{matrix} & s ⇒ (· ⇒ ·), s \\ r ⊕ s ⇒ (· ⇒ r), s \end{matrix} \\ (p ⊸ q) ⊕ (r ⊕ s) ⇒ (p ⇒ q, r), s \end{matrix} ; (p ⊸ q) ⊕ (r ⊕ s) ⇒ (p ⇒ q ⊕ r), s ; (p ⊸ q) ⊕ (r ⊕ s) ⇒ p ⊸ (q ⊕ r), s

Note that no ⇒ on the left is introduced at any stage in this proof, so every sequent has a FILL translation (without −<). This is a general property of the calculus (separation).

Annotation-Free Sequent Calculi for FILL 20

Theorems

Equivalence of Calculi. A formula is derivable in the display calculus iff it is derivable in the deep inference calculus.

• via an intermediate shallow inference nested sequent calculus.

Separation. The derivations of FILL formulae involve FILL-translatable sequents only.

Soundness. The calculi are sound for FILL’s semantics.

• by separation we need only check each nested rule on FILLtranslatable sequents.

NP-completeness.

• via encoding of Constants-Only multiplicative linear logic.

Conclusion

FILL is (multiplicative) intuitionistic linear logic with ⊕. Contrary to the literature, proof annotations are not necessary for a cut-free sequent calculus. Instead use display calculus or deep inference. The former gives completeness, and cut elimination ‘for free’, and its modularity makes FILL’s relationship to other logics clear. The latter gives soundness and a complexity result. Future work

• Extensions (exponentials, additives, MIX).

• Computational applications.

Annotation-Free Sequent Calculi for FILL 22