Isabelle work on Full Intuitionistic Linear Logic

Jeremy E. Dawson

January 2, 2014

1 Introduction and Acknowledgements

This document describes my work in Isabelle from July 2013 relating to the paper ”Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic”, subsequently published in CSL 2013 [1].

During the early part of 2013 I worked on proving, in Isabelle, the lemmas and theorems of the then version of that paper, but discovered a problem with the exclusion-deletion procedure described in it.

A revised version of the paper which did not use this procedure was prepared (with my name added as a co-author).

Since then I have been trying to verify the lemmas and theorems of the revised version of the paper.

2 The nested sequent datatype cannot involve multisets

A nested sequent could be defined (and is defined in Isabelle) using a tree structure with two binary operators, “⇒” and “,”, and this could be expressed as a datatype in Isabelle. However, in the paper a nested sequent is constructed using the operator “⇒”, with a multiset of nested sequents on either side of the “⇒”.

Thus the formulation in the paper does not require explicit rules for commutativity or associativity, or for M, Φ (where Φ is the empty multiset).

Now Isabelle permits nested datatypes. For example, a derivation tree is made up of an end-sequent and a list of derivation trees (whose end-sequents are the premises of the final rule of the whole tree). Thus the datatype is nested, ie the derivation tree contains a list of derivation trees. But this is possible only because “list” is also a datatype. We couldn’t do this if “list” were replaced by “multiset” in the description above.

CITE Traytel et al.

So we defined a relation, multiset-equivalence, ms deep equiv, under which any two Isabelle nested sequents are equivalent if they would be the same if each collection of sequents, separated by commas, were considered the same.

This includes where the difference between two Isabelle nested sequents occurs at any depth.

INCLUDE definitions for this.

While we used the relation ms deep equiv to describe the situation where two nested sequents are equivalent, we defined the shallow and deep nested sequent calculi BiILL_{sn} and BiILL_{dn} to contain rules expressing the monoid (commutativity, associativity and Φ) rules (sn ac0 and dn ac0), in addition to the rules shown in the paper.

2.1 Lemmas about ms deep equiv

There were a number of seemingly basic lemmas about the ms deep equiv relation which were not easy to prove. For example,

mins_msde_lem
msde_ex_plus
msde_mins_inv
msde_plus_inv
msde_commasD
ctxt_nseq_lem

3 The display calculus and the shallow nested sequent calculus

As discussed above, for nested sequents we used a datatype with connectives comma and ⇒, and a constant for the empty multiset (as in the display calculus).

For the display calculus we have rules named (for example) rp, drp, pA (permutation of the antecedent), aS (associativity of the succedent), anda and ands (∧-rule, antecedent and succedent), etc.

The entire set of rules is called rlscf (for BiILL_{dc}, including drp), or frlscf (for FILL_{dc}, excluding drp). See file F Rls.thy.

For the nested sequent calculus we have rules named (for example) sn rp, sn drp, sn pA (permutation of the antecedent), sn aS (associativity of the succedent), sn anda and sn ands. Because of the apparent difficulty of formalising nested sequents using multisets, we needed additional rules to handle commutativity and associativity, and the identity for the comma operator. These rules correspond to equivalent rules for the display calculus.

The entire set of rules is called sn rlscf. See file N Rls.thy.

We have proved equivalence between these two systems. 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 equivalence between a nested sequent and a display calculus sequent is expressed by

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

where the display calculus sequent must satisfy the condition seq LtGtOK which means that < and > symbols must be only found in antecedent and succedent positions respectively, and the nested sequent must be a single sequent (not a comma-separated list of sequents).

Since, in both systems, we have rules in which we explicitly substitute for structure and formula variables, we also need functions which convert between a substitution of display calculus structures and substitution of nested sequents.

3.1 Shallow Nested Sequent Calculus to Display Calculus

With a lot of lemmas deriving a display calculus rule from a set of nested sequent rules, like

