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 0200, Australia

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 K4D, S4 and S4.3 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.

1 Introduction

Sequent calculi provide a rigorous basis for meta-theoretic studies of various logics. The central theorem is cut-elimination/admissibility, which states that detours through lemmata can be avoided, since it can help to show many important logical properties like consistency, interpolation, and Beth definability. Cut-free sequent calculi are also used for automated deduction, for nonclassical extensions of logic programming, and for studying the connection between normalising lambda calculi and functional programming. Sequent calculi, and their extensions, therefore play an important role in logic and computation.

Meta-theoretic reasoning about sequent calculi is error-prone because it involves checking many combinatorial cases, with some being very difficult, but many being very similar. Invariably, authors resort to expressions like “the other cases are similar”, or “we omit details”. The literature contains many examples of meta-theoretic proofs containing serious and subtle errors in the original pencil-and-paper proofs. For example, the cut-elimination theorem for the modal “provability logic” GL, where □φ can be read as “φ is provable in Peano Arithmetic”, has a long and chequered history which has only recently been resolved [8].

Here, we describe how we formalised cut-elimination for traditional, propositional, multiset-based sequent calculi without explicit structural rules for the modal logics KD, S4, S4.3 and S4C using the interactive proof-assistant Is- KD here, K4D

in abstract, K4De in §3 ? abelle/HOL. As far as we know, the proofs for S4 and S4.3 are new, and avoid the complexities of previous proofs for these logics. Our results also confirm the recent proof of cut-elimination for S4C due to Mints, although our proof is different.

∗Supported by Australian Research Council Grant DP120101244.

In Section 2, we briefly describe traditional sequent calculi, discuss the need for multisets, and describe ???

In Section ?? we describe techniques and functions we have defined for reasoning about derivations, and show how we formalise formulae, sequents and rules, showing some of the sequent rules as examples. In Section ?? we describe the cut-admissibility proof for ???.

We assume the reader is familiar with basic proof-theory, ML and Isabelle/HOL.

Our Isabelle code can be found at http://users.rsise.anu.edu.au/~jeremy/

isabelle/2005/seqms/. Some of this work was reported informally in [7].

2 Sequents Built From Multisets Verssus Sets

Proof-theorists typically work with sequents Γ ⊢ Δ where Γ and Δ are “collections” of formulae. The “collections” found in the literature increase in complexity from simple sets for classical logic, to multisets for linear logic, to ordered lists for substructural logics, to complex tree structures for display logics. A sequent rule typically has a rule name, a (finite) number of premises, a sidecondition and a conclusion. Rules are read top-down as “if all the premises hold then the conclusion holds”. A derivation of the judgement Γ ⊢ Δ is typically a finite tree of judgements with root Γ ⊢ Δ where parents are obtained from children by “applying a rule”. We use “derivation” to refer to a proof within a calculus, reserving “proof” for a meta-theoretic proof of a theorem about the calculus.

Sequent calculi typically contain three structural rules called weakening, contraction and cut. These rules are bad for automated reasoning using backward proof-search since they can be applied at any time. Thus for backward proofsearch, we are interested in sequent calculi which do not contain explicit rules for weakening, contraction and cut. The traditional way to design such calculi is to assume that sequents are built out of multisets, omit these rules from the calculus itself, and prove that each of these rules is admissible. That is, for each rule, we have to prove that the conclusion sequent is derivable if each of its premises are derivable.

For example, our formalisation does not regard the cut rules shown below as being part of the system:

Γ ⊢ A, Δ  Γ, A ⊢ Δ (cut) Γ ⊢ Δ Γ_{1} ⊢ A, Δ_{1}  Γ_{2}, A ⊢ Δ_{2} (cut) Γ_{1}, Γ_{2} ⊢ Δ_{1}, Δ_{2}

Thus our results will be lemmata of the form: if Γ ⊢ A, Δ is (cut-free) derivable and Γ, A ⊢ Δ is (cut-free) derivable then Γ ⊢ Δ is (cut-free) derivable.

3 Basic Modal Logics

The sequent calculi we study are designed to reason about the meta-theory of the basic modal logics S4, S4.3, K4De (called GTD by Mints) and S4C. Semantically, the first three are mono-modal logics characterised by Kripke frames having reflexive and transitive; reflexive, transitive and linear frames; and transitive and dense frames respectively. The logic S4C, called dynamic topological logic, is a bimodal logic where □ is captured by a reflexive and transitive binary relation R_{□} and where ◯ is captured by a serial and discrete linear relation R_{◯} why ◯ not ∘? with an interaction of “confluency”:

∀x∀y∀z∃u.R_{□} (x, y) & R_{◯}(x, z) ⇒ R_{◯}(y, u) & R_{□} (z, u)  (1)

The Hilbert-calculi for these logics are obtained by extending a traditional Hilbert-calculus for classical propositional logic with the following axioms and inference rules using the naming conventions given in the rightmost column:

Axiom/Rule Name Schema  Logic Axioms Rules
K  □(φ → ψ) → (□φ → □ψ) S4  K,4,T  RN□
De  □□φ → □φ  S4.3 K,4,T,.3 RN□
T  □φ → φ  K4De K,4,De RN□
4  □φ → □□φ
.3  □(□φ → ψ) ∨ (□φ → ψ)
RN□  φ/□φ

The logic S4C is obtained from S4 by adding the following axioms and rule:

Axiom/Rule Name Schema
K_{◯}  ◯(φ → ψ) ↔ (◯φ → ◯ψ)
◯⊥  ◯⊥ ↔ ⊥
C  ◯□φ → □ ◯ φ
RN◯  φ/◯φ

The modal logic S4C is designed to capture the basic logic for hybrid systems where equation (1) captures the continuity of the linear discrete relation with respect to the topological interpretation of the □-connective.

4 Interactive Proof Assistants

Interactive proof-assistants are now a mature technology for “formalising mathematics”. They come in many different flavours as indicated by the names

of some of the most popular ones Mizar, HOL, Coq, LEGO, NuPrl, NqThm,
Isabelle, λ-Prolog, HOL-Lite, LF, ELF, Twelf · · · with apologies to those

whose favourite proof-assistant I have omitted.

Most of the modern proof-assistants are implemented using a modern functional programming language such as ML, which was specifically designed for the implementation of, and interaction with, such proof-assistants.

The lowest levels typically implement a typed lambda-calculus with hooks provided to allow the encoding of further logical notions such as equality of terms on top of this base implementation. The base implementation is usually

\begin{matrix}[β_{1} ; β_{2} ; ⋯; β_{n}] ⟹ α & β \\ θ = match(β, α) & β_{1}θ ; β_{2}θ ; ⋯; β_{n}θ \end{matrix}

Fig. 1: Backward Chaining in Logical Frameworks

very small, comprising of a few hundred lines of code, so that this code can be scrutinised by experts to ensure its correctness.

Almost all aspects of proof-checking eventually compile down to a typechecking problem using this small core, so that trust rests on strong typing and a well-scrutinised small core of (ML) code.

