From 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.

1 Introduction

Belnap’s Display Calculus [1] is a powerful modular approach to structural proof theory. Display calculi are often easy to design for a given logic [9] and enjoy a generic algorithm for cut-elimination. However they usually require the logic to be expanded with new structural connectives, raising 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. Various authors [4, 15, 10, 11, 14, 5] have addressed these shortcomings by using some variation of nested sequent calculus with deep inference [13]. Such deep nested calculi employ a syntax similar to display calculi, but lack their ease of design and generic cut-elimination algorithm. Conversely, deep nested calculi can be designed to have a genuine subformula property, and a “separation property” that trivially yields conservativity results [10, 11, 5]. Since display calculi and deep nested calculi can have contrasting strengths, it is useful to provide sequent calculi in both styles for a given logic. The crux of such a development is the proof of equivalence between 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 via an intermediate calculus, a shallow inference nested sequent calculus, and it is the proof of the equivalence of shallow and deep calculi 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) [12], following our earlier work on display and deep nested calculi for this logic [5].

Schellinx [16] considered the standard multiple-conclusioned sequent calculus for intuitionistic logic (where the right-implication rule is restricted to prevent collapse to classical logic) without weakening and contraction, and showed that it does not enjoy cut-elimination. Hyland and de Paiva [12] gave this logic (with cut) the name Full Intuitionistic Linear Logic, and defined categorical semantics for it, giving several natural examples of categories exhibiting the required structure. They further claimed to have found a cut-free sequent calculus for FILL, in which term-assignments on formulae are put to novel use to block unsound applications of right-implication, via a freeness check on abstracted variables. Reasoning about freeness in the presence of binders is a well known source of subtle error, and a major topic of formalisation research (e.g. [19]). Indeed Bierman [2] found a counter-example to Hyland and de Paiva’s cut-elimination proof exploiting a binding-related error, and presented two solutions using even more complex type-annotations, one due to Bellin. Braüner and de Paiva [3] subsequently suggested a cut-free calculus relying on annotations on sequents, rather than formulae. Two previous claims in the literature to annotation-free sequent calculi for FILL were erroneous, as discussed in [5].

Our recent contribution [5] to this rather vexed history was to show that annotations are not necessary; we gave a sound and complete display calculus for FILL and showed how it can be compiled into two equivalent nested sequent calculi, one with shallow inference and the other with deep inference. In particular the deep calculus is cut-free complete for FILL, enjoys the sub-formula property, and supports terminating backward proof-search, from which we obtained the NP-completeness of the validity problem for FILL. The derivation of these results, given in more detail in [6], is unavoidably highly technical, and given its difficulty and the history of FILL outlined above we sought to formalise our results in the proof assistant Isabelle/HOL. The completed formalisation presented in this paper finally establishes the correctness of a sequent calculus for this logic. In fact an initial attempt to prove the soundness of our calculus was found to be flawed only when we tried to formalise it (see below for more details), so this development has been an invaluable part of even our ‘pen-and-paper’ work.

We now outline our proof stategy [5] as formalised in this paper. FILL has the usual relation between multiplicative conjunction ⊗ and implication ⊸, where → denotes an arrow in a category (see Section 3):

(A ⊗ B) → C iff (B ⊗ A) → C iff A → (B ⊸ C)  (1)

The display property of display calculi, which underlies the generic cut-elimination algorithm, requires the introduction of new structural connectives, so it is clarifying to regard a display calculus as defining a larger logic with new logical connectives. In this case we have a multipicative exclusion −<, defined with respect to multiplicative disjunction (or par) � in a manner dual to (1):

C → (A � B) iff C → (B � A) iff (C −< B) → A  (2)

