From Categorical Semantics to Display Calculi to Deep Nested Sequent Calculi: Formalised for

Full Intuitionistic Linear Logic

Jeremy E. Dawson^{1}, Ranald Clouston^{2}, Rajeev Goré^{1}, and Alwen Tiu^{3}

1 Research School of Computer Science, Australian National University 2 Department of Computer Science, Aarhus University 3 School of Computer Engineering, Nanyang Technological University

Abstract. Proof theory for a logic with categorical semantics can be developed by the following methodology: define a sound and complete display calculus for an extension of the logic with additional adjunctions; translate this calculus to a shallow inference nested sequent calculus; translate this calculus to a deep inference nested sequent calculus; then prove this final calculus is sound with respect to the original logic. This complex chain of translations between the different calculi require proofs that are technically intricate and involve a large number of cases, and hence are ideal candidates for formalisation. We present a formalisation of this methodology in the case of Full Intuitionistic Linear Logic (FILL), which is multiplicative intuitionistic linear logic extended with par. We discuss how our previous formalisations of display calculi and generalised derivability relations proved useful in this work, and discuss the difficulties we encountered in formalising recursive data structures built out of multisets.

1 Introduction

Belnap’s Display Calculi [1, 2] and Kashima’s deep (inference) nested sequent calculi [14] are two powerful modular approaches to structured proof theory with many similarities, but with contrasting strengths. Display calculi are often easy to design for a given logic [10] and enjoy a generic algorithm for cut-elimination. But they usually require the logic to be expanded with additional new logical connectives, begging the question of conservativity, and hence soundness, with respect to the original logic. They also do not enjoy a genuine subformula property and hence are ill-suited to backwards proof search. Deep nested sequent calculi, on the other hand, are not so easy to design, do not come equipped with generic cut-elimination, but do have a genuine subformula property. Often, they enjoy a “separation property” which trivially ensures conservativity, and hence soundness, with respect to the original logic. Recent work claims the best of both worlds by giving sequent calculi in both styles for various logics [5, 16, 11, 12, 18, 15], with the crux being the equivalence of the display and deep nested calculi.

Proving the equivalence of display and deep nested calculi is technically intricate and can involve the verification of hundreds of cases. Such proofs proceed

[figure: FILL-category; BiILL-category; BiILL_{dc}; _{FILL_{dn}}; _{BiILL_{dn}}; _{BiILL_{sn}}]

Fig. 1. The relation between the semantics and proof systems for FILL/BILL.

via an intermediate calculus, a shallow inference nested sequent calculus, and it is the proof of the equivalence of shallow and deep systems that is the most demanding, requiring that every possible interaction of shallow and deep proof rules be covered. We hence have a fruitful proof theoretic methodology which cries out both for mechanised proof checking to increase confidence in its results, and for the use of automated tactics to reduce the drudgery of attaining them. We describe such a formalisation for Full Intuitionistic Linear Logic (FILL) [13], following our earlier work on display and deep nested calculi for this logic [6].

FILL [13] is a substructural logic with linear connectives ⊗, �, ⊸, a unit I for ⊗, and a unit ⊥ for �. Schellinx [17] noted that the standard multipleconclusioned sequent rules for this logic do not enjoy cut-elimination. Hyland and de Paiva [13] claimed to have found a cut-free sequent calculus where typeannotations on formulae tracked and blocked unsound applications of the standard multiple-conclusioned rules. Biermann [3] found a counter-example to Hyland and de Paiva’s cut-elimination proof and gave two solutions using even more complex type-annotations, one due to Bellin. Braüner and de Paiva [4] replaced the type-annotations with a binary relation to track variable occurrences, which also gave cut-elimination. None of these authors give a computational interpretation for their annotations, so they are merely complex syntactical devices to block unsound applications of one multiple-conclusioned rule. Recently, we gave a sound and complete display calculus for FILL and showed how it could be compiled into two sound and complete nested sequent calculi for FILL. Our shallow nested sequent calculus obeys cut-elimination while our deep nested calculus is cut-free complete for FILL, enjoys the sub-formula property, and enjoys terminating backward proof-search, from which we obtained the NP-completeness of the validity problem for FILL [6]. The detailed proofs of these results are highly technical, and require some fifty pages to spell out [7]. Our formalisation formally establishes the correctness of our proof theory for this logic.

Our final proof system FILLdn for FILL is a nested sequent calculus with deep inference, in which the inference rules can act on arbitrary substructures inside a nested sequent. We derive this proof system following the methodology we just outlined and summarised in Figure 1 where a solid arrow indicates that every valid formula in the source is also valid in the target, and a dashed arrow represents the same notion restricted to FILL formula only.

We start at the categorical semantics for FILL in which ⊸ and ⊗ are intimately related by adjunctions shown below as (1):

(A ⊗ B) → C iff (B ⊗ A) → C iff A → (B ⊸ C)  (1)
C → (A � B) iff C → (B � A) iff (C −< B) → A  (2)

We extend FILL with an “exclusion” connective −<, which is intimately related to linear disjunction � by the adjunctions shown in (2). The generalisation ensures that the extended logic BiILL can be encoded directly as a display calculus BiILLdc (with the display property). As explained previously, it is not obvious that BiILL is conservative over FILL, but we resolve this issue later.