Most proof-assistants also allow the user to create a proof-transcript which can be cross-checked using other proof-assistants to guarantee correctness.

Figure 4 shows how these logical frameworks typically work. Thus given some goal β and an inference step which claims that α is implied by β_{1} up to β_{n}, we pattern-match α and β to find their most general unifier θ, and then reduce the original goal β to the n subgoals β_{1}θ ⋯ β_{n}θ.

The pattern matching required is usually (associative-commutative) higher ?? what does associativecommutative mean here? order unification.

The important point is that the logical framework keeps track of sub-goals and the current proof state.

The syntax of the “basic propositions” such as α, β is defined via an “object logic”, which is a parameter. Different “object logics” can be invoked using the same logical-framework for the task at hand.

The logical properties of “;” such as associativity or commutativity, and properties of the “⟹” such as classicality or linearity are determined by the “meta-logic”, which is usually fixed for the logical framework in question.

For example, the meta-logic of Isabelle is higher-order intuitionistic logic. Higher order simply means that functions can accept other functions as arguments and can produce functions as results.

5 A Deeper Embedding: Change Object Logic

Recall that the meta-logic provides us with a method for backward chaining via expressions of the form:

β_{1} ; ⋯; β_{n} ⟹ α

The usual method for obtaining the power for reasoning about sequent derivations is to use the full power of higher-order classical logic (HOL) to build the basic propositions β_{i}.

Isabelle’s incarnation of HOL provides the usual connectives of logic such as conjunction, disjunction, implication, negation and the higher order quantifiers. But it also provides many powerful facilities allowing us to define new types, define functions which accept and return other functions as arguments, and even define infinite sets using inductive definitions.

For example, the following HOL expressions capture the usual inductive definition of the natural numbers by encoding the facts that “zero is a natural number, and if n is a natural number then so is its successor s(n)”:

                       0 ∈ nat
                       n ∈ nat ⟹ s(n) ∈ nat

Most proof-assistants will automatically generate an induction principle from a given inductive definition. For example, Isabelle will automatically generate the usual induction principle which states that we can prove a property P holds of all natural numbers if we can show that P (0) holds and we can show that P (n) implies P (s(n)). An implicit assumption which facilitates such induction principles is that the inductive definitions are the only way to construct its members. Thus, if n is a natural number, then it is either 0, or is of the form s(m) for some natural number m.

To encode sequent calculus into HOL we first encode the grammar for recognising formulae as below:

   datatype fml = FC string (fml list)    (* fml connective *)
                | FV string               (* fml variable   *)
                | PP string               (* prim prop      *)

There are three type constructors FC, FV and PP which encode formula connectives, formula variables, and atomic formulae (primitive propositions). Each of them takes one string argument which is simply the string we want to use for that construction. The formula connective constructor also accepts a list of formulae, which constitute its subformulae.

For example, FC "&&" [FV "A", PP "q"] encodes A ∧ q where we use && as the symbol for conjunction. Since we want to encode modal logics, we require only the classical connectives, plus two unary modalities FC "Box" [.] for □.

and FC "Dia" [.] for ♢. and FC "Circ" [.] for ◯.

Isabelle’s HOL allows us to form sets and multisets of objects of an arbitrary type, so the HOL expressions fml set and fml multiset capture the types of formula sets and formula multisets.

Using these types we can build a sequent type using an infix constructor

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

An alternative notation for the constructor Sequent is ⊢ or |- (used infix). We define the rule type by the type definitions

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

so a rule is a pair of a list of sequents (the premises) and a single sequent (the conclusion).

Note that in common parlance we may say that (eg) A ⇒ B ⇒ A ∧ B is a “rule”, in the usage of our Isabelle implementation we would call ths a pattern which can be instantiated to give infinitely many rules. So all our rule sets are in fact the sets of instances of a finite number of “rule patterns”.

Thus, we can use the HOL type declaration rli :: rule set to declare that rli is a set of inferences, each a pair of the form (seq list, seq), and inductively define the set rli by giving a finite collection of rule instances which belong to this set. For example, the traditional rule (⊢ ∧) for introducing a conjunction into the right hand side of a sequent, as shown below, is given by the encoding below it where we use the string && to encode ∧:

Γ ⊢ A, Δ  Γ ⊢ B, Δ (⊢ ∧) Γ ⊢ A ∧ B, Δ

