From Display Calculi to Decision Procedures for Full Intuitionistic Linear Logic

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

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

              rajeev.gore@anu.edu.au

August 14, 2014

Published in Proc. 22nd EACSL Annual Conference on Computer Science Logic, Turin September 2013 as

“Annotation-free sequent calculi for Full Intuitionistic Linear Logic”

Overview

What is FILL? Existing sequent calculi A Display Calculus for FILL Nested Sequent Calculus for FILL Separation Decidability and Complexity Further Work

Full Intuitionistic Linear Logic

LL: modal substructural logic without weakening and without

contraction ⊗, ⊕, 1, 0, ⊸, ∧, ∨, ⊤, ⊥,!,? Girard 1987 MALL: ⊗, ⊕, 1, 0, ⊸, ∧, ∨, ⊤, ⊥ drop exponentials MILL: ⊗, 1, ⊸ intuitionistic MLL: ⊗, 1, ⊸, ⊕, 0 classical ((A ⊸ 0) ⊸ 0) ⊸ A FILL: ⊗, 1, ⊸, ⊕, 0 Hyland and de Paiva 1993

Categorial Semantics for FILL

(⊗, 1, ⊸) is a symmetric monoidal closed structure A ⊗ B ⊸ C iff A ⊸ (B ⊸ C) iff B ⊸ (A ⊸ C) (A ⊗ 1) ⊸ A and A ⊸ (A ⊗ 1)

(⊕, 0) is a symmetric monoidal structure (A ⊕ B) ⊸ (B ⊕ A) (A ⊕ 0) ⊸ A and A ⊸ (A ⊕ 0)

interaction via either of

weak distributivity ((A ⊗ B) ⊕ C) ⊸ (A ⊗ (B ⊕ C))
Grishin(b)  ((A ⊸ B) ⊕ C) ⊸ (A ⊸ (B ⊕ C))

Collapse to (classical) MLL: if we add converse of Grishin(b)

Grishin(a)  (A ⊸ (B ⊕ C)) ⊸ ((A ⊸ B) ⊕ C)

Proof Theory of Full Intuitionistic Linear Logic

LL: substructural logic without weakening and without contraction

MILL ⊗ ⊸ 1 intuitionistic cut-elimination
Γ_{1} ⊢ A  Γ_{2} ⊢ B
Γ_{1}, Γ_{2} ⊢ A ⊗ B

\begin{matrix}Γ, A ⊢ B \\ Γ ⊢ A ⊸ B \end{matrix}

MLL ⊗ ⊸ 1 ⊕ ⊥ classical cut-elimination
Γ_{1}, A ⊢ B, Δ_{1}  Γ_{2}, A ⊢ B, Δ_{2}
Γ_{1}, Γ_{2} ⊢ Δ_{1}, A ⊗ B, Δ_{2}

Γ ⊢ A, B, Δ ; Γ ⊢ A ⊕ B, Δ Γ, A ⊢ B, Δ Γ ⊢ A ⊸ B, Δ

FILL ⊗ ⊸ 1 ⊕ ⊥ intuitionistic cut-elimination fails
Γ_{1}, A ⊢ B, Δ_{1}  Γ_{2}, A ⊢ B, Δ_{2}
Γ_{1}, Γ_{2} ⊢ Δ_{1}, A ⊗ B, Δ_{2}

Γ ⊢ A, B, Δ ; Γ ⊢ A ⊕ B, Δ \begin{matrix}Γ, A ⊢ B \\ Γ ⊢ A ⊸ B, Δ \end{matrix}

Problem and a solutions via annotated derivations

Remember: we need comma on the right to accommodate ⊕ Problem and existing solutions:

multiple conclusions single conclusion existing solutions
Γ, A ⊢ B, Δ
Γ ⊢ A ⊸ B, Δ

\begin{matrix}Γ, A ⊢ B \\ Γ ⊢ A ⊸ B, Δ \end{matrix}

Γ, A ⊢ B, Δ
(†)
Γ ⊢ A ⊸ B, Δ
unsound no cut-elimination cut-elimination

†: side-conditions which ensure that A is “independent” of Δ Hyland, de Paiva 1993: type assignments to ensure that the

variable typed by A not appear free in the terms typed by Δ

Further problems and solutions using annotations

Hyland and de Paiva 1993:

Γ, A ⊢ B, Δ
(†)
Γ ⊢ A ⊸ B, Δ

†: side-conditions which ensure that A is “independent” of Δ Bierman 1996: (a ⊕ b) ⊕ c ⊢ a, ((b ⊕ c) ⊸ d) ⊕ (e ⊸ (d ⊕ e))

has no cut-free derivation in the Hyland and de Paiva calculus Bierman, Bellin 1996: refined annotations to regain cut-elimination Bräuner and de Paiva 1997: annotate rules with a binary relation

between antecedent formulae and succedent formulae, which effectively trace variable occurrence What do derivations look like ?

Hyland , de Paiva and Biermann