Sticking with BiILL, we prove the soundness and completeness of BiILLdc wrt. BiILL-categories in Section 4. From BiILLdc, we derive a nested sequent calculus BiILLsn which is very similar to a display calculus, but with more Gentzen-like introduction rules. We prove that BiILLdc and BiILLsn are equivalent in Section 5. A problem with both BiILLdc and BiILLsn is that the structural connective (proxy) for −< is needed when proving purely FILL-formulae, even though they contain no occurrences of −<. This problem is caused by the structural rules present in both proof systems that guarantee that each has the display property. These structural rules can be absorbed if we allow deep inference, so we refine our shallow nested sequent calculus BiILLsn into a deep nested sequent calculus BiILLdn for BiILL. In Section 6 we show that BiILLsn and BiILLdn are in fact equivalent. This is the most difficult part of our methodology since it involves a highly combinatorial proof. Indeed, in mechanising this proof, we need to consider hundreds of ways in which the shallow rules in BiILLsn may interact with the deep rules in BiILLdn. Automatic tactics in Isabelle/HOL help to discharge many of these cases automatically. Unlike both BiILLdc and BiILLsn, the proof system BiILLdn enjoys a “separation” property [6]: every structural connective that appears in any cut-free proof of a formula is a structural proxy for a logical connective of that formula. Thus a cut-free FILLdn-proof of a FILLformula does not require the structural proxy for −< since FILL-formulae never contain occurrences of −<. Then, simply deleting the introduction rules for −< from BiILLdn gives us a proof system FILLdn for FILL. We resolve the issue of soundness by showing that FILLdn is sound w.r.t. FILL-categories in Section 7. Section 8 concludes.

The Isabelle/HOL theory files for our formalisation can be found at:

   http://users.cecs.anu.edu.au/~jeremy/isabelle/2005/fill

2 Formulae, sequents and derivations

We explain briefly the data structures we use to encode formulae, structures, sequents and derivations.

The language of formula for BiILL is defined using the grammar below:

A ::= p | I | ⊥ | A ⊗ A | A � A | A ⊸ A | A−<A

where p denotes a propositional variable. A FILL formula is just a BiLL formula without any occurrences of −<.

BiLL formulae are defined formally in Isabelle as follows. We let the type variable 's be (Isabelle) strings.

datatype 's pformula =
    Btimes pformula pformula ("_&&& _" [68,68] 67)
  | Bplus pformula  pformula ("_+++ _" [66,66] 65)
  | Blolli pformula pformula ("_--o _" [64,64] 63)
  | Bexcl pformula pformula ("_--< _" [64,64] 63)
  | Btrue ("T") | Bfalse("F") | FV string | PP string

Here the binary constructors correspond to, respectively, ⊗, �, ⊸ and −<. The unary constructors Btrue and Bfalse encode the units I and ⊥, respectively. The constructor PP is used to encode propositional variables, whereas FV is used to encode “scheme variables”; we shall come back to this shortly.

We define the immediate (proper) subformula relation, ipsubfml, which will not need to be changed when new connectives are added.

ipsubfml     :: "('a pformula * 'a pformula) set"
inductive "ipsubfml" (* proper immediate subformula relation *)
  intrs ips_and1 "(P, P &&& Q) : ipsubfml" (etc)

A sequent is made up of antecedent and succedent structures, defined, respectively, as follows:

X_{a} ::= A | Φ | X_{a}, X_{a} | X_{a} < X_{s} X_{s} ::= A | Φ | X_{s}, X_{s} | X_{a} > X_{s}

where Φ is a structural constant. The symbols < and > are the structural counterparts of the connectives −< and ⊸, respectively.

Structures are represented by the datatype below:

datatype 's pstructr = Comma ('s pstructr) ('s pstructr)
  | Gt ('s pstructr) ('s pstructr) | Lt ('s pstructr) ('s pstructr)
  | I | Structform ('s pformula) | SV 's

where Comma, Gt, Lt and I correspond to the structural connectives ‘,’, >, < and Φ. The operator Structform “casts ” a formula into a structure. The constructor SV represents scheme variables for structures. Since we must reason about arbitrary derivations, we have to allow derivations to contain structure variables and reason about their instantiations. We do not encode explicitly the notion of antecedent/succeedent structures in the data type; these notions are enforced via separate predicates when needed (see e.g., Section 5).

Sequents and rules of the calculus are represented by

datatype 'a sequent = Sequent 'a 'a
types 'a psc = "'a list * 'a" (* single step inference *)
types 'a rule = 'a sequent psc

The premises of a rule are represented using a list of sequents while the conclusion is a single sequent. Thus (prems, concl) means a rule with premises prems and conclusion concl. A sequent (Sequent X Y) can also be represented as $X |-

$Y.

We now briefly describe the functions we used to encode derivability. A fuller account is given in [9]. This framework is general in that a rule merely consists of “premises” and a “conclusion”, and is independent of whether the things derived are formulae or sequents, but we will refer to them as formulae.

types 'a psc = "'a list * 'a"       (* single step inference *)
consts
  derl, adm :: "'a psc set => 'a psc set"
  dersl     :: "'a psc set => ('a list * 'a list) set"
  dercsl    :: "'a psc set => ('a list list * 'a list) set"
  derrec    :: "'a psc set => 'a set => 'a set"
  dersrec   :: "'a psc set => 'a set => 'a list set"

An inference rule 'a psc is a list of premises ps and a conclusion c. Then, derl rls is the set of rules derivable from the rule set rls, and derrec rls prems is the set of formulae derivable using rules rls from the set prems of premises. These were defined as inductive sets, using also the functions dersl and dersrec. So (ps, c) ∈ derl rls reflects the shape of a derivation tree: ps is a list of exactly the premises used, in the correct order, whereas c ∈ derrec rls prems holds even if the set of premises prems contains extra formulae.

The auxiliary function dersrec represents several formulae, all derivable from the premises. The auxiliary function dersl represents several derivation trees side by side; (ps, cs) ∈ dersl rls when ps is the concatenation of their lists of premises, and cs is the list of their conclusions. The function dercsl is similar, but it shows which premises are part of which tree. That is, (pss, cs) ∈ dercsl rls implies (concat pss, cs) ∈ dersl rls. Some proofs about derl are easier using dercsl rather than dersl as the auxiliary function.

Finally, (ps, c) is an admissible rule iff: if all premises in ps are derivable, then c is derivable:

(ps, c) ∈ adm rls ⟺ (set ps ⊆ derrec rls ⇒ c ∈ derrec rls).

3 Formalising Display Calculi

Our formalisation of the display calculus BiILLdc is very similar to that in [8], so we shall not go into details of the formalisation and refer the reader instead to [8]. The display system BiILLdc is given in Figure 2, where double-lined inference rules are invertible. The display calculus FILLdc is obtained from BiILLdc by removing the introduction rules for −<.

As in our previous formalisation [8], structure variables like X are encoded as $"X" and formula variables like A are encoded as "A". The quotes are necessary since we handle substitutions explicitly rather than via Isabelle variables [8]. For example, the cut rule is encoded as:

Cut and identity:

(id) p ⊢ p  \begin{aligned}& X ⊢ A & A ⊢ Y \\ (cut) \\ & X ⊢ Y \end{aligned}

Logical rules:

\begin{aligned}& Φ ⊢ X \\ (I ⊢) \\ & I ⊢ X \end{aligned}  (⊥ ⊢) ⊥ ⊢ Φ  (⊢ I) Φ ⊢ I  \begin{aligned}& X ⊢ Φ \\ (⊢ ⊥) \\ & X ⊢ ⊥ \end{aligned}
\begin{aligned}& A, B ⊢ X \\ (⊗ ⊢) \\ & A ⊗ B ⊢ X \end{aligned}  \begin{aligned}X ⊢ A & Y ⊢ B \\ (⊢ ⊗) \\ & X, Y ⊢ A ⊗ B \end{aligned}
\begin{aligned}A ⊢ X & B ⊢ Y \\ (� ⊢) \\ & A � B ⊢ X, Y \end{aligned}  \begin{aligned}& X ⊢ A, B \\ (⊢ �) \\ & X ⊢ A � B \end{aligned}
\begin{aligned}X ⊢ A & B ⊢ Y \\ (⊸⊢) \\ & A ⊸ B ⊢ X > Y \end{aligned}  \begin{aligned}& X ⊢ A > B \\ (⊢⊸) \\ & X ⊢ A ⊸ B \end{aligned}
\begin{aligned}& A < B ⊢ X \\ (−< ⊢) \\ & A−<B ⊢ X \end{aligned}  \begin{aligned}X ⊢ A & B ⊢ Y \\ (⊢ −<) \\ & X < Y ⊢ A−<B \end{aligned}

Structural rules:

\begin{aligned}& X ⊢ Y > Z \\ (rp) \\ & X, Y ⊢ Z \end{aligned}  \begin{aligned}& X, Y ⊢ Z \\ (rp) \\ & Y ⊢ X > Z \end{aligned}  \begin{aligned}& X < Y ⊢ Z \\ (drp) \\ & X ⊢ Y, Z \end{aligned}  \begin{aligned}& X ⊢ Y, Z \\ (drp) \\ & X < Z ⊢ Y \end{aligned}
\begin{aligned}& X, Φ ⊢ Y \\ (Φ ⊢) \\ & X ⊢ Y \end{aligned}  \begin{aligned}& X ⊢ Φ, Y \\ (⊢ Φ) \\ & X ⊢ Y \end{aligned}  \begin{aligned}& X, Y ⊢ Z \\ (Com ⊢) \\ & Y, X ⊢ Z \end{aligned}  \begin{aligned}& X ⊢ Y, Z \\ (⊢ Com) \\ & X ⊢ Z, Y \end{aligned}
\begin{aligned}& W, (X, Y) ⊢ Z \\ (Ass ⊢) \\ & (W, X), Y ⊢ Z \end{aligned}  \begin{aligned}& W ⊢ (X, Y), Z \\ (⊢ Ass) \\ & W ⊢ X, (Y, Z) \end{aligned}
\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}

Fig. 2. FILLdc and BiILLdc: display calculi for FILL and BiILL

 cutr == ([($"X" |- "A"), ("A" |- $"Y")], ($"X" |- $"Y"))

To prove the cut-admissibility result we largely reuse the code we used to prove cut-admissibility for the display calculus for relation algebras [8]. The proof that a connective satisfies Belnap’s C8 condition had to be coded in part individually for each connective, but, even so, we were able to reuse most of our previous code. Each display logic rule of BiILLdc is encoded as shown above for cut, giving rlsb, and its strict subset rlscfb which excludes the cut rule.

Given a set S of encoded rules, the set rulefs S is the (infinite) set of substitutional instances of members of S. From our previous work [9], the rule (ps, c) with list of premise (sequents) ps and conclusion (sequent) c is an admissible rule of S if the following holds, where colon is set-membership ∈:

(?ps : dersrec ?rls {} --> ?c : derrec ?rls {})
 ==> (?ps, ?c) : adm ?rls

We then proved cut-admissibility as below where colon now simply states the name of the theorem:

Theorem 1 (Cut-Admissibility). From cut-free BiILLdc-derivations of X ⊢ A and A ⊢ Y we can obtain a cut-free BiILLdc-derivation of X ⊢ Y.

dc_cut_adm : "rulefs {cutr} <= adm (rulefs rlscfb)"

4 Formalising Categorial Semantics

Definition 1. A FILL-category is a category equipped with

– a symmetric monoidal closed structure (⊗, I, ⊸)

– a symmetric monoidal structure (�, ⊥)

– a natural family of weak distributivity arrows A ⊗ (B � C) → (A ⊗ B) � C.

A BiILL-category is a FILL-category where the � bifunctor has a co-closure −<, so there is a natural isomorphism between arrows A → B � C and A−<B → C.

To interpret BiILL sequents in the category semantics, we use the following translation from (antecedent/succeedent) structures to formulae:

\begin{aligned}& A & Φ & X, Y & X > Y & X < Y \\ τ^{a} & A & I & τ^{a}(X) ⊗ τ^{a}(Y) & & τ^{a}(X)−<τ^{s}(Y) \\ τ^{s} & A & ⊥ & τ^{s}(X) � τ^{s}(Y) & τ^{a}(X) ⊸ τ^{s}(Y) \end{aligned}

Definition 2. A FILL- (resp. BiILL-) sequent X ⊢ Y is satisfied by a FILL- (resp. BiILL-) category if, given any valuation of its propositional variables as objects, there exists an arrow I → τ^{a}(X) ⊸ τ^{s}(Y). It is FILL- (resp. BiILL-) valid if it is satisfied by all such categories. In fact, we only need to check the free categories under their generic valuations.

Definition 3. The free FILL- (resp. BiILL-) category has FILL- (resp. BiILL-) formulae as objects and the following arrows (quotiented by certain equations) where we are given objects A, A′, A′′, B, C and arrows f : A → A′, f′ : A′ → A′′, g : B → C, (♡, K) ∈ {(⊗, I), (�, ⊥)}, and where the co-closure arrows exist in the free BiILL-category only:

\xymatrix{Category: & A \ar[r]^{id} & A & A \ar[r]^{f′∘f} & A′′}
\xymatrix{Symmetric Monoidal: & A♡B \ar[r]^{f♡g} & A′♡C & (A♡B)♡C \ar[r]^{α} & A♡(B♡C) \ar[l]^{α^{−1}}}
\xymatrix{K♡A \ar[r]^{λ} & A \ar[l]^{λ^{−1}} & A♡K \ar[r]^{ρ} & A \ar[l]^{ρ^{−1}} & A♡B \ar[r]^{γ} & B♡A}

Closed:

\xymatrix{A ⊸ B \ar[r]^{A⊸g} & A ⊸ C & (A ⊸ B) ⊗ A \ar[r]^{ε} & B & A \ar[r]^{η} & B ⊸ A ⊗ B}
Weak Distributivity: \xymatrix{A ⊗ (A′ � A′′) \ar[r]^{ω} & (A ⊗ A′) � A′′}

Co-Closed:

\xymatrix{A−<B \ar[r]^{f− <B} & A′−<B & A � B−<A \ar[r]^{ε} & B & A \ar[r]^{η} & B � (A−<B)}

We will suppress explicit reference to the associativity and symmetry arrows.

Definition 3 can also be written as a deducibility relation between formulae where we use the “turnstile” to assert the existence of an arrow, without specifying how it is constructed. For example, the “rules” below capture the definition of “closed” above in which the finer details of the construction A ⊸ g are elided:

\begin{matrix}B ⊢ C \\ A ⊸ B ⊢ A ⊸ C \end{matrix}  (A ⊸ B) ⊗ A ⊢ B  A ⊢ B ⊸ (A ⊗ B)

We formalised this deducibility relation using the display calculus turnstile which we had already defined in Isabelle, but with only a formula (not a more complex structure) on each side. Then the identity arrow and composition of arrows become the usual display calculus identity rule and cut rule. For example, the “closure” rules above are encoded as:

 lolli_monoR == (["B" |- "C"], "A" --o "B" |- "A" --o "C")
 lolliD == ([], ("A" --o "B") &&& "A" |- "B")
 lolliI == ([], "A" |- "B" --o ("A" &&& "B"))

Our encoding is faithful because each arrow required by Definition 3 is encoded as one such rule giving the rules biill cat rules with subset fill cat rules.

In the following, (?A |- ?B) is a sequent with arbitrary formulae on each side. Arbitrary structures would appear as ($?A |- $?B) [8].

Theorem 2. BiILLdc is sound and cut-free complete for BiILL-validity (where the appellation cf captures cut-free).

dc_cat_equiv_cf : "((?A |- ?B) : derrec (rulefs rlscfb) {}) =
  ((?A |- ?B) : derrec (rulefs biill_cat_rules) {})"

5 Shallow Nested Sequent Calculi

In [6], nested sequents are defined as below where A_{i} and B_{j} are formulae:

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

We use Γ and Δ for multisets of formulae and use P, Q, S, T, X, Y, etc., for nested sequents, and S, X, etc., for multisets of nested sequents and formulae. The empty multiset is · (‘dot’). A nested sequent is essentially a display structure, but with the associativity and commutativity of the comma structural connective implicit in the use of multisets. The sequent arrow ⇒ overloads both > and <, depending on whether it occurs in an antecedent or a succeedent position in the sequent. This overloading is intentional, as it allows us to simplify significantly the presentation of the nested sequent rules. The shallow inference system BiILLsn for BiILL is given in Fig. 3.

The most faithful encoding of a nested sequent would be one that uses multisets as a datatype, which is supported by the recent versions of Isabelle [19].

However due to incompatibilities between certain versions of Isabelle we have been constrained to use an older version of Isabelle so as to allow us to reuse proofs for display calculi developed in that version [8]. Our definition of nested sequents is thus as below:

datatype nested = NComma nested nested | Nseq nested nested
                  | NI | NStructform formula | NSV string

In our definition, NSeq is the nested sequent turnstile ⇒, NComma is the comma of nested sequent calculi and NI is its unit. As for display calculi, we allow => instead of Nseq and ,,, instead of NComma. In our Isabelle formalisation, BiILLsn rules are prefixed by sn, e.g., the rp rule is named sn rp. The entire set of rules is called snb rls and its cut-free subset is snb rlscf (see file N Rls.thy). As with the display calculus, we define a function nrulefs to generate the (infinite) set of all substitution instances of a given rule.

Note that our encoding nested does not capture the notion of nested sequent exactly since it allows structures which may not contain a top-level =>. Since our rules always have a => as the top-level operator, all uses of nested in our formalisation do capture nested sequents as defined. Note also that associativity and commutativity of NComma and the fact that NI is its unit is not enforced in the datatype. Rather, we need to define additional structural rules to account for these. These rules are straightforward and are omitted here.

We defined a relation ms deep equiv of multiset-equivalence, under which any two Isabelle nested sequents are equivalent if they would be the same if a collection of Isabelle nested sequents, separated by commas, were considered as a multiset. This includes where the difference between two Isabelle nested sequents occurs at any depth. Its definition relies on a function ms of ns for “multiset of Isabelle nested sequent” which turns (eg) the Isabelle nested sequent (S, T), U into the multiset {# S, T, U #}, and a relation ms ms deep equiv, which expresses equivalence of multisets of Isabelle nested sequents.

We now prove the equivalence between the display calculus and the shallow nested sequent calculus. First we defined translation functions

consts
  nested_to_str :: "bool => nested => structr"
  nested_to_seq :: "nested => structr sequent"
  seq_to_nested :: "structr sequent => nested"
  str_to_nested :: "structr => nested"

where the translation from a nested sequent to a display calculus structure depends on whether it is in an antecedent or succedent position.

The first two of these functions convert a nested sequent to a display calculus sequent or structure by converting ‘⇒’ to ‘⊢’ (for nested to seq), to ‘>’ (for nested to str True), or to ‘<’ (for nested to str False), and converting comma to comma. The latter two convert ‘⊢’, ‘>’, and ‘<’ to ‘⇒’.

For example nested to seq takes (A ⇒ B) ⇒ (C ⇒ D) to A < B ⊢ C > D, and seq to nested does the reverse.

Cut and identity:  p ⇒ p id  \begin{matrix}S ⇒ U, A & A, V ⇒ T \\ S, V ⇒ U, T \end{matrix} cut

Structural rules:

\begin{matrix}{S ⇒ T , T′ \atop (S ⇒ T ) ⇒ T′} ^{drp^{1}} & {S, T ⇒ T′ \atop S ⇒ (T ⇒ T′)} ^{rp^{1}} & {(S ⇒ S′), T ⇒ T′ \atop (S, T ⇒ S′) ⇒ T′} gl \\ {(S ⇒ T ) ⇒ T′ \atop S ⇒ T , T′} drp_{2} & {S ⇒ (T ⇒ T′) \atop S, T ⇒ T′} rp_{2} & {S ⇒ (S′ ⇒ T′), T \atop S ⇒ (S′ ⇒ T′, T )} gr \end{matrix}

Logical rules:

⊥ ⇒ · ⊥_{l}  {S ⇒ T \atop S ⇒ T , ⊥} ⊥_{r}  {S ⇒ T \atop S, I ⇒ T} I_{l}  · ⇒ I I_{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}}

Fig. 3. The shallow inference system BiILLsn.

If we consider only the set of display calculus sequents with < and > in antecedent and succedent positions respectively (expressed by seq LtGtOK), and the set of nested sequents of the form S ⇒ T, then nested to seq and seq to nested are mutually inverse bijections between these sets. We can express this by:

nest_seq_equiv : "(seq_LtGtOK ?seq & seq_to_nested ?seq = ?nes) =
      ((EX a s. ?nes = ($a => $s)) & nested_to_seq ?nes = ?seq)"

The proof systems BiILLdc and BiILLsn are very similar. In fact, their structural rules are the same (modulo some notational variance). The only difference is that BiILLdc requires that introduction rules be applied only to a ‘displayed’ formula, i.e., the principal formula must appear in isolation either on the left or on the right of the turnstile. Their equivalence is not really surprising, so we state their equivalence here and refer the reader to Isabelle proof scripts for details.

Theorem 3. The display sequent A ⊢ B is cut-free BiILLdc-derivable iff the nested sequent A ⇒ B is cut-free BiILLsn-derivable. The display sequent I ⊢ A is cut-free BiILLdc-derivable iff the nested sequent ⇒ B is cut-free BiILLsnderivable.

If X_{1}[ ] = [ ] and X_{2}[ ] = [ ] then X_{1}[ ] • X_{2}[ ] = {[ ]}

If X_{1}[ ]  = (Γ_{1}, Y_{1}[ ], P_{1}, …, P_{m} ⇒ Δ_{1}, Q_{1}, …, Q_{n}) and
X_{2}[ ]  = (Γ_{2}, Y_{2}[ ], S_{1}, …, S_{m} ⇒ Δ_{2}, T_{1}, …, T_{n}) then
X_{1}[ ] • X_{2}[ ] = { (Γ_{1}, Γ_{2}, Y [ ], U_{1}, …, U_{m} ⇒ Δ_{1}, Δ_{2}, V_{1}, …, V_{n}) |
Y [ ] ∈ Y_{1}[ ] • Y_{2}[ ] and U_{i} ∈ P_{i} • S_{i} for 1 ≤ i ≤ m and
V_{j} ∈ Q_{j} • T_{j} for 1 ≤ j ≤ n }
If X_{1}[ ]  = (Γ_{1}, P_{1}, …, P_{m} ⇒ Δ_{1}, Y_{1}[ ], Q_{1}, …, Q_{n}) and
X_{2}[ ]  = (Γ_{2}, S_{1}, …, S_{m} ⇒ Δ_{2}, Y_{2}[ ], T_{1}, …, T_{n}) then
X_{1}[ ] • X_{2}[ ] = { (Γ_{1}, Γ_{2}, U_{1}, …, U_{m} ⇒ Δ_{1}, Δ_{2}, Y [ ], V_{1}, …, V_{n}) |
Y [ ] ∈ Y_{1}[ ] • Y_{2}[ ] and U_{i} ∈ P_{i} • S_{i} for 1 ≤ i ≤ m and
V_{j} ∈ Q_{j} • T_{j} for 1 ≤ j ≤ n }

Fig. 4. Merging of contexts

dc_sn_equiv_alt = "((?A |- ?B) : derrec (rulefs rlscfb) {}) =
         ((?A => ?B) : derrec (nrulefs snb_rlscf) {})"
dc_sn_equiv : "((T |- ?A) : derrec (rulefs rlscfb) {}) =
         (($NI => ?A) : derrec (nrulefs snb_rlscf) {})"

6 Deep Nested Sequent Calculi

The nested sequent system BiILLdn is given in Figure 5. Inference rules in BiILLdn are applied in a context, i.e., a nested sequent with a hole [ ]. Notice that structural rules are missing from BiILLdn. The branching rules require operations to merge contexts and nested sequents, which are explained below. The zero-premise rules require that certain sequents or contexts are hollow, i.e., containing no occurrences of formulae.

We needed to define several notions of contexts in our formalisation. The first two accept a set of nested sequent rules and returns a set of nested sequent rules while the third accepts a set of Isabelle nested “sequents” and returns a set of Isabelle nested “sequents”

  ctxt :: "nested psc set => nested psc set"
  dctxt :: "nested psc set => nested psc set"
  hctxt :: "nested set => nested set"

For example, if ([P], C) ∈ R where [P] is a singleton list containing one premise rather than a context, then ([X[P]], X[C]) ∈ ctxt R is also a single premise rule. Likewise, if C ∈ R and X[ ] is a hollow context then X[C] ∈ hctxt R.

Some of the proofs involving ctxt were easier using a related definition dctxt where X[S ⇒ T] means adding nested sequents to S or to T, rather than to S ⇒ T. For example, if ([P_{1} ⇒ P_{2}], (C_{1} ⇒ C_{2})) ∈ dctxtR, then ([P_{1}, X ⇒ P_{2}], (C_{1}, X ⇒ C_{2})) ∈ dctxtR. Similarly, if ([P_{1} ⇒ P_{2}], (C_{1} ⇒ C_{2})) ∈ dctxtR then ([(P_{1} ⇒ P_{2}) ⇒ X], ((C_{1} ⇒ C_{2}) ⇒ X)) ∈ dctxtR

The merge set X_{1} • X_{2} of two sequents X_{1} and X_{2} is defined as:

Propagation rules:

{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}

Identity and logical rules: In branching rules, X[ ] ∈ X_{1}[ ] • X_{2}[ ], S ∈ S_{1} • S_{2} and T ∈ T_{1} • T_{2}.

X[ ], U and V are hollow. X[U, p ⇒ p, V] id^{d}  X[ ], U and V are hollow. X[⊥, U ⇒ V] ⊥_{l}^{d}  {X[S ⇒ T ] \atop X[S ⇒ T , ⊥]} ⊥_{r}^{d}

{X[S ⇒ T ] \atop X[S, I ⇒ T ]} I_{l}^{d}  X[ ], U and V are hollow. X[U ⇒ I, V] I_{r}^{d}
{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}

Fig. 5. The deep inference system BiILLdn.

X_{1} • X_{2} = { (Γ_{1}, Γ_{2}, Y_{1}, …, Y_{m} ⇒ Δ_{1}, Δ_{2}, Z_{1}, …, Z_{n}) | X_{1} = (Γ_{1}, P_{1}, …, P_{m} ⇒ Δ_{1}, Q_{1}, …, Q_{n}) and

X_{2} = (Γ_{2}, S_{1}, …, S_{m} ⇒ Δ_{2}, T_{1}, …, T_{n}) and

Y_{i} ∈ P_{i} • S_{i} for 1 ≤ i ≤ m and Z_{j} ∈ Q_{j} • T_{j} for 1 ≤ j ≤ n }

When X ∈ X_{1} • X_{2}, we say that X_{1} and X_{2} are a partition of X.

The merge set X_{1}[ ] • X_{2}[ ] of two contexts X_{1}[ ] and X_{2}[ ] is defined in Figure 4. If X[ ] = X_{1}[ ] • X_{2}[ ] we say X_{1}[ ] and X_{2}[ ] are a partition of X[ ]. We extend the notion of a merge set between multisets of formulae and sequents as follows. Given X = Γ ∪ {X_{1}, …, X_{n}} and Y = Δ ∪ {Y_{1}, …, Y_{n}} their merge set contains all multisets of the form: Γ ∪ Δ ∪ {Z_{1}, …, Z_{n}} where Z_{i} ∈ X_{i} • Y_{i}.

In Isabelle we defined merged sequents, using triples, so in effect (X_{1}, X_{2}, X) ∈ rmerge means X is a sequent in X_{1} • X_{2}. This is easier to define than in the paper where multisets are used, because we require simply that each structural atom (formula or structure variable) in X is replaced by Φ in exactly one of X_{1} or X_{2}. That is, each atom has to go in one partition or the other. Likewise, to express the idea of X_{1}[ ] • X_{2}[ ] we define (X_{1}, X_{2}, X) ∈ rmerge1(Y_{1}, Y_{2}, Y) to be similar except that at one spot X contains Y, where X_{i} contains Y_{i}.

We illustrate here some key steps in the formalisation of the equivalence between BiILLsn and BiILLdn. We show here only the translation from shallow nested sequent proofs to deep nested sequent proofs, which is the more difficult part of the equivalence.

The key lemma here is that the rules rp_{i}, drp_{i}, gl and gr which are in BiILLsn but not in the deep calculus BiILLdn are admissible in BiILLdn.

Lemma 1. The rules drp_{1}, rp_{1}, drp_{2}, rp_{2}, gl, and gr permute up over all logical rules of BiILLdn.

This is the permutation lemma, that (in general) where one of the shallow rules in question follows a rule of BiILLdn in a derivation, then the derivation can be re-ordered so that the shallow rule precedes the deep rule. To prove this lemma, we need to use two additional structural rules, called eg and ig [7], that can be shown to be admissible in BiILLsn. We illustrate here a step in the proof of this permutation lemma, i.e., when permuting structural rules over a single-premise logical rule. We proved theorems of the following form

p_rp_anda : "?c = ($?ca => $?cs) -->
 ([?p], ?c) : ctxt (nrulefs {sn_anda}) -->
 (?c, ?c') : ms_deep_equiv --> ([?c'], ?d') : nrulefs {sn_rp} -->
 (EX p' q q' d.  (?p, p') : ms_deep_equiv &
  [p'], q) : nrulefs {sn_rp} & (q, q') : ms_deep_equiv &
  ([q'], d) : dctxt (nrulefs {sn_anda}) & (d, ?d') : ms_deep_equiv)"

That is, where a structural rule, e.g., rp_{1}, appears below a deep logical rule in a derivation, the derivation steps may be permuted so that the logical rule follows the other rule.

It may be noted that this result uses dctxt, not ctxt, in the conclusion. This made semi-automatic proof easier; the lemmas for all the logical rules concerned (6 of them) for all the structural rules involved (6 of them) were done using just three separate sets of tactics.

The proofs of the permutation lemma involved a large number of cases, because a sequent expression such as X[S ⇒ T ] can match a given sequent Z in numerous ways, for two reasons:

– when S and T are multisets, there are many ways that (S, …) ∈ ms deep equiv can be achieved, and

– the context X[ ] may be of any size, which means that S ⇒ T can match any part of Z.

The attempted proof encounters plenty of obviously impossible cases such as a formula matching S ⇒ T . After these are detected and eliminated, we counted the cases where a goal (such as the conclusion of p rp anda) is actually solved. These cases numbered 616, which shows the value of automating the process as much as possible.

Theorem 4. Every rule that is cut-free derivable in BiILLsn is (cut-free) admissible in BiILLdn.

sn_dn_der : "derl (nrulefs snb_rlscf) <= adm biilldn"

A sequent is cut-free provable (derivable from the empty set of assumption sequents) in BiILLsn iff it is provable BiILLdn.

sn_dn_equiv : "(?r : derrec (nrulefs snb_rlscf) {}) =
               (?r : derrec biilldn {})"

The formula A is cut-free provable in the display calculus iff it is (cut-free) provable in BiILLdn.

dc_dn_equiv : "((T |- ?A) : derrec (rulefs rlscfb) {}) =
               (($NI => ?A) : derrec biilldn {})"

7 Soundness of the Deep Nested Sequent FILL

Definition 4. A nested sequent S is BiILL-valid if there is an arrow I → τ^{s}(S) in the free BiILL-category. A nested sequent is a (nested) FILL-sequent if it has no nesting of sequents on the left of ⇒, and no occurrences of −< at all.

The formula translation of τ^{s} (see Section 4) can be adapted straightforwardly to map FILL-sequents to FILL-formulae. Such a sequent S is FILL-valid if there is an arrow I → τ^{s}(S) in the free FILL-category.

In the Isabelle proofs we defined a FILL-sequent S as a sequent such that τ^{s}(S) has no occurrence of −<.

Let FILLdn be the proof system obtained from BiILLdn by restricting to FILL-sequents and removing the rules pr_{1}, pl_{2}, −<_{l}^{d} and −<_{r}^{d}. Our goal in this section is to show that FILLdn is sound w.r.t. FILL categories.

In our formalisation, we in fact defined the rules filldn of FILLdn without requiring the sequents involved to be FILL-sequents. We then defined a corresponding set sfilldn of rules, requiring that the sequents are FILL-sequents.

dn_der_biill_sfill : "[| ?c : derrec biilldn ?ps;
    ALL U. (U, ntau True ?c) : ipsubfml^* --> U ~: excl_fmls |] ==>
    ?c : derrec sfilldn ?ps"

The soundness proof consists of a series of lemmas showing that the rules of FILLdn preserves validity going downward (from premises to conclusion). We illustrate one particularly challenging lemma that involves context merging.

Lemma 2. Take X[ ] ∈ X_{1}[ ]•X_{2}[ ] and T ∈ T_{1} •T_{2}. Then the following arrows exist in the free FILL-category for all A, B, Γ_{1} and Γ_{2}:

(a) τ^{s}(X_{1}[Γ_{1} ⇒ A, T_{1}]) ⊗ τ^{s}(X_{2}[Γ_{2} ⇒ B, T_{2}]) → τ^{s}(X[Γ_{1}, Γ_{2} ⇒ A ⊗ B, T ]);

(b) τ^{s}(X_{1}[Γ_{1} ⇒ A, T_{1}]) ⊗ τ^{s}(X_{2}[Γ_{2}, B ⇒ T_{2}]) → τ^{s}(X[Γ_{1}, Γ_{2}, A ⊸ B ⇒ T ]);

(c) τ^{s}(X_{1}[Γ_{1}, A ⇒ T_{1}]) ⊗ τ^{s}(X_{2}[Γ_{2}, B ⇒ T_{2}]) → τ^{s}(X[Γ_{1}, Γ_{2}, A � B ⇒ T ]);

This lemma corresponds to soundness of branching logical rules of FILLdn. We proved the inductive part (involving the contexts X_{i} and X) once, in the form of fill rmerge1 der nseq. Then we proved the base case (without X_{i} and X) for each connective, resulting in three theorems lem27s of which one is shown.

fill_rmerge1_der_nseq : "[| (?Ta, ?Tb, ?Tc) : rmerge1 (?A, ?B, ?C);
  ?prems = {ntau True ?A &&& ntau True ?B |- ntau True ?C};
  (?W, ntau False ?C) : ipsubfml^* & ?W : excl_fmls;
  ALL U. (U, ntau True ?Tc) : ipsubfml^* --> U ~: excl_fmls |] ==>
  (ntau True ?Ta &&& ntau True ?Tb |- ntau True ?Tc) :
    derrec (rulefs fill_cat_rules) ?prems"
lem27s (first one) :
  "[| (?A, ?B, ?C) : dn_ands; (?Ta, ?Tb, ?Tc) : rmerge1 (?A, ?B, ?C);
    ALL U. (U, ntau True ?Tc) : ipsubfml^* --> U ~: excl_fmls |] ==>
  (ntau True ?Ta &&& ntau True ?Tb |- ntau True ?Tc) :
    derrec (rulefs fill_cat_rules) {}"