( [ G ⊢ {#A#} + D , G ⊢ {#B#} + D ], G ⊢ {#A && B#} + D ) ∈ rli

The encoding uses HOL’s notation “+” for multiset union, and uses {# and #} to encode the braces for multisets. Thus each element of rli is a pair whose first component is a list of its premises, and whose second component is its conclusion.

We are now in a position to encode the set derrec of “recursively derivable sequents” given an initial set pms of premise sequents and an initial set rli of inference rules. The set derrec could be defined inductively as shown below:

    1  derrec :: (seq list ∗ seq) set ⇒ seq set ⇒ seq set
    2  c ∈ pms ⟹ c ∈ derrec rli pms

3  [ (ps, c) ∈ rli ;

    4  ∀ p. p ∈ (set ps) ⟹ p ∈ derrec rli pms ]
    5  ⟹ c ∈ derrec rli pms

The explanation is as below:

1: A type declaration which tells the proof-assistant that derrec accepts a set of inference rules and a set of sequents, and produces a set of sequents;

2 The base case of the inductive definition of derrec captures that “each premise is itself (vacuously) derivable from the premises using the rules”. Note that there is an implicit outermost universal quantifier which is not shown explicitly, but which binds free variables such as c, ps, rli, pms.

3 The first conjunct of an inductive clause stating that ps/c is a rule instance;

4: The second conjunct of the inductive clause which captures that “each premise p in the set obtained from sequent list ps is derivable from the premises pms using the rules rli”. Here we use a function set to convert a list into the set of its members;

5: The “then” part of the inductive clause which concludes that sequent “c is derivable from pms using rli”.

6 Inductive Proofs via Automated Inductive Principles

Induction principles are generated automatically by Isabelle from the inductive definition of derrec. A heavily simplified version for proving an arbitrary property P is shown below:

1  ∀x.∀P.

    2  [ x ∈ derrec rli pms ;

3  ∀c.c ∈ pms ⟹ P(c) ;
4  ∀c.∀ps.[ (ps, c) ∈ rli ; ∀y ∈ (set ps). P(y) ] ⟹ P(c)
5  ] ⟹ P(x)

An explanation is:

1: for all sequents x and all properties P

2 : if x is derivable from premises pms using rules rli, and

3 : P holds for every premise c in pms, and

4 : for each rule, P of its premises implies P of its conclusion,

5 : then P holds of x

If you look closely, you will see that this is an induction principle which we use often in proof-theory: prove that some property holds of the leaves of a derivation, and prove that the property is preserved from the premises to the conclusion of each rule. For example, consider the standard translation from sequents of LK to formulae given by τ(A_{1}, ⋯, A_{n} ⊢ B_{1}, ⋯, B_{m}) = A_{1} ∧ ⋯ ∧ A_{n} → B_{1} ∨⋯∨B_{m}. We typically use this translation to argue that all derivable sequents are valid in the semantics of first-order logic. The proof proceeds by showing that the translation of the leaves of a derivation are all valid, and showing that if the translations of the premises are valid then the translations of the conclusion are valid, for every rule. NB derrec

introduced in previous section Thus we have the lemma:

make uniform with text at start of section Lemma 6.1: For a property P1.0, if

• if every premise in prems obeys P1.0,

• for every rule (ps, concl) in rls, if each premise in ps being derivable from leaves prems using rules in rls and obeying P1.0 implies that concl obeys P1.0, and

• the sequent xb is derivable from leaves prems using the rules in rls,

then xb obeys P1.0:

Proof: Isabelle automatically generates an induction principle from the definition of derrec. Since the definition also involves defining dersrec (which expresses that a list of items are all derivable), the automatically generated principle involves a property P_{1} of derivable sequents and a property P_{2} of lists of derivable sequents. Naturally we choose property P_{2} of a list to be that all members of the list satisfy P_{1}. That instantiation gives us the lemma. Q.E.D.

standard drs.inductr:
 "[| ?xb : derrec ?rls ?prems ;
     !!concl. concl : ?prems ==> ?P1.0 concl ;
     !!concl ps. [| (ps, concl) : ?rls; ps : dersrec ?rls ?prems;
        Ball (set ps) ?P1.0 |] ==> ?P1.0 concl |] ==> ?P1.0 ?xb"

Using these inductive principles we proved the following lemma about derivability using Isabelle, where the question marks indicate free-variables which are implicitly universally quantified:

Lemma 6.2:

?ps ⊆ derrec ?rli ?pms ; ?c ∈ derrec ?rli ?ps ⟹ ?c ∈ derrec ?rli ?pms

If each premise in ps is derivable from premises pms using rules rli, and c is derivable from ps using rli, then c is derivable from pms using rli.

7 An Even Deeper Embedding: Derivation Trees As Objects

The main advantage of the method outlined in the previous section was that there was no concrete representation of a derivation. That is, we relied on the proof-assistant to perform pattern-matching and rule instantiations in an appropriate way, so that all we needed was to capture the idea that derivations began with premises and ended with a single sequent.

When we reason about cut-elimination, often we are required to perform transformations on explicit derivations. We therefore need a representation of such trees inside our encoding.

In previous work [?], we described such an encoding using the following datatype:

   datatype seq dertree = Der seq (seq dertree list)
                        | Unf seq

The declaration states that a derivation tree can either be an Unfinished (unproved) leaf sequent built using the constructor Unf, or it can be a pair consisting of a conclusion sequent and a list of sub-derivation-trees bound together using the constructor Der.

In that work, we also described how we maintained substitutions as lists of pairs of the form (x, t) representing the substitution x := t. We also described how we manipulated substitutions and instantiation directly to obtain rule instances.

We required such low-level aspects to be made explicit so that we could reason about display logic which required us to check conditions on rules such as “a rule is closed under substitution of arbitrary structures for variables”.

Our use of dertee can be seen as an even deeper embedding of proof-theory into Isabelle/HOL since it utilises the proof-assistant to describe a “proof object” rather than to specify directly the provable sequents.

Omitting details now, suppose we define valid rli dt to hold when derivation tree dt uses rules from rli only and has no Unfinished leaves. We linked these two approaches to specifying the provable sequents by proving:

Lemma 7.1:

          valid ?rli ?dt ⟹ (conclDT ?dt) ∈ derrec ?rls {}

If derivation tree dt is valid wrt the rules rli then its conclusion is derivable from the empty set of premises using rli.

Lemma 7.2:

    ?c ∈ derrec ?rli {} ⟹ EX dt. valid ?rli dt & conclDT dt = ?c

If the sequent c is derivable from the empty set of premises using rules rli then there exists a derivation tree dt which is valid wrt rli, whose conclusion is c.

Thus we now know that our “deep embedding” of derivability using derrec can be faithfully captured using the “even deeper” embedding using explicit derivation trees. Indeed, the lemmas allow us to move freely between the two embeddings at will to omit or include details as required.

8 Our General Derivability Predicates

SOME OF THIS IS COVERED IN §5 We now briefly describe the functions we used to describe derivability. A fuller account is given in [7]. This framework is general in that a rule merely consists of “premises” and a “conclusion”, and is independent of whether the things derived are formulae, sequents, or other constructs, but we will refer to them as formulae.

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

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

The auxiliary function dersrec represents several formulae, all derivable from the premises. The auxiliary function dersl represents several derivation trees side by side; (ps, cs) ∈ dersl rls when ps is the concatenation of their lists of premises, and cs is the list of their conclusions. The function dercsl is similar, but it shows which premises are part of which tree. That is, (pss, cs) ∈ dercsl rls implies (concat pss, cs) ∈ dersl rls. Curiously, we have used this framework for several years, and only recently we found the need to redefine derl using dercsl rather than dersl as the auxiliary function.

The key clauses for these functions are shown below:

  dtderI : "[| (ps, concl) : pscrel ; (pss, ps) : dersl pscrel |]
              ==> (pss, concl) : derl pscrel"
  derI : "[| (ps, concl) : pscrel ; ps : dersrec pscrel prems |]
              ==>  concl : derrec pscrel prems"

We obtained the expected results linking derl and derrec, and a number of results expressing transitivity of derivation and the results of derivation using derived rules, for example:

derl_trans : "[| (?ps, ?c) : derl ?rls; (?x, ?ps) : dersl ?rls |]
                 ==> (?x, ?c) : derl ?rls"
derl_deriv_eq : "derl (derl ?rls) = derl ?rls"
derrec_trans_eq : "derrec ?rls (derrec ?rls ?prems) = derrec ?rls ?prems"

A simplified version of the induction principle generated by the definition of the inductive set derrec is as follows:

\frac{x ∈ derrec rls prems ∀c ∈ prems.P c ∀(ps, c) ∈ rls.(∀p in ps.P p) ⇒ P c}{P x}

We may contrast use of this principle with induction on the height of a derivation tree. Using induction on the height, it is possible, and in some proofs necessary, to transform a sub-tree in some height-preserving (or height-reducing) way, and use the assumption that the transformed tree has property P. That approach is not available when using the induction principle above, and was not needed for our earlier proofs.

Where we have a property of two derivations, such as cut-admissibility, we need a more complex induction principle, which we derived (limited to the case where the set prems of ultimate assumptions is empty) :

cl ∈ derrec rlsl {} cr ∈ derrec rlsr {}

∀(lps, lc) ∈ rlsl, (rps, rc) ∈ rlsr. (∀lp in lps.P lp rc) ∧ (∀rp in rps.P lc rp) ⇒ P lc rc P cl cr

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

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

We obtained the following four results, which were surprisingly tricky since adm is not monotonic:

"derl ?rls <= adm ?rls"              "adm (adm ?rls) = adm ?rls"
"adm (derl ?rls) = adm ?rls"         "derl (adm ?rls) = adm ?rls"

9 Subformula Relation and Rule Extensions with Arbitrary Contexts

Our generalised definition of formulae allows a single definition of the immediate (proper) subformula relation, ipsubfml, which will not need to be changed when new connectives are added.

consts ipsubfml :: "(formula * formula) set"
inductive "ipsubfml" (* proper immediate subformula relation *)
  intros  ipsI : "P : set Ps ==> (P, FC conn Ps) : ipsubfml"

As noted in §5 a sequent is a pair of multisets of formulae, written Γ ⊢ Δ. Given a rule such as (⊢ ∧) in the form on the left,

R_{s} = \frac{⊢ A ⊢ B}{⊢ A ∧ B} R_{e} = \frac{X ⊢ Y, A X ⊢ Y, B}{X ⊢ Y, A ∧ B}

we define functions extend and pscmap, such that (for example)

extend (X ⊢ Y) (U ⊢ V) = (X + U) ⊢ (Y + V)

                  R_{e} = pscmap (extend (X ⊢ Y)) R_{s}

Thus pscmap uniformly extends the skeleton provided by R_{s} with arbitrary contexts X and Y on respective sides to encode R_{e} using multiset addition +.

Then extrs S means the set of all such extensions of all rules in the set S.

consts
  extend :: "'a sequent => 'a sequent => 'a sequent"
  extrs  :: "'a sequent psc set => 'a sequent psc set"
defs
  extend_def : "extend fmls seq == seq + fmls"
  pscmap_def : "pscmap f (ps, c) = (map f ps, f c)"

Then we define lksss, the set of rules for Gentzen’s LK; we show just a selection. The rules below are the traditional invertible logical introduction rules from LK (without any context):

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

inductive "lksir" (* LK right introduction rules *)
intros
 andr : "([{#} |- {#A#}, {#} |- {#B#}], {#} |- {#A && B#}) : lksir"
 orr  : "([{#} |- {#A#} + {#B#}], {#} |- {#A v B#}) : lksir"
 ...

Similar rules lksil give the traditional invertible rules for left-introduction. By adding the initial rule “axiom” below we obtain the set of “unextended” rules lksne for LK:

inductive "lksne" (* LK rules before being extended *)
intros
 axiom : "([], {#A#} |- {#A#}) : lksne"
 ilI   : "(ps, c) : lksil ==> (ps, c) : lksne"
 irI   : "(ps, c) : lksir ==> (ps, c) : lksne"
 ...

We can now form the full extended set of rules lksss for LK, where flr is an arbitrary pair of contexts X, Y (regarded as a sequent, X ⊢ Y).

inductive "lksss"
  intros
    extI : "psc : lksne ==> pscmap (extend flr) psc : lksss"

The traditional K-rule below at left may be encoded as shown below by extending the skeleton shown at right, in its conclusion only:

\begin{aligned}Γ ⊢ A \\ & (K) \\ Σ, □Γ ⊢ □A, Δ \end{aligned}  \begin{matrix}Γ ⊢ A \\ □Γ ⊢ □A \end{matrix}

inductive "K"
  intros
    I : "([X |- {#B#}], mset_map Box X |- {#Box B#}) : K"

Note that X is a multiset, and □X is informal notation for applying □ to each member of X; this is formalised as mset map, used in the formalised K rule. Using a similar notation we write □B^{k} for (□B)^{k}, the multiset containing n copies of □B. Development of mset map and relevant lemmas is in the source

files Multiset no le.{thy,ML}.

By extending the skeleton of the LK calculus and adding the new K rule above, we could obtain an encoding of the traditional sequent calculus for the modal logic K: We don’t ac-

tually do this - the closest is Jesse’s definition of

                                                                    gs4 rls

inductive "lksK"
intros
 extI : "psc : lksne ==> pscmap (extend flr) psc : lksK"
 K : "psc : K ==> psc : lksK"

10 Generalising Cut-Admissibility Proofs

We now show how our previous work on multicut admissibility for LK can be formulated to make it as general as possible.

For proofs of contraction-admissibility, without height-preservation, a stronger induction principle is required. The axioms of our systems will be allowed to apply to arbitrary formula, not only atoms, and this excludes the possibility of proving height-preserving invertibility and contraction-admissibility results. To compensate for the lack of an explicit height, a double induction on premises (instead of explicit derivation height) and formula size (as measured by any wellfounded subformula relation) is used. The implementation of this first encodes an inductive step condition:

Definition 10.1 (gen step): For a formula A, a property P, a subformula relation sub, a set of sequents derivs, and a particular rule r = (ps, c),

   gen step P A sub derivs r means:

If

• forall A′ such that (A′, A) ∈ sub and all sequents D ∈ derivs the property P A′ D holds,

• for every premise p ∈ ps both p ∈ derivs and P A p holds, and

   • c ∈ derivs

then P A c holds.

Typically derivs will be the set of sequents derivable using a given set rls

of rules, derivs = derrec rls prems.

In English, this step condition states that if a property P is true generally for formulae of lower rank A′, and for the (derivable) premises of a particular rule then the property holds for the conclusion of that rule. The main theorem, named gen step lem and given as Theorem 10.1 below, states that if this step case can be proved for all possible rule instances then P holds for all cases.

Theorem 10.1 (gen step lem): If

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

• sequent S is rls-derivable and

• for all formulae A′ and all possible rules r in rls, the induction step

     condition gen step P A′ sub (derrec rls {}) r holds

then P A S holds.

In §?? we mentioned the induction principle used for deriving cut-admissibility, or indeed any property P of two-premise subtrees. In the diagram below, to prove P (R_{l}, R_{r}), the induction assumption is that P (Q_{li}, R_{r}) and P (R_{l}, Q_{rj}) hold for all i and j:

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

?

A proof of P (R_{l}, R_{r}) using this induction assumption inevitably proceeds according to what the rules ρ_{l} and ρ_{r} are, and further, for a cut-formula A, whether it is principal in either or both of ρ_{l} and ρ_{r}. But our proofs 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 A (cl, cr) where psl are the premises Q_{l1} … Q_{ln} of rule ρ_{l}, and cl is its conclusion R_{l}, and analogously for ρ_{r}, and A is the cut-formula. In proving P A (R_{l}, R_{r}), in addition to the inductive assumption above, we assume that P A′ (da, db) holds generally for A′ smaller than A and all sequents da and db which are “rls-derivable”, ie, 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:

Definition 10.2 (gen step2sr): For a formula A, a property P, a subformula relation sub, a set of rules rls, inference rules (psl, cl), and (psr, cr), the property gen step2sr holds iff: If

• P A' (da, db) holds for all subformulae A' of A and all rls-derivable sequents da and db;

• for each pa in psl, pa is rls-derivable and P A (pa, cr) holds;

• for each pb in psr, pb is rls-derivable and P A (cl, pb) holds;

• cl and cr are rls-derivable,

then P A (cl, cr) holds.

gen_step2sr_simp :
"gen_step2sr ?P ?A ?sub ?rls ((?psl, ?cl), (?psr, ?cr)) =
( (ALL A'. (A', ?A) : ?sub -->
   (ALL da:derrec ?rls {}. ALL db:derrec ?rls {}. ?P A' (da, db)))
  -->
  (ALL pa:set ?psl. pa : derrec ?rls {} & ?P ?A (pa, ?cr)) -->
  (ALL pb:set ?psr. pb : derrec ?rls {} & ?P ?A (?cl, pb)) -->
    ?cl : derrec ?rls {} --> ?cr : derrec ?rls {}
     --> ?P ?A (?cl, ?cr) )"

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 (psl, cl) and (psr, cr) on each side, then P holds in all cases.

Theorem 10.2 (gen step2sr lem): If A is in the well-founded part of the subformula relation; sequents seql and seqr are rls-derivable ; and for all formulae A, and all rules (psl, cl) and (psr, cr), our induction step condition

gen step2sr P A sub rls ((psl, cl), (psr, cr)) holds, then P A (seql,

seqr) holds.

gen_step2sr_lem :
 "[| ?A : wfp ?sub ;
     ?seql : derrec ?rls {} ; ?seqr : derrec ?rls {} ;
     ALL A. ALL (psl, cl):?rls. ALL (psr, cr):?rls.
         gen_step2sr ?P A ?sub rls ((psl, cl), (psr, cr)) |]
     ==> ?P ?A (?seql, ?seqr)"

This enables us to split up an inductive proof, by showing, separately, that gen step2sr holds for particular cases of the final rules (psl, cl) and (psr, cr) on each side. In some cases these results apply generally to different calculi. 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 (?cl, ?cr) means that the conclusion of a multicut on A with premises cl and cr is derivable using rules erls.

Theorem 10.3: If weakening is admissible for the rule set erls, all extensions of some rule (ps, c) are in the rule set erls, and the final rule instance of the left hand subtree is an extension of (ps, c) where the cut-formula A is not in the succedent of c (meaning that A is parametric on the left), then

gen_step2sr (prop2 mar ?erls) ?A ?sub ?rls (?pscl, ?pscr) holds.
mk_sr1 lmg_gen_step' :
   "[| wk_adm ?erls; extrs {(?ps, ?c)} <= ?erls; ~ ?A :# succ ?c;
         ?pscl = pscmap (extend ?flr) (?ps, ?c) |]
      ==> gen_step2sr (prop2 mar ?erls) ?A ?sub ?rls (?pscl, ?pscr)"

Of course, for a system containing explicit weakening rules, weakening is a fortiori admissible.

Notice that all of this section deals with a shallow embedding of derivations; it does not apply to proofs which require derivation trees to be represented explicitly. As noted in §7, the derivability of a sequent is equivalent fo the existence of a valid derivation tree for it, and in §11 we describe the similar approach for explicit derivation trees.

11 Statements of the Main Lemmas in Isabelle

We now describe how we encoded the statements of the main lemmas regarding the admissibility of weakening, contraction and cut, along with the encoding of the invertibility lemmas required for contraction admissibility.

A set rls of rules satisfies the weakening admissibility property if, whenever a sequent X ⊢ Y is derivable, any larger sequent (X ⊢ Y) + (U ⊢ V) = (X, U ⊢ Y, V) is derivable:

  wk_adm    :: "'a sequent psc set => bool"
  wk_adm_def : "wk_adm rls ==
    ALL XY. XY : derrec rls {} --> (ALL UV. XY + UV : derrec rls {})"

Here, the variable rls is forced to be a set of sequent rules by the type of wk adm, and thence the variables XY and UV will be forced to be of type sequent by the typing restrictions on the inputs to derrec.

Definition 11.1: A rule (ps, c) is invertible with respect to a set rls of rules if, whenever c is derivable using rls, then every member of ps is derivable using

rls.

Here, the definition of dersrec hides a universal quantifier over the members of the list ps:

inv_rl.simps:  "inv_rl ?rls (?ps, ?c)
                 = (?c : derrec ?rls {} --> ?ps : dersrec ?rls {})"

To encode contraction, we utilise an axiomatic type class for sequents, described in more detail elsewhere [?]. Thus we can write (A ⊢ 0) + (A ⊢ 0) ≤ (X ⊢ Y) to mean that the multiset X contains at least two copies of A and write (X ⊢ Y)−(A ⊢ 0) for the sequent obtained by deleting one of these copies from X.

A set rls of rules satisfies the contraction admissibility property for the formula A if, whenever a derivable sequent X ⊢ Y satisfies (A ⊢ 0) + (A ⊢ 0) ≤ (X ⊢ Y), the sequent (X ⊢ Y) − (A ⊢ 0) is derivable, and likewise for 0 ⊢ A.

The first condition ms_of_seq As = {#?A#} says that the multiset of formulae on both sides of the sequent UV is the singleton multiset {#?A#}, thus capturing that the contraction can happen on either side of the turnstile:

ctr_adm_def :
   "ctr_adm ?rls ?A == ALL UV. ms_of_seq UV = {#?A#} -->
       (ALL XY. XY : derrec ?rls {} --> UV + UV <= XY -->
         XY - UV : derrec ?rls {})"

A pair of sequents satisfies the properties cas and car if cut-admissibility is available (in different senses) for that pair of sequents.

Precisely, (X_{l} ⊢ Y_{l}, X_{r} ⊢ Y_{r}) ∈ car rls A iff (X_{l}, (X_{r} − A) ⊢ (Y_{l} − A), Y_{r}) is derivable using rls, whereas cas means that this holds, conditionally on X_{l} ⊢ Y_{l} and X_{r} ⊢ Y_{r} being themselves derivable.

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 these by induction on the derivation of the two sequents, that is, we are talking about two sequents which are derivable, then these two concepts become 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"

Sometimes we need to proceed by induction on (for example) the length of a derivation by which a sequent can be ontained, rather than by the fact of a sequent having been obtained earlier in the same derivation.

So to compare (say) the heights of derivations, we must be able to define them and for this we need to look at explicit derivation trees.

Firstly we define casdt: two valid (ie. no unproved leaves, and all steps are rules of rls) derivation trees satisfy casdt rls A if their conclusions satisfy

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

The step of the induction proof based on explicit derivation trees is expressed using the following definitions and lemmas. THIS STUFF BASICALLY COMBINES THE APPROACHES OF SECTIONS 6 and 7 - SHOULD IT GO EARLIER?

Definition 11.2 (gen step tr): For all properties P, all formulae B, all “subformula” relations sub and all derivation trees dta, gen step tr P B sub dta holds iff: if

• P C dtb holds for all subformulae C of B and all derivation trees dtb, and

• P B dtp holds for all the immediate subtrees dtp of dta

then P B dta holds.

gen_step_tr_def: "gen_step_tr ?P ?B ?sub ?dta ==
    (ALL C. (C, ?B) : ?sub --> (ALL dtb. P C dtb)) -->
    (ALL dtp:set (nextUp ?dta). ?P ?B dtp) --> ?P ?B ?dta"

Lemma 11.1 (gen step tr lem): For all properties P, for all formulae A, for all relations sub, for all derivations dt, if A is in the well-founded part of sub, and gen_step_tr P B sub dtb holds for all formulae B and all derivations dtb, then P A dt holds.

gen_step_tr_lem: "[| ?A : wfp ?sub ;
      ALL B dtb. (gen_step_tr ?P B ?sub dtb) |] ==> ?P ?A ?dt"

Definition 11.3 (gen step2 tr): For all properties P, for all formulae B, for all “sub-formula” relations sub, for all pairs (dta, dtb) of derivation trees, gen step2 tr

P B sub (dta, dtb) holds iff:

if

• P C (dtaa, dtbb) holds for sub-formulae C of B and all derivation trees

     dtaa and dtbb, and

• P B (dtp, dtb) holds for all immediate subtrees dtp of dta, and

• P B (dta, dtq) holds for all immediate subtrees dtq of dtb

then P B (dta, dtb) holds:
gen_step2_tr.simps: "gen_step2_tr ?P ?B ?sub (?dta, ?dtb) =
   ((ALL C. (C, ?B) : ?sub --> (ALL dtaa dtbb. P C (dtaa, dtbb))) -->
   (ALL dtp:set (nextUp ?dta). ?P ?B (dtp, ?dtb)) -->
   (ALL dtq:set (nextUp ?dtb). ?P ?B (?dta, dtq)) --> ?P ?B (?dta, ?dtb))"

Lemma 11.2 (gen step2 tr lem): For all properties P, for all formulae A, for all relations sub, for all derivation trees dta and dtb, if A is in the well-founded

part of sub, and gen_step2_tr P B sub (dtaa, dtbb) holds for all formulae

B and all derivations dtaa and dtbb, then P A (dta, dtb) holds:

gen_step2_tr_lem: "[| ?A : wfp ?sub ;
    ALL B dtaa dtbb. gen_step2_tr ?P B ?sub (dtaa, dtbb) |]
        ==> ?P ?A (?dta, ?dtb)"

These properties are exact analogues, for explicit derivation trees, of the

properties gen step and gen step2sr and lemmas gen step lem and gen step2sr lem,

with the following theorem linking them.

Lemma 11.3:

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

However, the purpose of using explicit derivation trees is to define different induction patterns.

For example, we defined an induction pattern which depends on the inductive assumption that the property P holds for the given tree on one side, and any smaller tree on the other side.

Definition 11.4: For all a, all b, and all functions f, the pair (a, b) is in

measure f iff f a < f b.

For all properties P, for all formulae A, for all subformula relations sub, for all

pairs (dta, dtb) of derivations, height step2 tr P A sub (dta, dtb) holds

iff: if • P B (a, b) holds for all subformulae B of A and for all derivation trees a

and b,

• for all derivation trees dtp of smaller height than dta, P A (dtp, dtb), and

• for all derivation trees dtq of smaller height than dtb, P A (dta, dtq),

then P A (dta, dtb) holds.
measure_eq: "((?a, ?b) : measure ?f) = (?f ?a < ?f ?b)"
"height_step2_tr ?P ?A ?sub (?dta, ?dtb) =
      ((ALL A'. (A', ?A) : ?sub --> (ALL a b. ?P A' (a, b))) -->
       (ALL dtp. heightDT dtp < heightDT ?dta --> ?P ?A (dtp, ?dtb)) -->
       (ALL dtq. heightDT dtq < heightDT ?dtb --> ?P ?A (?dta, dtq)) -->
       ?P ?A (?dta, ?dtb))"

In some cases we found that this wasn’t enough, and defined a more general pattern, where the inductive assumption applies where the sum of heights of the two trees is smaller.

Definition 11.5: For a property P, a formula A, a subformula relation sub, and a

pair of derivations (dta, dtb), sumh step2 tr P A sub (dta, dtb) holds iff:

if

• P B (a, b) holds for all subformulae B of A and all derivation trees a and b, and

• for all derivation trees dta' and dtb' such that heightDT dta'+heightDT dtb' <

     heightDT dta + heightDT dtb, P A (dta', dtb') holds
then P A (dta, dtb) holds
sumh_step2_tr_eq: "sumh_step2_tr ?P ?A ?sub (?dta, ?dtb) =
  ((ALL B. (B, ?A) : ?sub --> (ALL a b. ?P B (a, b))) -->
   (ALL dtaa dtbb.
      heightDT dtaa + heightDT dtbb < heightDT ?dta + heightDT ?dtb -->
           ?P ?A (dtaa, dtbb)) -->
  ?P ?A (?dta, ?dtb))"

We could of course generalise this by replacing heightDT by any natural number function, which may be differrent for trees on the left and right sides. Indeed it could be further generalised to any well-founded relation on pairs of derivation trees.

Each of these properties is successively weaker since the corresponding inductive assumption is stronger, hence P applies to a correspondingly wider class of derivations: as formalised next.

Lemma 11.4: For a property P, a formula A, a relation sub, and for a pair (dta, dtb) of derivations:

 (a) gen_step2_tr implies height_step2_tr
 (b) height_step2_tr implies sumh_step2_tr
gs2_tr_height: "gen_step2_tr ?P ?A ?sub (?dta, ?dtb) ==>
   height_step2_tr ?P ?A ?sub (?dta, ?dtb)"
hs2_sumh: "height_step2_tr ?P ?A ?sub (?dta, ?dtb) ==>
   sumh_step2_tr ?P ?A ?sub (?dta, ?dtb)"

Accordingly we need the lemma that proving these step results is sufficient for only the weakest of them.

Lemma 11.5 (sumh step2 tr lem): For a property P and a formula A in the well-

founded part of a relation sub, if sumh_step2_tr P A sub (dta, dtb) holds

for all derivations dta and dtb then P A (dtaa, dtbb) holds for all derivations

dtaa and dtbb:
sumh_step2_tr_lem: "[| ?A : wfp ?sub ;
   ALL A dta dtb. sumh_step2_tr ?P A ?sub (dta, dtb) |] ==>
   ?P ?A (?dtaa, ?dtbb)"

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” of their theorem only discusses one actual transformation, and in particular 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

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 require atoms, and that there are only rules for □ formulae with ♢φ interpreted as ¬□¬φ. The rules of the calculus are shown in Figure 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: For all sets A and all unary predicates P, the property Ball A P holds iff every member of A satisfies P:

Ball_def: "Ball ?A ?P == ALL x. x : ?A --> ?P x"

Definition 12.2: A set of rules rls satisfies ext_concl iff: for every list of premises ps and conclusion c that form an extended rule instance of some 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:

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}