(⊸ R) legal as v and (w ⊕ x ⊸ y) ⊕ z share no free variables.

v : a ⊢ v : a  w : b ⊢ w : b

v ⊕ w : a ⊕ b ⊢ v : a, w : b x : c ⊢ x : c

(v ⊕ w) ⊕ x : (a ⊕ b) ⊕ c ⊢ v : a, w : b, x : c (v ⊕ w) ⊕ x : (a ⊕ b) ⊕ c ⊢ v : a, w ⊕ x : b ⊕ c y : d ⊢ y : d (v ⊕ w) ⊕ x : (a ⊕ b) ⊕ c, w ⊕ x ⊸ y : b ⊕ c ⊸ d ⊢ v : a, y : d z : e ⊢ z : e (v ⊕ w) ⊕ x : (a ⊕ b) ⊕ c, (w ⊕ x ⊸ y) ⊕ z : (b ⊕ c ⊸ d) ⊕ e ⊢ v : a, y : d, z : e (v ⊕ w) ⊕ x : (a ⊕ b) ⊕ c, (w ⊕ x ⊸ y) ⊕ z : (b ⊕ c ⊸ d) ⊕ e ⊢ v : a, y ⊕ z : d ⊕ e

(v ⊕ w) ⊕ x : (a ⊕ b) ⊕ c ⊢ v : a, λ(w ⊕ x ⊸ y) ⊕ z^{(b⊕c⊸d)⊕e}.(y ⊕ z) : (b ⊕ c ⊸ d) ⊕ e ⊸ d ⊕ e

But the type annotations have no computational content

Bellin-style Proof

(⊸ R) is legal because r is not free in

        let t be u ⊕ - in let u be v ⊕ - in v

v : a ⊢ v : a  w : b ⊢ w : b

u : a ⊕ b ⊢ let u be v ⊕ - in v : a, let u be - ⊕ w in w : b x : c ⊢ x : c

t : (a ⊕ b) ⊕ c ⊢ let t be u ⊕ - in let u be v ⊕ - in v : a, let t be u ⊕ - in let u be - ⊕ w in w : b, let t be - ⊕ x in x : c t : (a ⊕ b) ⊕ c ⊢ let t be u ⊕ - in let u be v ⊕ - in v : a, (let t be u ⊕ - in let u be - ⊕ w in w) ⊕ (let t be - ⊕ x in x) : b ⊕ c y : d ⊢ y : d

t : (a ⊕ b) ⊕ c, s : b ⊕ c ⊸ d ⊢ let t be u ⊕ - in let u be v ⊕ - in v : a, (s(let t be u ⊕ - in let u be - ⊕ w in w) ⊕ (let t be - ⊕ x in x)) : d z : e ⊢ z : e

t : (a ⊕ b) ⊕ c, r : (b ⊕ c ⊸ d) ⊕ e ⊢ let t be u ⊕ - in let u be v ⊕ - in v : a, let r be s ⊕ - in (s(let t be u ⊕ - in let u be - ⊕ w in w) ⊕ (let t be - ⊕ x in x)) : d, let s be - ⊕ z in z : e t : (a ⊕ b) ⊕ c, r : (b ⊕ c ⊸ d) ⊕ e ⊢ let t be u ⊕ - in let u be v ⊕ - in v : a, (let r be s ⊕ - in (s(let t be u ⊕ - in let u be - ⊕ w in w) ⊕ (let t be - ⊕ x in x))) ⊕ (let s be - ⊕ z in z) : d ⊕ e

t : (a ⊕ b) ⊕ c ⊢ let t be u ⊕ - in let u be v ⊕ - in v : a, λr^{(b⊕c⊸d)⊕e}.(let r be s ⊕ - in (s(let t be u ⊕ - in let u be - ⊕ w in w) ⊕ (let t be - ⊕ x in x))) ⊕ (let s be - ⊕ z in z) : (b ⊕ c ⊸ d) ⊕ e ⊸ d ⊕ e

Again, the type annotations are not given any computational content and this derivation does not even fit on the page!

Bräuner and de Paiva-style proof

(⊸ R) legal because (b ⊕ c ⊸ d) ⊕ e is not related to a

\begin{aligned}(a, a) \\ & a ⊢ a \end{aligned}  \begin{aligned}& (b, b) \\ b ⊢ b \end{aligned}

(a ⊕ b, a), (a ⊕ b, b)

a ⊕ b ⊢ a, b

(c, c) c ⊢ c

((a ⊕ b) ⊕ c, a), ((a ⊕ b) ⊕ c, b), ((a ⊕ b) ⊕ c, c)

(a ⊕ b) ⊕ c ⊢ a, b, c

((a ⊕ b) ⊕ c, a), ((a ⊕ b) ⊕ c, b ⊕ c) (a ⊕ b) ⊕ c ⊢ a, b ⊕ c

(d, d) d ⊢ d

((a ⊕ b) ⊕ c, a), ((a ⊕ b) ⊕ c, d), (b ⊕ c ⊸ d, d)