In Sec. 2 and Sec. 3, we extend the syntax of FILL with −< and extend the semantics of FILL to obtain Bi-Intuitionistic Linear Logic (BiILL). In Sec. 4 we give a display calculus BiILLdc which is easily seen to be sound and complete for BiILL and hence complete for the sublogic FILL. The soundness of BiILLdc for FILL corresponds to the conservativity of BiILL over FILL. We first attempted to prove the soundness result directly via a rewriting strategy which removed occurrences of exclusion from a BiILLdc-derivation of a FILL-formula to give an exclusion-free BiILLdc-derivation of the same FILL-formula. This rewriting strategy turned out to be flawed, as it may not always terminate. Instead, we define two nested sequent calculi for BiILL: BiILLsn with shallow inference in Sec. 5, and BiILLdn with deep inference in Sec. 6. The equivalence of BiILLsn and BiILLdn, established as Thm. 4 in Sec. 6, is the technical highlight of the formalisation, with 616 cases verified. Thm. 5 in Sec. 7 shows that because of a separation property, BiILLdn easily specialises to a deep nested calculus FILLdn with no trace of exclusion. Thm. 6 then shows that the calculus FILLdn is sound for FILL, thereby proving conservativity of BiILL over FILL. Sec. 8 concludes.

Our methodology is summarised below, 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 formulae only:

[figure: FILL-category; Def. 1; BiILL-category; Thm. 2; BiILL_{dc}; Thm. 3; _{FILL_{dn}}; Thm. 6; _{BiILL_{dn}}; Thm. 5; _{BiILL_{sn}}; Thm. 4]

We used Isabelle/HOL 2005 so that we could rework the cut-elimination proofs from our previous work on formalising cut elimination for display calculi [7]. As discussed in Section 5, one problem we found was the lack of support for nested datatypes involving multisets. The Isabelle/HOL theory files for our formalisa-

tion are 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 formulae for BiILL is defined using the grammar below where p denotes a propositional variable:

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

A FILL formula is just a BiILL formula without any occurrences of −<.

BiILL 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, and FV is used to encode “scheme variables”; we shall come back to these shortly.

We define the immediate (proper) subformula relation, ipsubfml.

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

A BiILL-sequent is a pair X_{a} ⊢ X_{s} of an antecedent and a succedent structure, 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. A FILL-sequent is a BiILL-sequent containing no occurrence of < or −<. The relation between formulae and structures will be made precise in the next section.

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)
  | Phi | Structform ('s pformula) | SV 's

where Comma, Gt, Lt and Phi 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. Sec. 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. We write $X |- $Y to denote (Sequent X Y).

We now briefly describe the functions we used to encode derivability. A fuller account is given in [8]. 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.

consts  derl, adm :: "'a psc set => 'a psc set"
        derrec    :: "'a psc set => 'a set => 'a set"
        dersl     :: "'a psc set => ('a list * 'a list) set"
        dersrec   :: "'a psc set => 'a set => 'a list set"

An inference rule (ps, c) : '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 auxiliary functions dersl and dersrec, which concern the derivability of all members of a list. So to say (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 for any set of premises prems containing those required.

Since we use cut-admissibility for Display Calculi, and also some rules of BiILLsn are admissible (not derivable) in BiILLdn (see Theorem 4), we we need to formalise the notion that a rule of one system is admissible in another system: (ps, c) is admissible 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 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.

To establish validity it suffices to show a hom-set is non-empty in the free Ranald, please check FILL- (resp. BiILL-) categories. We sketch the definitions of these below, omit- this. ting the equations that hold between arrows in these categories.

\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)}

Fig. 1. Arrows of the free BiILL-category

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

Def. 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 formalise this deducibility relation using the sequents of the previous section, but with only a formula (not a more complex structure) on each side. Then the identity arrow and composition of arrows become the usual identity and cut rules. As another 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.

4 Formalising Display Calculi

Our formalisation of the display calculus BiILLdc is very similar to that in [7], so we shall not give full details here. The display system BiILLdc is given in Fig. 2, where double-lined inference rules are invertible.

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. Display calculus BiILLdc for BiILL