inductive "lksne" intros
axiom : "([], {#A#} |- {#A#}) : lksne"
ilI   : "psc : lksil ==> psc : lksne"
irI   : "psc : lksir ==> psc : lksne"
inductive "lksss" intros
extI : "psc : lksne ==> pscmap (extend flr) psc : lksss"
inductive "lkrefl" intros
I : "([{#A#} + {#Box A#} |- {#}], {#Box A#} |- {#}) : lkrefl"
inductive "lkbox" intros
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: Sequent calculus GS4 for S4.

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'}"

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"

Lemma 12.2: The set of rule gs4_rls satisfies ext_concl.

gs4_ext_concl: "ext_concl gs4_rls"

Lemma 12.3: The rules of S4 satisfy weakening admissibility.

gs4_wk_adm: "wk_adm gs4_rls"

Proof: The lemma wk_adm_ext_concl is simple enough to prove simply by the MOVE TO proof of Lemma 12.1 induction principle shown above for derrec. 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. Q.E.D.

Same as Lemma 11.4. Have I misunderstood something? DELETE Theorem 12.1 (weakening for GS4): Weakening is admissible for GS4:

wk_adm gs4_rls

Proof: This follows from the fact that all rules in gs4_rls allow arbitrary contexts in their conclusion. That is, from the fact that gs4_rls satisfies