(a ⊕ b) ⊕ c, b ⊕ c ⊸ d ⊢ a, d

(e, e) e ⊢ e

((a ⊕ b) ⊕ c, a), ((a ⊕ b) ⊕ c, d), ((b ⊕ c ⊸ d) ⊕ e, d), ((b ⊕ c ⊸ d) ⊕ e, e)

(a ⊕ b) ⊕ c, (b ⊕ c ⊸ d) ⊕ e ⊢ a, d, e

((a ⊕ b) ⊕ c, a), ((a ⊕ b) ⊕ c, d ⊕ e), ((b ⊕ c ⊸ d) ⊕ e, d ⊕ e)

(a ⊕ b) ⊕ c, (b ⊕ c ⊸ d) ⊕ e ⊢ a, d ⊕ e

((a ⊕ b) ⊕ c, a), ((a ⊕ b) ⊕ c, (b ⊕ c ⊸ d) ⊕ e ⊸ d ⊕ e)

(a ⊕ b) ⊕ c ⊢ a, (b ⊕ c ⊸ d) ⊕ e ⊸ d ⊕ e

Pure annotational device to track variable occurrences

Cut-free derivation in our display calculus

a ⊢ a  b ⊢ b

a ⊕ b ⊢ a, b c ⊢ c (a ⊕ b) ⊕ c ⊢ a, b, c (a ⊕ b) ⊕ c < a ⊢ b, c (a ⊕ b) ⊕ c < a ⊢ b ⊕ c d ⊢ d b ⊕ c ⊸ d ⊢ ((a ⊕ b) ⊕ c < a) > d e ⊢ e (b ⊕ c ⊸ d) ⊕ e ⊢ (((a ⊕ b) ⊕ c < a) > d), e (b ⊕ c ⊸ d) ⊕ e ⊢ ((a ⊕ b) ⊕ c < a) > d, e (b ⊕ c ⊸ d) ⊕ e, ((a ⊕ b) ⊕ c < a) ⊢ d, e (b ⊕ c ⊸ d) ⊕ e, ((a ⊕ b) ⊕ c < a) ⊢ d ⊕ e (a ⊕ b) ⊕ c < a ⊢ (b ⊕ c ⊸ d) ⊕ e > d ⊕ e (a ⊕ b) ⊕ c < a ⊢ (b ⊕ c ⊸ d) ⊕ e ⊸ d ⊕ e (a ⊕ b) ⊕ c ⊢ a, (b ⊕ c ⊸ d) ⊕ e ⊸ d ⊕ e

No annotations, but many extra structural connectives

Cut-free derivation in the deep nested calculus

a ⇒ a, (· ⇒ ·) {· ⇒ (b ⇒ b) \atop b ⇒ (· ⇒ b)}

a ⊕ b ⇒ a, (· ⇒ b)

{· ⇒ (c ⇒ c) \atop c ⇒ (· ⇒ c)}

(a ⊕ b) ⊕ c ⇒ a, (· ⇒ b, c)
(a ⊕ b) ⊕ c ⇒ a, (· ⇒ b ⊕ c)

· ⇒ (d ⇒ d)

(a ⊕ b) ⊕ c ⇒ a, (b ⊕ c ⊸ d ⇒ d)

· ⇒ (e ⇒ e)

(a ⊕ b) ⊕ c ⇒ a, ((b ⊕ c ⊸ d) ⊕ e ⇒ d, e) (a ⊕ b) ⊕ c ⇒ a, ((b ⊕ c ⊸ d) ⊕ e ⇒ d ⊕ e) (a ⊕ b) ⊕ c ⇒ a, (b ⊕ c ⊸ d) ⊕ e ⊸ d ⊕ e

No annotations, only commas as structural connective, but sequents are nested (⋯ ⇒ ⋯) ⋯ ⇒ ⋯ (⋯ ⇒ ⋯)

Display calculus for (an extension of) FILL

Structural Constant and Binary Connectives: Φ  ,  <  >

Antecedent Structure: X_{a} Y_{a} ::= A | Φ | X_{a}, Y_{a} | X_{a} < Y_{s} Succcedent Structure: X_{s} Y_{s} ::= A | Φ | X_{s}, Y_{s} | X_{a} > Y_{s} Sequent: X_{a} ⊢ Y_{s} (drop subscripts to avoid clutter)

Display Postulates: reversible structural rules

X_{a} ⊢ Y_{a} > Z_{s} X_{a}, Y_{a} ⊢ Z_{s}
Y_{a} ⊢ X_{a} > Z_{s}

Z_{a} < Y_{s} ⊢ X_{s} Z_{a} ⊢ X_{s}, Y_{s}
Z_{a} < X_{s} ⊢ Y_{s}

Display Property: For every antecedent (succedent) part Z of the sequent X ⊢ Y , there is a sequent Z ⊢ Y′ (resp. X′ ⊢ Z) obtainable from X ⊢ Y using only the display postulates, thereby displaying the Z as the whole of one side