Theorem 5. For every rule of FILLdn, if the premises are FILL-valid then so is the conclusion.

filldn_rules_valid : "[| (?ps, ?c) : filldn;
  ALL U. (U, ntau True ?c) : ipsubfml^* --> U ~: excl_fmls |] ==>
  (T |- ntau True ?c) : derrec (rulefs fill_cat_rules)
    ((%p. T |- ntau True p) ` set ?ps)"

Theorem 6. A FILL-formula is FILL-valid iff it is FILLdn-provable, and BiILL is conservative over FILL.

8 Conclusion and future work

Finding a cut-free sequent calculus for FILL has been a notoriously difficult problem, as we have reviewed in our introduction, and involved candidate proof systems that turned out to be incomplete. Indeed, our initial attempt at the soundness proof for one candidate proof system was found to be flawed, only after we attempted to formalise it in Isabelle/HOL. Our formalisation finally establishes convincingly that our deep nested calculus FILLdn is both sound and complete for FILL. Apart from our FILLdn, all other existing proof calculi for FILL still require complex annotations to ensure cut-elimination.

Taking a broader perspective, we have shown a detailed formalisation of a methodology for deriving a deep nested sequent calculus for a logic from its categorical semantics via a display calculus and a shallow nested sequent calculus for a natural extension containing new additional connectives. For future work, we plan to apply this same formalised methodology to derive deep nested sequent calculi for a wide range of logics [5, 16, 11, 12, 18, 15]. There are indications that a substantial part of our current formalisation can be adapted to such logics.

A crucial difference between these logics and FILL is the additional structural rules of contraction and weakening. Contraction and weakening give rise to “additive” context splitting in branching rules, where contexts are duplicated across both premises. Our multiplicative context splitting is actually more general and can simulate such additive splitting, when contraction and weakening are present. Thus we think a similar formalisation effort for, say, nested sequent calculi for modal logics [12], would benefit significantly from our current formalisation.

References

1. N. D. Belnap. Display logic. Journal of Philosophical Logic, 11:375–417, 1982.

2. N. D. Belnap. Linear logic displayed. Notre Dame Journal of Formal Logic, 31:15– 25, 1990.

3. G. M. Bierman. A note on full intuitionistic linear logic. APAL, 79(3):281–287, 1996.

4. T. Bräuner and V. de Paiva. A formulation of linear logic based on dependencyrelations. In CSL ’97, volume 1414 of LNCS, pages 129–148, 1997.

5. K. Brünnler. Deep sequent systems for modal logic. Archive for Mathematical Logic, 48(6):551–577, 2009.

6. R. Clouston, J. E. Dawson, R. Goré, and A. Tiu. Annotation-free sequent calculi for full intuitionistic linear logic. In CSL, volume 23 of LIPIcs, pages 197–214. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013.

7. R. Clouston, J. E. Dawson, R. Goré, and A. Tiu. Annotation-free sequent calculi for full intuitionistic linear logic - extended version. CoRR, abs/1307.0289, 2013.

8. J. E. Dawson and R. Goré. Formalised cut admissibility for display logic. In TPHOLs, pages 131–147, 2002.

9. J. E. Dawson and R. Goré. Generic methods for formalising sequent calculi applied to provability logic. In LPAR (Yogyakarta), pages 263–277, 2010.

10. R. Goré. Substructural logics on display. Log. J. IGPL, 6(3):451–504, 1998.

11. R. Goré, L. Postniece, and A. Tiu. Cut-elimination and proof search for biintuitionistic tense logic. In Advances in Modal Logic, pages 156–177. College Publications, 2010.

12. R. Goré, L. Postniece, and A. Tiu. On the correspondence between display postulates and deep inference in nested sequent calculi for tense logics. LMCS, 7(2), 2011.

13. M. Hyland and V. de Paiva. Full intuitionistic linear logic (extended abstract). Ann. Pure Appl. Logic, 64(3):273–291, 1993.

14. R. Kashima. Cut-free sequent calculi for some tense logics. Studia Log., 53:119–135, 1994.

15. J. Park, J. Seo, and S. Park. A theorem prover for boolean bi. In POPL, pages 219–232. ACM, 2013.

16. F. Poggiolesi. The method of tree-hypersequents for modal propositional logic. In J. M. D. Makinson and H. Wansing, editors, Trends in Logic: Towards Mathematical Philsophy, pages 31–51. Springer, 2009.

17. H. Schellinx. Some syntactical observations on linear logic. JLC, 1(4):537–559, 1991.

18. L. Straßburger. Cut elimination in nested sequents for intuitionistic modal logics. In FoSSaCS, volume 7794 of LNCS, pages 209–224, 2013.

19. D. Traytel, A. Popescu, and J. C. Blanchette. Foundational, compositional (co)datatypes for higher-order logic: Category theory applied to theorem proving. In LICS, pages 596–605, 2012.