Structural Rule Admissibility for S4 and S4.3

Jesse Wu

November 17, 2014

1 Isabelle Framework

COMBINE THIS SECTION WITH JEREMY’S STUFF

TODO: perhaps begin with shallow stuff below, then bring in Jeremy’s section 2. or start with Jeremy’s section 2, cover mix for GTD, then move to S4, and then introduce shallow stuff for weak/inv/ctr proofs. not sure how to organise this.

Meta-level proofs generally follow an inductive procedure on derivations. However, many transformations do not actually require use of the height of an original derivation Π in creating some new derivation, they only refer to the endsequents derived by Π. In particular, an induction on height can often be mimicked by an induction on rule applications. Rather than using an actual derivation tree, where the induction hypothesis is applied on a sub-tree of height n, it is normally simpler in a formal proof to deal only with the last rule, where the induction hypothesis is applied on the premises of that rule.

This leads to a shallow embedding of derivations, as inductively defined sets:

consts derrec :: "'a psc set => 'a set => 'a set"

where derrec rls prems is the set of sequents derivable using the rules rls from a set prems of premises. Formally this is encoded as:

  c ∈ prems ⟹ c ∈ derrec rules prems
 [| (ps, c) ∈ rules ; ps ⊆ derrec rules prems |] ⟹ c ∈ derrec rules prems

Shallow embeddings will be used for many of the formalised proofs in this work. These have the advantage of simplifying representations of derivations and also the proofs themselves.

As the shallow embedding of derivations uses inductively defined sets, Isabelle provides an induction principle for proving properties for such derivations. A slightly simplified version is used as a basis for proving results about weakening-admissibility and invertibility.

Lemma 1.1 (drs.inductr).

For a derivable sequent x ∈ derrec rls prems, if property P holds for all initial sequents prems (such initial assumptions are always empty for this work), and also for all (ps, c) ∈ rls it can be shown that ∀p ∈ ps. P p implies P c, then P x also holds.

Lemma 1.1 essentially replaces the standard pen and paper induction on height, with an induction on rule applications – if every rule preserves a property P from premises to conclusion, then so does the whole derivation. The downside of this principle is that there is never an explicit derivation tree, only the exact premises of a rule application are accessible, so transforming sub-trees in some height-preserving way is impossible. Nevertheless, this principle is sufficient to prove weakening-admissibility for the class of sequent calculi which allow arbitrary contexts in the conclusion of all rules.

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 1.1 (gen step). For a formula A, a property P, a subformula relation sub, a set of rules rls, a set of rls-derivable sequents derivs (e.g. derrec rls prems), and a particular rule r = (ps, c),

   gen step P A sub rls derivs r means:

if forall A′ such that (A′, A) ∈ sub and all rls-derivable sequents D the property P A′ D holds and for every premise p ∈ ps both p ∈ derivs and P A p holds

then P A c holds.

In English, this step condition states that if a property P is true 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 1.1 below, states that if this step case can be proved for all possible rule instances then P holds for all cases.

Theorem 1.1 (gen step lem).

if item A is in the well-founded part of the subformula relation sub and sequent S is rls-derivable and for all formulae A′, all possible rules r in rls, and all rls-derivable sequents derrec rls {}, the induction step condition gen step P A′

sub (derrec rls {}) r holds

then P A S holds.

1.1 Weakening, Invertibility and Contraction

Weakening admissibility, invertibility, and contraction-admissibility are stated using wk adm, inv rl and ctr adm respectively:

wk adm rls

This states that Weakening is admissible for rls. In particular, for any rls-derivable sequent S, the addition of any other sequent As to this is also rls-derivable. Formally, given S ∈ derrec rls {} then S + As ∈ derrec rls {}. This is part of the base formalisation.

inv rl rls (ps, c)

Given a rule instance (ps, c), within a particular calculus rls, inv rl holds if whenever c is rls-derivable, then all the premises ps are also rls-derivable.

ctr adm rls A

Contraction-admissibility is given as a property for a set of rules rls, and a single contraction-formula A: for all sequents As, if the only formula in As is equal to A then for all rls-derivable sequents S where As + As is a sub-sequent of S, it holds that S−As is also rls-derivable.

1.2 Cut

NEED JEREMY’S STUFF FOR CUT BASED ON DEEP TREES HERE ... TODO: could introduce the following in the proof for Cut for S4, if we want

to intertwine the formalisation and pen and paper stuff more.

For a cut-formula A, cut-admissibility is expressed as:

(Xl |- mins A Yl, mins A Xr |- Yr) :  cas rls A)

The property name is cas, and rls once again represents a calculus (set of rules). mins is multiset insertion, while X and Y for both the left and right represent arbitrary multisets. The pair of sequents in the cut-admissibility statement then simply correspond to two potential premises for an application of the Cut rule. The definition of cas states that if both these left and right sequents are rls-derivable, then so is the sequent, (Xl + Xr |- Yl + Yr), which would result from applying Cut on A.