As in our previous formalisation [7], 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 [7]. For example, the cut rule is encoded as:

 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 [7]. Belnap [1] gave eight conditions, C1-C8, which guarantee cut-elimination for a given display calculus. Previous work has shown that all except C8 are trivial or can be checked automatically [7]. The proof that a connective satisfies Belnap’s C8 condition has 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 the set of rules named biilldc, and its strict subset biilldc_cf 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 [8], 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

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.

We then proved cut-admissibility as below, where colon now simply states the name of the theorem. The formal proof reuses the work described in [7].

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 biilldc_cf)"

We can now gain our first result linking proof theory and semantics. In the following, (?A |- ?B) is a sequent with arbitrary formulae on each side. Arbitrary structures would appear as ($?A |- $?B) [7].

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 biilldc_cf) {}) =
  ((?A |- ?B) : derrec (rulefs biill_cat_rules) {})"

5 Shallow Nested Sequent Calculi

In [5] 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 simplifies the presentation of the nested sequent rules [5]. 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 recent versions of Isabelle [18]. However due to incompatibilities between versions of Isabelle we have been constrained to use an older version of Isabelle to allow us to reuse proofs for display calculi developed in that version [7]. Our definition of nested sequents is thus as below:

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

In our definition, NSeq is the nested sequent turnstile ⇒, NComma is the comma of nested sequent calculi and NPhi 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 biillsn and its cut-free subset is biillsn cf (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.

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.

To prove BiILLdc and BiILLsn equivalent, we define 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.

Considering the set of display calculus sequents with < and > only in antecedent and succedent positions respectively (expressed as seq LtGtOK), and the set of nested sequents, then we have mutually inverse bijections nested to seq and seq to nested 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; their structural rules are the same (modulo some notational variance). The only difference is that BiILLdc requires that logical 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 surprising, so we state their equivalence here and refer the reader to the 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, and I ⊢ A is cut-free BiILLdc-derivable iff the nested sequent · ⇒ A is cut-free BiILLsn-derivable.

dc_sn_equiv_alt = "((?A |- ?B) : derrec (rulefs biilldc_cf) {}) =
         ((?A => ?B) : derrec (nrulefs biillsn_cf) {})"
dc_sn_equiv : "((T |- ?A) : derrec (rulefs biilldc_cf) {}) =
         (($NPhi => ?A) : derrec (nrulefs biillsn_cf) {})"

6 Deep Nested Sequent Calculi

Deep inference rules for nested sequents are applied in a context, i.e., a nested sequent with a hole [ ]. We use several notions of contexts in our formalisation. The first two accept a set of nested sequent rules and return a set of nested sequent rules while the third accepts 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 (rather than a context) containing one premise, 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})) ∈ dctxt R, then ([P_{1}, X ⇒ P_{2}], (C_{1}, X ⇒ C_{2})) ∈ dctxt R. Similarly, if ([P_{1} ⇒ P_{2}], (C_{1} ⇒ C_{2})) ∈ dctxt R then ([(P_{1} ⇒ P_{2}) ⇒ X], ((C_{1} ⇒ C_{2}) ⇒ X)) ∈ dctxt R

The nested sequent system BiILLdn is given in Fig. 4. Notice that it lacks the structural rules. The zero-premise rules require that certain sequents or contexts are hollow, i.e., contain no occurrences of formulae. The branching rules require operations to merge contexts and nested sequents, which are explained below.

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

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 }

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. 4. The deep inference system BiILLdn.

