Machine-checked Proof-Theory for Propositional Modal Logics

Jeremy E. Dawson^{∗}, Rajeev Goré and Jesse Wu Logic and Computation Group, School of Computer Science The Australian National University, Canberra ACT 2601

Abstract

We describe how we machine-checked the admissibility of the standard structural rules of weakening, contraction and cut for multiset-based sequent calculi for the unimodal logics S4, S4.3 and K4De, as well as for the bimodal logic S4C recently investigated by Mints. Our proofs for both S4 and S4.3 appear to be new while our proof for S4C is different from that originally presented by Mints, and appears to avoid the complications he encountered. The paper is intended to be an overview of how to machine-check proof theory for readers with a good understanding of proof theory.

∗Supported by Australian Research Council Grant DP120101244.

Contents

1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2 Sequents Built From Multisets Versus Sets . . . . . . . . . . . . . 3 3 Our Modal Logics . . . . . . . . . . . . . . . . . . . . . . . . . . 3 4 Interactive Proof Assistants . . . . . . . . . . . . . . . . . . . . . 3 5 A Deep Embedding of Formulae and Sequents . . . . . . . . . . . 3 6 Implicit Derivations: a shallow embedding of . . . . . . . . . . . 3 7 Explicit Derivation Trees: a deep embedding of derivations … 3 8 Subformula Relation and Rule Extensions with Arbitrary Contexts 3 9 The Weakening, Inversion and Contraction Properties . . . . . . 3 10 Generalising Cut-Admissibility Proofs . . . . . . . . . . . . . . . 3 11 Statement of Cut-Admissibility in Isabelle . . . . . . . . . . . . . 3 12 Weakening, Contraction and Cut Admissibility for S4 . . . . . . 5 12.1 Calculus for S4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 12.2 Weakening for S4 . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 12.3 Invertibility and Contraction for S4 . . . . . . . . . . . . . . . . . 8 12.4 Cut-admissibility for S4 . . . . . . . . . . . . . . . . . . . . . . . 13 13 Weakening, Contraction and Cut Admissibility for S4.3 . . . . . 15 13.1 Calculus for S4.3 . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 13.2 Weakening for S4.3 . . . . . . . . . . . . . . . . . . . . . . . . . . 17 13.3 Invertibility and Contraction for S4.3 . . . . . . . . . . . . . . . . 19 13.4 Cut-admissibility for S4.3 . . . . . . . . . . . . . . . . . . . . . . 22 14 The system GTD . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 14.1 Calculus for GTD . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 14.2 Weakening-admissibility for GTD . . . . . . . . . . . . . . . . . . 25 14.3 Inversion and Contraction-admissibility for GTD . . . . . . . . . 26 14.4 Cut-admissibility for GTD . . . . . . . . . . . . . . . . . . . . . . 28 15 Dynamic Topological Logic S4C . . . . . . . . . . . . . . . . . . . 31 15.1 Calculus for S4C . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 15.2 Weakening for S4C . . . . . . . . . . . . . . . . . . . . . . . . . . 32 15.3 Inversion and Contraction-admissibility for S4C . . . . . . . . . . 33 15.4 Cut-admissibility for S4C . . . . . . . . . . . . . . . . . . . . . . 34 15.5 Comparing our proofs and the proofs of Mints . . . . . . . . . . . 39 16 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 17 Further Work and Conclusion . . . . . . . . . . . . . . . . . . . . 40

1 Introduction

2 Sequents Built From Multisets Versus Sets

3 Our Modal Logics

4 Interactive Proof Assistants

5 A Deep Embedding of Formulae and Sequents

6 Implicit Derivations: a shallow embedding of

7 Explicit Derivation Trees: a deep embedding of derivations

8 Subformula Relation and Rule Extensions with Arbitrary Contexts

9 The Weakening, Inversion and Contraction Properties

10 Generalising Cut-Admissibility Proofs

11 Statement of Cut-Admissibility in Isabelle

Definition 11.1 (cas,car): A pair of sequents (XY_{l}, XY_{r}) satisfies the property car if the sequent obtained by applying the cut rule to them is derivable. That is, (X_{l} ⊢ Y_{l}, X_{r} ⊢ Y_{r}) ∈ car rls A iff (X_{l}, (X_{r} − A) ⊢ (Y_{l} − A), Y_{r}) is rlsderivable.

A pair of sequents satisfies the property cas if cut-admissibility is available for that pair of sequents. That is, (X_{l} ⊢ Y_{l}, X_{r} ⊢ Y_{r}) ∈ cas rls A means that if X_{l} ⊢ Y_{l} and X_{r} ⊢ Y_{r} are rls-derivable, then (X_{l} ⊢ Y_{l}, X_{r} ⊢ Y_{r}) ∈ car rls A.