Logical rules: introduced formula is always displayed

(id) p ⊢ p

X ⊢ A  A ⊢ Y

(cut)

X ⊢ Y
\begin{aligned}& Φ ⊢ X \\ (1 ⊢) \\ & 1 ⊢ X \end{aligned}  (⊢ 1) Φ ⊢ 1
(0 ⊢) 0 ⊢ Φ  \begin{aligned}& X ⊢ Φ \\ (⊢ 0) \\ & X ⊢ 0 \end{aligned}

\begin{aligned}& A, B ⊢ X \\ (⊗ ⊢) \\ & A ⊗ B ⊢ X \end{aligned}

X ⊢ A  Y ⊢ B

(⊢ ⊗)

X , Y ⊢ A ⊗ B
A ⊢ X  B ⊢ Y

(⊕ ⊢)

A ⊕ B ⊢ X , Y

\begin{aligned}& X ⊢ A, B \\ (⊢ ⊕) \\ & X ⊢ A ⊕ B \end{aligned}

X ⊢ A  B ⊢ Y

(⊸⊢)

A ⊸ B ⊢ X > Y

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

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

read upwards, one rule is a “rewrite” while other “constrains”

Structural rules: no occurrences of formula meta-variables

all sub-structural properties captured in a modular way

\begin{aligned}& X , Φ ⊢ Y \\ (Φ ⊢) \\ & X ⊢ Y \end{aligned}  \begin{aligned}& X ⊢ Φ, Y \\ (⊢ Φ) \\ & X ⊢ Y \end{aligned}
W , (X , Y ) ⊢ Z

(Ass ⊢)

(W , X ), Y ⊢ Z

W ⊢ (X , Y ), Z
(⊢ Ass)
W ⊢ X , (Y , Z)
X , Y ⊢ Z ; (Com ⊢) ; Y , X ⊢ Z Z ⊢ Y , X ; (⊢ Com) ; Z ⊢ X , Y
W , (X < Y ) ⊢ Z

(Grnb ⊢)

(W , X ) < Y ⊢ Z

W ⊢ (X > Y ), Z
(⊢ Grnb)
W ⊢ X > (Y , Z)
((A ⊸ B) ⊕ C) ⊸ (A ⊸ (B ⊕ C))

Example derivation in our display calculus

a ⊢ a  b ⊢ b

(⊕ ⊢)

a ⊕ b ⊢ a, b c ⊢ c

(⊕ ⊢)

(a ⊕ b) ⊕ c ⊢ (a, b), c

(ass)

(a ⊕ b) ⊕ c ⊢ a, (b, c)

(drp)

(a ⊕ b) ⊕ c < a ⊢ b, c

(⊢ ⊕)

(a ⊕ b) ⊕ c < a ⊢ b ⊕ c d ⊢ d

(⊸⊢)

b ⊕ c ⊸ d ⊢ ((a ⊕ b) ⊕ c < a) > d e ⊢ e

(⊕ ⊢)

(b ⊕ c ⊸ d) ⊕ e ⊢ (((a ⊕ b) ⊕ c < a) > d), e

(⊢ Grnb)

(b ⊕ c ⊸ d) ⊕ e ⊢ ((a ⊕ b) ⊕ c < a) > (d, e)

(rp)

(b ⊕ c ⊸ d) ⊕ e,((a ⊕ b) ⊕ c < a) ⊢ d, e

(⊢ ⊕)

(b ⊕ c ⊸ d) ⊕ e, ((a ⊕ b) ⊕ c < a) ⊢ d ⊕ e

(rp)

(a ⊕ b) ⊕ c < a ⊢ (b ⊕ c ⊸ d) ⊕ e > (d ⊕ e)

(⊢⊸)

(a ⊕ b) ⊕ c < a ⊢ (b ⊕ c ⊸ d) ⊕ e ⊸ (d ⊕ e)

(drp)

(a ⊕ b) ⊕ c ⊢ a,(b ⊕ c ⊸ d) ⊕ e ⊸ (d ⊕ e)

But we implicitly created an occurrence of −< via <

Categorial semantics for bi-intuitionistic linear logic BiILL

(⊗, 1, ⊸) is a symmetric monoidal closed structure A ⊗ B ⊸ C iff A ⊸ (B ⊸ C) iff B ⊸ (A ⊸ C) (A ⊗ 1) ⊸ A and A ⊸ (A ⊗ 1)

(−<, ⊕, 0) is a symmetric monoidal co-closed structure A ⊸ (B ⊕ C) iff (A−<B) ⊸ C iff (A−<C) ⊸ B (A ⊕ 0) ⊸ A and A ⊸ (A ⊕ 0)

interaction via either of

Grishin(b)  ((A ⊸ B) ⊕ C) ⊸ (A ⊸ (B ⊕ C))
dualGrishin(b) ((A ⊗ B)−<C) ⊸ (A ⊗ (B−<C))

Collapse to (classical) MLL: if we add converse of either