The merge set X_{1}[ ] • X_{2}[ ] of two contexts X_{1}[ ] and X_{2}[ ] is defined in Figure 5. 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 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.

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. 5. Merging of contexts

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. 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_irp_anda : "?c = ($?ca => $?cs) -->
  ([?p], ?c) : ctxt (nrulefs {sn_anda}) -->
  (?c, ?c') : ms_deep_equiv --> ([?c'], ?d') : nrulefs {invert sn_rp} -->
  (EX p' q q' d. (?p, p') : ms_deep_equiv &
    ([p'], q) : nrulefs {invert 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:

– for multisets S and T , there are many ways to achieve (S, …) ∈ ms deep equiv – the size of context X[ ] is arbitrary, so S ⇒ T can match any part of Z.

The attempted proof encounters many obviously impossible cases such as a formula matching S ⇒ T . After these are 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. All rules cut-free derivable in BiILLsn are (cut-free) admissible in BiILLdn.

sn_dn_der : "derl (nrulefs biillsn_cf) <= 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 biillsn_cf) {}) =
               (?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 biilldc_cf) {}) =
               (($NPhi => ?A) : derrec biilldn {})"

7 Soundness of the Deep Nested Calculus FILLdn

Definition 4. A nested sequent is a nested FILL-sequent if it has no nesting of sequents on the left of ⇒, and no occurrences of −<.

BiILLdn enjoys the separation property that rule applications with FILLsequents as their conclusions may only have FILL-sequents as their premises; note that the display calculus BiILLdc obviously lacks this property, given (drp). We hence define FILLdn as the proof system obtained from BiILLdn by restricting to FILL-sequents and removing the unnecessary rules pr_{1}, pl_{2}, −<_{l}^{d} and −<_{r}^{d}. Our goal here is to show that FILLdn is sound with respect to FILL categories.

The formula translation of τ^{s} (see Sec. 3) can be adapted straightforwardly to map (nested) 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 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.

Theorem 5. A BiILLdn-derivation of a FILLdn-sequent is a FILLdn-derivation.

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 6. 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 7. A 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. 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.

The formalisation and verification described here was a significant task: it was the major activity for an experienced Isabelle user (Dawson) for about seven months, not including some months more working on the proof which ultimately was found to be flawed (see §1). and not counting the proof of Thm 1, reused from [7]. The most difficult single part of it was the proof of Lemma 1, discussed in §6. The difficulty in defining a nested sequent datatype containing multisets of nested sequents (see §5) was also significant. The value of the formal verification is clear since it led us to find the flaw in the previous attempt at a proof.

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 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 [4, 15, 10, 11, 17, 14]. A difference between these logics and FILL is the use of “additive” context splitting in branching rules, where contexts are duplicated across premises. In the presence of contraction rules, our multiplicative context splitting can simulate such additive splitting, just as in the traditional sequent calculus. That is, one can apply contraction to duplicate every formula occurrence in the context before splitting them. Thus we think a similar formalisation effort for, say, nested sequent calculi for modal logics [11], would benefit significantly from our current formalisation.

References

1. N. D. Belnap. Display logic. J. Philos. Logic, 11:375–417, 1982.

2. G. M. Bierman. A note on full intuitionistic linear logic. Ann. Pure Appl. Logic, 79(3):281–287, 1996.

3. T. Bräuner and V. de Paiva. A formulation of linear logic based on dependencyrelations. In CSL, pages 129–148, 1997.

4. K. Brünnler. Deep sequent systems for modal logic. Arch. Math. Logic, 48(6):551– 577, 2009.

5. R. Clouston, J. E. Dawson, R. Goré, and A. Tiu. Annotation-free sequent calculi for full intuitionistic linear logic. In CSL, pages 197–214, 2013.

6. 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.

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

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

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

10. R. Goré, L. Postniece, and A. Tiu. Cut-elimination and proof search for biintuitionistic tense logic. In AiML, pages 156–177, 2010.

11. 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.

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

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

14. J. Park, J. Seo, and S. Park. A theorem prover for boolean BI. In POPL, pages 219–232, 2013.

15. F. Poggiolesi. The method of tree-hypersequents for modal propositional logic. In Trends in Logic IV, pages 31–51, 2009.

16. H. Schellinx. Some syntactical observations on linear logic. J. Logic Comput., 1(4):537–559, 1991.

17. L. Straßburger. Cut elimination in nested sequents for intuitionistic modal logics. In FoSSaCS, pages 209–224, 2013.

18. 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.

19. C. Urban. Nominal techniques in isabelle/HOL. J. Automat. Reason., 40(4):327– 356, 2008.