Isabelle proofs of Cut-Admissibility for GTD and S4C

Jeremy E. Dawson

November 17, 2014

1 Introduction and Acknowledgements

This document describes my work in Isabelle in 2014 relating to the cut admissibility proofs for two logics described in a set of slides entitled ”Two Examples of Cut-Elimination for Non-classical Logics”, by Grigori Mints, presented at the Jägerfest in December 2013.

2 The system GTD

This section and the next describe Isabelle proofs of the cut admissibility of the logic GTD described in [?]

Semantically this system is K with the additional axiom □A ⇔ □□A. The sequent inference rules involving □ are

\frac{Γ, □Γ ⊢ A}{□Γ ⊢ □A}(⊢ □) \frac{Γ, □Γ ⊢ □A}{□Γ ⊢ □A}(□ ⊢)

We first formalised GT D as glssc GTD using a framework which had previously been applied to other logics. GTD means the rules involving □, and glssc refers to a set of classical logic rules, including explicit weakening and contraction rules.

Our formalisation involves sequents consisting of multisets of formulae on either side of a turnstile.

datatype 'a sequent = Sequent "'a multiset" "'a multiset"

Here are the definitions of glssc and GTD

inductive "GTD"
  intros
    I : "A = B | A = Box B ==>
      ([mset_map Box X + X |- {#A#}], mset_map Box X |- {#Box B#}) : GTD"
inductive "glssc glrs"

  intros
    axiom : "([], {#D#} |- {#D#}) : glssc glrs"
    extI : "psc : glne ==> pscmap (extend flr) psc : glssc glrs"
    glrI : "psc : glrs ==> psc : glssc glrs"

The second clause for glssc takes the rules in glne and adds a context (the same context) to the conclusion and all premises. This means that the logical rules with two premises are of the context-sharing form. The following definitions explain this further.

types
  'a psc = "'a list * 'a" (* single step inference *)
consts
  pscmap :: "('a => 'b) => 'a psc => 'b psc"
  (* extend a sequent by adding context to conclusion and premises *)
  extend :: "'a sequent => 'a sequent => 'a sequent"
primrec
   pscmap_def "pscmap f (ps, c) = (map f ps, f c)"
defs
  extend_def : "extend fmls seq == seq + fmls"

We reused some code from previous work in which the logical rules (⊢ ∨), (∧ ⊢) and (⊢ ∨) were of the forms shown (without the context)

\frac{A ⊢}{A ∧ B ⊢}  \frac{B ⊢}{A ∧ B ⊢}  \frac{⊢ A}{⊢ A ∨ B}  \frac{⊢ B}{⊢ A ∨ B}  \frac{A ⊢ B}{⊢ A → B}

The rules used for classical logic (before extending them with a context) form the set glne: the rule sets wkrls, ctrrls A, glil and glir are the weakening rules, contraction (on A) rules, and the left and right logical introduction rules.

inductive "glne" (* rules before being extended *)
  intros
    wkI : "(ps, c) : wkrls ==> (ps, c) : glne"
    ctrI : "(ps, c) : ctrrls A ==> (ps, c) : glne"
    ilI : "(ps, c) : glil ==> (ps, c) : glne"
    irI : "(ps, c) : glir ==> (ps, c) : glne"

To prove cut admissibility we actually used induction on a derivation to prove admissibility of the mix (multicut rule).

2.1 Framework of our induction proofs

FOLLOWING TEXT FROM OUR LPAR PAPER Many cut-elimination proofs proceed via two main phases. The first phase transforms the given derivations using several “parametric” steps so that the cut-formula is the principal formula of the final rule in the resulting sub-derivations. The “principal cut” is then “reduced” into cuts which are “smaller” in some well-founded ordering such as size of cut-formula. We describe how we captured this two-phase structure of cut-elimination proofs, and present a widely applicable result that a parametric step is possible under certain conditions.

We use the following framework for deriving cut-admissibility, or indeed any property P of pairs of subtrees. In the diagram below, to prove P (C_{l}, C_{r}), the induction hypothesis is that P (P_{li}, C_{r}) and P (C_{l}, P_{rj}) hold for all i and j:

P_{l1} … P_{ln} ; ρ_{l} ; C_{l}  P_{r1} … P_{rm} ; ρ_{r} ; C_{r} ........................ (cut ?)

?

A proof of P (C_{l}, C_{r}) using this induction hypothesis inevitably proceeds by cases on the actual rules ρ_{l} and ρ_{r}, and for a cut-formula A, on whether it is principal in either or both of ρ_{l} and ρ_{r}. But we also use induction on the size of the cut-formula, or, more generally, on some well-founded relation on formulae.

So we actually consider a property P of a (cut) formula A and (left and right subtree conclusion) sequents (C_{l}, C_{r}). In proving P A (C_{l}, C_{r}), in addition to the inductive hypothesis above, we assume that P A′ (D_{l}, D_{r}) holds generally for A′ smaller than A and all “rls-derivable” sequents D_{l} and D_{r}: i.e. derivable from the empty set of premises using rules from rls. These intuitions give the following definition gen step2sr of a condition which permits one step of the inductive proof. Setting out proofs by using a number of lemmas, each stating gen step2sr … for specific cases of the final rules on each side above the cut enables us to avoid having one huge monolithic proof in the Isabelle code.

Definition 2.1 (gen step2sr) For a formula A, a property P, a subformula relation sub, a set of rules rls, inference rule instances R_{l} = (P_{l1} … P_{ln}, C_{l}) and R_{r} = (P_{r1} … P_{rm}, C_{r}), gen step2sr P A sub rls (R_{l}, R_{r}) means:

if forall A′ such that (A′, A) ∈ sub and all rls-derivable sequents D_{l} and D_{r}, P A′ (D_{l}, D_{r}) holds

and for each P_{li} in P_{l1} … P_{ln}, P_{li} is rls-derivable and P A (P_{li}, C_{r}) holds

and for each P_{rj} in P_{r1} … P_{rm}, P_{rj} is rls-derivable and P A (C_{l}, P_{rj}) holds

and C_{l} and C_{r} are rls-derivable.

then P A (C_{l}, C_{r}) holds.

gen_step2sr_simp: "gen_step2sr ?P ?A ?sub ?rls ((?aa, ?ba), ?ab, ?bb) =
    ((ALL A'.  (A', ?A) : ?sub -->
       (ALL dl:derrec ?rls {}.  ALL dr:derrec ?rls {}. ?P A' (dl, dr))) -->
     (ALL pl:set ?aa. pl : derrec ?rls {} & ?P ?A (pl, ?bb)) -->
     (ALL pr:set ?ab. pr : derrec ?rls {} & ?P ?A (?ba, pr)) -->
     ?ba : derrec ?rls {} --> ?bb : derrec ?rls {} --> ?P ?A (?ba, ?bb))"

So the property P we want to prove using this induction framework is that the final sequents C_{l} and C_{r} can be combined using the mix rule.

The main theorem gen step2sr lem below for proving an arbitrary property P states that if the step of the inductive proof is possible for all cases of final rule instances R_{l} and R_{r} on each side, then P holds in all cases.

Theorem 2.1 (gen step2sr lem) If

• A is in the well-founded part of the subformula relation sub,

• sequents S_{l} and S_{r} are rls-derivable, and

• for all formulae A′, and all rules R_{l} and R_{r}, our induction step condition

     gen step2sr P A′ sub rls (R_{l}, R_{r}) holds

then P A (S_{l}, S_{r}) holds.

This enables us to split up an inductive proof, by showing, separately, that gen step2sr holds for particular cases of the final rules (P_{l}, C_{l}) and (P_{r}, C_{r}) on each side. For example, the inductive step for the case where the cut-formula A is parametric, not principal, on the left is encapsulated in the following theorem where prop2 mar erls A (C_{l}, C_{r}) means that the conclusion of a multicut on A whose premises are C_{l} and C_{r} is derivable using rules erls.

Theorem 2.2 (lmg gen step) For any relation sub and any rule set rls, given an instance of multicut with left and right subtrees ending with rules R_{l} and R_{r}:

if weakening is admissible for the rule set erls,

and all extensions of some rule (P, X ⊢ Y) are in the rule set erls,

and R_{l} is an extension of (P, X ⊢ Y),

and the cut-formula A is not in Y (meaning that A is parametric on the left)

then gen step2sr (prop2 mar erls) A sub rls (R_{l}, R_{r}) holds.

Theorem 2.2 codifies multi-cut elimination for parametric cut-formulae, and applies generally to many different calculi since it holds independently of the values of sub and rls. Of course, for a system with explicit weakening rules, such as GT D, weakening is a fortiori admissible.

The above theorem uses the property prop2 mar erls (for rule set erls. We show the definitions of prop2 and mar below.

inductive "mar rls A"
    I : "(Xl + ms_delete {A} Xr |- ms_delete {A} Yl + Yr) : derrec rls {}
      ==> (Xl |- Yl, Xr |- Yr) : mar rls A"
inductive "mas rls A"

    I : "seql : derrec rls {} & seqr : derrec rls {} -->
        (seql, seqr) : mar rls A ==> (seql, seqr) : mas rls A"
prop2_def : "prop2 f rls A seqs == seqs : f rls A"

It may be noticed that mar and mas are similar except that mas contains explicitly the condition that the premises of the putative cut are derivable. In the context of induction on derivations, this is true anyway, so we have the following theorem

gs2_mas_mar: "gen_step2sr (prop2 mas ?rls) ?A ?sub ?rls =
            gen_step2sr (prop2 mar ?rls) ?A ?sub ?rls"

(Later we will refer to car and cas which are corresponding concepts for single, rather than multiple, cuts).

Then we get the following theorems:

glssc_gs2sr_GTD_r :
   "[| (?psa, ?ca) : extrs glne; (?psb, ?cb) : GTD |] ==>
  gen_step2sr (prop2 mar (glssc GTD)) ?A ?sub (glssc GTD)
       ((?psa, ?ca), ?psb, ?cb)"
glssc_gs2sr_GTD_l :
   "[| (?psa, ?ca) : GTD; (?psb, ?cb) : extrs glne |] ==>
   gen_step2sr (prop2 mar (glssc GTD)) ?A ?sub (glssc GTD)
     ((?psa, ?ca), ?psb, ?cb)"

That is, with a GTD rule on one side and one of the usual logical rule on the other, the inductive step is available. These results are easy because if the cutformula is not the principal formula of the logical rule then Theorem 2.2 (and the corresponding result on the right) apply. If the cut-formula (which must be boxed) is the principal formula of the logical rule then the logical rule must be weakening or contraction, in which case applying multicut to its premise gives the required result.

With logical rules on both sides, the following theorem applies: note that it applies to any logic glssc ?R (where ?R can stand for any set of rules).

glssc_gs2sr_ng:
  "[| c8ger_prop ?psubfml (glssc ?R) ?A (glne - wkrls - UNION UNIV ctrrls);
         (?psa, ?ca) : extrs glne; (?psb, ?cb) : extrs glne |] ==>
   gen_step2sr (prop2 mar (glssc ?R)) ?A ?psubfml (glssc ?R)
     ((?psa, ?ca), ?psb, ?cb)"

The property c8ger prop says essentially that if single cuts on subformulae of A are admissible then a single cut on A is admissible where the last rules on either side are logical introduction rules introducing the cut-formula A.

"c8ger_prop ?isubfml ?drls ?A ?c8rls ==
      ALL ps qs pse qse X Y.
         (ps, 0 |- {#?A#}) : ?c8rls -->
         (qs, {#?A#} |- 0) : ?c8rls -->
         pse = map (extend (X |- Y)) ps -->
         qse = map (extend (X |- Y)) qs -->
         set pse Un set qse <= derrec ?drls {} -->
         (ALL sfa.
             (sfa, ?A) : ?isubfml --> (ALL seqs. seqs : cas ?drls sfa)) -->
         (X |- Y) : derrec ?drls {}"

In the cases of the logical introduction rules proving multicut admissibility is more difficult than proving single cut admissibility. Where introduction of (just one instance of) the cut-formula A is the last step on each side before the cut, it is nesessary to perform multicut elimination on A between P_{l1} … P_{ln} and C_{r}, and between C_{l} and P_{r1} … P_{rm}; then one performs single-cut elimination on the sub-formulae of A. These steps are part of the proof of c8 gs2 mas. An example follows. Note that here (unlike some of the other diagrams) the contexts U and Y may contain copies of the cut-formula. Let Y′ be Y with copies of A ∧ B deleted, and U′ be U with copies of A ∧ B deleted.

\begin{aligned}X ⊢ A, Y & X ⊢ B, Y \\ & (⊢ ∧) \\ X ⊢ A ∧ B, Y \end{aligned} \begin{aligned}U, A, B ⊢ V \\ & (∧ ⊢) \\ U, A ∧ B ⊢ V \end{aligned} ................................................. (mix ?)
X, U′ ⊢ Y′, V

This is replaced by

X ⊢ A, Y  U, A ∧ B ⊢ V
................................ (inductive mix)

X, U′ ⊢ A, Y′, V . . . . . . . . . . . . . . . . . . .

(A)

X ⊢ B, Y  U, A ∧ B ⊢ V
................................ (inductive mix)

X, U′ ⊢ B, Y′, V . . . . . . . . . . . . . . . . . . .

(B)

X ⊢ A ∧ B, Y  U, A, B ⊢ V
................................... (inductive mix)

X, U′, A, B ⊢ Y′, V . . . . . . . . . . . . . . . . . . . . . .

(C)

Then (A), (B) and (C) are combined using inductive cuts on the smaller cut-formulae A and B, and the necessary contractions, to derive the required sequent X, U′ ⊢ Y′, V.

c8_gs2_mas:
   "[| wk_adm ?drls; ?prl = (?ps, 0 |- {#?A#}); ?qrl = (?qs, {#?A#} |- 0);
         ?prl : ?c8rls; ?qrl : ?c8rls;
         ?eprl = pscmap (extend (?Xl |- ?Yl)) ?prl;
         ?eqrl = pscmap (extend (?Xr |- ?Yr)) ?qrl;
         c8ger_prop ?sub ?drls ?A ?c8rls |] ==>
       gen_step2sr (prop2 mas ?drls) ?A ?sub ?drls (?eprl, ?eqrl)"

We proved that c8ger prop holds in the following theorem.

rls_c8: "c8ger_prop ipsubfml (glssc ?rls) ?A
   (glne - wkrls - UNION UNIV ctrrls)"

It remains to look at the case where the final rule on both sides of the desired cut are instances of the GT D rules. Here there are two quite distinct cases, depending on which GT D rule is used as the final step for the left premise of the cut.

For the first case, the rule on the left is the (□ ⊢) rule as shown, and for the rule on the right, only its conclusion matters, and is as shown.

Γ, □Γ ⊢ □A ; (□ ⊢) ; □Γ ⊢ □A \begin{matrix}⋯ \\ □A^{n}, □Δ ⊢ □B \end{matrix} .......................................... (mix ?)
□Γ, □Δ ⊢ □B

we use the inductive hypothesis permitting multicutting □A between Γ, □Γ ⊢ □A with □A^{n}, □Δ ⊢ □B then we use weakening and the (□ ⊢) rule, to get

Γ, □Γ ⊢ □A  \begin{matrix}⋯ \\ □A^{n}, □Δ ⊢ □B \end{matrix}
..................................... (inductive mix)

Γ, □Γ, □Δ ⊢ □B (weak) Γ, Δ, □Γ, □Δ ⊢ □B (□ ⊢) □Γ, □Δ ⊢ □B

The second case, with the (⊢ □) rule on the left as shown, is more complicated. Note that, for the rule on the right, B′ can be either □B or B.

Γ, □Γ ⊢ A ; (□ ⊢) ; □Γ ⊢ □A {A^{n}, □A^{n}, Δ, □Δ ⊢ B′ \atop □A^{n}, □Δ ⊢ □B}
............................................. (mix ?)
□Γ, □Δ ⊢ □B

In this case, from the premise on the right, we perform inductive mix on □A with the conclusion on the left, then mix on A with the premise on the left, contraction(s) on □Γ, and finally an instance of the (⊢ □) or (□ ⊢) rule (whichever was on the right before). The result is shown below.

Γ, □Γ ⊢ A

□Γ ⊢ □A  A^{n}, □A^{n}, Δ, □Δ ⊢ B′
......................................... (inductive mix)

A^{n}, □Γ, Δ, □Δ ⊢ B′

................................................ (inductive mix)

Γ, □Γ, □Γ, Δ, □Δ ⊢ B′ (ctr^{∗} ⊢) Γ, □Γ, Δ, □Δ ⊢ B′

□Γ, □Δ ⊢ □B

glssc_gs2sr_GTD_GTD:
   "[| (?psa, ?ca) : GTD; (?psb, ?cb) : GTD |] ==>
   gen_step2sr (prop2 mar (glssc GTD)) ?A ipsubfml (glssc GTD)
       ((?psa, ?ca), ?psb, ?cb)"

Finally we combine these results to get the mix admissibility result.

mas_GTD: "(?seql, ?seqr) : mas (glssc GTD) ?A"

3 Inductive proof of cut (not mix) admissibility for GTD

The previous section dealt with a proof of cut admissibility where the inductive hypothesis was essentially that mix-admissibility is available for the endsequents of “smaller” pairs of derivations.

We now want to explore what it takes to produce an inductive proof where the inductive hypothesis is that (specifically) single-cut admissibility is available for “smaller” pairs of derivations.

We define the ordinary logical rules of the differently from the above, so that the rules (⊢ ∨) and (∧ ⊢) are of the forms shown (without the context)

\frac{A, B ⊢}{A ∧ B ⊢}  \frac{⊢ A, B}{⊢ A ∨ B}

In these forms, these rules are invertible.

We define the rules of the system as follows. The rules used for classical logic (before extending them with a context) form the set lkxcne: the rule sets idrls, wkrls, ctrrls A, lksil and lksir are the axioms, weakening rules, contraction (on A) rules, and the left and right logical introduction rules.

inductive "lkxcss xrls"
  intros
    extI : "psc : lkxcne ==> pscmap (extend flr) psc : lkxcss xrls"
    x : "psc : xrls ==> psc : lkxcss xrls"
inductive "lkxcne"
  intros
    id : "psc : idrls ==> psc : lkxcne"
    wk : "psc : wkrls ==> psc : lkxcne"
    ctr : "psc : ctrrls A ==> psc : lkxcne"
    ilI : "psc : lksil ==> psc : lkxcne"
    irI : "psc : lksir ==> psc : lkxcne"

When proving single-cut admissibility, the contraction rule causes a difficulty, since going up one step in the proof gives us an extra copy of the cutformula to deal with, and the inductive hypothesis enables us to use an inductively available cut only to get rid of one copy of the cut-formula.

The solution is to use the invertibility of the logical introduction rules, which reduces the problem of cut on a cut-formula A containing a logical connective to cut on sub-formulae of A.

Unfortunately the contraction rule causes the same sort of difficulty here as it does with the cut rule. So we have to prove, inductively, a sort of “multiinvertibilty” property, that multiple copies of a formula are invertible according to the introduction rule for that formula. Again, we define a predicate indicating that one step of an inductive proof of this result is available.

Firstly, we define the set of inverses of a sequent according to a rule set: if (ps, seq) ∈ irls and p ∈ ps, then p ∈ invs of irls seq.

Then the property of interest is that when a sequent is derivable, its inverses are also derivable. The predicate inv step describes that this property holds for the end-sequent of a derivation, assuming that it holds for the preceding sequent(s). Note that there are two rule sets involved, the rules used for derivations and the rules being shown to be invertible.

In the definition of inv step, derivs will be the set of derivable sequents. Then inv step … means that for the last rule (ps, concl) of a derivation: if the inverses of the premises ps of that rule are derivable, then the inverses of the conclusion concl are derivable.

Finally, gtd inv step shows that the logical introduction rules, with each formula repeated n times, and with contexts, are invertible, and gtd inv rl is the invertibility result.

invs_of_def: "invs_of ?irls ?seq ==
         {x. EX p ps. x = p & p : set ps & (ps, ?seq) : ?irls}"
inv_step.simps: "inv_step ?derivs ?irls (?ps, ?concl) =
   (set ?ps <= ?derivs --> (ALL p:set ?ps. invs_of ?irls p <= ?derivs) -->
   invs_of ?irls ?concl <= ?derivs)"
gtd_inv_step: "[| ?r : lksil Un lksir; ?x : lkxcss GTD |] ==>
  inv_step (derrec (lkxcss GTD) {}) (extrs (multiples {?r})) ?x"
gtd_inv_rl: "Ball (extrs (multiples lksne)) (inv_rl (lkxcss GTD))"

NOTE: From here the proof of cut admissibility is a single theorem with one long monolithic proof. Perhaps I should rearrange it so as to better enable a description of the intermediate results.

First we need a change in the pattern of proof by induction. Referring to the diagram in §2.1, the induction hypothesis that P (P_{li}, C_{r}) and P (C_{l}, P_{rj}) hold for all i and j will not be sufficient. Rather we will need an assumption that P (P′_{li}, C_{r}) and P (C_{l}, P′_{rj}) hold whenever P′_{li} is derived by a derivation no larger than the derivation of P_{li} (likewise for P′_{rj}).

This means that we need to define the height of a derivation tree, and therefore that we need to define a derivation tree value whose height can be defined and calculated.

(FOLLOWING FROM GLS LPAR PAPER - which also contains, earlier, discussion about deep/shallow embeddings, and extensive introduction to derrec, derl, etc)

In [?], we modelled a derivation tree in HOL as a recursive structure which consists of a root sequent (which should be the conclusion of some rule), and an associated list of (sub)trees (each of which should derive a premise of that rule). The type of explicit derivation trees is a recursive datatype, such as:

   datatype 'a dertree = Der 'a ('a dertree list)
       | Unf 'a (* unfinished leaf which remains unproved *)

We then had to express the property of such a tree, that it is in fact correctly based on the given rules, and so represents a valid derivation.

A valid tree is one whose inferences are in the set of rules and which as a whole has no premises.

Thus we “mix and match” a deep embedding of derivation trees with a shallow embedding of inductively defined sets of derivable sequents. To ensure the correctness of our “mixing and matching” we needed the following relationship between our definitions of derivability according to the two embeddings.

Lemma 3.1 Sequent X ⊢ Y is derivable, shallowly, from the empty set of premises using rules rls (ie, is in derrec rls {}) iff some explicit derivation tree dt is valid wrt. rls and has a conclusion X ⊢ Y.

"(?a : derrec ?rls {}) = (EX dt. valid ?rls dt & conclDT dt = ?a)"

We can now define the height of such a tree, as

primrec (* height (max) of derivation tree *)
  "heightDT (Der seq dts) = Suc (heightDTs dts)"
  "heightDTs [] = 0"
  "heightDTs (dt # dts) = max (heightDT dt) (heightDTs dts)"

Note that we had to use height as defined: we found that our first choice, to use the number of nodes in a derivation tree, did not work.

So height step2 tr … states that the inductive step works for the two derivation trees above the putative cut (or whatever property we use this induction pattern for). Unlike in the case of gen step2sr, the (final) argument is a pair of derivation trees rather than the pair of bottom rules. Apart from this, gen step2sr is a stronger property (as it uses a weaker induction property), so we get the result gs2 cas hs tr which links the two. This uses the relation on trees casdt, where cut-admissibility works between the conclusions of those trees. We also have a corresponding definition masdt and result gs2 mas hs tr for multicuts. And, corresponding to gen step2sr lem, we use the property by

the lemma height step2 tr lem.

height_step2_tr_eq: "height_step2_tr ?P ?A ?sub (?dta, ?dtb) =
      ((ALL A'. (A', ?A) : ?sub --> (ALL a b. ?P A' (a, b))) -->
       (ALL dtp. (dtp, ?dta) : measure heightDT --> ?P ?A (dtp, ?dtb)) -->
       (ALL dtq. (dtq, ?dtb) : measure heightDT --> ?P ?A (?dta, dtq)) -->
       ?P ?A (?dta, ?dtb))"
inductive "casdt rls A"
  intros
      I : "valid rls dtl & valid rls dtr -->
        (conclDT dtl, conclDT dtr) : car rls A ==> (dtl, dtr) : casdt rls A"
cas_casdt: "(conclDT ?dtl, conclDT ?dtr) : cas ?rls ?A ==>
  (?dtl, ?dtr) : casdt ?rls ?A
gs2_cas_hs_tr:
   "gen_step2sr (prop2 cas ?rls) ?A ?sub ?rls (botRule ?dta, botRule ?dtb)
      ==> height_step2_tr (prop2 casdt ?rls) ?A ?sub (?dta, ?dtb)"
height_step2_tr_lem: "[| ?A : wfp ?sub;
  ALL A dta dtb. height_step2_tr ?P A ?sub (dta, dtb) |] ==>
   ?P ?A (?dta, ?dtb)"

Since we have proved invertibility for the logical introduction rules, when the cut-formula is a compound formula, then, regardless of what the final rules in the actual derivation trees are, we can use the invertibility and reduce the problem to that of cuts on smaller formula.

We then use the fact that for all the logical connnectives, with their left and right logical introduction rules, we can use cuts on the subformulae on the premises of the introduction rules to achieve the effect of a cut on the whole formula on the conclusions of those introduction rules. This is expressed in the following theorem:

gprstep_q: "[| All (ctr_adm ?drls); wk_adm ?drls;
   (?ps, {#} |- {#?A#}) : lksir; (?qs, {#?A#} |- {#}) : lksil;
   ?pse = map (extend (?Xl |- ?Yl)) ?ps;
   ?qse = map (extend (?Xr |- ?Yr)) ?qs;
   set ?pse Un set ?qse <= derrec ?drls {};
   ALL sfa.  (sfa, ?A) : ipsubfml --> (ALL Xl Yl Xr Yr.
        (Xl |- mins sfa Yl, mins sfa Xr |- Yr) : cas ?drls sfa);
   extrs lksne <= ?drls |] ==> (?Xl + ?Xr |- ?Yl + ?Yr) : derrec ?drls {}"

There then remains the cases where the cut-formula A is not a compound formula introduced by the logical introduction rules in the sets lksil and lksir.

This means that A is either a boxed formula or a primitive proposition (or, in our formulation, a formula variable). Because the bottom rule on either side may be a contraction on A, in which case cutting with the premise of that rule is of no help, we look upwards on either side to the lowest rule which is not a contraction on A.

We have a lemma top ctr r which says that you can go up a derivation tree to a rule which is not contraction on A on the right. A similar lemma top ctr l applies to contraction on the left.

top_ctr_r: "[| ?ctrrl = ([{#} |- {#?A#} + {#?A#}], {#} |- {#?A#});
   valid ?rls ?dt; conclDT ?dt = extend ?flr ({#} |- {#?A#}) |] ==>
   EX dtn n.  botRule dtn ~: extrs {?ctrrl} & valid ?rls dtn &
         heightDT ?dt = heightDT dtn + n &
         conclDT dtn = extend ?flr (times (Suc n) ({#} |- {#?A#}))"

We then look at the final rule of that derivation tree (which is necessarily not a contraction). There are cases where the rule is either one of the box rules or is an extension ρ′ of a rule ρ in lkxcne, and in this case the rule may or may not have A as its principal formula.

Where the rule has A (in succedent position) as its principal formula, it can only be weakening (or the axiom, which is a trivial case). In this case either there are no contractions following the weakening, in which case weakening (of A) makes the cut-elimination trivial, or we construct a tree without the weakening step and with one fewer contractions, and this tree has the same conclusion; as this tree is smaller, we can apply the inductive hypothesis that cut-elimination is available.

Next there is the case where the principal formula of the rule ρ is not A. This case is like the parametric rule case of the simpler cut-elimiation proofs.

X′ ⊢ Y′, A^{n} ; (ρ′) ; X ⊢ Y, A^{n} ; (ctr^{∗} ⊢) ; X ⊢ Y, A A, U ⊢ V ..................................... (cut ?)
X, U ⊢ Y, V

Here we must apply the requisite number of contractions on A to the premises of ρ′, then apply (using the inductive hypothesis) cut on A to each of them, and finally apply ρ′′ which is the appropriate (but different from ρ′) extension of ρ.

X′ ⊢ Y′, A^{n} ; (ctr^{∗} ⊢) ; X′ ⊢ Y′, A A, U ⊢ V
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . (inductive cut)

X′, U ⊢ Y′, V (ρ′′) X, U ⊢ Y, V

The remaining case is where the last rule on the left above the contractions on A is one of the GT D rules. But as their conclusion is of the form □Γ ⊢ □A, this tells us that there are in fact no contractions following this rule.

We now look at the right side, and again, look for the last rule above a continuous sequence of contractions on the cut-formula.

Among the cases of the last rule on the right above the contractions, the cases of axiom or weakening involving A, or an extension of a rule in lkxcne whose principal formula is not A, are similar to those above.

This leaves us the case where the last rules on both sides above any contractions are the GTD rules.

For the first case, the rule on the left is the (□ ⊢) rule as shown, and for the rule on the right, only its conclusion matters, and is as shown.

Γ, □Γ ⊢ □A ; (□ ⊢) ; □Γ ⊢ □A \begin{matrix}⋯ \\ □A^{n}, □Δ ⊢ □B \end{matrix} ; (ctr^{∗} ⊢) ; □A, □Δ ⊢ □B
.......................................... (cut ?)
□Γ, □Δ ⊢ □B

We use the inductive hypothesis permitting cutting □A between Γ, □Γ ⊢ □A and □A, □Δ ⊢ □B then we use weakening and the (□ ⊢) rule, to get

Γ, □Γ ⊢ □A  \begin{matrix}⋯ \\ □A, □Δ ⊢ □B \end{matrix}
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . (inductive cut)

Γ, □Γ, □Δ ⊢ □B (weak) Γ, Δ, □Γ, □Δ ⊢ □B (□ ⊢) □Γ, □Δ ⊢ □B

The second case, with the (⊢ □) rule on the left as shown, is more complicated. Note that, for the rule on the right, B′ can be either □B or B.

Γ, □Γ ⊢ A ; (□ ⊢) ; □Γ ⊢ □A {A^{n}, □A^{n}, Δ, □Δ ⊢ B′ \atop □A^{n}, □Δ ⊢ □B} ; (ctr^{∗} ⊢) ; □A, □Δ ⊢ □B
............................................ (cut ?)
□Γ, □Δ ⊢ □B

In this case, from the premise on the right, we perform contractions on □A, then inductive cut on □A with the conclusion on the left, then contractions on A, then cut on A with the premise on the left, contraction(s) on □Γ, and finally an instance of the (⊢ □) or (□ ⊢) rule (whichever was on the right before). The result is shown below.

Γ, □Γ ⊢ A

□Γ ⊢ □A  A^{n}, □A^{n}, Δ, □Δ ⊢ B′ ; (ctr^{∗} ⊢) ; A^{n}, □A, Δ, □Δ ⊢ B′
........................................ (inductive cut)
A^{n}, □Γ, Δ, □Δ ⊢ B′
(ctr^{∗} ⊢)
A, □Γ, Δ, □Δ ⊢ B′
............................................... (inductive cut)

Γ, □Γ, □Γ, Δ, □Δ ⊢ B′ (ctr^{∗} ⊢) Γ, □Γ, Δ, □Δ ⊢ B′ (⊢ □) or (□ ⊢) □Γ, □Δ ⊢ □B

Finally we combine these results to get the cut admissibility result, in terms of explicit derivation trees, and then in terms of derivability.

gtd_casdt: "(?dta, ?dtb) : casdt (lkxcss GTD) ?A" : Thm.thm
gtd_cas: "(?cl, ?cr) : cas (lkxcss GTD) ?A" : Thm.thm

4 Dynamic Topological Logic: the system S4C

This section describes Isabelle proofs of the cut admissibility of the logic S4C described in [?]

This system has two “modal” operators, □ and ∘. The S4-axioms hold for □, ∘ commutes with the boolean operators, and the following are given:

∘(A → B) ↔ (∘A → ∘B)
∘⊥ ↔ ⊥
∘□A → □ ∘ A

The following sequent rules are given for S4C

\frac{∘^{k}A, Γ ⊢ Δ, ∘^{k}B}{Γ ⊢ Δ, ∘^{k}(A → B)}(⊢→) \frac{Γ ⊢ Δ, ∘^{k}A ∘^{k} B, Γ ⊢ Δ}{∘^{k}(A → B), Γ ⊢ Δ}(→⊢)

\frac{∘^{k}A, Γ ⊢ Δ}{∘^{k}□A, Γ ⊢ Δ}(□ ⊢)  \frac{Γ ⊢ Δ}{∘Γ ⊢ ∘Δ}(∘)  \frac{B ⊢ A}{B ⊢ □A}(⊢ □)

In the (⊢ □) rule, B must consist of “□-formulae”, that is, formulae of the form ∘^{k}□A.

As this presentation omits the other logical operators, we include, for them, the usual logical introduction rules with the principal and side formulae preceded by ∘^{k} just as with the (⊢→) and (→⊢) rules shown above.

The property we will prove inductively is mix (rather than cut) admissibility. In fact the presence of the ∘ rule adds to the complexity of the proof and is dealt with in a rather similarly to how we dealt with contraction in proving cut admissibility for GTD.

We now describe how we formalised the system. First we define the rules which can be extended by an arbitrary context. Without the context, these rules form the set s4cnne.

Applying nkmap k to a rule applies ∘^{k} to each formula appearing in that rule.

inductive "s4cnne"
  intros
    id : "psc : idrls ==> psc : s4cnne"
    wk : "psc : wkrls ==> psc : s4cnne"
    ctr : "psc : ctrrls A ==> psc : s4cnne"
    circ_il : "rl : lksil ==> nkmap k rl : s4cnne"
    circ_ir : "rl : lksir ==> nkmap k rl : s4cnne"
    circ_T : "rl : Tsnc ==> nkmap k rl : s4cnne"
inductive "Tsnc" (* simpler T rule with no context *)
  intros
    I : "([{#A#} |- {#}], {#Box A#} |- {#}) : Tsnc"

defs
  nkmap_def : "nkmap k == pscmap (seqmap (funpow Circ k))"
inductive "s4cn"
  intros
    extI : "rl : s4cnne ==> pscmap (extend (U |- V)) rl : s4cn"
    circI : "([seq], seqmap Circ seq) : s4cn"
    boxI : "M : msboxfmls ==> ([M |- {#A#}], M |- {#Box A#}) : s4cn"
inductive "boxfmls"
  intros
    I : "funpow Circ k (Box B) : boxfmls"
inductive "msboxfmls"
  intros
    I : "ALL f. f :# M --> f : boxfmls ==> M : msboxfmls"

To prove mix admissibility, the basic method is to look for the last rule application on each side of a rule other than the ∘ rule. This resembles the proof described in §3, where we looked for the last rule on each side which is not contraction on the cut-formula. For this we use the theorem top circ. We also need the fact that in some cases we need the fact that if the bottom rule is not ∘, then the tree asserted to exist is actually the original one. The function forget exists simply to prevent automatic case splitting of its argument: logically it does nothing.

top_circ: "valid ?rls ?dt ==> EX dtn k.
   botRule dtn ~: circrules & valid ?rls dtn &
   conclDT ?dt = seqmap (funpow Circ k) (conclDT dtn) &
   heightDT ?dt = heightDT dtn + k &
   forget ((k = 0) =
     (botRule ?dt ~: circrules) & (k = 0) = (dtn = ?dt))"
forget_def: "forget ?f == ?f"

But one easy case is where the last rule on both sides is the ∘ rule: then we can apply cut (on a smaller formula) to the premises of the ∘ rules, and then apply the ∘ rule. So when we look at the ∘ rules on both sides immediately preceding the cut, we need only bother about the case where the number of those ∘ rules is zero on one side.

First, the case where both rules are the (⊢ □) rule. Then there must be zero ∘ rules on the right side (because if there are zero ∘ rules on the left, then the cut-formula must be □A, whence there would also be zero ∘ rules on the right.

\begin{aligned}M ⊢ A \\ & (⊢ □) \\ M ⊢ □A \end{aligned} ; (∘^{∗}) ; ∘^{k}M ⊢ ∘^{k}□A \begin{aligned}∘^{k}□A, M′ ⊢ B \\ & (⊢ □) \\ ∘^{k}□A, M′ ⊢ □B \end{aligned} ............................................. (mix ?)
∘^{k}M, M′ ⊢ □B

Here we do the cut, by induction, before the (⊢ □) rule on the right, then we apply the (⊢ □) rule.

\begin{aligned}M ⊢ A \\ & (⊢ □) \\ M ⊢ □A \end{aligned} ; (∘^{∗}) ; ∘^{k}M ⊢ ∘^{k}□A ∘^{k}□A, M′ ⊢ B
........................................... (inductive mix)

∘^{k}M, M′ ⊢ B (⊢ □) ∘^{k}M, M′ ⊢ □B

For the other cases, we first consider the “parametric” cases, where the last rule above the ∘ rules is an extension ρ′ of a rule ρ in s4cnne, and the principal formula of ρ is not the “de-circled” cut-formula A.

X′ ⊢ Y′, A^{n} ; (ρ′) ; X ⊢ Y, A^{n} ; (∘^{∗}) ; ∘^{k}X ⊢ ∘^{k}Y, ∘^{k}A^{n} ∘^{k}A^{m}, U ⊢ V ............................................. (mix ?)
∘^{k}X, U ⊢ ∘^{k}Y, V

Here we must apply the ∘ rule the requisite number of times to the premise(s) of ρ′, then apply (using the inductive hypothesis) multicut on ∘^{k}A to each of them, and finally apply ρ′′ which we get by applying ∘^{k} to ρ, and then extending it appropriately.

This uses the result that if a rule is in s4cnne then so is the result of applying ∘^{k} to all formulae in its premises and conclusion.

s4cnne_nkmap: "?r : s4cnne ==> nkmap ?k ?r : s4cnne"

\begin{aligned}X′ ⊢ Y′, A^{n} \\ & (∘^{∗}) \\ ∘^{k}X′ ⊢ ∘^{k}Y′, ∘^{k}A^{n} \end{aligned} ∘^{k}A^{m}, U ⊢ V
............................................... (inductive mix)

∘^{k}X′, U ⊢ ∘^{k}Y′, V (ρ′′) ∘^{k}X, U ⊢ ∘^{k}Y, V

Next we consider the cases of weakening or contraction on the “de-circled” cut-formula.

X ⊢ Y, A^{n′} ; (wk/ctr) ; X ⊢ Y, A^{n} ; (∘^{∗}) ; ∘^{k}X ⊢ ∘^{k}Y, ∘^{k}A^{n} ∘^{k}A^{m}, U ⊢ V
............................................... (mix ?)
∘^{k}X, U ⊢ ∘^{k}Y, V

Here we must apply the ∘ rule the requisite number of times to the premise of the weakening or contraction, and then apply (using the inductive hypothesis) multicut on ∘^{k}A to each of them.

\begin{aligned}X ⊢ Y, A^{n′} \\ & (∘^{∗}) \\ ∘^{k}X ⊢ ∘^{k}Y, ∘^{k}A^{n′} \end{aligned} ∘^{k}A^{m}, U ⊢ V
.............................................. (inductive mix)
∘^{k}X, U ⊢ ∘^{k}Y, V

It is similar for the parametric, weakening or contraction cases on the right. The axiom rule is trivial in all cases.

For the (⊢ □) rule on the left, where the rule on the right is an extension of rule ρ whose principal formula is the “de-circled” cut-formula, the only case remaining is where ρ is (□ ⊢).

\begin{aligned}M ⊢ A \\ & (⊢ □) \\ M ⊢ □A \end{aligned} ; (∘^{∗}) ; ∘^{k}M ⊢ ∘^{k}□A \begin{aligned}∘^{k′′}A, U ⊢ V \\ & (□ ⊢) \\ ∘^{k′′}□A, U ⊢ V \end{aligned} ; (∘^{∗}) ; ∘^{k′+k′′}□A, ∘^{k′}U ⊢ ∘^{k′}V .................................................... (mix ?)
∘^{k}M, ∘^{k′}U′ ⊢ ∘^{k′}V

Here k′ + k′′ = k, but since we also have that k = 0 or k′ = 0, this means that k′ = 0 and k′′ = k. Here is is more complicated than it would be for a single cut, since we have to perform inductive cuts on formulae first with, then without, □: here U may contain further occurrences of ∘^{k}□A, and U′ represents U with these deleted.

M ⊢ A (∘^{∗}) ∘^{k}M ⊢ ∘^{k}A

\begin{aligned}M ⊢ □A \\ & (∘^{∗}) \\ ∘^{k}M ⊢ ∘^{k}□A \end{aligned} ∘^{k}A, U ⊢ V
....................................... (inductive mix)
∘^{k}M, ∘^{k}A, U′ ⊢ V
...................................................... (inductive mix)

∘^{k}M, ∘^{k}M, U′ ⊢ V (ctr) ∘^{k}M, U′ ⊢ V

Next we look at the case of the (⊢ □) rule on the right, but for this, since the cut-formula must be a □-formula, all cases have already been dealt with.

Finally, there is the case where the last rules (above the final sequence of ∘-rules) on both sides are extensions of rules in s4cnne. Most of these cases have been covered, ie,

• the “parametric” cases, where the “de-circled” cut-formula is the principal formula of the rule

• axiom, weakening, and contraction rules

So there remain the cases where the rules on either side are the logical introduction rules. For these, the proofs are essentially the same as for other logics generally, except that we need to allow for a number of circles. Conceptually it is easiest to imagine that in each case the final ∘ rules are moved upwards to precede the final logical introduction rules, although we didn’t actually prove it this way.

We proved that the usual logical introduction rules, with ∘^{k} applied to principal and side formulae (as used in S4C), satisfy the property c8ger prop mentioned in §2.1. Recall that this means that assuming (single-)cut admissibility on smaller formulae, you have cut admissibility of a more complex formula where the last rule on either side is a logical introduction rule.

s4cn_c8: "c8ger_prop (circrel ipsubfml) s4cn ?A
    (nkmap ?k ` (lksil Un lksir))"

The following diagrams show an example. Again, doing mix-admissibility makes it more complicated because we have to do inductive applications of mix (for the original cut-formula) as well as applications of cut on smaller formulae. We let t = k + k′ = l + l′, and we let Y′ be Y with copies of ∘^{k′}(A ∧ B) deleted, and U′ be U with copies of ∘^{l′}(A ∧ B) deleted. In this case we do not make use of the fact that either k or l must be zero.

\begin{aligned}X ⊢ ∘^{k′}A, Y & X ⊢ ∘^{k′}B, Y \\ & (⊢ ∧) \\ X ⊢ ∘^{k′}(A ∧ B), Y \end{aligned} ; (∘^{∗}) ; ∘^{k}X ⊢ ∘^{t}(A ∧ B), ∘^{k}Y \begin{aligned}U, ∘^{l′}A, ∘^{l′}B ⊢ V \\ & (∧ ⊢) \\ U, ∘^{l′}(A ∧ B) ⊢ V \end{aligned} ; (∘^{∗}) ; ∘^{l}U, ∘^{t}(A ∧ B) ⊢ ∘^{l}V ................................................................ (mix ?)
∘^{k}X, ∘^{l}U′ ⊢ ∘^{k}Y′, ∘^{l}V

This is replaced by

\begin{aligned}X ⊢ ∘^{k′}A, Y \\ & (∘^{∗}) \\ ∘^{k}X ⊢ ∘^{t}A, ∘^{k}Y \end{aligned} ∘^{l}U, ∘^{t}(A ∧ B) ⊢ ∘^{l}V
.................................................... (inductive mix)

∘^{k}X, ∘^{l}U′ ⊢ ∘^{t}A, ∘^{k}Y′, ∘^{l}V . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

(A)

\begin{aligned}X ⊢ ∘^{k′}B, Y \\ & (∘^{∗}) \\ ∘^{k}X ⊢ ∘^{t}B, ∘^{k}Y \end{aligned} ∘^{l}U, ∘^{t}(A ∧ B) ⊢ ∘^{l}V
.................................................... (inductive mix)

∘^{k}X, ∘^{l}U′ ⊢ ∘^{t}B, ∘^{k}Y′, ∘^{l}V . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

(B)

∘^{k}X ⊢ ∘^{t}(A ∧ B), ∘^{k}Y  \begin{aligned}U, ∘^{l′}A, ∘^{l′}B ⊢ V \\ & (∘^{∗}) \\ ∘^{l}U, ∘^{t}A, ∘^{t}B ⊢ ∘^{l}V \end{aligned}
.................................................... (inductive mix)

∘^{k}X, ∘^{l}U′, ∘^{t}A, ∘^{t}B ⊢ ∘^{k}Y′, ∘^{l}V ....................................

(C)

Then (A), (B) and (C) are combined using inductive cuts on the smaller cutformulae ∘^{t}A and ∘^{t}B, and the necessary contractions, to derive the required sequent ∘^{k}X, ∘^{l}U′ ⊢ ∘^{k}Y′, ∘^{l}V.

Finally we combine these results to get the mix admissibility result, in terms of explicit derivation trees, and then in terms of derivability.

s4cn_masdt: "(?dta, ?dtb) : masdt s4cn ?A"
s4cn_mas: "(?cl, ?cr) : mas s4cn ?A"

References

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