Soundness, completeness and cut-elimination

Thm: The sequent X ⊢ Y is derivable iff the formula-translation

τ_{a}(X ) ⊸ τ_{s}(Y ) is BiILL-valid Proof: the display calculus proof rules and the arrows of the free

BiILL-category are inter-definable.

Thm: If X ⊢ Y is derivable then it is cut-free derivable. Proof: The rules obey conditions C1-C8 given by Belnap (1982),

hence the calculus enjoys cut-admissibility

Method: Essentially Gentzen’s original method Left-principal cuts: turned into left and right principal cuts Right-principal cuts: turned into left and right principal cuts Left&right principal cuts: replaced by multiple “smaller” cuts Need: substitution principles guaranteed by display property

and explicit structural rules Termination: double induction on grade and size of cut-formula

Proof search via display calculi

Given end-sequent X ⊢ Y how to find a derivation? Apply (invertible) “rewrite” rules immediately For “constraint” rules, use structural rules to match structure

Backward Proof-search for display calculus

a ⊢ a  b ⊢ b

a ⊕ b ⊢ a, b c ⊢ c (a ⊕ b) ⊕ c ⊢ (a, b), c (a ⊕ b) ⊕ c ⊢ a, (b, c)

(?)

(a ⊕ b) ⊕ c < a ⊢ b, c

(⊢ ⊕)

(a ⊕ b) ⊕ c < a ⊢ b ⊕ c d ⊢ d

(⊸⊢)

b ⊕ c ⊸ d ⊢ ((a ⊕ b) ⊕ c < a) > d e ⊢ e

(⊕ ⊢)

(b ⊕ c ⊸ d) ⊕ e ⊢ (((a ⊕ b) ⊕ c < a) > d), e

(?)

(b ⊕ c ⊸ d) ⊕ e ⊢ ((a ⊕ b) ⊕ c < a) > (d, e)

(?)

(b ⊕ c ⊸ d) ⊕ e,((a ⊕ b) ⊕ c < a) ⊢ d, e

(⊢ ⊕)

(b ⊕ c ⊸ d) ⊕ e, ((a ⊕ b) ⊕ c < a) ⊢ d ⊕ e

(?)

(a ⊕ b) ⊕ c < a ⊢ (b ⊕ c ⊸ d) ⊕ e > (d ⊕ e)

(⊢⊸)

(a ⊕ b) ⊕ c < a ⊢ (b ⊕ c ⊸ d) ⊕ e ⊸ (d ⊕ e) (a ⊕ b) ⊕ c ⊢ a,(b ⊕ c ⊸ d) ⊕ e ⊸ (d ⊕ e)

(?)

Proof search via display calculi

Given end-sequent X ⊢ Y how to find a derivation? Apply (invertible) “rewrite” rules immediately For “constraint” rules, use structural rules to match structure But there are just too many possibilities for this to be efficient Need to compile “display”, “undisplay” and “structural rules” into the logical rules as much as possible (maintaining cut-elimination)

Cut-free derivation in the deep nested calculus

a ⇒ a, (· ⇒ ·) {· ⇒ (b ⇒ b) \atop b ⇒ (· ⇒ b)}

a ⊕ b ⇒ a, (· ⇒ b)

{· ⇒ (c ⇒ c) \atop c ⇒ (· ⇒ c)}

(a ⊕ b) ⊕ c ⇒ a, (· ⇒ b, c)
(a ⊕ b) ⊕ c ⇒ a, (· ⇒ b ⊕ c)

· ⇒ (d ⇒ d)

(a ⊕ b) ⊕ c ⇒ a, (b ⊕ c ⊸ d ⇒ d)

· ⇒ (e ⇒ e)

(a ⊕ b) ⊕ c ⇒ a, ((b ⊕ c ⊸ d) ⊕ e ⇒ d, e) (a ⊕ b) ⊕ c ⇒ a, ((b ⊕ c ⊸ d) ⊕ e ⇒ d ⊕ e) (a ⊕ b) ⊕ c ⇒ a, (b ⊕ c ⊸ d) ⊕ e ⊸ d ⊕ e

No annotations, only commas as structural connective, but sequents are nested

Nested sequent calculi: Kashima 1994 (for tense logics)

Nested sequent: where comma is associative and commutative

S T ::= S_{1}, …, S_{k}, A_{1}, …, A_{m} ⇒ B_{1}, …, B_{n}, T_{1}, …, T_{l} Context: nested sequent with exactly one hole [ ] Positive/Negative: if [ ] occurs immediately to right/left of ⇒ Turn Rules: reversible rules using multisets of nested sequents

and formulae

{S_{2} ⇒ (S_{1} ⇒ T ) \atop S_{1}, S_{2} ⇒ T}  {(S ⇒ T_{2}) ⇒ T_{1} \atop S ⇒ (T_{1}, T_{2})}
X_{a} ⊢ Y_{a} > Z_{s} X_{a}, Y_{a} ⊢ Z_{s}
Y_{a} ⊢ X_{a} > Z_{s}