ext_concl. Q.E.D.

12.3 Invertibility 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.3 (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) holds iff: if, assuming that every premise in ps is in derivs, 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: (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.4: For all rule sets rls, for all rule sets irls, for all rules (ps, concl),

inv_stepm drls irls (ps, concl) holds iff: irls-inverses of concl are deriv-

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

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

Lemma 12.4: 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.5: For every set drls of rules and every set prems of sequents, the function (derrec drls prems) returns the set of sequents derivable from prems 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 prems:

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

Lemma 12.6 (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 using derrec, 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.7: 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.8: 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.6, it suffices to prove (inv_step (derrec gs4_rls {}) lksss) psc

for every rule psc from gs4_rls. By Lemma 12.5, it suffices to prove inv_stepm gs4_rls lksss psc for every rule psc from gs4_rls: We proceed by cases on the rule psc from gs4_rls, noting that lksss == extrs lksne: the rule set lksne extended with arbitrary contexts.

Where the rule psc is Refl:

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

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.4 to obtain

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

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 arbitrary

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.2 (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. 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.3 (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 what is G3cp? manner as in the literature (see [?] and [?]) using the invertibility results above. The formalisation performs the necessary transformations using the induction principle gen step lem of Theorem 10.1. actually uses

theorem

                                                               gen ctr adm step

which involves the predicate

                                                               ctr adm step,

but these are simple instantiations of

                                                               gen step and
                                                               gen step lem

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.

27

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. (DON’T UN-DERSTAND!)

Γ, □Γ ⊢ φ 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 on height, and then on rank. The S4□ rule can then be applied to Doesn’t need

height, just induction on the derivation, ie, assuming ctradm applies to premises of last rule. Given the discussion in §11 we should be precise on this 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.

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

Proof: The two most difficult cases to consider correspond to when the cutformula is principal below an application of the S4□ rule on the left, and also principal 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 2 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 sumh step2 tr lem is actually required. As the combined height of Surely we have

to use the same principle throughout? In all the other cases

                                                                    gen step2sr lem

would have sufficed. So in fact all the other cases prove

                                                                    gen step2sr,

and use the theorem

                                                                    gs2 car sumhs tr

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. Q.E.D.

THEOREM referred to in marginal note
(combines Lemmas 11.3 and 11.4)
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)"

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

The rules of the sequent calculus for S4.3 are listed in Figure 3. The calculus is based on the structural 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, the rule will be represented in the following form shown below at left:

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

Σ, □Γ ⊢ □Φ⃗, Δ

Axioms

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

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

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. In order to simplify the case for the S4.3□ rule and its multiple premises, weakeningadmissibility 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.

wk adm single antec rls

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

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

Like S4, we prove inversion lemmas for the G3cp and Refl rules within the overall calculus. The only notable case occurs for the G3cp rules, where the last rule applied in the original derivation is S4.3□. 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

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

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.

Before, for S4, proving invertibility is sufficient to lead to a contractionadmissibility 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 height, for all Γ and Δ. 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. Like 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 clarify, 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: 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:

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

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

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

Proof: 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 new sequents D_{L} and D_{R} have the same height as the original cut-sequents.

\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 and the next describe Isabelle proofs of the cut admissibility of the logic GTD described in [10] Axiomatically, GTD is K with the additional axiom □A ⇔ □□A. The sequent inference rules involving □ 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"

The second clause for glssc takes the rules in glne and adds a context This needs to (the same context) to the conclusion and all premises. This means that the be fixed! logical rules with two premises are of the context-sharing form. The following definitions explain this further where pscmap uniformly applies a function f to each of the premises in the list ps and to the conclusion c, while extend extends a given sequent seq of the form Γ ⊢ Δ with a sequent XY of the form X ⊢ Y built out of arbitrary contexts X and Y to give the extended sequent seq + XY of the form Γ, X ⊢ Δ, Y:

primrec pscmap_def "pscmap f (ps, c) = (map f ps, f c)"
defs extend_def : "extend XY seq == seq + XY"

15 GTD without structural rules CHANGE TITLE

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 2. JED please

check verbatim code!

Definition 15.1: 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"

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 gtdns for the logic GTD is obtained by extending only the conclusion of the rule GTD and by extending every rule of lknse:

            gtdns == lkssx (extcs GTD)

First we prove weakening admissibility. It follows directly from

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

which is proved in the same way that weakening admissibility is proved for S4.

For contraction admissibility, first we need to prove invertibility of the logical rules.

SIMILAR to S4. Uses

lks_inv_stepm:
val it = "?psc : extrs lksne ==> inv_stepm (extrs lksne) (extrs lksne) ?psc"
inv_stepm_disj_cs:
  "[| seq_meet ?c ?ic = 0; extcs {(?ps, ?c)} = ?rls; ?rl : ?rls |] ==>
  inv_stepm ?rls (extrs {(?ips, ?ic)}) ?rl"
inv_stepm_disj:
   "[| seq_meet ?c ?ic = 0; extrs {(?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"

The results inv stepm disj cs and inv stepm disj 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.

The result inv stepm scrls (whose proof uses inv stepm disj) 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 15.1: Every rule of lksss is invertible in the calculus gtdns_rls:

       gtdns_inv_rl: "Ball lksss (inv_rl gtdns_rls)"

Then, to prove contraction admissibility, SIMILAR to S4

we use

ctxt_ctr_adm_step1_cs: "[| pg_meet ?concl (?As + ?As) <= ?As;
  ?rl = (?ps, ?concl); (?ps, extend ?flr ?concl) = ?erl;
  extcs {?rl} <= ?rules |] ==> ctr_adm_step1 (derrec ?rules {}) ?erl ?As"

to handle the case where at least one of the copies of the formula to be contracted arises from the extension of the conclusion of the box rule.

ctr adm step1 is a simplified version of ctr adm step, without the inductive hypothesis relating to smaller formulae.

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

Since the proof is effectively the same whichever of the two rules is on the right, we define

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

and we prove the two results

s4_box_box_lem:
   "[| ?prsl = (%B. {B}); wk_adm ?drls; All (ctr_adm ?drls);
         extcs (s4g ?prsl) <= ?drls; extcs (s4g ?prsr) <= ?drls;
         (map conclDT ?dtll, ?cl) : extcs (s4g ?prsl);
         (map conclDT ?dtlr, ?cr) : extcs (s4g ?prsr) |]
      ==> sumh_step2_tr (prop2 casdt ?drls) ?A ipsubfml
       (Der ?cl ?dtll, Der ?cr ?dtlr)"
gtd_box_box_lem:
   "[| ?prsl = (%B. {Box B}); wk_adm ?drls; All (ctr_adm ?drls);
         extcs (s4g ?prsl) <= ?drls; extcs (s4g ?prsr) <= ?drls;
         (map conclDT ?dtll, ?cl) : extcs (s4g ?prsl);
         (map conclDT ?dtlr, ?cr) : extcs (s4g ?prsr) |]
      ==> sumh_step2_tr (prop2 casdt ?drls) ?A ipsubfml
       (Der ?cl ?dtll, Der ?cr ?dtlr)"

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

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 the general result

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