In addition to the height step2 tr eq lemma, we also use the following induction principle, named sum step2 tr. The assumption now is that the inductive property holds for two new derivations, where some well-founded measure on the new derivations is strictly less than the same measure on the derivations leading to C_{l} and C_{r}. For Cut, this measure will be derivation height. Essentially, cut-admissibility of new derivations can be assumed, as long as their combined height is less than the level of the original cut-sequents C_{l} and C_{r}.

Definition 1.2 (sum step2 tr). For a formula A, a property P, a subformula relation sub, measures on derivation trees gsl and gsr, and explicit derivation trees dta and dtb,

   sum step2 tr P A sub gsl gsr (dta, dtb) means:

if forall A′ such that (A′, A) ∈ sub the property P A′ (a, b) holds for all derivation trees a and b and for all derivation trees dta' and dtb' where

     gsl dta' + gsr dtb' < gsl dta + gsr dtb

the property P A(dta′, dtb′) holds

then P A (dta, dtb) holds.

Instantiating the measures in sum step2 tr with measures of derivation height results in the final principle used to prove cut-admissibility:

Theorem 1.2 (sumh step2 tr lem).

Where heightDT dt gives the height of an explicit derivation tree dt.

if A is in the well-founded part of the subformula relation sub and for all formulae A', and derivation trees dta and dtb

     the induction step condition sum step2 tr P A' sub heightDT heightDT
     (dta, dtb) holds
then P A (dta, dtb) holds

2 S4

2.1 Related Work

TODO: how much background do we want?

There exist both pen and paper ?? and a formalised proof ? of mixelimination for sequent calculi describing S4 which include explicit Weakening and Contraction rules. 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, Δ, Δ′

? acknowledges the problem posed by absorbing Weakening into the R□ rule. However, the solutions discussed are given in the context of typed λ-calculi for a minimal version of S4, interpreted as 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.

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

2.2 Calculus

The sequent calculus we use for S4 is based on the calculus G3cp, with the addition of two modal rules. Note that the axiom does not require atoms, and that there are only rules for □ formulae with ♢φ interpreted as p_{0} ∧ ¬p_{0}. The rules of the calculus are shown in Figure 1.

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.

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"

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}  \begin{aligned}& Γ, □Γ ⊢ φ \\ S4□ \\ & Σ, □Γ ⊢ □φ, Δ \end{aligned}

Figure 1: Sequent calculus for S4.

  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  : "(p, c) : lkbox ==> (p, extend flr c) : gs4_rls"

2.3 Results

Theorem 2.1 (gs4 wk adm). Weakening is admissible for gs4 rls.

Proof. This follows from the fact that all rules allow arbitrary contexts in their conclusion. ⊣

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

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, Δ′, φ, ψ

⊣

Theorem 2.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 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 1.1.

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

In the former case, 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 is (where either □φ = A or A ∈ Δ):

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

Applying the S4□ rule without introducing the second copy of A in the context gives a proof of Σ, □Γ ⊢ □φ, Δ as required (note A is still in the succedent as □φ = A or A ∈ Δ). Similarly, if A is in the context Σ the new S4□ rule is then:

Γ, □Γ ⊢ φ 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 is thus represented by:

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 give the required 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. ⊣

Theorem 2.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 there 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 ?.

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

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

In the formalised proof, this instance is the only case where the inductive principle sumh step2 tr lem is actually required. As the combined height of the derivations leading to □Γ_{L} ⊢ □A and A, □A, Γ_{R}, □Γ_{R} ⊢ B is lower than the level of the original Cut, the induction hypothesis on level can be applied. ⊣

3 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 ? and ? are perhaps the closest representatives in the literature. As noted in Section 2.1, 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.

3.1 Calculus

The rules of the sequent calculus for S4.3 are listed in Figure 2. Note, in the S4.3□ rule of Figure 2, 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

\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□ Σ, □Γ ⊢ □Φ⃗, Δ

Figure 2: Sequent calculus for S4.3.

of these premises will be shown as a representative for all n premises. That is, the rule will be represented in the following form:

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

There are two different versions of the S4.3□ rule. Either the context (Σ and Δ) can contain any formulae, or they cannot include top-level Boxes. 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 nonboxed version is preferred as it does not require backtracking.

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

(* 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.
   "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 overall S4.3 calculus, as an extension of the LK calculus *)
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  : "(p, c) : lkbox ==> (p, extend (nboxseq flr) c) : gs4_rls"

Figure 3: S4.3 calculus as encoded in Isabelle

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

Theorem 3.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:

\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, Δ′

⊣

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

Theorem 3.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 a 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 to produce the following transformation:

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

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

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

⊣

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

3.4 Cut

Theorem 3.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. ⊣