Z_{a} < Y_{s} ⊢ X_{s} Z_{a} ⊢ X_{s}, Y_{s}
Z_{a} < X_{s} ⊢ Y_{s}

Nested sequent calculi: Kashima 1994 (for tense logics)

Nested sequent: where comma is associative and commutative

S T ::= S_{1}, …, S_{k}, A_{1}, …, A_{m} ⇒ B_{1}, …, B_{n}, T_{1}, …, T_{l} Context: nested sequent with exactly one hole [ ] Positive/Negative: if [ ] occurs immediately to right/left of ⇒ Turn Rules: reversible rules using multisets of nested sequents

and formulae

{S_{2} ⇒ (S_{1} ⇒ T ) \atop S_{1}, S_{2} ⇒ T}  {(S ⇒ T_{2}) ⇒ T_{1} \atop S ⇒ (T_{1}, T_{2})}
X_{a} ⊢ Y_{a} > Z_{s} X_{a}, Y_{a} ⊢ Z_{s}
Y_{a} ⊢ X_{a} > Z_{s}

Z_{a} < Y_{s} ⊢ X_{s} Z_{a} ⊢ X_{s}, Y_{s}
Z_{a} < X_{s} ⊢ Y_{s}

Nested sequent calculi: Kashima 1994 (for tense logics)

Nested sequent: where comma is associative and commutative

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

Context: nested sequent with exactly one hole [ ] Positive/Negative: if [ ] occurs immediately to right/left of ⇒ Turn Rules: reversible rules using multisets of nested sequents

and formulae

{S_{2} ⇒ (S_{1} ⇒ T ) \atop S_{1}, S_{2} ⇒ T}  {(S ⇒ T_{2}) ⇒ T_{1} \atop S ⇒ (T_{1}, T_{2})}

Display Property: For every positive (negative) context X [ ] and every S, there exists T such that T ⇒ S (respectively S ⇒ T ) is derivable from X [S] using only the structural turn rules above. Thus S is “displayed” in T ⇒ S (resp. S ⇒ T ).

Polarity: note that ⇒ always points to the positive contexts

Shallow nested sequent calculus for BiILL

Logical rules:

p ⇒ p id  \begin{matrix}S ⇒ S′, A & A, T ⇒ T′ \\ S, T ⇒ S′, T′ \end{matrix} cut
0 ⇒ · 0_{l}  {S ⇒ T \atop S ⇒ T , 0} 0_{r}  {S ⇒ T \atop S, 1 ⇒ T} 1_{l}  · ⇒ 1 1_{r}
{S, A, B ⇒ T \atop S, A ⊗ B ⇒ T} ⊗_{l}  \begin{matrix}S ⇒ A, T & S′ ⇒ B, T′ \\ S, S′ ⇒ A ⊗ B, T , T′ \end{matrix} ⊗_{r}
\begin{matrix}S, A ⇒ T & S′, B ⇒ T′ \\ S, S′, A ⊕ B ⇒ T , T′ \end{matrix} ⊕_{l}  {S ⇒ A, B, T \atop S ⇒ A ⊕ B, T} ⊕_{r}
\begin{matrix}S ⇒ A, T & S′, B ⇒ T′ \\ S, S′, A ⊸ B ⇒ T , T′ \end{matrix} ⊸_{l}  {S ⇒ T , (A ⇒ B) \atop S ⇒ T , A ⊸ B} ⊸_{r}
{S, (A ⇒ B) ⇒ T \atop S, A−<B ⇒ T} ^{−<^{l}}  \begin{matrix}S ⇒ A, T & S′, B ⇒ T′ \\ S, S′ ⇒ A−<B, T , T′ \end{matrix} ^{−<^{r}}

Shallow nested sequent calculus for BiILL

Structural Rules: Grishin (b) analogues

{T , (S ⇒ S′) ⇒ T′ \atop (S, T ⇒ S′) ⇒ T′} gl  {S ⇒ (S′ ⇒ T′), T \atop S ⇒ (S′ ⇒ T′, T )} gr
W , (X < Y ) ⊢ Z
(Grnb ⊢)
(W , X ) < Y ⊢ Z

W ⊢ (X > Y ), Z
(⊢ Grnb)
W ⊢ X > (Y , Z)

Thm: Every formula has a cut-free nested shallow sequent

derivation iff it has cut-free display calculus derivation Thm: if a nested sequent is derivable it is cut-free derivable Proof: essentially the same as for display calculus

Prof search: how to absorb the turn and gl and gr rules ?

Deep nested sequents: just apply the rules inside contexts