car_eq: "((?Xl |- ?Yl, ?Xr |- ?Yr) : car ?rls ?A) =
         ((?Xl + (?Xr - {#?A#}) |- ?Yl - {#?A#} + ?Yr) : derrec ?rls {})"
cas_eq: "((?seql, ?seqr) : cas ?rls ?A) =
            (?seql : derrec ?rls {} & ?seqr : derrec ?rls {} -->
               (?seql, ?seqr) : car ?rls ?A)"

When we are talking about proving cas or car by induction on the (implicit) derivation of the two sequents, that is, we are talking about two sequents which are derivable, then these two concepts become equivalent. This is because the definition of gen step2sr only involves the property of the pair of sequents in the cases where those two sequents are derivable. Recall that prop2 simply gives an equivalent concept with a different type.

Lemma 11.1: The induction steps for proving cas and car are equivalent.

prop2_def     : "prop2 f rls A seqs == seqs : f rls A"
gs2_cas_eq_car: "gen_step2sr (prop2 cas ?rls) ?A ?sub ?rls =
                 gen_step2sr (prop2 car ?rls) ?A ?sub ?rls"

Definition 11.2 (casdt): Two valid (ie. no unproved leaves, and all steps are rules of rls) derivation trees dtl and dtr satisfy casdt rls A if their conclusions satisfy car

casdt_eq: "((?dtl, ?dtr) : casdt ?rls ?A) =
         (valid ?rls ?dtl & valid ?rls ?dtr -->
                (conclDT ?dtl, conclDT ?dtr) : car ?rls ?A)"

Here is the lemma linking the induction step for cut-admissibility in terms of implicit derivability with the corresponding induction step for explicit derivation trees.

Lemma 11.2 (gs2 tr casdt sr): Given two derivation trees dta and dtb, a cutformula A, a sub-formula relation sub, and a rule set rls, if the bottom rules of those trees satisfy the step condition gen step2sr for cut-admissibility, then the two trees satisfy the step condition gen step2 tr for cut-admissibility:

gs2_tr_casdt_sr:
   "gen_step2sr (prop2 cas ?rls) ?A ?ipsubfml ?rls
        (botRule ?dta, botRule ?dtb) ==>
    gen_step2_tr (prop2 casdt ?rls) ?A ?ipsubfml (?dta, ?dtb)"

In fact the two concepts are essentially equivalent:

Theorem 11.1 (gs2 casdt equiv): Given a set of derivation rules rls, a formula A, a sub-formula relation ipsubfml and two bottom rules pscl and pscr, then the following are equivalent:

(a) if pscl and pscr are in rls, then they satisfy the step condition gen step2sr for cut-admissibility (for implicit derivations)

(b) all trees dta and dtb whose bottom rules are pscl and pscr respectively, satisfy the step condition gen step2 tr for cut-admissibility (for explicit derivations)

gs2_casdt_equiv:
  "(?pscl : ?rls --> ?pscr : ?rls -->
       gen_step2sr (prop2 cas ?rls) ?A ?ipsubfml ?rls (?pscl, ?pscr)) =
    (ALL dta dtb.  botRule dta = ?pscl --> botRule dtb = ?pscr -->
      gen_step2_tr (prop2 casdt ?rls) ?A ?ipsubfml (dta, dtb))"

We are now ready to apply all of our formalisation work to particular calculi.

12 Weakening, Contraction and Cut Admissibility for S4

There exist both pen and paper [?, ?] and a formalised proof [?] of mixelimination for sequent calculi describing S4 which include explicit weakening and contraction rules. As stated previously, the inclusion of structural rules is detrimental for automated reasoning and so provides a practical motivation for proving admissibility results for a calculus free of such rules. This is our goal.

Troelstra and Schwichtenberg also state cut-elimination for a sequent calculus G3s that no longer uses explicit structural rules. Unfortunately, the “proof” Jesse, is this of their theorem only discusses one actual transformation, and in particular for S4? overlooks one non-trivial case – when Cut is applied on a formula □A, with both premises being an instance of the G3s R□ rule (shown below). In this case, the deduction cannot be transformed by simply permuting the Cut, or introducing a new Cut of smaller rank, on the sequents in the original deduction. Greater detail is given later in this section.

□Γ ⊢ A, Δ R□ Γ′, □Γ ⊢ □A, Δ, Δ′

Goubault [?] acknowledges the problem posed by absorbing Weakening into the R□ rule. However, his solutions are given in the context of typed λ-calculi for a minimal version of S4, interpreted as a sequent calculus through a version of the Curry-Howard correspondence. Based on a proposal from [?], Goubault-Larrecq replaces the R□ rule by a different rule with multiple premises (for subformula within the principal formula), along with both re-write and garbage collection rules for the λ terms involved. While this solution could possibly be extended to sequent calculi, the creation of new premises and hence branching is detrimental to backward proof search. The solution presented in this section also has the advantage of being significantly simpler.

Negri [?] proves various admissibility theorems for S4, but the calculus involved is labelled. These labels include elements of the Kripke semantics within the calculus, and so the resulting theorems are thus not entirely syntactical proofs. Furthermore, there are rules in the calculus which deal only with reachability between worlds. While perhaps not as inefficient as the standard structural rules, these rules nevertheless do not operate on logical connectives. In particular to S4, from the perspective of automated reasoning, applying all possible instances of the transitivity rule (shown below) or checking whether the transitivity rule has been saturated can be a very time-consuming process.

xRz, xRy, yRz, Γ ⊢ Δ Transitivity xRy, yRz, Γ ⊢ Δ

R is the accessibility relation. x, y, z are worlds.

12.1 Calculus for S4

The sequent calculus we use for S4 is based on the calculus G3cp, with the addition of two modal rules. Note that the initial sequents Γ, φ ⊢ φ, Δ do not Initial Sequents

\begin{aligned}id \\ & Γ, φ ⊢ φ, Δ \end{aligned}

Classical rules

\begin{aligned}& Γ, φ, ψ ⊢ Δ \\ L∧ \\ & Γ, φ ∧ ψ ⊢ Δ \end{aligned}  \begin{aligned}Γ ⊢ φ, Δ & Γ ⊢ ψ, Δ \\ R∧ \\ & Γ ⊢ φ ∧ ψ, Δ \end{aligned}
\begin{aligned}Γ, φ ⊢ Δ & Γ, ψ ⊢ Δ \\ L∨ \\ & Γ, φ ∨ ψ ⊢ Δ \end{aligned} \begin{aligned}& Γ ⊢ φ, ψ, Δ \\ R∨ \\ & Γ ⊢ φ ∨ ψ, Δ \end{aligned}
\begin{aligned}Γ ⊢ φ, Δ & Γ, ψ ⊢ Δ \\ L→ \\ & Γ, φ → ψ ⊢ Δ \end{aligned} \begin{aligned}& Γ, φ ⊢ ψ, Δ \\ R→ \\ & Γ ⊢ φ → ψ, Δ \end{aligned}
\begin{aligned}& Γ ⊢ φ, Δ \\ L¬ \\ & Γ, ¬φ ⊢ Δ \end{aligned}  \begin{aligned}& Γ, φ ⊢ Δ \\ R¬ \\ & Γ ⊢ ¬φ, Δ \end{aligned}

Modal rules

\begin{aligned}& Γ, φ, □φ ⊢ Δ \\ Refl \\ & Γ, □φ ⊢ Δ \end{aligned}  \begin{aligned}& Γ, □Γ ⊢ φ \\ S4□ \\ & Σ, □Γ ⊢ □φ, Δ \end{aligned}

Fig. 1: Sequent calculus GS4 for S4.

inductive "lksne" intros (* skeletons of LK rules *)
axiom : "([], {#A#} |- {#A#}) : lksne"
ilI   : "psc : lksil ==> psc : lksne"
irI   : "psc : lksir ==> psc : lksne"
inductive "lksss" intros (* extended skeletons for LK *)
extI : "psc : lksne ==> pscmap (extend flr) psc : lksss"
inductive "lkrefl" intros (* refl rule skeleton *)
I : "([{#A#} + {#Box A#} |- {#}], {#Box A#} |- {#}) : lkrefl"
inductive "lkbox" intros (* S4 Box rule skeleton *)
I : "([gamma + mset_map Box gamma |- {#A#}],
               mset_map Box gamma |- {#Box A#}) : lkbox"
inductive "gs4_rls" intros
lksI  : "psc : lksss ==> psc : gs4_rls"
reflI : "psc : lkrefl ==> pscmap (extend flr) psc : gs4_rls"
(* Note Box rule allows extra formulae in conclusion only *)
boxI  : "(prem, conc) : lkbox ==> (prem, extend flr conc) : gs4_rls"

Fig. 2: Isabelle rules for GS4. require atoms, and that there are only rules for □ formulae with ♢φ interpreted as ¬□¬φ. The rules of the calculus are shown in Figures 1 and 2. Note that the clause boxI in the inductive definition for gs4_rls applies extend only to the conclusion, corresponding to the appearance of the two sets Σ and Δ in the conclusion of the rule S4□.

In Isabelle, the calculus is encoded in a modular manner. With the overall calculus, called gs4 rls, built up from separate declarations of the id rule, the classical rules acting on antecedents and succedents, and the two modal rules.

12.2 Weakening for S4

Definition 12.1: A set of rules rls satisfies ext_concl iff: for every list of premises ps and conclusion c that form a rule in rls, and all possible sequents UV, there exists a list of premises ps' such that the premises ps' and the extended conclusion c + UV also form an instance of some rule in rls and for every premise p from ps there is a corresponding premise p' in ps' such that p' is either p itself or is an extension of p.

                       \frac{p_{1} . . . p_{k}}{c} \frac{p'_{1} . . . p'_{k}}{c + UV}

The Isabelle text uses <= as described in §??, and (ps, ps') : allrel r means that ps and ps' are lists of the same length where each corresponding pair of their members is in r.

ext_concl_def: "ext_concl ?rls ==
    ALL (ps, c):?rls. ALL UV. EX ps'.
    (ps', c + UV) : ?rls & (ps, ps') : allrel {(p, p'). p <= p'}"
inductive "allrel r"
  intrs
    allrel_Nil "([], []) : allrel r"
    allrel_Cons "[| (ha, hb) : r ; (ta, tb) : allrel r |] ==>
      (ha # ta, hb # tb) : allrel r"

Lemma 12.1: If a set of rules rls obeys ext_concl then rls admits weakening:

wk_adm_ext_concl: "ext_concl ?rls ==> wk_adm ?rls"

The lemma wk_adm_ext_concl is simple enough to be proved directly by the induction principle for derrec, Lemma ??, ie without using gen_step_lem. Use of lemmas like gen_step_lem is really only for the purpose of breaking up the proofs, so that various different cases of gen_step (ie various final rules of the derivation) can be put into separate lemmas, some of which may be able to be reused for different calculi.

Lemma 12.2: The set of rule gs4_rls satisfies ext_concl.

gs4_ext_concl: "ext_concl gs4_rls"

Corollary 12.1: The rules of S4 satisfy weakening admissibility.

gs4_wk_adm: "wk_adm gs4_rls"

12.3 Invertibility and Contraction for S4

We now describe how we captured the traditional proof of invertibility.

Suppose that we are given a calculus consisting of the rule set drls and suppose that we want to reason about the derivability predicate derrec defined earlier. Let derivs be the set derrec drls {} of all sequents that are derivable from the empty set of leaves using the rules of drls. Suppose that we wish to prove that every rule in irls is invertible wrt drls (where irls is usually a subset of drls).

Without describing it in detail, the function invs_of irls c returns the set of sequents obtainable by applying each rule of irls to the sequent c backwards once. That is, a sequent seq is in invs_of irls c if applying some rule ρ of irls to c backwards, once, will give seq as one of the premises of ρ.

To prove that a rule (ps, concl) is invertible wrt drls requires us to prove that each sequent seq from the list ps of premises is in derivs if concl is in derivs. To prove that each rule in a set of rules irls is invertible wrt drls requires us to prove that the above property holds for each rule (ps, concl)

from irls: that is, invs_of irls concl <= derivs where <= encodes the

subset relation.

Traditional proofs of invertibility proceed by an induction on the structure of a given derivation of a sequent concl from derivs. Assuming that the final rule in this derivation is (ps, concl), the induction hypothesis is to assume that the invertibility lemma holds for each premise in ps. That is, we assume that every sequent seq obtained by applying any rule from irls backwards, once, to any premise p in ps is itself in derivs:

           ALL p:set ps. invs_of irls p <= derivs

Use of the induction hypothesis stated above can then be encoded in inv step. Let an “irls-inverse” of a sequent s be a sequent s′ obtained from s by

applying a rule from irls backwards once.

Definition 12.2 (inv step): Then for a given set derivs of derivable sequents, for a rule set irls, and for every rule instance (ps, concl), the property:

inv_step derivs irls (ps, concl) means:

If every premise in ps being in derivs implies that every “irls-invert” of premises in ps is in derivs,

then every “irls-invert” of the conclusion concl is in derivs.

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

This is the key result for doing invertibility by stating various cases of the induction step as separate lemmas.

The expression UNION (set ?ps) (invs_of ?irls) represents the set X of all sequents which can be obtained by applying some rule from irls backwards once to every sequent p from a list of sequents ps viewed as a set:

                 X := ⋃_{p ∈ set ps}(invs_of ?irls p)

   Then, the expression (set ?ps Un UNION (set ?ps) (invs_of ?irls))

represents the union of X and the list of sequents ps treated as a set, ie

(set ps) ∪ X.

The property inv_stepm is weaker than inv_step but is monotonic in its first argument, which makes reusing lemmas such as lks_inv_stepm possible as follows.

Definition 12.3 (inv stepm): For all rule sets rls, for all rule sets irls, for all

rules (ps, concl): inv_stepm drls irls (ps, concl) means: irls-inverses

of concl are derivable using derrec from (set ps) and the irls-inverses of every p from set ps:

inv_stepm.simps:
   "inv_stepm ?drls ?irls (?ps, ?concl) =
      (invs_of ?irls ?concl
       <= derrec ?drls (set ?ps Un UNION (set ?ps) (invs_of ?irls)))"

Lemma 12.3: inv_stepm is monotonic in its first argument:

inv_step_mono:
   "[| inv_stepm ?drlsa ?irls ?psc ; ?drlsa <= ?drlsb |]
   ==> inv_stepm ?drlsb ?irls ?psc"

Lemma 12.4: For every set drls of rules and every set plvs of sequents, the function (derrec drls plvs) returns the set of sequents derivable from plvs using the rules of drls. Let us call this set of derivable sequents derivs. For every set drls of rules used for derivations, for every rule set irls, for every rule psc,

if inv_stepm drls irls psc holds then do does inv_step derivs irls psc

for any set of leaf premises plvs:

inv_step_m:
val it =
   "inv_stepm ?drls ?irls ?psc
            ==> inv_step (derrec ?drls ?plvs) ?irls ?psc"

Lemma 12.5 (gen inv by step): For every rule set rls which is used to construct a set derrec rls {} of derivations from the empty set of leaves, for every rule set irls, every rule psc from irls is invertible wrt rls if every rule instance

(ps, concl) from rls obeys inv_step (derrec rls {}) irls (ps, concl):
gen_inv_by_step:
   "[| Ball ?rls (inv_step (derrec ?rls {}) ?irls) ; ?psc : ?irls |]
      ==> inv_rl ?rls ?psc"

Lemma 12.6: Every instance of the rule Refl, extended with arbitrary contexts, is invertible in the rule set gs4_rls:

          Ball (extrs lkrefl) (inv_rl gs4_rls)

Proof: Suppose that Γ, □φ ⊢ Δ is derivable. We can show that the premise Γ, φ, □φ ⊢ Δ is derivable by applying weakening, which has already been shown to be admissible in gs4_rls. Q.E.D.

Lemma 12.7: Every instance of the rule set lksss (of classical propositional logic) is invertible in the rule set gs4_rls:

      Ball lksss (inv_rl gs4_rls)

Proof: By Lemma 12.5, it suffices to prove (inv step (derrec gs4 rls {}) lksss) psc for every rule psc from gs4_rls. By Lemma 12.4, it suffices to

prove inv stepm gs4 rls lksss psc for every rule psc from gs4_rls: Note

that lksss == extrs lksne: the rule set lksne extended with arbitrary contexts. For psc in gs4_rls, we proceed by cases on the rule psc:

psc = Refl This case is immediate since the inverse of the Refl rule is a case of weakening.

     "?psc : extrs lkrefl ==> inv_stepm gs4_rls (extrs lksne) ?psc"

psc is from LK Where the rule psc is a classical rule, we first prove that the set of classical rules is invertible wrt itself:

     "?psc : extrs lksne ==>
         inv_stepm (extrs lksne) (extrs lksne) ?psc"

Since the rules lksss are a subset of the rules gs4_rls, we can use (the monotonicity) Lemma 12.3 to obtain

     "?psc : extrs lksne ==> inv_stepm gs4_rls (extrs lksne) ?psc"

psc = S4□ Where last rule is S4□ ( with arbitrary contexts in conclusion only), to make weakening admissible, we prove a very general result. If the rule set rls contains exactly one rule extcs {(ps, c)} which is the rule (skeleton) (ps, c) with only the conclusion extended by an arbi-

trary context, then inv_stepm rls (extrs {(ips, ic)}) rl holds for

any rule (ips, ic) extended with arbitrary contexts if the (skeletons of the) conclusion ic and the the (skeletons of the) conclusion c are disjoint:

inv_stepm_disj_cs:
   "[| seq_meet ?c ?ic = 0; extcs {(?ps, ?c)} = ?rls; ?rl : ?rls |]
         ==> inv_stepm ?rl (extrs {(?ips, ?ic)}) ?rl"

In particular, we can put extcs {(?ps, ?c)} to be the rule S4□ and put (extrs {(?ips, ?ic)}) to be any rule from lksss since the skeletons of the conclusions of the lksss rules contain only the principal formula of the respective rule and none of these is a □-formula.

Q.E.D.

Theorem 12.1 (inv rl gs4 refl and inv rl gs4 lks): The Refl (lkrefl) rule

and all Classical (lksss) rules are invertible within gs4 rls.

Proof: TODO: remove this? Takes up too much space.

As an example, consider invertibility for the R∨ rule. The proof proceeds by an induction on height, and uses the induction principle from Lemma 12.5. Which of

the gen-step lemmas does it actually use ? It uses

                                                               gen inv by step

Case 1. Axiom If Γ ⊢ φ ∨ ψ, Δ is an axiom, and φ ∨ ψ is principal, then Γ = Γ′, φ ∨ ψ. The derivation for Γ ⊢ φ, ϕ, Δ is then:

\begin{aligned}id \\ & Γ′, φ ⊢ φ, ϕ, Δ \end{aligned} \begin{aligned}id \\ & Γ′, ψ ⊢ φ, ϕ, Δ \end{aligned} L∨ Γ′, φ ∨ ψ ⊢ φ, ϕ, Δ

If φ ∨ ψ is parametric in the axiom, then Γ ⊢ Δ is an axiom, and so is Γ ⊢ φ, ϕ, Δ.

Case 2. Principal If Γ ⊢ φ ∨ ψ, Δ is not an axiom, but φ ∨ ψ is principal, then R∨ must have been the last rule applied. Invertibility follows immediately from the premises of the R∨ rule.

Case 3. Parametric If Γ ⊢ φ ∨ ψ, Δ is not an axiom, and φ ∨ ψ is parametric, then an application of a new instance of that last rule (perhaps using the induction hypothesis) obtains the necessary endsequent. This is because all rules allow arbitrary contexts in their conclusion (and premises when the premises contain context). To illustrate, consider the two cases when the last rule used to originally derive Γ ⊢ φ ∨ ψ, Δ is either the Refl or the S4□ rule.

• If the last rule was Refl then Γ = Γ′, □A and the original derivation is:

\begin{matrix}Π \\ Γ′, A, □A ⊢ Δ, φ ∨ ψ \end{matrix} Refl Γ′, □A ⊢ Δ, φ ∨ ψ

Applying the inductive hypothesis on the premises gives a derivation of Γ′, A, □A ⊢ Δ, φ, ψ. Apply Refl to this gives the required Γ′, □A ⊢ φ, ϕ, Δ.

• If the last rule was S4□ then Γ = Σ, □Γ′ and Δ = □A, Δ′ and the original derivation looks like:

\begin{matrix}Π \\ Γ′, □Γ′ ⊢ A \end{matrix} S4□ Σ, □Γ′ ⊢ □A, Δ′, φ ∨ ψ

To derive Γ ⊢ φ, ψ, Δ, simply apply a new instance of S4□ to the original premises, this time with φ, ψ as the context instead of φ ∨ ψ:

\begin{matrix}Π \\ Γ′, □Γ′ ⊢ A \end{matrix} S4□ Σ, □Γ′ ⊢ □A, Δ′, φ, ψ

Q.E.D.

Theorem 12.2 (gs4 ctr adm): Contraction is admissible for the calculus gs4 rls.

Proof: The cases for the G3cp and Refl rules are handled in the standard manner as in the literature (see [?] and [?]) using the invertibility results above. The formalisation performs the necessary transformations using a simple instantiation gen ctr adm step (not shown) of the induction principle gen step lem of Theorem ??.

When the rule above the contraction is an instance of the S4□ rule, there are two possible cases. Either one or both copies of the contraction-formula exist within the context of the S4□ rule, or both copies are principal.

In the first case, deleting one copy still leaves an instance of the rule. That is, if the contraction-formula is A, with A in the succedent, then the original rule instance is as shown below where either □φ = A or A ∈ Δ:

Γ, □Γ ⊢ φ S4□ Σ, □Γ ⊢ □φ, A, Δ

Applying the S4□ rule without introducing the shown second copy of A in the conclusion above gives a proof of Σ, □Γ ⊢ □φ, Δ as required since an occurrence of A is still in the succedent as □φ = A or A ∈ Δ. Similarly, if A is in the context Σ the new S4□ rule instance is then: Was just φ

in succedent of conclusion. (for Jesse to check)

Γ, □Γ ⊢ φ S4□ Σ − A, □Γ ⊢ □φ, A, Δ

The harder case occurs when both instances of the contraction-formula A are principal. Due to the nature of the S4□ rule this requires A to occur in the antecedent only, as there cannot be two principal formulae in the succedent. As only boxed formulae are principal, A has form □B. The original rule instance is thus represented by: Was just φ in

succedent of

conclusion. B, B, □B, □B, Γ, □Γ ⊢ φ S4□ Σ, □B, □B, □Γ ⊢ □φ, Δ

The copies of □B and B can be contracted upon, first using the induction hypothesis that the result applies to preceding sequents in the derivation, and then on the rank of the contraction-formula. The S4□ rule can then be applied to give the required conclusion. Was just φ in

succedent of

conclusion. B, □B, Γ, □Γ ⊢ φ S4□ Σ, □B, □Γ ⊢ □φ, Δ

In the Isabelle proof, this step is unfortunately rather more tedious. A significant number of proof steps in the formalisation are dedicated to manipulating the ordering of formulae to convince the proof assistant that the S4□ can be applied after applying the induction hypotheses, and that the resulting sequent is indeed what is required. Q.E.D.

gs4_ctr_adm: "ctr_adm gs4_rls ?A"

12.4 Cut-admissibility for S4

We first state a lemma used several times in the proof of cut-admissibility.

Lemma 12.8: Given two derivation trees dta and dtb, a cut-formula A, a subformula relation sub, and a rule set rls, if the bottom rules of those trees satisfy the step condition gen step2sr for cut-admissibility, then the two trees satisfy the step condition sumh step2 tr for cut-admissibility:

Proof: By combining Lemmas ??, 11.2 and 11.1 Q.E.D.

gs2_car_sumhs_tr:
   "gen_step2sr (prop2 car ?rls) ?A ?sub ?rls (botRule ?dta, botRule ?dtb)
         ==> sumh_step2_tr (prop2 casdt ?rls) ?A ?sub (?dta, ?dtb)"

Theorem 12.3 (gs4 cas): Cut is admissible in the calculus gs4 rls.

Proof: Our proof essentially uses a double induction on level and rank, where level measures the sum of the heights of the derivation trees for the left and right premises of the cut, and rank measures the complexity of the cut-formula. It uses Lemma ??, in which ?sub is instantiated to the immediate subformula property. which means,

strictly speaking, that so far as rank is concerned, the induction assumes only cut admissibility for cut-formula which are immediate subformulae

The two most difficult cases to consider correspond to when the cut-formula is principal below an application of the S4□ rule on the left, and also principal

13 in either the Refl or the S4□ rule on the right. As these are all modal rules, the Cut in question must be on a boxed formula, □A.

In the former case, the original Cut has form:

\begin{matrix}Π_{l} \\ Γ_{L}, □Γ_{L} ⊢ A \end{matrix} S4□ Σ, □Γ_{L} ⊢ Δ_{L}, □A

\begin{matrix}Π_{r} \\ A, □A, Γ_{R} ⊢ Δ_{R} \end{matrix} Refl □A, Γ_{R} ⊢ Δ_{R} Cut on □A Σ, □Γ_{L}, Γ_{R} ⊢ Δ_{L}, Δ_{R}

This is transformed as follows:

Π_{l} Γ_{L}, □Γ_{L} ⊢ A \begin{matrix}Π_{l} \\ Γ_{L}, □Γ_{L} ⊢ A \end{matrix} ; S4□ ; Σ, □Γ_{L} ⊢ Δ_{L}, □A  \begin{matrix}Π_{r} \\ A, □A, Γ_{R} ⊢ Δ_{R} \end{matrix} Cut on □A A, Σ, □Γ_{L}, Γ_{R} ⊢ Δ_{L}, Δ_{R} Cut on A Σ, Γ_{L}, □Γ_{L}, □Γ_{L}, Γ_{R} ⊢ Δ_{L}, Δ_{R} Contraction-admissibility Σ, Γ_{L}, □Γ_{L}, Γ_{R} ⊢ Δ_{L}, Δ_{R} Refl Σ, □Γ_{L}, Γ_{R} ⊢ Δ_{L}, Δ_{R}

Importantly, the new Cut on □A has lower level, and the Cut on A is of smaller rank. Thus both can be eliminated by the induction hypotheses.

For the latter case, when S4□ is principal on both sides, the original Cut has form:

\begin{matrix}Π_{l} \\ Γ_{L}, □Γ_{L} ⊢ A \end{matrix} ; S4□ ; Σ_{L}, □Γ_{L} ⊢ Δ_{L}, □A \begin{matrix}Π_{r} \\ A, □A, Γ_{R}, □Γ_{R} ⊢ B \end{matrix} ; S4□ ; □A, Σ_{R}, □Γ_{R} ⊢ □B, Δ_{R} Cut on □A Σ_{L}, Σ_{R}, □Γ_{L}, □Γ_{R} ⊢ □B, Δ_{L}, Δ_{R}

The normal process of reducing Cut level would apply Cut on the left cutsequent and the premise of the right cut-sequent, as follows:

\begin{matrix}Π_{l} \\ Γ_{L}, □Γ_{L} ⊢ A \end{matrix} ; S4□ ; Σ_{L}, □Γ_{L} ⊢ Δ_{L}, □A  \begin{matrix}Π_{r} \\ A, □A, Γ_{R}, □Γ_{R} ⊢ B \end{matrix} Cut on □A A, Σ_{L}, □Γ_{L}, Γ_{R}, □Γ_{R} ⊢ B, Δ_{L}

Unfortunately, this results in a deduction where we can no longer recover the □B present in the conclusion of the original Cut. The nature of the calculus and the S4□ rule means that new box formulae cannot be introduced in any succedent which contains some context Δ (or where there are additional formula Σ in the antecedent). As stated earlier, this case is omitted in the cut-elimination theorem of Troesltra and Schwichtenberg [?].

To overcome this issue, without introducing the complications and new branching rule in the solution of Goubault [?], we modify the original derivation of the left premise, to produce one of equal height upon which we can still apply the induction hypothesis on level. The new application of the S4□ rule differs from the original by simply not adding any context in the conclusion. Formally, the Σ and Δ of the generic S4□ rule in Figure 1 are ∅ in the new S4□ instance below:

Π_{l} Γ_{L}, □Γ_{L} ⊢ A \begin{matrix}Π_{l} \\ Γ_{L}, □Γ_{L} ⊢ A \end{matrix} ; S4□ (new) ; □Γ_{L} ⊢ □A  \begin{matrix}Π_{r} \\ A, □A, Γ_{R}, □Γ_{R} ⊢ B \end{matrix} Cut on □A A, □Γ_{L}, Γ_{R}, □Γ_{R} ⊢ B Cut on A Γ_{L}, □Γ_{L}, □Γ_{L}, Γ_{R}, □Γ_{R} ⊢ B Contraction-admissibility Γ_{L}, □Γ_{L}, Γ_{R}, □Γ_{R} ⊢ B S4□ Σ_{L}, Σ_{R}, □Γ_{L}, □Γ_{R} ⊢ □B, Δ_{L}, Δ_{R}

In the formalised proof, this instance is the only case where the inductive principle Lemma ?? is actually required. As the combined height of the derivations leading to □Γ_{L} ⊢ □A and A, □A, Γ_{R}, □Γ_{R} ⊢ B is lower than the level of the original Cut, the induction hypothesis on level can be applied. In all the other cases Theorem ?? would have sufficed. So in fact in all the other cases the property we prove is gen step2sr ... and we use Lemma 12.8 to link it to the required property sumh step2 tr .... Q.E.D.

13 Weakening, Contraction and Cut Admissibility for S4.3

There exists a syntactic pen and paper proof for S4.3 in the literature [?], however the calculus involved contains Weakening and Contraction as explicit rules, and mix-elimination is proved rather than cut. There also exist published semantic proofs of closure under Cut for both sequent and hypersequent calculi for S4.3 [?, ?]. But, there are no syntactic pen and paper proofs of cut-admissibility in the literature, nor any machine checked proofs.

To our knowledge, there are also no published papers for S4.3 explicitly providing a sequent calculus containing only logical rules and proving cutelimination. The labelled calculi of Negri [?] and Castellini [?] are perhaps the closest representatives in the literature. As noted previously, while these calculi do not use Weakening or Contraction, they explicitly include the semantics of the logic in the calculi, along with corresponding operations on world accessibility rather than logical operators.

13.1 Calculus for S4.3

The rules of the sequent calculus for S4.3 are listed in Figure 3. The calculus is based on the version of Goré [?], but with Weakening absorbed into the modal rules. Note, in the S4.3□ rule of Figure 3, that Φ⃗ = {φ_{1}, …, φ_{n}} and Φ⃗_{−i} = {φ_{1}, …, φ_{i−1}, φ_{i+1}, …, φ_{n}} for 1 ≤ i ≤ n.

From the perspective of backward proof search, the S4.3□ rule can be thought of as producing a new premise for all boxed formula in its conclusion, each of these formula being un-boxed separately in its own premise. Thus the general statement of the rule contains an indeterminate number of premises, one is necessary for each φ_{i} ∈ Φ⃗. For the sake of simplicity and clarity, at times only one of these premises will be shown as a representative for all n premises. That is, Zero Premise Rule

\begin{aligned}id \\ & Γ, φ ⊢ φ, Δ \end{aligned}

Classical rules

\begin{aligned}& Γ, φ, ψ ⊢ Δ \\ L∧ \\ & Γ, φ ∧ ψ ⊢ Δ \end{aligned}  \begin{aligned}Γ ⊢ φ, Δ & Γ ⊢ ψ, Δ \\ R∧ \\ & Γ ⊢ φ ∧ ψ, Δ \end{aligned}
\begin{aligned}Γ, φ ⊢ Δ & Γ, ψ ⊢ Δ \\ L∨ \\ & Γ, φ ∨ ψ ⊢ Δ \end{aligned} \begin{aligned}& Γ ⊢ φ, ψ, Δ \\ R∨ \\ & Γ ⊢ φ ∨ ψ, Δ \end{aligned}
\begin{aligned}Γ ⊢ φ, Δ & Γ, ψ ⊢ Δ \\ L→ \\ & Γ, φ → ψ ⊢ Δ \end{aligned} \begin{aligned}& Γ, φ ⊢ ψ, Δ \\ R→ \\ & Γ ⊢ φ → ψ, Δ \end{aligned}
\begin{aligned}& Γ ⊢ φ, Δ \\ L¬ \\ & Γ, ¬φ ⊢ Δ \end{aligned}  \begin{aligned}& Γ, φ ⊢ Δ \\ R¬ \\ & Γ ⊢ ¬φ, Δ \end{aligned}

Modal rules

\begin{aligned}& Γ, φ, □φ ⊢ Δ \\ Refl \\ & Γ, □φ ⊢ Δ \end{aligned}

Γ, □Γ ⊢ φ_{1}, □Φ⃗_{−1} ⋯ Γ, □Γ ⊢ φ_{i}, □Φ⃗_{−i} ⋯ Γ, □Γ ⊢ φ_{n}, □Φ⃗_{−n} S4.3□ Σ, □Γ ⊢ □Φ⃗, Δ

Fig. 3: Sequent calculus for S4.3.

the rule will be represented in the following form shown below at left:

Γ, □Γ ⊢ φ_{i}, □Φ⃗_{−i} S4.3□ Σ, □Γ ⊢ □Φ⃗, Δ Γ, □Γ ⊢ φ_{i}, □Φ⃗_{−i} S4.3□  ∀ψ.□ψ ∉ Σ ∪ Δ

Σ, □Γ ⊢ □Φ⃗, Δ

There are two different versions of the S4.3□ rule. Either the context (Σ and Δ) can contain any formulae, as shown above left, or they cannot include toplevel boxed-formulae, as shown above right. In the latter case, the □Γ and □Φ⃗ in the conclusion of the S4.3□ rule must correspond to exactly all the top-level boxed formulae within that sequent. The two versions of the calculus are in fact equivalent, following a proof of the admissibility of Weakening for the latter; however, for efficient backward proof search, the version above right is preferred as it is invertible and hence does not require backtracking during proof search.

Henceforth, Σ and Δ within the S4.3□ rule will be restricted from containing the □ operator at the top-level. In Isabelle, this is implemented by creating a new type of formula, based on the default formula type. HOL’s typedef allows a concise method of declaring new types as a subset of an existing type:

    typedef nboxfml =
        "{f::formula. ALL (a::formula). f ~= FC ''Box'' [a]}"

The Isabelle formalisation of the overall calculus is based on the calculus for S4 given in Figure 1. The only change is in the S4.3□ rule, which requires the mapping function nboxseq to create a new premise for each individual boxed formula in the succedent. The code for this is given in Figure 4.

(* Functions to unbox one formula for each premise *)
consts
  ithprem :: "formula multiset => formula list => formula
               => formula sequent"
  nprems  :: "formula multiset => formula list
               => formula sequent list"
(* The boxes in the succedent are treated as a list As.
   "ms_of_list (remove1 Ai As)" is the multiset consisting of
    all elements in "As", with one copy of "Ai" removed. *)
defs
  ithprem_def : "ithprem Gamma As Ai ==
        mset_map Box Gamma + Gamma |-
        {#Ai#} + mset_map Box (ms_of_list (remove1 Ai As))"
  nprems_def : "nprems Gamma As == map (ithprem Gamma As) As"
consts
  gs43_rls :: "formula sequent psc set"
    s43box :: "formula sequent psc set"
(* The S4.3 box rule *)
inductive "s43box" intros
    I : "(nprems gamma As, mset_map Box gamma |-
         mset_map Box (ms_of_list As)) : s43box"
(* The S4.3 calculus as an extension of the LK calculus *)
inductive "gs43_rls" intros
    lksI  : "psc : lksss ==> psc : gs43_rls"
    reflI : "psc : lkrefl ==>
                          pscmap (extend flr) psc : gs43_rls"
    (* boxI allows extra formulae in conclusion only *)
    boxI  : "(p, c) : lkbox ==>
                       (p, extend (nboxseq flr) c) : gs43_rls"

Fig. 4: S4.3 calculus as encoded in Isabelle

13.2 Weakening for S4.3

As the S4.3□ rule does not allow arbitrary contexts, weakening-admissibility must be proved by induction, in this case on both height and rank (of the implicit derivation tree, ie, using Lemma ??). In order to simplify the case for the S4.3□ rule and its multiple premises, weakening-admissibility is proven for the antecedent and succedent separately, and only considering a single formula at a time. The Isabelle encodings for these properties are given below. The induction itself proceeds on the height of the derivation, as well as a sub-induction on the rank of the formula A being inserted into the conclusion.

Definition 13.1:

wk adm single antec rls means:

For any rls-derivable sequent S, and any single formulae A,

     if S ∈ derrec rls {} then S+({#A#} |- {#}) ∈ derrec rls {}.
wk adm single succ rls means:

For any rls-derivable sequent S, and any single formulae A,

     if S ∈ derrec rls {} then S+({#} |- {#A#}) ∈ derrec rls {}.
Lemma 13.1 (wk adm sides): If wk adm single antec and wk adm single succ

both hold for a set of rules rls, then so does wk adm.

Proof: By multiset induction, repeatedly applying the results for single formulae. Q.E.D.

Theorem 13.1 (gs43 wk adm): Weakening is admissible for the calculus gs43 rls.

Proof:

In the case of the S4.3□ rule, if A is not boxed, then it is allowed to be contained in the context of the rule’s conclusion. The derivability of the original premises, followed by an application of a new S4.3□ rule including A as part of its context, then gives the required sequent. The difficulty arises when A is a boxed formula, say A = □B. For the sake of clarity, the representation of the original sequent can be split into its boxed and non-boxed components, so the original derivation is: Was Φ⃗_{−i} in

succedent of premiss.

\begin{matrix}Π \\ Γ, □Γ ⊢ φ_{i}, □Φ⃗_{−i} \end{matrix} S4.3□ Σ, □Γ ⊢ □Φ⃗, Δ

When A is to be added to the antecedent, the induction on height can be used to add A = □B to each of the original premises. Following this by an application of the sub-induction on formula rank, allows the addition of B, giving the derivability of B, □B, Γ, □Γ ⊢ φ_{i}, □Φ⃗_{−i}. An application of the S4.3□ rule then completes the case:

B, □B, Γ, □Γ ⊢ φ_{i}, □Φ⃗_{−i} S4.3□ □B, Σ, □Γ ⊢ □Φ⃗, Δ

The final case to consider is that of adding A = □B to the succedent. The goal once again is to use the S4.3□ rule to give the desired conclusion. From the original premises, the induction hypothesis on height (inserting □B) gives the derivability of Γ, □Γ ⊢ φ_{i}, □Φ⃗_{−i}, □B. A different application of the S4.3□ rule, bringing in empty contexts, on the original premises also gives the derivability of □Γ ⊢ □Φ⃗. Applying the induction on formula rank then shows that □Γ ⊢ B, □Φ⃗ is derivable.

At this point, the derivability of all necessary premises for a new S4.3□ rule has been proven. These are sequents of the form Γ, □Γ ⊢ φ′_{i}, □Φ⃗′_{−i} where Φ⃗′ = Φ⃗, B. The final rule application is then:

Γ, □Γ ⊢ φ′_{i}, □Φ⃗′_{−i}

S4.3□ Σ, □Γ ⊢ □Φ⃗, □B, Δ

Q.E.D.

13.3 Invertibility and Contraction for S4.3

As for S4, we prove inversion lemmas for the G3cp and Refl rules within the overall calculus.

Theorem 13.2 (inv rl gs43 refl and inv rl gs43 lks): Refl (lkrefl) and all

Classical rules (lksss) are invertible within the calculus gs43 rls.

Proof: Since the inverse of the Refl rule is an instance of weakening, which we have shown is admissible, the only notable case occurs for the G3cp rules, where the last rule applied in the original derivation is S4.3□. The proof uses the induction principle of Lemma 12.5. If the original derivation is given by

\begin{matrix}Π \\ Γ, □Γ ⊢ φ_{i}, □Φ⃗_{−i} \end{matrix} S4.3□ Σ, □Γ ⊢ □Φ⃗, Δ

then proving invertibility for G3cp requires showing the derivability of all premises after applying a G3cp rule backwards from the endsequent of the S4.3□ rule. As the classical rules do not operate on boxed formulae, the rule can only modify Σ or Δ:

Σ′, □Γ ⊢ □Φ⃗, Δ′

G3cp rule

Σ, □Γ ⊢ □Φ⃗, Δ

Clarifying again, invertibility of the G3cp rule requires deriving Σ′, □Γ ⊢ □Φ⃗, Δ′. The usual tactic would apply another instance of the S4.3□ rule to the original premises, but bringing in a different context. However, this does not admit a proof if there are boxed formula in Σ′ or Δ′. For example, if the G3cp rule is L∧ and the principal formula is A∧□B then Σ′ contains a boxed formula, □B, which cannot be introduced within the (box-free) context of a new S4.3□ rule application.

To accommodate this case, the premises of the modal rule are used to derive the conclusion without any context. Then weakening-admissibility is used to bring the remaining formulae in the premise of the G3cp rule:

\begin{matrix}Π \\ Γ, □Γ ⊢ φ_{i}, □Φ⃗_{−i} \end{matrix}
S4.3□
□Γ ⊢ □Φ⃗

Weakening-admissibility

Σ′, □Γ ⊢ □Φ⃗, Δ′

Q.E.D.

For S4, proving invertibility is sufficient to lead to a contraction-admissibility proof. However, using invertibility alone does not allow an obvious transformation when dealing with the S4.3□ rule. In order to prove contractionadmissibility, we first require the following lemma:

TODO: possibly change the statement of this lemma?

Lemma 13.2 (gs43 refl): The rule R-refl is admissible in gs43 rls.

Γ ⊢ Δ, □A ; R-refl ; Γ ⊢ Δ, A

The corresponding statement of the lemma in Isabelle states that if a sequent seq is derivable in gs43 rls and the sequent is equivalent to X ⊢ Y, □A for any X and Y, then X ⊢ Y, A is also derivable.

Proof: By an induction on the structure of the (implicit) derivation tree, using the derrec-induction principle, Lemma ??. The analysis is on the last rule applied in deriving Γ ⊢ Δ, □A.

Case 1. The last rule applied was id. If □A is parametric then Γ ⊢ Δ is an axiom, and the conclusion will be also. If □A is principal, then Γ = {□A} ∪ Γ′ and the following transformation is applied:

\begin{aligned}id \\ & A, □A, Γ′ ⊢ Δ, A \end{aligned} Refl □A, Γ′ ⊢ Δ, A

Case 2. The last rule applied was from G3cp. No rules in G3cp operate on a boxed formula, so □A must be parametric. The induction hypothesis on height can thus be applied to the premise of the G3cp rule. Applying the original G3cp on the resulting sequent gives the desired conclusion.

Case 3. The last rule applied was Refl. As in Case 2, □A must be parametric, as Refl only operates on boxed formula in the antecedent.

Case 4. The last rule applied was S4.3□. Then one premise of the original deduction un-boxes □A. Using Refl followed by weakening-admissibility on this premise is enough to produce the conclusion. For clarity, here we express Γ = Σ ∪ □Γ′ and Δ = □Φ⃗ ∪ Δ′. The original derivation is:

\begin{matrix}Π_{1} \\ Γ′, □Γ′ ⊢ □Φ⃗, A \end{matrix}  \begin{matrix}Π_{2} \\ Γ′, □Γ′ ⊢ φ_{i}, □Φ⃗_{−i}, □A \end{matrix}
Σ, □Γ′ ⊢ □Φ⃗, Δ′, □A

This is transformed into:

\begin{matrix}Π_{1} \\ Γ′, □Γ′ ⊢ □Φ⃗, A \end{matrix}

Refl

□Γ′ ⊢ □Φ⃗, A

Weakening-admissibility

Σ, □Γ′ ⊢ □Φ⃗, Δ′, A

Q.E.D.

Theorem 13.3 (gs43 ctr adm): Contraction is admissible in gs43 rls.

Proof: This proof uses the induction principle Lemma ??, for implicit derivation trees. If the last rule used in the derivation was the S4.3□ rule, there are two cases to consider. The case where the contraction-formula is parametric is handled by simply re-applying another instance of the S4.3□ rule like the S4 case. Similarly, when the contraction-formula is principal in the antecedent, then the proof proceeds like in S4. Specifically, one copy of □A from Σ, □A, □A, □Γ ⊢ □Φ⃗, Δ must be removed. The original derivation is:

\begin{matrix}Π \\ A, A, □A, □A, Γ, □Γ ⊢ φ_{i}, □Φ⃗_{−i} \end{matrix} S4.3□ Σ, □A, □A, □Γ ⊢ □Φ⃗, Δ

By contracting twice using first the induction hypothesis on height, then the induction hypothesis on rank, on all premises followed by an application of the S4.3□ rule, the desired endsequent is obtained:

\begin{matrix}Π \\ A, A, □A, □A, Γ, □Γ ⊢ φ_{i}, □Φ⃗_{−i} \end{matrix} IH on height

A, A, □A, Γ, □Γ ⊢ φ_{i}, □Φ⃗_{−i} IH on rank A, □A, Γ, □Γ ⊢ φ_{i}, □Φ⃗_{−i} S4.3□ Σ, □A, □Γ ⊢ □Φ⃗, Δ

When the contraction-formula is principal in the succedent, then there are two cases of the premises to consider. Either a premise “un-boxes” one of the contraction-formulae ^{1}, or it leaves both boxed. The original deduction is given by:

1 Technically, there are two syntactically identical premises which individually un-box one of the two copies of □A

\begin{matrix}Π_{1} \\ Γ, □Γ ⊢ □Φ⃗, A, □A \end{matrix}  \begin{matrix}Π_{2} \\ Γ, □Γ ⊢ φ_{i}, □Φ⃗_{−i}, □A, □A \end{matrix}
Σ, □Γ ⊢ □Φ⃗, □A, □A, Δ

In the latter case, the induction hypothesis can be directly applied, removing one copy of the boxed formulae:

\begin{matrix}Π_{2} \\ Γ, □Γ ⊢ φ_{i}, □Φ⃗_{−i}, □A, □A \end{matrix} IH on height

Γ, □Γ ⊢ φ_{i}, □Φ⃗_{−i}, □A

In the former case, the original derivation is:

\begin{matrix}Π_{1} \\ Γ, □Γ ⊢ □Φ⃗, A, □A \end{matrix}  \begin{matrix}Π_{2} \\ Γ, □Γ ⊢ φ_{i}, □Φ⃗_{−i}, □A, □A \end{matrix}
Σ, □Γ ⊢ □Φ⃗, □A, □A, Δ

For this sub-case, we use the above Lemma 13.2 to produce the following transformation:

\begin{matrix}Π_{1} \\ Γ, □Γ ⊢ □Φ⃗, A, □A \end{matrix} R-refl Γ, □Γ ⊢ □Φ⃗, A, A IH on rank Γ, □Γ ⊢ □Φ⃗, A

\begin{matrix}Π_{2} \\ Γ, □Γ ⊢ φ_{i}, □Φ⃗_{−i}, □A, □A \end{matrix} IH on height

Γ, □Γ ⊢ φ_{i}, □Φ⃗_{−i}, □A S4.3□ Σ, □Γ ⊢ □Φ⃗, □A, Δ

Q.E.D.

13.4 Cut-admissibility for S4.3

Theorem 13.4 (gs43 cas): Cut is admissible in the calculus gs43 Rls.

Proof: As with Theorem 12.3, we use the induction principle of Lemma ??, involving induction on the sums of heights of two explicit trees, although for the majority of cases the simpler principle Theorem ?? would suffice. So again, in those cases, we prove gen step2sr ... and we use Lemma 12.8 to link it to the required property sumh step2 tr ...

When S4.3□ leads to the left cut-sequent, and the Refl rule is used on the right, the transformation mimics the corresponding case for S4. However, for the case where S4.3□ principal is principal on both sides requires a new transformation. For clarity, the premises above the S4.3□ rule on the left are given as two cases, depending on whether the cut-formula is un-boxed or not. The boxed formula in the succedents of the premises are also distinguished by the superscripts L and R for left and right cut premises respectively. Explicitly, these are Φ⃗^{L} = {φ_{1}^{L} … φ_{i}^{L} … φ_{n}^{L}} and Φ⃗^{R} = {ψ_{1}^{R} … ψ_{k}^{R} … ψ_{m}^{R}}. The original cut thus has form:

\begin{matrix}Π_{L}^{a} \\ Γ_{L}, □Γ_{L} ⊢ φ_{i}^{L}, □Φ⃗_{−i}^{L}, □A \end{matrix}  \begin{matrix}Π_{L}^{b} \\ Γ_{L}, □Γ_{L} ⊢ A, □Φ⃗^{L} \end{matrix}

S4.3□

Σ_{L}, □Γ_{L} ⊢ □Φ⃗^{L}, Δ_{L}, □A

\begin{matrix}Π_{R} \\ A, □A, Γ_{R}, □Γ_{R} ⊢ ψ_{k}^{R}, □Φ⃗_{−k}^{R} \end{matrix}

S4.3□

□A, Σ_{R}, □Γ_{R} ⊢ □Φ⃗^{R}, Δ_{R} Cut on □A

Σ_{L}, Σ_{R}, □Γ_{L}, □Γ_{R} ⊢ □Φ⃗^{L}, □Φ⃗^{R}, Δ_{L}, Δ_{R}

To remove this cut, the derivation is transformed into one where the principal rule (S4.3□) is applied last to produce the desired endsequent. The problem is then proving that the premises of the following S4.3□ rule application are derivable. This in itself requires two different transformations of the original derivation, depending on the two forms that the premises can take; either the un-boxed formula in the succedent originated from the left cut premise, that is from □Φ⃗^{L}, or from the right, within □Φ⃗^{R}. These cases are named P_{L} and P_{R} respectively. The final S4.3□ rule used in our new transformation is then:

\begin{matrix}P_{L} \\ Γ_{L}, □Γ_{L}, Γ_{R}, □Γ_{R} ⊢ φ_{i}^{L}, □Φ⃗_{−i}^{L}, □Φ⃗^{R} \end{matrix}  \begin{matrix}P_{R} \\ Γ_{L}, □Γ_{L}, Γ_{R}, □Γ_{R} ⊢ □Φ⃗^{L}, ψ_{k}^{R}, □Φ⃗_{−k}^{R} \end{matrix}

S4.3□ Σ_{L}, Σ_{R}, □Γ_{L}, □Γ_{R} ⊢ □Φ⃗^{L}, □Φ⃗^{R}, Δ_{L}, Δ_{R}

For both transformations, the same idea behind the principal S4□ rule case is used. We first derive the original cut-sequents but without their original contexts. These new sequents will be called D_{L} and D_{R} respectively. These are derived using the derivations in the original cut, but applying new instances of the S4.3□ rule. Importantly, the derivations of the new sequents D_{L} and D_{R} have the same height as the original cut-sequents. This is the case where the induction principle of Lemma ?? is required.

\begin{matrix}Π_{L}^{a} \\ Γ_{L}, □Γ_{L} ⊢ φ_{i}^{L}, □Φ⃗_{−i}^{L}, □A \end{matrix}  \begin{matrix}Π_{L}^{b} \\ Γ_{L}, □Γ_{L} ⊢ A, □Φ⃗^{L} \end{matrix}

S4.3□ D_{L} = □Γ_{L} ⊢ □Φ⃗^{L}, □A

\begin{matrix}Π_{R} \\ A, □A, Γ_{R}, □Γ_{R} ⊢ ψ_{k}^{R}, □Φ⃗_{−k}^{R} \end{matrix}

S4.3□ D_{R} = □A, □Γ_{R} ⊢ □Φ⃗^{R}

Having introduced all the necessary notation and pre-requisites, the first actual case to consider is deriving P_{L}. The induction on level allows D_{R} to be cut, on cut-formula □A, with all of the sequents given by the derivation Π_{L}^{a} above the original left S4.3□ rule. The transformation performs n cuts, for all premises corresponding to the formulae in Φ⃗^{L}. The results of this cut then match exactly with P_{L} after using the admissibility of Weakening to introduce the formulae of Γ_{R} in the antecedent.

\begin{matrix}Π_{L}^{a} \\ Γ_{L}, □Γ_{L} ⊢ φ_{i}^{L}, □Φ⃗_{−i}^{L}, □A \end{matrix}  \begin{matrix}D_{R} \\ □A, □Γ_{R} ⊢ □Φ⃗^{R} \end{matrix}

Cut on □A

Γ_{L}, □Γ_{L}, □Γ_{R} ⊢ φ_{i}^{L}, □Φ⃗_{−i}^{L}, □Φ⃗^{R}

Weakening-admissibility

P_{L} = Γ_{L}, □Γ_{L}, Γ_{R}, □Γ_{R} ⊢ φ_{i}^{L}, □Φ⃗_{−i}^{L}, □Φ⃗^{R}

To derive the sequents in P_{R}, the induction hypothesis on level is used to cut D_{L} with all of the premises above the right S4.3□ in the original cut, with cutformula □A. The induction on formula rank on A is then used to cut the sequent resulting from Π_{L}^{b} with all these new sequents. Finally, contraction-admissibility allows the removal of the extra copies of □Γ and □Φ⃗^{L}, and concludes the case.

Π_{L}^{b} Γ_{L}, □Γ_{L} ⊢ A, □Φ⃗^{L} \begin{matrix}D_{L} \\ □Γ_{L} ⊢ □Φ⃗^{L}, □A \end{matrix}  \begin{matrix}Π_{R} \\ A, □A, Γ_{R}, □Γ_{R} ⊢ ψ_{k}^{R}, □Φ⃗_{−k}^{R} \end{matrix}

Cut on □A □Γ_{L}, A, Γ_{R}, □Γ_{R} ⊢ □Φ⃗^{L}, ψ_{k}^{R}, □Φ⃗_{−k}^{R}

Cut on A

Γ_{L}, □Γ_{L}, □Γ_{L}, Γ_{R}, □Γ_{R} ⊢ □Φ⃗^{L}, □Φ⃗^{L}, ψ_{k}^{R}, □Φ⃗_{−k}^{R}

Contraction-admissibility

P_{R} = Γ_{L}, □Γ_{L}, Γ_{R}, □Γ_{R} ⊢ □Φ⃗^{L}, ψ_{k}^{R}, □Φ⃗_{−k}^{R}

To conclude, the transformations above derive P_{L} and P_{R} while reducing cut-level or cut-rank. These are the premises of an instance of the S4.3□ rule which results in the conclusion of the original cut. This completes the cutadmissibility proof.

Q.E.D.

14 The system GTD

This section describes Isabelle proofs of the cut admissibility of the logic GTD described in [?] Axiomatically, GTD is K with the additional axiom □A ⇔ □□A. The sequent inference rules involving □, allowing arbitrary context inthe conclusion so as to make weakening admissible, are shown below:

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

The above two rules are encoded as GTD shown below by factoring out the form of A as either B or as □B:

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

14.1 Calculus for GTD

We now look at proving cut admissibility for a version of GTD without structural rules, where the box rules have their conclusions (only) extended with an arbitrary context, which permits weakening to be admissible.

We define the rules of the system as follows. The rules used for classical logic (before extending them with a context) form the set lksne where the rule sets idrls, lksil and lksir are the axioms and the left and right logical introduction rules: see Figure 1. JED please

check verbatim code!

Definition 14.1 (lkssx): Given, a rule set xrls, every rule of xrls is in the rule set lkssx xrls, and every rule psc in rule set lknse gives a rule in lkssx xrls obtained by uniformly extending both the premise and conclusion of psc with an arbitrary context (sequent) flr:

inductive "lkssx xrls" intros
      x : "psc : xrls ==> psc : lkssx xrls"
   extI : "psc : lksne ==> pscmap (extend flr) psc : lkssx xrls"

Definition 14.2 (extcs): Given a rule set rules, the rule set extcs rules is obtained by extending only the conclusion c of each rule (ps, c) in rules by an arbitrary context (sequent) flr (while leaving the premises unchanged):

inductive "extcs rules" intros
    I : "(ps, c) : rules ==> (ps, extend flr c) : extcs rules"

The rule set for the logic GTD is obtained by extending only the conclusion of the rule GTD and by extending every rule of lknse, giving the rule set lkssx

(extcs GTD).

14.2 Weakening-admissibility for GTD

First we prove weakening admissibility. We use a lemma which allows us to apply Lemma 12.1.

Lemma 14.1: For any rule sets rls and rlsa

 (a) extrs rlsa ∪ extcs rls satisfies ext concl

(b) extrs rlsa ∪ extcs rls satisfies weakening admissibility

Proof: The first part is easy, and the second follows using Lemma 12.1. Q.E.D.

extrs_cs_ext_concl: "ext_concl (extrs ?rlsa Un extcs ?rls)"
wk_adm_extrs_cs: "wk_adm (extrs ?rlsa Un extcs ?rls)"

Corollary 14.1: GTD satisfies weakening admissibility.

Proof: Since the rule set for GTD, lkssx (extcs GTD), is also equal to extrs lksne ∪ extcs GTD, the result follows from Lemma 14.1. Q.E.D.

wk_adm_lkssx_cs: "wk_adm (lkssx (extcs ?xrls))"

14.3 Inversion and Contraction-admissibility for GTD

For contraction admissibility, first we need to prove invertibility of the logical rules. The general method for doing this is that described in §12.3.

Recall the predicate inv stepm, which is used in an inductive proof of invertibility, and that its three arguments are

• first, the set of derivation rules with respect to which the invertibility (a case of admissibility) is defined,

• second, the set of rules whose invertibility is being considered (the inversion rules)

• third, the final rule of a derivation — since we are talking about proving the invertibility result by induction on the derivation, so the inductive hypothesis is that the invertibility result applies to the premises of this final rule

Recall that inv stepm (although not inv step) is monotonic in the derivation rules argument, see Lemma 12.3.

For the second argument the following property holds:

Lemma 14.2: For a given set of derivation rules drls and a given final rule psc, if inv stepm applies for inversion rule sets irlsa and irlsb, then it applies for

irlsa ∪ irlsb.
inv_stepm_Un:
   "[| inv_stepm ?drls ?irlsa ?psc; inv_stepm ?drls ?irlsb ?psc |]
         ==> inv_stepm ?drls (?irlsa Un ?irlsb) ?psc"

So far as the third argument is concerned, the requirement to prove a rule is invertible is simply that inv stepm ... applies for all cases of the third argument (see Lemmas 12.5 and 12.4): thus the lemmas we use are expressed to apply to single cases of the third argument.

We now describe the lemmas used as building-blocks for the required invertibility result.

Lemma 14.3: (a) inv stepm ... applies where the derivation rules and the set of rules to be inverted are the classical logical rules extrs lksne, and the final rule is any one of those rules

(b) where the set of inversion rules is the set of extensions of a single skeleton whose conclusion is ic, and the set of derivation rules is the set of extensions of a single skeleton rule whose conclusion is c, and ic and c are disjoint (ie, have no formula in common on the same side of the turnstile), and the final rule is one of those derivation rules, then inv stepm ... applies

(c) as for (b), except that the set of derivation rules is the set of extensions in the conclusion only (using extcs) of the single skeleton (d) where the set of inversion rules and the set of derivation rules are each

the set of extensions of a single skeleton rule whose conclusion has a single formula, and if those two skeletons’ conclusions are equal then the two skeletons are equal, then inv stepm ... applies

lks_inv_stepm:
  "?psc : extrs lksne ==> inv_stepm (extrs lksne) (extrs lksne) ?psc"
inv_stepm_disj:
   "[| seq_meet ?c ?ic = 0; extrs {(?ps, ?c)} = ?rls; ?rl : ?rls |] ==>
   inv_stepm ?rls (extrs {(?ips, ?ic)}) ?rl"
inv_stepm_disj_cs:
  "[| seq_meet ?c ?ic = 0; extcs {(?ps, ?c)} = ?rls; ?rl : ?rls |] ==>
  inv_stepm ?rls (extrs {(?ips, ?ic)}) ?rl"
inv_stepm_scrls:
   "[| extrs {?srl} = ?rls; ?rl : ?rls; ?srl : scrls; ?irl : scrls;
        snd ?srl = snd ?irl --> ?srl = ?irl |] ==>
    inv_stepm ?rls (extrs {?irl}) ?rl"

Parts (b) and (c) (inv stepm disj and inv stepm disj cs) are for the case where the formula to be inverted is in the context of the conclusion of the last rule of the derivation: the first premise gives you that the formula to be inverted is not the principal formula of the rule, though it is expressed in a way which is relevant to a case where the rules in question have more than just one principal formula.

Part (d) (inv stepm scrls) (whose proof uses part (b)) uses the fact that for each formula there is a unique introduction rule, so an inversion step is either parametric or gives you the premise(s) of the last rule applied.

Lemma 14.4: Every rule of lksss is invertible in the calculus for GTD.

gtdns_inv_rl: "Ball (extrs lksne) (inv_rl (lkssx (extcs GTD)))"

Proof: This uses Lemmas 12.5, 12.4 and 14.3. Q.E.D.

Then, to prove contraction admissibility, we follow an approach very similar to §12.3. For the rules (□ ⊢) and (⊢ □), the proof for the cases where either of these is the final rule is just the same as for the S4□ rule in §12.3.

Thus we get the result

Lemma 14.5: Contraction is admissible in GTD.

gtdns_ctr_adm: "ctr_adm (lkssx (extcs GTD)) ?A"

14.4 Cut-admissibility for GTD

Now, for cut admissibility: the difficult cases are where the last rule on both sides is one of the two box rules (⊢ □) and (□ ⊢).

Since the proof is effectively the same whichever of these two rules is on the right, we define s4g such that

• s4g (λB. {B, □B}) is all instances of either (⊢ □) or (□ ⊢),

• s4g (λB. {B}) is all instances of (⊢ □), and

• s4g (λB. {□B}) is all instances of (□ ⊢).

\frac{□Γ, Γ ⊢ B}{Σ, □Γ ⊢ □B, Δ}(⊢ □) \frac{□Γ, Γ ⊢ □B}{Σ, □Γ ⊢ □B, Δ}(□ ⊢)

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

The case of the (⊢ □) rule on the left is dealt with in §12.4: depending on whether we have the rule (⊢ □) or (□ ⊢) on the right, we may need to change B to □B in the diagrams there.

For the case where we have the (□ ⊢) rule on the left, the proof is as in the following diagram, where B′ is B or □B.

\begin{matrix}Π_{l} \\ Γ_{L}, □Γ_{L} ⊢ □A \end{matrix} □ ⊢ Σ_{L}, □Γ_{L} ⊢ Δ_{L}, □A

\begin{matrix}Π_{r} \\ A, □A, Γ_{R}, □Γ_{R} ⊢ B′ \end{matrix} □ ⊢ or ⊢ □ □A, Σ_{R}, □Γ_{R} ⊢ □B, Δ_{R} Cut on □A Σ_{L}, Σ_{R}, □Γ_{L}, □Γ_{R} ⊢ □B, Δ_{L}, Δ_{R}

As in §12.4, we modify the original derivation of a premise, in this case the right premise, by simply not adding any context in the conclusion. This produces a derivation of equal height upon which we can still apply the induction hypothesis on level. Formally, the Σ and Δ of the generic box rule (⊢ □) or (□ ⊢). are ∅ in the new instance below:

Π_{l} Γ_{L}, □Γ_{L} ⊢ □A Π_{r} A, □A, Γ_{R}, □Γ_{R} ⊢ B′ □ ⊢ or ⊢ □ (new) □A, □Γ_{R} ⊢ □B Cut on □A Γ_{L}, □Γ_{L}, □Γ_{R} ⊢ □B Weakening-admissibility Γ_{L}, □Γ_{L}, Γ_{R}, □Γ_{R} ⊢ □B □ ⊢ Σ_{L}, Σ_{R}, □Γ_{L}, □Γ_{R} ⊢ □B, Δ_{L}, Δ_{R}

For the cut-elimination proof we also use results for the parametric cases, that is, where the cut-formula appears in the context of the last rule on either side above the cut. This includes cases where that rule is in extrs … (where the rule has a context which appears in premises and conclusion) and where that rule is in extcs … (where the rule has a context which appears only in the conclusion).

The following lemma is used for the common situation of a cut which is parametric with respect to the last rule of the left-hand derivation.

Lemma 14.6 (lcg gen step): Consider a set erls of derivation rules, for which weakening is admissible, and which contains all extensions a skeleton rule ρ whose conclusion is U ⊢ V. Consider two derivations of which the final rule of the left side is an extension of ρ. Then for a cut-formula A which is not contained in V, the inductive step condition gen step2 sr ... holds for the admissibility of a cut on A.

A similar lemma lcg gen steps extcs holds for the case where only extensions in the conclusion of ρ are contained in erls.

lcg_gen_step: "[| wk_adm ?erls; extrs {(?ps, ?U |- ?V)} <= ?erls; ~ ?A :# ?V;
  ?pscl = pscmap (extend (?W |- ?Z)) (?ps, ?U |- ?V) |] ==>
  gen_step2sr (prop2 car ?erls) ?A ?any ?erls (?pscl, ?pscr)"
lcg_gen_steps_extcs:
  "[| wk_adm ?rls; extcs {(?ps, ?c)} <= ?rls; ~ ?A :# succ ?c |] ==>
  gen_step2sr (prop2 car ?rls) ?A ?sub ?rls ((?ps, extend ?flr ?c), ?psr, ?cr)"

Finally we need to deal with the cases of matching instances of the usual logical introduction rules. Here we use a general result giving requirements for certain cases of the final rules on either side of a putative cut to satisfy the step condition for cut-admissibility.

It uses a property c8 ercas prop, which encodes the property that a cut which is principal (ie, the cut formula is introduced by a logical introduction rule in the final step) on both sides is reducible to cuts on sub-formulae. It is loosely defined as follows:

Definition 14.3 (c8 ercas prop): Given a set of derivation rules prls, a cutformula A, a subformula relation psubfml, and a set of skeleton rules (typically logical introduction rules) rls, c8 ercas prop psubfml prls A rls means: assuming that we have cut-admissibility for cut-formulae smaller than A, where two derivations have as their final sequents X_{l} ⊢ A, Y_{l} and X_{r}, A ⊢ Y_{r}, and on both sides the final rule introduces A using logical introduction rules in rls, then X_{l}, X_{r} ⊢ Y_{l}, Y_{r} is derivable, that is, the cut on A is admissible.

Of course whether c8 ercas prop holds depends on the specific set of logical rules in question. Beyond that, however, the following lemma is quite general.

Lemma 14.7: Given a set of derivation rules prls, a cut-formula A, and a subformula relation psubfml, if

• prls satisfy weakening admissibility • there is a set rls of skeleton rules all of whose extensions are contained

     in prls

• all rules in rls, other than axiom rules B ⊢ B, have a single formula in their conclusion

• the axiom rules are also in prls

   • prls and rls satisfy c8 ercas prop

• the final rules of two derivations are extensions of rules in rls

then the step condition gen step2sr for cut-admissibility for the two derivations is satisfied.

gs2sr_alle: "[| wk_adm ?prls; c8_ercas_prop ?psubfml ?prls ?A ?rls;
  ?rls <= iscrls; idrls <= ?prls; extrs ?rls <= ?prls;
  (?psa, ?ca) : extrs ?rls; (?psb, ?cb) : extrs ?rls |] ==>
  gen_step2sr (prop2 car ?prls) ?A ?psubfml ?prls ((?psa, ?ca), ?psb, ?cb)"

We apply this result to the logic GTD using first another general result

Lemma 14.8 (gen lksne c8): If a set of derivation rules drls satisfies weakening admissibility and contraction admissibility, and contains the extensions of the logical introduction rule skeletons lksne then the condition c8 ercas prop is satisfied (for the usual immediate proper subformula relation and for any cutformula).

gen_lksne_c8:
  "[| ALL A'. ctr_adm ?drls A' ; wk_adm ?drls; extrs lksne <= ?drls |]
         ==> c8_ercas_prop ipsubfml ?drls ?A lksne"

Corollary 14.2 (gtdns lksne c8): GTD satisfies c8 ercas prop in relation to the logical introduction rule skeletons lksne.

gtdns_lksne_c8: "c8_ercas_prop ipsubfml (lkssx (extcs GTD)) ?A lksne"

Finally we get the cut admissibility result:

Theorem 14.1 (gtdns casdt, gtdns cas): GTD satisfies cut-admissibility.

gtdns_casdt: "(?dt, ?dta) : casdt (lkssx (extcs GTD)) ?A"
gtdns_cas:
   "(?Xl |- mins ?A ?Yl, mins ?A ?Xr |- ?Yr) : cas (lkssx (extcs GTD)) ?A"

15 Dynamic Topological Logic 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 by Mints [?]

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

We use a version of the system without structural rules: we prove invertibility of the logical rules and contraction 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.

As we do not have the structural rules, we use a presentation of the system which

• allows an arbitrary context to be added to the conclusion (only) of the (⊢ □) and (∘) rules

• uses a version of the (□ ⊢) rule which includes the principal formula in the premise

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

15.1 Calculus for S4C

We now describe how we formalised the system. First we define the rules which can be extended by an arbitrary context in their premises and conclusion. Without the context, these rules form the set s4cnsne.

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

inductive "s4cnsne"
  intros
    id : "psc : idrls ==> psc : s4cnsne"
    circ_il : "rl : lksil ==> nkmap k rl : s4cnsne"
    circ_ir : "rl : lksir ==> nkmap k rl : s4cnsne"
    circ_T : "rl : lkrefl ==> nkmap k rl : s4cnsne"
inductive "lkrefl"
  intros
    I : "([{#A#} + {#Box A#} |- {#}], {#Box A#} |- {#}) : lkrefl"
defs
  nkmap_def : "nkmap k == pscmap (seqmap (funpow Circ k))"
inductive "s4cns"
  intros
    extI : "rl : s4cnsne ==> pscmap (extend (U |- V)) rl : s4cns"
    extcsI : "(ps, c) : circ Un s4cbox ==> (ps, extend (U |- V) c) : s4cns"
inductive "circ"
  intros
    I : "([seq], seqmap Circ seq) : circ"
inductive "s4cbox"
  intros
    boxI : "M : msboxfmls ==> ([M |- {#A#}], M |- {#Box A#}) : s4cbox"
inductive "msboxfmls"
  intros
    I : "ALL f. f :# M --> f : boxfmls ==> M : msboxfmls"
inductive "boxfmls"
  intros
    I : "funpow Circ k (Box B) : boxfmls"

We first need to prove admissibility of the structural rules, weakening and contraction. QUESTION - we did prove contraction admissibility, but is it essential?

15.2 Weakening for S4C

Weakening admissibility was straightforward using Lemma 12.1.

15.3 Inversion and Contraction-admissibility for S4C

Invertibility of the logical introduction rules was dealt with using multiple lemmas showing various cases of inv stepm, as described in §12.3: as noted there, a proof of invertibilty can be split up into

• the invertibility of various different rules

• cases of what the last rule in the derivation, from whose conclusion we wish to apply one of the inverted rules

As in §12.3, we make significant use of Lemma 12.3.

We then prove contraction admissibility. In part this also makes use of the general result

This uses predicates and results which are essentially Definition ?? and Lemma ??, but instantiated to apply to the property of contraction admissibility, giving the property ctr adm step and a lemma gen ctr adm step.

We now look at proving ctr adm step for each possible case for the last rule of a derivation.

Lemma 15.1: If

• rule set lrls consists of rules which are the identity (axiom) rules A ⊢ A, or are rules with a single formula in their conclusion,

• all rule in lrls have the “subformula” property (which here means that for every premise other than a premise which contains the conclusion, every formula in that premise is a subformula of a formula in the conclusion

• the rule set drls (derivation rules) contains the extensions of lrls

• in regard to the derivation rules drls, the inverses of extensions of lrls are admissible

• rule (ps, c) is an extension of a rule of lrls

then the contraction admissibility step ctr adm step holds for the final rule (ps, c) and the derivation rule set drls.

So the conclusion of this lemma means: assuming that

• contraction on formulae A′ smaller than A is admissible, and

• contraction on A is admissible in the sequents ps

then contraction on A in sequent c is admissible.

gen_ctr_adm_step_inv:
   "[| ?epsc : extrs ?lrls; ?lrls <= iscrls; extrs ?lrls <= ?drls;
         Ball ?lrls (subfml_cp_prop ?sub);
         Ball (extrs ?lrls) (inv_rl ?drls) |] ==>

   ctr_adm_step ?sub (derrec ?drls {}) ?epsc ?A"
subfml_cp_prop.simps:
   "subfml_cp_prop ?sub (?ps, ?c) =
      (ALL p:set ?ps. ?c <= p |
        (ALL fp. ms_mem fp p --> (EX fc. ms_mem fc ?c & (fp, fc) : ?sub)))"

Then the other cases of ctr adm step were proved separately:

Lemma 15.2: In S4C, for derivations with final rules (⊢ □) and (∘) (extended in their conclusions), the inductive contraction admissibility step ctr adm step holds.

ctr_adm_step_s4cbox:
   "[| ?psc = (?ps, ?c); ?psc : extcs s4cbox; extcs s4cbox <= ?drls |]
      ==> ctr_adm_step ?sub (derrec ?drls {}) ?psc ?A"
ctr_adm_step_circ:
   "[| ?psc = (?ps, ?c); ?psc : extcs circ; extcs circ <= ?drls |]
      ==> ctr_adm_step ipsubfml (derrec ?drls {}) ?psc ?A"

Consequently, we get contraction admissibilty. The only case not convered above is for the reflexivity rule (□ ⊢), in its form where the principal formula is copied to the premise. This is required for contraction admissibility, which becomes simple with the rule in this form.

Lemma 15.3 (s4cns ctr adm): Contraction is admissible in GTD.

s4cns_ctr_adm: "ctr_adm s4cns ?A"

15.4 Cut-admissibility for S4C

To prove cut admissibility for a system of rules containing an explicit contraction rule, two methods are

• to prove mix-elimination directly, where the property proved by induction on the derivation is that any instance of the mix rule is admissible

• in respect of the derivations on either side of the cut, to look up the derivation skipping over consecutive instances of contraction on the cutformula, and consider the various cases of the next rule on either side above those contractions.

We do something similar to the second approach here, but we look up the derivations on either side to find the last rule before a consecutive sequence of (∘) rules. For this we use the theorem top circ ns. In some cases we also 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.

Lemma 15.4 (top circ ns): Given a valid derivation tree dt, then there is a valid tree dtn and an integer k such that

• the bottom rule of dtn is not (∘),

• the conclusions c and c′ of dt and dtn are related by c = ∘^{k}c′

• height of dt = height of dtn +k

• dt and dtn iff k = 0 iff the bottom rule of dt is not (∘)

top_circ_ns: "valid ?rls ?dt ==> EX dtn k.
   botRule dtn ~: extcs circ & valid ?rls dtn &
   seqmap (funpow Circ k) (conclDT dtn) <= conclDT ?dt &
   heightDT ?dt = heightDT dtn + k &
   forget ((k = 0) = (botRule ?dt ~: extcs circ) & (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. The fact that the conclusions of both the (∘) rule and the (⊢ □) rule may be extended by an arbitrary context complicates matters. Consider the following diagram of a number of (∘) rules followed by the (⊢ □) rule.

M ⊢ A (⊢ □) Γ, M ⊢ □A, Δ (∘^{∗}) Γ′, ∘^{k}Γ, ∘^{k}M ⊢ ∘^{k}□A, ∘^{k}Δ, Δ′

In this case we can instead construct the following derivation tree, which is of the same height.

\begin{aligned}M ⊢ A \\ & (⊢ □) \\ M ⊢ □A \end{aligned} (∘^{∗}) ∘^{k}M ⊢ ∘^{k}□A

Thus we can use, in proving an inductive step, the fact that ∘^{k}M ⊢ ∘^{k}□A is derivable, and with a derivation of the same height as that of Γ′, ∘^{k}Γ, ∘^{k}M ⊢ ∘^{k}□A, ∘^{k}Δ, Δ′. This will be used in our proofs without further comment.

Now, where the cut-formula is within ∘^{k}Δ, Δ′ (where this is the derivation tree on the left of a desired cut), or within Γ′, ∘^{k}Γ (where this tree is on the right), the cut is admissible because we can start from the derivable sequent M ⊢ A and apply (⊢ □) and ∘ rule without any extra formulae in the conclusions, as discussed above. In this case we just use weakening admissibility to obtain the result of the cut.

These situations are covered by Lemma 15.5 (s4cns cs param l'') and the symmetric result s4cns cs param r''.

Lemma 15.5: Let the left premise subtree of a desired cut be dt, with dtn and k as in Lemma 15.4, let the bottom rule of dtn be an extension (of the conclusion) of a rule in s4cns whose conclusion is cl ⊢ cr, and let C not be in ∘^{k}cr. Then the inductive step sumh step2 tr for proving cut-admissibility with cut-formula C holds.

s4cns_cs_param_l'':
  "[| (?ps, ?cl |- ?cr) : s4cns; botRule ?dtn : extcs {(?ps, ?cl |- ?cr)};
     count (mset_map (funpow Circ ?k) ?cr) ?C = 0; valid s4cns ?dtn |] ==>
   sumh_step2_tr (prop2 casdt s4cns) ?C ?sub
  (Der (seqmap (funpow Circ ?k) (conclDT ?dtn) + ?flr) ?list,
       Der ?dtr ?lista)"

A similar pair of results, discussed later (see Lemma 15.6), covers the case where the rule above the (∘) rules is a base rule which is extended by an arbitrary context in its conclusion and its premises.

Now we can assume that the cut-formula is within the principal part of the rule before the (∘) rules (noting that for the (⊢ □) rule the “principal part” means the entire M ⊢ □A). 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}Γ, ∘^{k}M ⊢ ∘^{k}□A, ∘^{k}Δ, Δ′  \begin{aligned}∘^{k}□A, M′ ⊢ B \\ & (⊢ □) \\ Γ′′, ∘^{k}□A, M′ ⊢ □B, Δ′′ \end{aligned}
....................................................................... (cut ?)
Γ′, ∘^{k}Γ, Γ′′, ∘^{k}M, M′ ⊢ □B, ∘^{k}Δ, Δ′, Δ′′

Here we do the cut, by induction, before the (⊢ □) rule on the right, using a derivation like that on the left, but without any context, then we apply the (⊢ □) rule, introducing the required context.

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

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

For the other cases, we first consider the “parametric” cases, where the last rule above the (∘) rules is an extension ρ′ of a rule ρ in s4cnsne, and the principal formula of ρ is not the “de-circled” cut-formula A. Recall that s4cnsne consists of the axiom, logical introduction rules and the (□ ⊢) rule, as skeletons (ie, not extended with context), but with ∘^{k} applied to their formulae.

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

Here we must apply the ∘ rule the requisite number of times to the premise(s) of ρ′, then apply (using the inductive hypothesis) cut 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 s4cnsne then so is the result of applying ∘^{k} to all formulae in its premises and conclusion.

s4cnsne_nkmap: "?r : s4cnsne ==> nkmap ?k ?r : s4cnsne"

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

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

Lemma 15.6 (s4cns param l') and the symmetric result s4cns param r' cover this case.

Lemma 15.6: Let the left premise subtree of a desired cut be dt, with dtn and k as in Lemma 15.4, let the bottom rule of dtn be an extension of a rule in s4cnsne whose conclusion is cl ⊢ cr, and let C not be in ∘^{k}cr. Then the inductive step sumh step2 tr for proving cut-admissibility with cut-formula C holds.

s4cns_param_l': "[| (?ps, ?cl |- ?cr) : s4cnsne;
     botRule ?dtn : extrs {(?ps, ?cl |- ?cr)};
     count (mset_map (funpow Circ ?k) ?cr) ?C = 0; valid s4cns ?dtn;
     Suc (heightDTs ?list) = heightDT ?dtn + ?k |] ==>
    sumh_step2_tr (prop2 casdt s4cns) ?C ?sub
       (Der (seqmap (funpow Circ ?k) (conclDT ?dtn) + ?flr) ?list,
        Der ?dtr ?lista)"

It is similar for the parametric case 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 \\ & (⊢ □) \\ X, M ⊢ □A, Y \end{aligned} ; (∘^{∗}) ; X′, ∘^{k}X, ∘^{k}M ⊢ ∘^{k}□A, ∘^{k}Y, Y′  \begin{aligned}∘^{k′′}A, U ⊢ V \\ & (□ ⊢) \\ ∘^{k′′}□A, U ⊢ V \end{aligned} ; (∘^{∗}) ; ∘^{k′+k′′}□A, ∘^{k′}U, U′ ⊢ ∘^{k′}V, V′ .............................................................................. (cut ?)
X′, ∘^{k}X, ∘^{k}M, ∘^{k′}U, U′ ⊢ ∘^{k}Y, Y′, ∘^{k′}V, V′

Here k′+k′′ = k, but since we also have that k = 0 or k′ = 0, this means that k′ = 0 and k′′ = k. The following diagram omits a final use of the admissibility of weakening.

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

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

∘^{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 s4cnsne. Most of these cases have been covered, ie, the axiom rules, and the “parametric” cases, where the “de-circled” cut-formula is not the principal formula of the rule.

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 c8 ercas prop (Definition 14.3). Recall that this means that assuming 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.

Lemma 15.7 (s4cns c8 ercas): S4C satisfies c8 ercas prop in relation to the logical introduction rule skeletons lksil cup lksir, with ∘^{k} applied to all formulae.

s4cns_c8_ercas: "c8_ercas_prop (circrel ipsubfml) s4cns ?A
    (nkmap ?k ` (lksil Un lksir))"

The following diagrams show an example. We let t = k + k′ = l + l′. 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 ................................................................ (cut ?)
∘^{k}X, ∘^{l}U ⊢ ∘^{k}Y, ∘^{l}V

The diagram above is simplified by not including the extra context which may be introduced in the conclusion of the (∘) rules. 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 cut)

∘^{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 cut)

∘^{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 cut)

∘^{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. Again, we can use weakening admissibility to get the extra context which was introduced by the (∘) rules, but omitted from the first diagram.

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

Theorem 15.1 (s4cns casdt, s4cns cas): S4C satisfies cut-admissibility.

s4cns_casdt: "(?dta, ?dtb) : casdt s4cns ?A"
s4cns_cas: "(?cl, ?cr) : cas s4cns ?A"

15.5 Comparing our proofs and the proofs of Mints

The presentation of Mints [?] contains a very abbreviated treatment of cutadmissibility for S4C. We attempted to follow the proof shown there, but were unable to. The slides state a lemma (“Substitution Lemma”), that the following rule is admissible

\frac{B ⊢ □C □C, Γ ⊢ Δ}{B, Γ ⊢ Δ}

As a lemma it is undoubtedly correct (it is a particular case of cut-admissibility). However, as part of the proof of cut-admissibility we were unable to prove it as it stands — it appears to need (at least) an assumption that cuts on C are admissible.

16 Related Work

We may compare this approach with that of Pfenning [?]. Pfenning uses the propositions-as-types paradigm, where a type represents (partially) a sequent. More precisely, for intuitionistic logic, a type hyp A -> hyp B -> conc C represents a sequent containing A and B in its antecedent, and C in its succedent. For classical logic, neg A -> neg B -> pos C -> pos D -> # represents a sequent containing A and B in its antecedent, and C and D in its succedent. A term of a given type represents a derivation of the corresponding sequent.

Pfenning’s proof of cut-admissibility proceeds by a triple induction, using structural induction on the formula and the two terms representing the derivations. It therefore most closely resembles our proofs involving explicit derivations, as described in §??.

However in §?? we go on to measure properties (such as the height) of an explicit derivation. It seems as though Pfenning’s approach does not allow the possibility of doing that.

17 Further Work and Conclusion