sd_dands : "[| {invert sn_ira} <= ?rules';  ... |] ==>
   ([?A => $?Za, ?B => $?Z], ?A +++ ?B => $?Za,,, $?Z) : derl (nrulefs ?rules')"

where the premises list the rules of BiILL_{sn} which are actually used, which shows that an individual display calculus rule can be proved in the shallow nested system (see N Rls.ML), we are able to prove

tr_rules_dc_snb :
  "?r : rulefs rlscfb ==> pscmap seq_to_nested ?r : derl (nrulefs snb_rlscf)"
tr_derl_dc_snb : "(?ps, ?c) : derl (rulefs rlscfb) ==>
   pscmap seq_to_nested (?ps, ?c) : derl (nrulefs snb_rlscf)"

that is, each BiILL_{dc} rule is derivable in BiILL_{sn}, and then that each sequent derivable in BiILL_{dc} is derivable in BiILL_{sn}. See the file Dc Sn.ML.

3.2 Display Calculus to Shallow Nested Sequent Calculus

In this case we get a set of results like

ds_dands : "[| {invert drp} <= ?rules'; {invert rp} <= ?rules'; ... |] ==>
      ([$?Za |- ?A,, $?Ya, $?Z |- ?B,, $?Y],
       $?Za,, $?Z |- ?A && ?B,, ($?Ya,, $?Y)) : derl (rulefs ?rules')"

where the premises list the rules of BiILL_{dc} which are actually used, which shows that an individual shallow nested calculus rule can be proved in the display calclus (see F Rls.ML), we are able to prove

tr_rules_snb_dc :
   "?r : nrulefs snb_rlscf ==> pscmap nested_to_seq ?r : derl (rulefs rlscfb)"
tr_derl_snb_dc : "(?ps, ?c) : derl (nrulefs snb_rlscf) ==>
   pscmap nested_to_seq (?ps, ?c) : derl (rulefs rlscfb)"

that is, each BiILL_{sn} rule is derivable in BiILL_{dc}, and then that each sequent derivable in BiILL_{sn} is derivable in BiILL_{dc}. See the file Dc Sn.ML.

4 The Deep Nested Sequent Calculus

4.1 Applying a context to a rule

We needed to define several notions of “context”, denoted X[ ] in the paper.

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

Thus, where ([P], C) ∈ R, ([X[P]], X[C]) ∈ ctxt R. Likewise, if C ∈ R and X[ ] is a hollow context then X[C] ∈ hctxt R.

4.2 An alternative definition for ctxt

Some of the proofs involving ctxt were easier using a related definition where X[S ⇒ T] means adding nested sequents to S or to T, rather than to S ⇒ T. For example, if ([P′ ⇒ P′′], C′ ⇒ C′′) ∈ dctxtR, then ([P′, X ⇒ P′′], C′, X ⇒ C′′) ∈ dctxtR.

Some proofs were easier using this formulation. We needed lemmas like the following, and also dc anda (see §4.7.2).

nseqs_ctxt_dctxt : "([$?pa => $?ps], $?ca => $?cs) : ctxt ?R ==>
   ([$?pa => $?ps], $?ca => $?cs) : dctxt ?R"

4.3 Alternative formulations of ctxt or dctxt

Initially we used the following introduction clauses as the base cases for the inductive definitions of ctxt and dctxt.

same "r : rs ==> r : ctxt rs"
same "r : rs ==> r : dctxt rs"

We contemplated changing these to

same "([Xp], Xc) : rs ==> ([Xp], Xc) : ctxt rs"
same "([$Yp => $Zp], $Yc => $Zc) : rs ==>
      ([$Yp => $Zp], $Yc => $Zc) : dctxt rs"

because we find that only in the base cases can we get r ∈ ctxt rs or r ∈ dctxt rs for any r not in the form shown (ie, where r has a single premise and, for dctxt, r contains nested sequents). We experimented with making this change, which would give us that always if r ∈ ctxt rs or r ∈ dctxt rs then r has this form (without assuming that rules in rs have this form). But we would then lose certain useful properties, such as

in_ctxt_derl : "(?ps, ?c) : derl ?pscrel ==>
  (?ps, ?c) : derl (ctxt ?pscrel)"

And, more importantly, nseqs ctxt dctxt (see above) would no longer hold.

4.4 Merging nested sequents

We also defined merged sequents, using triples, so in effect (X_{1}, X_{2}, X) ∈ rmerge, where 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}, X_{2}.

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

rmerge :: "(nested * nested * nested) set"
rmerge1 :: "(nested * nested * nested) => (nested * nested * nested) set"

We then prove the general result that if (X, Y, Z) : rmerge then Z => U can be derived from X, Y => U in the shallow calculus, and likewise U => Z from U => X, Y.

rmerge_derL : "(?X, ?Y, ?Z) : rmerge ==>
  ([$?X,,, $?Y => $?U], $?Z => $?U) : derl (nrulefs sn_rlscf)"

4.5 An alternative definition for rmerge1

As in the case of defining dctxt as an alternative to ctxt, we defined dmerge1 as an alternative to rmerge1. For example

\frac{((X_{1} ⇒ Y_{1}), (X_{2} ⇒ Y_{2}), (X ⇒ Y)) ∈ dmerge1(S_{1}, S_{2}, S)}{((X_{1} ⇒ Z_{1}, Y_{1}), (X_{2} ⇒ Z_{2}, Y_{2}), (X ⇒ Z, Y)) ∈ dmerge1(S_{1}, S_{2}, S)}

We then proved the lemmas linking dmerge1 with rmerge1

rmerge1_dmerge1 : "($?aa => $?as, $?ba => $?bs, $?ca => $?cs) :
    rmerge1 ($?Aa => $?As, $?Ba => $?Bs, $?Ca => $?Cs) ==>
  ($?aa => $?as, $?ba => $?bs, $?ca => $?cs) :
     dmerge1 ($?Aa => $?As, $?Ba => $?Bs, $?Ca => $?Cs)"

drmerge1_ands :
         "[| (?qa', ?qb', ?d) : dmerge1 ?t'; ?t' : dn_ands |]
            ==> EX qa qb da ds t.
               (qa, ?qa') : ms_deep_equiv &
               (qb, ?qb') : ms_deep_equiv &
               (qa, qb, $da => $ds) : rmerge1 t &
               t : dn_ands & (?d, $da => $ds) : ms_deep_equiv"

4.6 From Deep to Shallow Nested Sequent Calculi

We prove in turn that the deep propagation rules (dn bprs), single-premise logical rules (dn splrs) and monoid (commutativity, associativity and Φ) rules (dn ac0) are derivable in the shallow system. These proofs are simpler but have some features similar to the proofs using rule base0 and rule base2 described below.

ctxt_bprs_sn :
    "[| ([?p], $?ca => $?cs) = ?psc; ?psc : ctxt (nrulefs dn_bprs) |]
          ==> ?psc : derl (nrulefs sn_rlscf)"
ctxt_splrs_sn :
   "[| ([?p], $?ca => $?cs) = ?psc; ?psc : ctxt (nrulefs dn_splrs) |]
         ==> ?psc : derl (nrulefs sn_rlscf)"
ctxt_dn_ac0 :
    "[| ([$?pa => $?ps], $?ca => $?cs) = ?psc; ?psc : ctxt (nrulefs dn_ac0) |]
          ==> ?psc : derl (nrulefs sn_rlscf)"

For the axioms, we proved that the axioms themselves (without the context X[ ]) are derivable (dn axioms der), and using lemmas (dn axioms rb0 and hctxt rb0) we proved that the axioms with the hollow contexts X[ ] are derivable. A sequent S satisfies rule base0 rules if, for hollow X, X ⇒ S and S ⇒ X are derivable. Thus dn axioms rb0 says that the axioms (without context) can be extended by hollow X in this way once, and hctxt rb0 extends this inductively to apply to any hollow extension of an axiom.

dn_axioms_der : "?S : dn_axioms ==> ([], ?S) : derl (nrulefs sn_rlscf)"
dn_axioms_rb0 : "?S : dn_axioms ==> rule_base0 sn_rlscf ?S"
hctxt_rb0 : "[| rule_base0 ?rules ?S; sn_idps <= ?rules;
  {sn_pA, sn_pS} <= ?rules; ?H : hctxt {?S} |] ==> rule_base0 ?rules ?H"
rule_base0_def : "rule_base0 ?rules ?S ==
         (ALL X:hollows. ([], $X => $?S) : derl (nrulefs ?rules)) &
 (ALL X:hollows. ([], $?S => $X) : derl (nrulefs ?rules))"

For the two-premise logical rules, we prove theorems like

dn_ands_sn : "[| (?Sa, ?Sb, ?Sc) : rmerge; (?Ta, ?Tb, ?Tc) : rmerge |] ==>
  ([$?Sa => ?A,,, $?Ta, $?Sb => ?B,,, $?Tb],
        $?Sc => ?A && ?B,,, $?Tc) : derl (nrulefs sn_rlscf)"

rb2_ands : "[| (?Sa, ?Sb, ?Sc) : rmerge; (?Ta, ?Tb, ?Tc) : rmerge |] ==>
  rule_base2 sn_rlscf
    ($?Sa => ?A,,, $?Ta, $?Sb => ?B,,, $?Tb, $?Sc => ?A && ?B,,, $?Tc)"
deep2_ctxt : "[| sn_idps <= ?rules; {sn_pA, sn_pS} <= ?rules;
    rule_base2 ?rules (?Ya, ?Yb, ?Yc);
    (?Wa, ?Wb, ?Wc) : rmerge1 (?Ya, ?Yb, ?Yc) |] ==>
  rule_base2 ?rules (?Wa, ?Wb, ?Wc)"

Then by the lemmas rb2 ands, etc, and deep2 ctxt, we are able to show from dn ands sn (etc) that the deep two-premise logical rules are derivable in the shallow calculus. Similar to rule base0, rule base2 expresses that a triple of sequents (P_{1}, P_{2}, C) satisfies that X ⇒ C is derivable from X_{1} ⇒ P_{1} and X_{2} ⇒ P_{2}, for all (X_{1}, X_{2}, X) ∈ rmerge, and similarly for C ⇒ X, P_{1} ⇒ X_{1} and P_{2} ⇒ X_{2}. So, similarly to the use of rule base0 for the axioms, these results are used to show that the two-premise logical rules in their contexts are derivable.

These results are combined to show that nested sequents derivable in the deep calculus are derivable in the shallow calculus.

dn_sn_der : "?r : biilldn ==> ?r : derl (nrulefs sn_rlscf)"

4.7 From Shallow to Deep Nested Sequent Calculi

We first note that since our formulation of BiILL_{dn} involves the comma as a structural connective, and explicit inclusion of the monoid rules dn ac0 (see §2), it is necessary to prove that our system makes multiset-equivalent nested sequents interderivable using the monoid rules, and conversely.

msde_derl : "(?a, ?b) : ms_deep_equiv ==>
  ([?a], ?b) : derl (ctxt (nrulefs dn_ac0))"
dn_ac0_msde : "([?M], ?N) : ctxt (nrulefs dn_ac0) ==> (?M, ?N) : ms_deep_equiv"

The key lemma here is that the rules (the display rules, rp_{i} and drp_{i}, and the Grishin rules gl and gr) which are in the shallow calculus BiILL_{sn} but not in the deep calculus BiILL_{dn} are admissible in BiILL_{dn}.

For this we first prove a permutation lemma (Lemma 18), that (in general) where one of the shallow rules in question follows a rule of BiILL_{dn} in a derivation, then the derivation can be re-ordered so that the shallow rule precedes the deep rule. In some cases we need to use a different or additional deep rule, and where the deep rule is an axiom then the result is that we can dispense with the shallow rule.

4.7.1 Where the deep rule is an axiom

We define the set of hollow structures (see hollows.intrs), and the idea of a hollow context X[ ] (see hctxt.intrs).

Theorems dn gen id, dn gen tS and dn gen fA express that any nested sequent which is multiset-equivalent to the axioms as written in the paper is derivable using our rules.

Then theorems id then, tS then and fA then express that each of these axioms followed by an instance of the rules rp_{1}, drp_{1}, rp_{2}, drp_{2}, gl and gr, and also ig and eg (see the proof of Lemma 18, in page 19 in the Appendix), is derivable in BiILL_{dn}.

dn_gen_id : "[| set_of ?U <= hollows; set_of ?V <= hollows;
    ms_of_ns ?X = mins (NStructform ?A) ?U;
    ms_of_ns ?Y = mins (NStructform ?A) ?V;
    ($?Z => $?W) : hctxt {$?X => $?Y} |] ==>
  ([], $?Z => $?W) : derl biilldn"