X [ ] and U and V are hollow. X [U, p ⇒ p, V] id^{d}  similarly for units (no cut rule)
{X [S, A, B ⇒ T ] \atop X [S, A ⊗ B ⇒ T ]} ⊗_{l}^{d}  \begin{matrix}X_{1}[S_{1} ⇒ A, T_{1}] & X_{2}[S_{2} ⇒ B, T_{2}] \\ X [S ⇒ A ⊗ B, T ] \end{matrix} ⊗_{r}^{d}
\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 ⇒ T , (A ⇒ B)] \atop X [S ⇒ T , A ⊸ B]} ⊸_{r}^{d}
\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}
{X [S, (A ⇒ B) ⇒ T ] \atop X [S, A−<B ⇒ T ]} ^{−<d l}  \begin{matrix}X_{1}[S_{1} ⇒ A, T_{1}] & X_{2}[S_{2}, B ⇒ T_{2}] \\ X [S ⇒ A−<B, T ] \end{matrix} ^{−<d r}

Hollow: X [] contains no formulae (⇒-tree of empty nodes) Merge: X [ ] ∈ X_{1}[ ] • X_{2}[ ] and S ∈ S_{1} • S_{2} and T ∈ T_{1} • T_{2} Propagation rules: allow formulae to be moved in a context

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

Note: these are not just reversible rules expanded into two! Note: the rules do not need to track polarity Thm: the turn rules and rules gl and gr are (cut-free) admissible Thm: if a nested sequent is (cut-free) derivable in the deep

calculus then it is cut-free derivable in the shallow calculus Thm: if a nested sequent is cut-free derivable in the shallow

calculus then it is (cut-free) derivable in the deep calculus Cor: the deep and shallow nested calculi derive the same sequents Propagation rules: allow formulae to be moved in a context

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

Note: these are not just reversible rules expanded into two! Note: the rules do not need to track polarity Thm: the turn rules and rules gl and gr are (cut-free) admissible Thm: if a nested sequent is (cut-free) derivable in the deep

calculus then it is cut-free derivable in the shallow calculus Thm: if a nested sequent is cut-free derivable in the shallow

calculus then it is (cut-free) derivable in the deep calculus Cor: the deep and shallow nested calculi derive the same sequents

From BiILL back to FILL

a ⊢ a  b ⊢ b

a ⊕ b ⊢ a, b c ⊢ c (a ⊕ b) ⊕ c ⊢ (a, b), c (a ⊕ b) ⊕ c ⊢ a, (b, c)

(?)

(a ⊕ b) ⊕ c < a ⊢ b, c

(⊢ ⊕)

(a ⊕ b) ⊕ c < a ⊢ b ⊕ c d ⊢ d

(⊸⊢)

b ⊕ c ⊸ d ⊢ ((a ⊕ b) ⊕ c < a) > d e ⊢ e

(⊕ ⊢)

(b ⊕ c ⊸ d) ⊕ e ⊢ (((a ⊕ b) ⊕ c < a) > d), e

(?)

(b ⊕ c ⊸ d) ⊕ e ⊢ ((a ⊕ b) ⊕ c < a) > (d, e)

(?)

(b ⊕ c ⊸ d) ⊕ e,((a ⊕ b) ⊕ c < a) ⊢ d, e

(⊢ ⊕)

(b ⊕ c ⊸ d) ⊕ e, ((a ⊕ b) ⊕ c < a) ⊢ d ⊕ e

(?)

(a ⊕ b) ⊕ c < a ⊢ (b ⊕ c ⊸ d) ⊕ e > (d ⊕ e)

(⊢⊸)

(a ⊕ b) ⊕ c < a ⊢ (b ⊕ c ⊸ d) ⊕ e ⊸ (d ⊕ e) (a ⊕ b) ⊕ c ⊢ a,(b ⊕ c ⊸ d) ⊕ e ⊸ (d ⊕ e)

(?)

Problem: all our calculi are for BiILL ... are they sound for FILL? Display calculus: must create antecedent < structures in its

derivation of FILL-formulae in order to display and undisplay Question: is BiILL a conservative extension of FILL?

we were not able to find a categorial proof for BiILL

Compare: to tense logic Kt say where there is a simple semantic proof that Kt is a conservative extension of K (same frames)

Problem: all our calculi are for BiILL ... are they sound for FILL? Display calculus: must create antecedent < structures in its

derivation of FILL-formulae in order to display and undisplay Question: is BiILL a conservative extension of FILL?

we were not able to find a categorial proof for BiILL

Compare: to tense logic Kt say where there is a simple semantic proof that Kt is a conservative extension of K (same frames)

Nested FILL-sequent: nested sequent that has no nesting of

sequents on the left of ⇒ and no occurrences of −< Why? because then it is free of any traces of −< since only the

−<_{l}^{d} rule creates such nestings

FILL_{dn}: remove −<_{l}^{d}, −<_{r}^{d}, pl_{2} and pr_{1}

Separation Thm: nested FILL-sequents are (cut-free) derivable in

FILL_{dn} iff they are derivable in the original deep calculus Proof: if the end-sequent contains only FILL-formulae then

backward proof search will never create the offending nesting Thm: every rule of FILL_{dn} preserves FILL-validity downwards Cor: FILL_{dn} is sound and cut-free complete for FILL-validity Cor: BiILL is a conservative extension of FILL Nested FILL-sequent: nested sequent that has no nesting of