This theorem (which incorporates the parametric cases) uses c8 ercas prop which says essentially that if both sides of the cut are logical introduction rules, and cut is admissible on smaller cut-formulae, then the cut in question is admissible. The property c8sg prop is almost identical — the difference is weakening / contraction.

(LATER - on looking back at the previous section I find the result gprstep q shown - basically that result plus the case of the axiom rules gives you gen lksne c8sg below)

Omitting the definition of c8 ercas prop, here is the theorem which uses it:

c8_ercas_gs2: "[| c8_ercas_prop ?psubfml ?drls ?A ?c8rls;
  ?prl = (?ps, 0 |- {#?A#}); ?prl : ?c8rls;
  ?qrl = (?qs, {#?A#} |- 0); ?qrl : ?c8rls;
  ?eprl = pscmap (extend ?pe) ?prl; ?eqrl = pscmap (extend ?qe) ?qrl |] ==>
  gen_step2sr (prop2 car ?drls) ?A ?psubfml ?drls (?eprl, ?eqrl)"
c8sg_ger: "c8sg_prop ?sub ?rls ?drls ?A ==> c8_ercas_prop ?sub ?drls ?A ?rls"

The key property here is that

gtdns_lksne_c8sg: "c8sg_prop ipsubfml (lkssx (extcs GTD)) ?A lksne"

which in turn uses the more general result which is not specific to GTD

gen_lksne_c8sg: "[| All (ctr_adm ?drls); wk_adm ?drls; extrs lksne <= ?drls |]
         ==> c8sg_prop ipsubfml lksne ?drls ?A"

Finally we get the cut admissibility result:

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

16 Dynamic Topological Logic: the system S4C (without structural rules)

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

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.

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, Γ ⊢ Δ}(□ ⊢)

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?

Weakening admissibility was straightforward using Lemma 12.1.

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

We then prove contraction admissibility. In part this also makes use of the general result (NOTE - also used in S4, but not by Jesse as I hadn’t done this by then)

This uses predicates and results very similar to Definition 10.1 and Lemma 10.1, but instantiated to apply to the property of contraction admissibility.

gen_ctr_adm_step: "[| ?A : wfp ?sub;
       ALL dt. ALL (ps, concl):?rules.
               ctr_adm_step ?sub (derrec ?rules {}) (ps, concl) dt |]
      ==> ctr_adm ?rules ?A"
ctr_adm_step_eq: "ctr_adm_step ?sub ?derivs (?ps, ?concl) ?A =
  (ALL As.  ms_of_seq As = {#?A#} -->
    (ALL A'.  (A', ?A) : ?sub --> (ALL As.  ms_of_seq As = {#A'#} -->
      (ALL XY.  XY : ?derivs --> As + As <= XY --> XY - As : ?derivs))) -->
    (ALL p:set ?ps. p : ?derivs & (As + As <= p --> p - As : ?derivs)) -->
    As + As <= ?concl --> ?concl - As : ?derivs)"

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

Lemma 16.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: that is, 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:

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"

To prove cut 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 §??, 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 ns. 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_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}Y, V (where this is the derivation tree on the left of a desired cut), or within U, ∘^{k}X (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 the lemmas s4cns cs param l'' and s4cns cs param r''.

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

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

   Lemmas s4cns param l' and s4cns param r' cover this case.
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 the property c8ger prop mentioned in §??. 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.

s4cns_c8: "c8ger_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.

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

References

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

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

[3] J E Dawson and R Goré. Embedding display calculi into logical frameworks: Comparing Twelf and Isabelle. ENTCS 42, 89–103. 2001. Elsevier.

[4] J E Dawson and R Goré. Formalised Cut Admissibility for Display Logic. In Proc. TPHOLS’02, LNCS 2410, 131–147, Springer, 2002.

[5] A Gacek. The Abella interactive theorem prover (system description) In Proc. IJCAR 2008 LNCS 5195:154-161, Springer, 2008.

[6] M J C Gordon and T F Melham. Introduction to HOL: a Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993.

[7] R Goré. Invited talk in the Third Indian Conference on Logic and its Applications, Chennai, January 2009.

[8] R Goré and R Ramanayake. Valentini’s Cut-elimination for Provability Logic Resolved. Proc. AiML 2008, pp 67-86, College Publications http:

//users.rsise.anu.edu.au/~rpg/publications.html

[9] D Leivant. On the Proof Theory of the Modal Logic for Arithmetic Provability. Journal of Symbolic Logic, 46:531538, 1981.

[10] Grigori Mints. Two Examples of Cut-Elimination for Non-classical Logics. (talk, set of slides). Jägerfest, Bern (?), December 2013

[11] A Moen. The proposed algorithms for eliminating cuts in the provability calculus GLS do not terminate. NWPT 2001, Norwegian Computing

Center, 2001-12-10 http://publ.nr.no/3411

[12] T Nipkow, L C. Paulson, and M Wenzel. Isabelle’s logics: HOL. Technical report. 15 February 2001, doc/logics-HOL.dvi in the Isabelle distribution.

[13] L C. Paulson. The Isabelle reference manual. Technical report. 15 February 2001, doc/ref.dvi in the Isabelle distribution.

[14] F Pfenning. Structural cut elimination. In Proc. LICS 94, 1994.

[15] D. Pym and J. Harland. A Uniform Proof-theoretic Investigation of Linear Logic Programming. J. of Logic and Computation 4:2:175-207, 1994.

[16] F Pfenning and C Schrmann. System description: Twelf — a meta-logical framework for deductive systems. In Proc. CADE-16, pages 202–206, Springer-Verlag LNAI 1632.

[17] R M Solovay. Provability Interpretations of Modal Logic. Israel Journal of Mathematics, 25:287304, 1976.

[18] S Valentini. The Modal Logic of Provability: Cut-elimination. Journal of Philosophical Logic, 12:471476, 1983.

[19] H Wansing. Displaying Modal Logic, volume 3 of Trends in Logic. Kluwer Academic Publishers, Dordrecht, August 1998.