id_then : premises as for dn_gen_id, plus
     ([$?Z => $?W], ?S) : nrulefs {sn_rp, sn_drp, invert sn_rp,
       invert sn_drp, sn_gl, sn_gr, sn_ig, sn_eg} |] ==>
    ([], ?S) : derl biilldn"

See the file Rotate.ML.

4.7.2 Where the deep rule is 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 rule among rp_{1}, drp_{1}, rp_{2}, drp_{2}, gl, gr, eg and eg appears below a logical rule in a derivation, the derivation steps may be permuted so that the logical rule follows the other rule.

Before realising we needed to use rp_{1}, drp_{1}, eg and eg instead of rp_{1}, drp_{1}, rp_{2}, drp_{2}, gl and gr we proved the twelve theorems for the six logical rules and for rp_{2} and drp_{2} using the tactics mpttacs.

We proved the twelve theorems for rp_{1} and drp_{1} using the tactics mpttacs i. Having proved the twelve theorems for gl and gr using the tactics mpttacs g we found that the same tactics worked to prove the twelve theorems for eg and ig.

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.

To use dctxt in this way we needed the results dc anda and dcok anda (etc).

dc_anda : "([?p], ?c) : dctxt (nrulefs {sn_anda}) ==>
  EX p' c'. (?p, p') : ms_deep_equiv & (c', ?c) : ms_deep_equiv &
    ([p'], c') : ctxt (nrulefs {sn_anda})"
dcok_anda : "EX p' q q' d. (?p1, p') : ms_deep_equiv &
   ([p'], q) : nrulefs {?sn_rule1} & (q, q') : ms_deep_equiv &
   ([q'], d) : dctxt (nrulefs {sn_anda}) & (d, ?d'1) : ms_deep_equiv ==>
 EX p' q q' d. (?p1, p') : ms_deep_equiv &
   ([p'], q) : nrulefs {?sn_rule1} & (q, q') : ms_deep_equiv &
      ([q'], d) : ctxt (nrulefs {sn_anda}) & (d, ?d'1) : ms_deep_equiv"

These results, and similar ones for the other rules of BiILL_{dn}, and the results of §4.7.1, will give that the rules rp_{1}, drp_{1}, rp_{2}, drp_{2}, gl and gr are admissible in BiILL_{dn}. See §??.

   See the file CRotate.ML.

4.7.3 Where the deep rule is a two-premise logical rule

These are similar to the one-premise rules, except that the statement of the theorem is more complicated, as are accordingly the proof tactics.

The following lemmas needed to be used for some of these results. Of these, rmerge msde in particular was extraordinarily difficult to prove.

rmerge_msde : "[| (?c, ?c') : ms_deep_equiv; (?a, ?b, ?c) : rmerge |] ==>
   EX a' b'.  (?a, a') : ms_deep_equiv &
     (?b, b') : ms_deep_equiv & (a', b', ?c') : rmerge"
rmerge1_msde_comma :
 "[| (?a, ?b, ?c) : rmerge1 (?A, ?B, ?C); ms_of_ns ?C = {#?C#};
       (?c, $?dY,,, $?dZ) : ms_deep_equiv |] ==>
     EX aY aZ bY bZ cY cZ.
       (?a, $aY,,, $aZ) : ms_deep_equiv & (?b, $bY,,, $bZ) : ms_deep_equiv &
       (cY, ?dY) : ms_deep_equiv & (cZ, ?dZ) : ms_deep_equiv &
       ((aY, bY, cY) : rmerge1 (?A, ?B, ?C) & (aZ, bZ, cZ) : rmerge |
(aZ, bZ, cZ) : rmerge1 (?A, ?B, ?C) & (aY, bY, cY) : rmerge)"
msde_commasD : "($?Aa,,, $?Ab, $?Ba,,, $?Bb) : ms_deep_equiv ==>
   EX Caa Cab Cba Cbb.  (?Aa, $Caa,,, $Cab) : ms_deep_equiv &
     (?Ab, $Cba,,, $Cbb) : ms_deep_equiv &
     ($Caa,,, $Cba, ?Ba) : ms_deep_equiv &
     ($Cab,,, $Cbb, ?Bb) : ms_deep_equiv"
   See the file P2Rotate.ML.

4.7.4 Where the deep rule is a propagation rule

The statement of the theorems, and some of the proofs, are similar to those described in §4.7.2.

The eight theorems for the cases rp_{1}, drp_{1} with pl_{1}, pr_{1}, pl_{2}, pr_{2} were proved using the same set of tactics mpttacs ine, but the theorems for pl_{1} required replacing pl_{1} with either dn pl1t (which uses pl_{1} twice) or dn plc (which uses pl_{1} then pl_{2}), as shown in the first two cases of the proof of Lemma 36. Similarly for the theorems for pr_{1}.

Unfortunately we had to subsequently generalise these new rules dn pl1t and dn plc to dn pl1tg and dn plcg to enable proving the required theorems analogous to dc anda, see §4.7.2.

For the eight theorems for the cases ig, eg with pl_{1}, pr_{1}, pl_{2}, pr_{2} four were proved using the same set of tactics mpttacs ieg, but the other four needed to be proved individually. These were p ig pr1, p eg pl1, p ig pr2, p eg pl2.

Of these eight theorems, p ig pl1, p ig pr2, p eg pl2, p eg pr1 include cases where the propagation rule simply disappears rather than just being permuted to below the ig or eg rule, as shown in the third and fourth cases of the proof of Lemma 36. To express these it was simplest to define a rule sn rpt nes which just repeats a nested sequent unchanged.

   See the file Prop Rotate.ML.

4.7.5 Complication: using eg and ig versus gl and gr

The paper introduces rules eg and ig, which, given the rules rp_{1}, drp_{1}, rp_{2} and drp_{2}, are equivalent to gl and gr. Further, rp_{2} and drp_{2} are special cases of ig and eg. Therefore, given the admissibility of rp_{1}, drp_{1}, rp_{2} and drp_{2}, the admissibility of eg and ig is equivalent to the the admissibility of gl and gr.

However in proving some of the permutation lemmas described above, when permuting rp_{2} or drp_{2} above rules of BiILL_{dn}, we had to change the instance of rp_{2} and drp_{2} to an instance of ig and eg. We first planned to just consider ig as gr followed by rp_{2}, but realised this may cause a problem in proving termination of this permutation procedure. This affects rules p2 rp lollia

and p2 drp excls, and also p rp pr2 and p drp pl2.

This is because other instances of the permutation rule replace one of the rules of BiILL_{dn} by two rules of BiILL_{dn}, namely p2 irp lollia and p2 idrp excls.

Then the proof of termination is not obvious. For example, let B_{1} and B_{2} be rules of BiILL_{dn}, and let A_{1} and A_{2} be rules we are hoping to prove admissible. Suppose we have permutation lemmas which replace

• the subderivation B_{1}A_{2} (ie rule B_{1}, then rule A_{2}) by A_{1}A_{2} (whether or not followed by another B-rule), and

• B_{2}A_{1} by A_{1}B_{2}B_{1}

Then we get

B_{2}B_{1}A_{2} ⇒ B_{2}A_{1}A_{2} ⇒ A_{1}B_{2}B_{1}A_{2}

which loops indefinitely. That is, when permutation lemmas produce a result using two logical rules, and when other permutation lemmas produce a result using two of the hopefully admissible rules, we may get a problem.

So we now look at proving the permutation lemmas for rp_{1}, drp_{1}, eg and ig instead of rp_{1}, drp_{1}, rp_{2}, drp_{2}, gl and gr (as in Lemma 36 in the paper). But it seems we should also do this for Lemmas 34 and 35 of the paper (see §4.7.1).

So we defined the rule set snb ieg rlscf which has eg and ig in place of rp_{2}, drp_{2}, gl and gr in snb rlscf, and proved their equivalence in the theorem

snb rlscf eq ieg.
snb_rlscf_eq_ieg : "derl (nrulefs snb_rlscf) = derl (nrulefs snb_ieg_rlscf)"

4.7.6 Complication: admissibility of hollow context weakening

In § 4.7.1, 4.7.2, 4.7.3, 4.7.4 and 4.7.5 we proved the lemmas needed to show the BiILL_{dn}-admissibility of the rules rp_{1}, drp_{1}, eg and ig. It seemed at first that the remaining rules of BiILL_{dn} would be derivable in BiILL_{sn}.

However we found that the two-premise logical rules in the shallow calculus BiILL_{sn} differ from those in the deep calculus BiILL_{dn} (even when we ignore the contexts X[ ] and X_{i}[ ]). The difference is that where the shallow and deep rules are respectively

\frac{U ⇒ A, V U′ ⇒ B, V′}{U, U′ ⇒ A ⊗ B, V, V′}  \frac{S_{1} ⇒ A, T_{1} S_{2} ⇒ B, T_{2}}{S ⇒ A ⊗ B, T}

where S = S_{1} • S_{2} and T = T_{1} • T_{2}.

So to use the deep rule to derive the shallow rule we need to identify S with U, U′ and then find some S_{1} and S_{2} such that S = S_{1} • S_{2} and U and U′ can be weakened to S_{1} and S_{2} respectively (similarly for T , T_{i}, V, V′).

This requires showing that ”hollow-weakening” is admissible. We suspect that a more general result is true, where we replace (U, X ⇒ Y, V) below by any hollow context of (X ⇒ Y), but we didn’t need that. As with any admissibility result, the proof of this involved extending all the rules of BiILL_{dn} by hollow structures U and V. By lemma hollows rmerge, we extend both the premises as well as the conclusion of a two-premise logical rule by U and V.

hollow_weak' : "[| ($?X => $?Y) : derrec biilldn {};
      ?U : hollows; ?V : hollows |] ==>
    ($?U,,, $?X => $?Y,,, $?V) : derrec biilldn {}"
hollows_rmerge : "?H : hollows ==> (?H, ?H, ?H) : rmerge"

Hence we get that the two-premise rules of BiILL_{sn} are admissible (not derivable) in BiILL_{dn}. All the other rules are easier, and so we get that all the rules of

sn_ands_dn : "nrulefs {sn_ands} <= adm biilldn"

4.7.7 Wrapping it up

From § 4.7.1, 4.7.2, 4.7.3, 4.7.4 and 4.7.5 we have the BiILL_{dn}-admissibility of rp_{1}, drp_{1}, eg and ig, and from §4.7.6 we have BiILL_{dn}-admissibility of the twopremise logical rules. The other rules of BiILL_{sn} are BiILL_{dn}-derivable, so we get sn dn der. Combining this with dn sn der (see §4.6) we get sn dn equiv, which expresses Theorems 17 and 19. These proofs made good use of the lemmas relating derrec, derl, adm described in our LPAR 2010 (or Raj’s talk in India) paper [?]

sn_dn_der : "derl (nrulefs snb_rlscf) <= adm biilldn"
sn_dn_equiv : "(?r : derrec (nrulefs snb_rlscf) {}) =
  (?r : derrec biilldn {})"

To get Corollary 20, which looks like a straightforward consequence of Theorem 19, we in fact have to define a formula A being provable. Conventionally, in BiILL_{dc} we take this to mean that I ⊢ A is derivable, but in BiILL it seems more natural to use · ⇒ A, or, in our implementation, NI ⇒ A.

With these interpretations we need to prove the invertibility of either the (I ⊢) rule in BiILL_{dc} or the I_{l} rule of BiILL_{dn}. We did the former, using a lemma pscrel adm designed to facilitate proofs of the invertibility of logical rules.

pscrel_adm : "[| ALL ps c x.  (ps, c) : ?rls --> (c, x) : ?rel -->
(EX ps'. (ps', x) : derl ?rls & (ps, ps') : allrel ?rel);
      (?s, ?s') : ?rel |] ==> ([?s], ?s') : adm ?rls"
dc_dn_equiv : "((T |- ?A) : derrec (rulefs rlscfb) {}) =
         (($NI => ?A) : derrec biilldn {})"

References

[1] Ranald Clouston, Jeremy Dawson, Rajeev Goré & Alwen Tiu. Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic. In Proc. CSL, 2013. DETAILS