sequents on the left of ⇒ and no occurrences of −< Why? because then it is free of any traces of −< since only the

−<_{l}^{d} rule creates such nestings

FILL_{dn}: remove −<_{l}^{d}, −<_{r}^{d}, pl_{2} and pr_{1}

Separation Thm: nested FILL-sequents are (cut-free) derivable in

FILL_{dn} iff they are derivable in the original deep calculus Proof: if the end-sequent contains only FILL-formulae then

backward proof search will never create the offending nesting Thm: every rule of FILL_{dn} preserves FILL-validity downwards Cor: FILL_{dn} is sound and cut-free complete for FILL-validity Cor: BiILL is a conservative extension of FILL

Complexity of deciding FILL

Backward proof search: need to try all ways to partition a context

and apply all propagation rules in all ways, but this terminates Subformula property: every formula in the premises is a

subformula of a formula in the conclusion Complexity: FILL is in NP Proof: guess a cut-free derivation and check it in time polynomial

in size of the given formula. Possible since each formula is introduced exactly once in any derivation

Complexity: our calculus handles the problem of deciding constants-only multiplicative linear logic (COMLL) since the nnf-formulae of this logic contain no propositional atoms and no implication connectives and it is known to be NP-hard

Thm: deciding FILL-validity is NP-complete

Our Methodology

Start with a categorially formulated logic L Give a display calculus for L

✓ Easily shown to be complete.

✓ Easily shown to support a cut-elimination procedure. X Embeds L into an extension so conservativity, and hence

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

Refine to a nested sequent calculus with deep inference. ✓ Conservativity, and hence soundness, now clear. ✓ Supports proof search and complexity analysis.

Question: how far can we push this methodology?

We know: it works for the exponentials ! and ? But: BiILL plus additives not conservative over FILL plus

additivies e.g ⊤ ⊢ p, ⊤ is BiILL-valid but not FILL-valid

Our Methodology

Start with a categorially formulated logic L Give a display calculus for L

✓ Easily shown to be complete.

✓ Easily shown to support a cut-elimination procedure. X Embeds L into an extension so conservativity, and hence

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

Refine to a nested sequent calculus with deep inference. ✓ Conservativity, and hence soundness, now clear. ✓ Supports proof search and complexity analysis.

Question: how far can we push this methodology?

We know: it works for the exponentials ! and ? But: BiILL plus additives not conservative over FILL plus

additivies e.g ⊤ ⊢ p, ⊤ is BiILL-valid but not FILL-valid Happy (belated) birthday Gerhard!

Belnap’s Eight Conditions a lá Kracht

(C1) Each formula variable occurring in some premise of a rule ρ is a subformula of some formula in the conclusion of ρ.

(C2) Congruent parameters is a relation between parameters of the identical structure variable occurring in the premise and conclusion

(C3) Each parameter is congruent to at most one structure variable in the conclusion. Equivalently, no two structure variables in the conclusion are congruent to each other.

(C4) Congruent parameters are either all antecedent or all succedent parts of their respective sequent.

(C5) A formula in the conclusion of a rule ρ is either the entire antecedent or the entire succedent. Such a formula is called a principal formula of ρ.

(C6/7) Each rule is closed under simultaneous substitution of arbitrary structures for congruent parameters.

Belnap’s Eight Conditions a lá Kracht

(C8) If there are rules ρ and σ with respective conclusions X ⊢ A and A ⊢ Y with formula A principal in both inferences (in the sense of C5) and if cut is applied to yield X ⊢ Y , then either X ⊢ Y is identical to either X ⊢ A or A ⊢ Y ; or it is possible to pass from the premises of ρ and σ to X ⊢ Y by means of inferences falling under cut where the cut-formula always is a proper subformula of A.

X ⊢ C > D X ⊢ C ⊸ D

U ⊢ C  D ⊢ Z
C ⊸ D ⊢ U > Z

cut

X ⊢ U > Z

U ⊢ C

{X ⊢ C > D \atop X , C ⊢ D}  D ⊢ Z

cut

X , C ⊢ Z

C ⊢ X > Z

cut

U ⊢ X > Z

X , U ⊢ Z
X ⊢ U > Z

Devil’s Advocate Questions

Can’t we do all of this with labelled sequent calculi?

Γ, R(x, y, z), x : A ⊢ z : B, Δ

x and y do not occur in the conclusion

Γ ⊢ y : (A ⊸ B), Δ

Almost certainly we can, but the decidability cannot be read off as we are able to do, and I can’t see the “Grishin” condition

Where are the Grishin rules in the deep calculus? In the logical rules and propagation rules

\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, (S′ ⇒ T′), T ] \atop X [S ⇒ (S′ ⇒ A, T′), T ]} pr_{2}

Isn’t “merge” just another way of hiding annotations? No, it is a very natural definition ... superpose two identical ⇒-trees