Bounded Sequent Calculi for Non-classical Logics via Hypersequents

Abstract

Using substructural and modal logics as case studies, a uniform method is presented for transforming cut-free hypersequent proofs into sequent calculus proofs satisfying relaxations of the subformula property. As a corollary we prove decidability for a large class of commutative substructural logics with contraction and mingle, and get a simple syntactic proof of a well known result: the sequent calculus for $\mathbf {S5}$ is analytic.

1 Introduction

In 1935, Gentzen introduced the sequent calculi $\mathbf {LJ}$ and $\mathbf {LK}$ for intuitionistic and classical logic as alternatives to the prevailing axiomatic systems. For this purpose, he replaced the rule of modus ponens in the latter with the more general cut rule. His motivation was to obtain the subformula property (also called analyticity) which asserts that a proof need only contain subformulas of the end formula. This was achieved by exploiting the additional structure in the sequent calculus formalism to show the redundancy of the cut rule. Analyticity yields a strong restriction on the proof search space and it is this that is the key for using a proof calculus to prove metalogical results (e.g. decidability, complexity, interpolation, disjunction properties) and for automated reasoning.

Unfortunately, the sequent calculus is not expressive enough to support analyticity for most logics of interest. The structural proof theoretic response has been the development of numerous exotic proof formalisms (e.g. hypersequent, nested sequent, display, labelled calculi, tree-hypersequent)—typically extending the syntax of the sequent calculus—with the aim of regaining analyticity via cut-elimination. The hypersequent calculus, introduced independently by Mints [19], Pottinger [22] and Avron [1], is one of the most successful such formalisms. Cut-free hypersequent calculi have been presented for many non-classical logics that resist an analytic sequent calculus formulation. Especially noteworthy are the uniform constructions of cut-free hypersequent calculi via structural/modal rule extensions for commutative substructural [6] and modal [13, 14, 16] logics.

Many non-classical logics possess a cut-free calculus in some exotic formalism but such calculi tend to be less useful than cut-free sequent calculi because the presence of the extended structure is a hinderance to proving metalogical results.

Here we propose an alternative: retain the sequent calculus and seek systematic relaxations of analyticity. Of course, most logics will have a sequent calculus with arbitrary cuts that is complete for it, but this does not meaningfully restrict the proof search space. Therefore what we seek here a restriction on the ‘quality’ of the cut-formula in terms of shape, complexity and composition. Such a cut-restricted sequent calculus will be called a bounded sequent calculus.

In this work we obtain bounded sequent calculi by transforming cut-free hypersequent calculi. This is a natural starting point: hypersequents are simple extension of sequents (in fact, just one step further); the existing uniform constructions of cut-free hypersequent calculi can be exploited to obtain a uniform method for constructing bounded sequent calculi; and, given the novelty and inherent technicalities in our proposal, there is an advantage in simplifying one aspect of the problem by starting from proofs that already possess a nice structure (i.e. cut-free hypersequent proofs). The bounded sequent calculi that we obtain in this way are novel: a consideration of the quality of cut-formulas has never been attempted for logics lacking an analytic sequent calculus.

Specifically, we present a methodology to uniformly transform cut-free hypersequent calculi for a large class of propositional non-classical logics (substructural, intermediate and modal logics) into bounded sequent calculi. As a corollary we obtain the decidability of all acyclic $\mathcal {P}_{3}'$-axiomatic extensions (c.f. the substructural hierarchy [6]) of the commutative Full Lambek calculus with contraction and mingle [11] (including, e.g., $\mathbf {UML}$ [18]). This implies the decidability of the equational theory of the corresponding classes of residuated lattices [8]. We also obtain a simple and new syntactic proof of a well-known result [7]: analyticity of the sequent calculus for the modal logic $\mathbf {S5}$. We note that the syntactic proof from the literature due to Takano [23] is highly intricate.

Related Work. Using algebraic methods, Bezhanishvili and Ghilardi [4] show that several modal logics satisfy the bounded proof property, a restriction on the modal complexity of formulas that need appear in a Hilbert-style proof. However all those logics already have well-known analytic sequent calculi. Bezhanishvili et al. [5] extend these methods to cut-free hypersequent calculi for intermediate logics. In particular, it is shown that is it possible to restrict hypersequent calculus proofs (with cuts) to proofs consisting of formulas whose implicational depth is bounded by the implicational depth of the endsequent. This is in the spirit of this work (systematic relaxations of analyticity), although here our aim is not only to restrict the formulas in the proof but to eliminate the hypersequent structure as well. Moreover, our methods apply also to substructural logics. Lahav and Zohar [15] establish syntactic criteria for determining if a pure sequent calculus has analyticity. They introduce a subformula property modulo leading negation symbols and provide a method for constructing analytic calculi for sub-logics of a base logic from simple derivable rules in the base calculus. In contrast, for us, relaxations of analyticity are the parameter for capturing extensions of the base logic. In this sense, analyticity is the lower-limit of our investigation: we are willing to give up analyticity in a carefully considered way, to preserve the sequent calculus formalism. Fitting [7] proved analyticity of the sequent calculus for several modal logics by logic-specific semantic argument and asked if the “theorems could be established by a more uniform approach”. Our methodology suggests that it may indeed be possible to obtain analyticity (and its relaxations) for modal logics in a uniform manner.

Fig. 1.

The single-conclusioned sequent calculus $\mathbf {FL_{e}}$

2 Preliminaries

In this paper we consider extensions of the commutative Full Lambek calculus $\mathbf {FL_{e}}$ (see Fig. 1), including intermediate and normal modal logics. The language of these logics may be inferred from their calculi. The connective $\cdot$ is called fusion (or multiplicative conjunction), e.g. [6, 8]. A sequent is a tuple $(\varGamma ,\varDelta )$ of formula multisets (written as $\varGamma \Rightarrow \varDelta$). It is single-conclusioned if $\varDelta$ contains at most one formula, and multi-conclusioned otherwise. Throughout, $\lnot A$ will abbreviate $A\rightarrow \bot$. $A,B,C,\ldots$ will be used for formulas/formula variables, $\varGamma ,\varDelta ,\varPi , \dots$ for formula multisets/formula multiset variables. $\varPi$ is taken to contain at most one formula. A $\varOmega$-instantiation of a formula A is a uniform substitution of the propositional variables of A by elements from the set $\varOmega$.

Rules and Rule Instances. An explicit distinction between a rule and a rule instance will be made only where required. An instance of a rule $(r)$ is denoted $\sigma (r)$, where $\sigma$ is a function mapping the structure variables in $(r)$ to concrete elements of the corresponding type. E.g. in an instance $\sigma (cut)$ of $(cut)$ (Fig. 1), $\sigma$ maps the multiset variables $\varGamma$ and $\varDelta$ to (possibly empty) multisets of formulas, the formula variable A to a formula, and the structure variable $\varPi$ to a multiset of formulas of size $\le 1$.

Axiomatic Extensions. Let $\mathbf {S}$ be a sequent calculus and $\mathcal {F}$ a set of formulas. $\mathbf {S}+\mathcal {F}$ denotes the extension of $\mathbf {S}$ with initial sequents $\{ \Rightarrow A| A\in \mathcal {F}\}$. Initial sequents are rules with no premises. Except in special cases, it is easily seen that $\mathbf {S}+\mathcal {F}$ fails cut-elimination even if $\mathbf {S}$ has cut-elimination.

Derivability. For a set $\mathcal {F}\cup \{S\}$ of sequents, $\mathcal {F}\vdash _{\mathbf {S}} S$ (resp. $\mathcal {F}\vdash ^{cf}_{\mathbf {S}} S$) denotes that S is derivable (resp. cut-free derivable) from $\mathcal {F}$ using the rule instances in $\mathbf {S}$. If $\mathcal {F}=\emptyset$, then we say that S is derivable (cut-free derivable) and write $\vdash _{\mathbf {S}}S$ ($\vdash _{\mathbf {S}}^{cf}S$). Note: $\mathcal {F}\vdash _{\mathbf {S}} S$ denotes a derivation from a fixed set $\mathcal {F}$. In contrast, substitution instances of $\mathcal {F}$ can be used in $\vdash _{\mathbf {S}+\mathcal {F}} S$.

Let $\mathrm {subf}(S)$ denote the set of subformulas in a formula/sequent S. For a multiset $\mathcal {F}$ of formulas, let ${\odot }\mathcal {F}$ be the fusion of all formulas in $\mathcal {F}$ (1 if $\mathcal {F}$ is empty). For sequent calculi where conjunction $\wedge$ and fusion $\cdot$ conflate (i.e. in the presence of contraction c and weakening w), we use just the single connective $\wedge$. Then ${\odot }\mathcal {F}$ is defined as a conjunction of all formulas in $\mathcal {F}$ ($\top$ if $\mathcal {F}$ is empty).

A bounding function is a map from a sequent to a set of formulas. In the following two definitions, $\mathbf {S}$ is a sequent calculus, g is a bounding function, S is an arbitrary sequent and $\mathcal {F}$ is a set of initial sequents of $\mathbf {S}$.

Definition 1

($g$-, $(g,\mathcal {F})$-bounded derivation). A derivation of S in $\mathbf {S}$ is

$g$-bounded if every formula in the derivation is a subformula of an instantiation of an initial sequent of $\mathbf {S}$ by formulas in $g(S)$.

$(g,\mathcal {F})$-bounded if it is $g$-bounded and additionally every cut rule instance and every initial sequent instance $\Rightarrow A$ from $\mathcal {F}$ occurs together as shown below, where A is a $g(\varGamma \Rightarrow \varPi )$-instantiation of a formula in $\mathcal {F}$.

Intuitively, $g$-boundedness is a global relaxed-analyticity property on the derivation. Meanwhile, $(g,\mathcal {F})$-boundedness specifies also that cuts and initial sequent instances of $\mathcal {F}$ occur together and only together, and that the cut-formula satisfies a local relaxed-analyticity property.

The particular relaxation of analyticity is determined by the bounding function $g$. In particular, a $g_{a}$-bounded derivation of S with $g_{a}(S)=\{A|A\in \mathrm {subf}(S)\}$ is essentially an analytic derivation (but not quite, since subformulas of the initial sequents may also occur).

The global/local relaxed analyticity properties are analogous to the global/local subformula properties considered in Kowalski and Ono [12].

Definition 2

($g$-, $(g,\mathcal {F})$-bounded sequent calculus). A sequent calculus $\mathbf {S}$ is $g$-bounded $\mathrm{((}g,\mathcal {F})$-bounded) if every sequent derivable in $\mathbf {S}$ has a $g$-bounded (resp. $(g,\mathcal {F})$-bounded) derivation.

A $g$ - or $(g,\mathcal {F})$-bounded derivation/sequent calculus for some $g$ and $\mathcal {F}$ is referred to as a bounded derivation/sequent calculus.

For an associative binary connective $\heartsuit$, define the bounding functions:

$$\begin{aligned}&g^{\heartsuit }(S):=\{ A_{1}\heartsuit \ldots \heartsuit A_{n} | A_{i}\in \mathrm {subf}(S)\} \\&g^{1 \heartsuit }(S):=\{ A_{1}\heartsuit \ldots \heartsuit A_{n} | A_{i}\in \mathrm {subf}(S),\,\, \text {and} \ \ A_{i}=A_{j} \ \ \text {iff} \ \ i=j\} \end{aligned}$$

Note that the set $g^{1 \heartsuit }(S)$ is always finite, whereas $g^{\heartsuit }(S)$ is not. As an example, $g^{1 \cdot }(p\Rightarrow q)=\{p,q,p\cdot q,q\cdot p\}$. A $g^{\heartsuit }$-bounded derivation of S would only contain subformulas of instantiations of the initial sequents by formulas of the form $A_{1}\heartsuit \ldots \heartsuit A_{n}$ where $A_{i}\in \mathrm {subf}(S)$. A $g^{1 \heartsuit }$-bounded derivation additionally requires that there is no repetition in $A_{1},\ldots , A_{n}$.

Hypersequent Calculi are a generalisation of sequent calculi. Each proof rule is built from hypersequents i.e. finite multisets of sequents $S_1\mid \ldots \mid S_n$. Each $S_i$ is said to be a component of the hypersequent.

Every sequent calculus $\mathbf {S}$ can be embedded into a hypersequent calculus $\mathbf {HS}$; replace each rule $(r)$ in $\mathbf {S}$ with $(Hr)$ (see below) where the new structure variable G can be instantiated with a hypersequent (possibly empty). In addition to the rules $(Hr)$, $\mathbf {HS}$ contains the structural rules of external weakening (ew) and external contraction (ec).

The embedding is conservative, i.e. no new sequents are provable in $\mathbf {HS}$.

Some axiomatic extensions of $\mathbf {S}$ cannot be captured analytically by extending $\mathbf {S}$ with sequent rules, but they can be captured analytically by extending $\mathbf {HS}$ with “proper” hypersequent rules that act on many sequents simultaneously.

Example 3

Let $\mathbf {lin}$ denote $(p\rightarrow q)\vee (q\rightarrow p)$. A sequent calculus for propositional Gödel logic is obtained by adding $\Rightarrow \mathbf {lin}$ to Full Lambek calculus with exchange, contraction and weakening (denoted $\mathbf {FL_{ecw}}$, or $\mathbf {LJ}$). Cut is ineliminable. A cut-free hypersequent calculus is obtained by adding $(com)$ [2] to $\mathbf {HLJ}$.

Several [3, 13, 21] cut-free hypersequent calculi for $\mathbf {S5}$ have been given. E.g. in [3], a cut-free hypersequent calculus for $\mathbf {S5}$ is obtained by adding $(MS_{Av})$ to $\mathbf {HS4}$.

In the above examples, the structure variable G is called the context. The remaining components in the rule are called the active components.

3 A Guided Example Demonstrating the Methodology

We demonstrate by transforming a cut-free hypersequent derivation $d_{h}$ of $\Rightarrow F$ in $\mathbf {HLJ}+(com)$ into a bounded sequent derivation $d_{s}$ of $\Rightarrow F$ in $\mathbf {LJ} +\mathbf {lin}$ through an example. Assume that $d_{h}$ contains a single instance of (com) above an instance of (ec). Then it has the following form:

Construct the sequent derivation $d_{s}$ as follows, utilising portions of $d_{h}$:

The cut formula $\alpha$ is $\sigma (\mathbf {lin})$ where $\sigma (p)=\wedge {\varGamma _{2}}$ and $\sigma (q)=\wedge {\varGamma _{1}}$. Since $d_{h}$ is cut-free: $\varGamma _{1}\cup \varGamma _{2}\subseteq \mathrm {subf}(F)$. So $d_{s}$ is a $g^{ \wedge }$-bounded derivation. By construction, the cut-rule occurs together with and only with the $\mathbf {lin}$ initial sequent instance. Furthermore, again because $d_{h}$ is cut-free: $\varGamma _{1}\cup \varGamma _{2}\subseteq \mathrm {subf}(\varGamma '\cup \varPi ')$. Thus a stronger result holds: $d_{s}$ is a $(g^{ \wedge },\{ \mathbf {lin} \})$-bounded derivation.

4 The Disjunction Form of a Rule: A Formal Definition

Let us summarise the idea in the previous section. Given a cut-free hypersequent derivation of $\Rightarrow F$, we aim to obtain a sequent calculus derivation of each component of each hypersequent in it. If the hypersequent derivation contains an instance of a “proper” structural rule $(r)$, the sequent calculus derivation is forced to append to the LHS of its $i^{\text {th}}$ active conclusion component a suitable formula $D_{i}$. The formula $\vee _{i} D_{i}$ can be defined explicitly (Definition 9) from the form of $(r)$ such that it satisfies (Theorem 12) the properties of a disjunction form (Definition 5), which is formally defined in this section; these conditions make the transformation work. E.g. (provability) guarantees that $\vee _{i} D_{i}$ is no stronger than the axiom corresponding to $(r)$. Thus $\Rightarrow \vee _{i} D_{i}$ is used as an initial sequent without extending the logic. The disjunction form formulas are eliminated at the bottom of the sequent calculus derivation of $\Rightarrow F$ via bounded cuts on these initial sequents.

Definition 4

For a multiset $\varDelta$ of formulas, define $\varDelta \# (\varGamma \Rightarrow \varPi )$ as $\varDelta , \varGamma \Rightarrow \varPi$.

Let $\varGamma _{1},\ldots ,\varGamma _{m}$ be the structure variables in a hypersequent rule $(r)$; associate with each $\varGamma _{i}$ a propositional variable $\widehat{\varGamma } _{i}$. Given an instantiation $\sigma$ on $(r)$, define the extended instantiation $\widehat{\sigma }$ which maps each $\widehat{\varGamma } _{i}$ to the formula ${\odot }\sigma (\varGamma _{i})$.

Definition 5

(disjunction form of a rule). Let $\mathbf {H}$ be a hypersequent calculus and $(r)$ a hypersequent rule with set $\mathcal {H}$ of premises and conclusion $G|S_{1}|\ldots |S_{n}$ built from the structure variables $\varGamma _{1},\ldots ,\varGamma _{m}$. A formula $A_1\vee \ldots \vee A_n$ built from the propositional variables $\widehat{\varGamma } _{1},\ldots ,\widehat{\varGamma } _{m}$ is a disjunction form of $(r)$ if:

• (splitting) For every rule instance $\sigma (r)$ and every $i\le n$:

  $$ \sigma (\mathcal {H})\vdash ^{cf}_{\mathbf {H}}\sigma (G\mid \widehat{\sigma } (A_{i})\# S_i) $$

• (provability) $\vdash _{\mathbf {H} +(r)} A_1\vee \ldots \vee A_n$

We use the term “splitting” because the condition asserts that we can split the active components of a structural rule instance: the $i^{\text {th}}$ active component $\sigma (S_{i})$ appended with the disjunct $\widehat{\sigma } (A_{i})$ in the antecedent is cut-free derivable from the premises of the rule without using $(r)$. In effect:

There are pathological ways to obtain (splitting), for example by setting each $A_{i}$ as $\bot$. Such formulas are ruled out by the (provability) condition.

Example 6

$(\widehat{\varGamma } _2\rightarrow \widehat{\varGamma } _1)\vee (\widehat{\varGamma } _1\rightarrow \widehat{\varGamma } _2)$ is a disjunction form of (com) in Eg. 3.

5 Disjunction Forms for Commutative Substructural Logics

We show how to compute a disjunction form of analytic rules for substructural logics. The logics we consider are extensions of $\mathbf {FL_{e}}$ by axioms in the class $\mathcal {P}_{3}$ ($\mathcal {P}_{3}'$) of the substructural hierarchy [6]. Recall that the class $\mathcal {P}_{3}'$ is a modification of $\mathcal {P}_3$ used in absence of weakening. Let us write $B_{\wedge 1}$ to denote $B\wedge 1$. For $A =A_1 \vee \dots \vee A_n$ (head connective of $A_{i}$ is not disjunction), set $A^{\vee }:=(A_1)_{\wedge 1} \vee \dots \vee (A_n)_{\wedge 1}$ and let $\mathcal {P}_{3}':=\{ A^{\vee } | A \in \mathcal {P}_{3} \}$. Let $\mathcal {F}^{\vee }$ denote $\{A^{\vee }| A\in \mathcal {F}\}$.

Definition 7

(amenable). A set $\mathcal {F}$ of formulas is amenable if (i) $\mathcal {F}\subseteq \mathcal {P}_{3}$ and contains weakening $p\cdot q\rightarrow p$, or (ii) $\mathcal {F}\subseteq \mathcal {P}_{3}'$ consists of acyclic formulas.

The interest in amenable axiomatic extensions is that they admit a cut-free hypersequent calculus. This result is established in [6] and summarised below.

Theorem 8

([6]). From every finite set $\mathcal {F}$ of amenable formulas, a finite set $\mathcal {R}_{\mathcal {F}}$ of (‘analytic’) structural hypersequent rules can be computed such that

$$\begin{aligned} \textit{for every sequent} \ S: \;\; \vdash _{\mathbf {FL_{e}}+ \mathcal {F}} S \ \textit{if and only if} \ \ \vdash ^{cf}_{\mathbf {HFL_{e}}+ \mathcal {R}_{\mathcal {F}}} S \end{aligned}$$

E.g., $\mathcal {F}=\{p\cdot q\rightarrow p,\mathbf {lin}\}$ is an amenable set of formulas and $\mathcal {R}_{\mathcal {F}}$ is the set containing the rules of weakening and (com) (Example 3); hence $\mathbf {HFL_{ew}}+(com)$ is a cut-free hypersequent calculus for $\mathbf {FL_{ew}}+\mathbf {lin}$. Likewise, the set $\mathcal {F}'=\{\mathbf {lin}^{\vee }\}$ is amenable (where $\mathbf {lin}^{\vee }= (p\rightarrow q)_{\wedge 1}\vee (q\rightarrow p)_{\wedge 1}$), $\mathcal {R}_{\mathcal {F}'}$ is the rule $(com)$, and so $\mathbf {HFL_{e}}+(com)$ is a cut-free hypersequent calculus for $\mathbf {FL_{e}}+\mathbf {lin}$.

Analytic structural hypersequent rules have one active component in each premise and additionally satisfy the following properties.

• (linear conclusion) All structure variables in the conclusion are distinct.

• (separation) No structure variable occurs both on the left hand side (LHS) and the right hand side (RHS) of a sequent.

• (coupling) For each conclusion component with variable $\varPi$ on the RHS there is a variable $\varSigma$ on the LHS such that the pair $(\varSigma ,\varPi )$ always occur together in the premises.

• (subformula property) Each variable in the premise occurs in the conclusion.

Computing the Disjunction Form of an Analytic Rule. Select exactly one structure variable occurrence in the active component of each premise (‘distinguished variable occurrence’). This induces an association of the distinguished variable (and the premise it is contained in) to the unique conclusion component containing this variable. We furthermore stipulate that every variable $\varSigma$ that is coupled (i.e. as $(\varSigma ,\varPi )$ for some $\varPi$) is chosen as distinguished.

Fig. 2.

Association form. $\mathcal {S},\mathcal {T},\mathcal {U},\mathcal {V},\mathcal {W}$ denote multisets of structure variables. The distinguished variable occurrences in the premises and their associated occurrences in the components of the conclusion are indicated in boldface. The index sets $I,L,J_i,M_{ij}$ and $N_{ij}$ are assumed to be pairwise disjoint.

The analytic rule together with the choice of distinguished variables can be pictured in association form (see Fig. 2). Observe that:

• A structure variable declared as distinguished in a premise with empty RHS may appear in a conclusion component with or without empty RHS.

• Distinct premises may be associated to the same conclusion component, although not necessarily due to the same distinguished variable.

• Some conclusion components with empty RHS might not be associated to any premise (captured by the possibility that $s_i=0$).

• The multisets $\mathcal {S},\mathcal {T}$ and $\mathcal {U}$ may contain further (non-distinguished) occurences of the distinguished variables $\varGamma$ and $\varDelta$, but no further occurences of $\varSigma$ due to the coupling property. The multisets $\mathcal {V}$ and $\mathcal {W}$ do not contain any further occurences of distinguished variables due to the linear conclusion property.

For a multiset $\mathcal {S}=\{\varGamma _1,\ldots ,\varGamma _n\}$ of structure variables, let $\widehat{\mathcal {S}}$ denote the multiset $\{\widehat{\varGamma } _1,\ldots ,\widehat{\varGamma } _n\}$ of propositional variables.

Definition 9

($\mathbf {Form}({r},{i})$). For a rule $(r)$ in association form (Fig. 2), let

Finally, let $\text {Form}(r):=\bigvee _{i\in I\cup L}\text {Form}(r,i)$.

Example 10

Here are association forms of three well-known structural rules. In (com), the choice of distinguished variables $\varSigma _{1}$ and $\varSigma _{2}$ is determined by the coupling property. In (lq) and (wc), we could also have chosen $\varGamma$ resp. the second occurence of $\varDelta$ as distinguished.

Example 11

Consider the (com) rule from Example 10. Pattern-matching the rule with Fig. 2 we obtain: $I=\{1,2\}$, $L=\emptyset$, $\mathcal {V}_1=\{\varGamma _2\}$, $\mathcal {V}_2=\{\varGamma _1\}$, $J_1=J_2=\{1\}$, $\mathcal {S}_{11}=\{\varGamma _1\}$, $\mathcal {S}_{21}=\{\varGamma _2\}$, $r_1=r_2=0$:

So $\text {Form}(com) =(\widehat{\varGamma } _2\cdot 1\rightarrow \widehat{\varGamma } _1)_{\wedge 1}\vee (\widehat{\varGamma } _1\cdot 1\rightarrow \widehat{\varGamma } _2)_{\wedge 1}.$ Also:

$$\begin{aligned} \text {Form}(lq) =(\lnot (1\cdot (\widehat{\varDelta } \wedge \lnot \widehat{\varGamma })))_{\wedge 1}\vee (\lnot (\widehat{\varGamma } \cdot 1))_{\wedge 1}&\text {Form}(wc) =(\lnot (1\cdot (\widehat{\varDelta } \wedge \lnot \widehat{\varDelta })))_{\wedge 1} \end{aligned}$$

Theorem 12

$\text {Form}(r)$ is a disjunction form of the analytic rule $(r)$.

Proof

Given an analytic rule $(r)$, obtain $\text {Form}(r)$ from its association form. We require (c.f. Definition 5) (i) provability, i.e. $\vdash _{\mathbf {HFL_{e}}+(r)} \Rightarrow \text {Form}(r)$, and (ii) splitting.

• (i)  Apply the invertible rules $(ec)$, $(\vee _{L})$, $(\rightarrow _{R})$, $(\cdot _{L})$ backwards from $\Rightarrow \text {Form}(r)$ to obtain the hypersequent below. The substitution $\sigma$ that makes it the conclusion of an instance $\sigma (r)$ of $(r)$ in association form (cf. Fig. 2) is obtained by pattern-matching (refer to variables shown above hypersequent below),

  

  Applying $\sigma (r)$ backwards to the hypersequent above, it remains to derive each premise of $\sigma (r)$ in $\mathbf {HFL_{e}}$.

  We illustrate with the premise $G\mid {\mathcal {S}}_{ij},{\varSigma }_{i}\Rightarrow \varPi _{i}$ of $(r)$ ($i\in I$, $j\in J_{i}$). In $\sigma (r)$ this becomes $\sigma ({\mathcal {S}}_{ij})\Rightarrow \bigvee _{j'\in J_{i}}{\odot }({\widehat{\mathcal {S}}}_{ij'})$. Obtain $\sigma ({\mathcal {S}}_{ij})\Rightarrow {\odot }({\widehat{\mathcal {S}}}_{ij})$ using $(\vee _{R})$. Let ${\mathcal {S}}_{ij}=\{P_1,\ldots ,P_n\}$ (each $P_{s}$ is a structure variable). Applying $(\cdot _{R})$ backwards to the latter sequent we obtain $\sigma (P_{s})\Rightarrow \widehat{P} _{s}$ ($1\le s\le n$). It remains to verify derivability of the latter. Since $P_{s}$ occurs in the premise in the LHS, it must occur in the conclusion (subformula property) in the LHS (separation). Additionally it cannot be a $\varSigma$ variable (coupling). Therefore either $P_{s}\in {\mathcal {V}}_i$, $P_{s}\in {\mathcal {W}}_i$, $P_{s}=\varGamma _{uv}$ or $P_{s}=\varDelta _{uv}$. In the first two cases, due to the definition of $\sigma ({\mathcal {V}}_i)$ and $\sigma ({\mathcal {W}}_i)$, we have the assignment $\sigma (P_{s}):=\widehat{P} _{s}$ and hence derivability. In the latter two cases we get $\widehat{{\varGamma }} _{uv}\wedge \lnot \bigvee _{l\in M_{uv}}{\odot }({\widehat{\mathcal {T}}}_{uvl})\Rightarrow \widehat{\varGamma } _{uv}$ and $\widehat{{\varDelta }} _{uv}\wedge \lnot \bigvee _{l\in N_{uv}}{\odot }({\widehat{\mathcal {S}}}_{uvl})\Rightarrow \widehat{\varDelta } _{uv}$ respectively. Applying $(\wedge _{L})$ backwards we get $\widehat{\varGamma } _{uv}\Rightarrow \widehat{\varGamma } _{uv}$ and $\widehat{\varDelta } _{uv}\Rightarrow \widehat{\varDelta } _{uv}$.

• (ii) Proving that $\text {Form}(r)$ satisfies (splitting) follows from a straightforward inspection so we simply set out what needs to be proved. Let $(r)$ be given as

  

  We have to show that for any instantiation $\sigma$ and for any $i\in I\cup L$, the hypersequent $\sigma (G\mid \widehat{\sigma } ( \text {Form}(r,i))\# S_i)$ is derivable from $\sigma (\mathcal {H})$ without invoking $(r)$ or $(cut)$. For $i\in I$, the hypersequent $\sigma (G\mid \widehat{\sigma } (\text {Form}(r,i))\# S_i)$ is

  $$\begin{aligned} \sigma (G)\mid \widehat{\sigma } (\text {Form}(r,i)), \sigma ({\mathcal {V}}_{i}),\sigma (\varGamma _{i1}),\ldots ,\sigma (\varGamma _{ir_i}),\sigma (\Sigma _i)\Rightarrow \sigma (\varPi _i) \end{aligned}$$

  (1)

  From Definition 9 we have that $\widehat{\sigma } (\text {Form}(r,i))$ has the following form:

  $$\begin{aligned} \left( {\odot }\sigma ({\mathcal {V}}_{i})\cdot {\odot }\left\{ \sigma (\varGamma _{ij})\wedge (\lnot \bigvee _{l\in M_{ij}}{\odot }\sigma ({\mathcal {T}}_{ijl})) \mid j\le r_i\right\} \rightarrow \bigvee _{j\in I_j}{\odot }\sigma ({\mathcal {S}}_{ij})\right) _{\wedge 1} \end{aligned}$$

  Now $\sigma (\mathcal {H})\vdash _{\mathbf {HFL_{e}}}^{cf}$ (1) can be witnessed by decomposing $\widehat{\sigma } (\text {Form}(r,i))$.    $\blacksquare$

Remark 13

$\text {Form}(r)$ is not necessarily the $\mathcal {P}_{3}$/$\mathcal {P}_{3}'$ formula that generates $(r)$ and might not coincide with the formula obtained by suitably reversing the algorithm in [6]. E.g., in the guided example (Sect. 3) we used the formula $(\widehat{\varGamma } _2\rightarrow \widehat{\varGamma } _1)\vee (\widehat{\varGamma } _1\rightarrow \widehat{\varGamma } _2)$ as a disjunction form of $(com)$, but our method computes a slightly different (though equivalent) form (Example 11). The advantage of the method given here is that it works uniformly for substructural and modal logics, and it does not require any familiarity with the algorithm in [6].

6 Bounded Calculi for Commutative Substructural Logics

Let $\mathcal {F}$ be a set of amenable axioms and $\mathcal {R}_{\mathcal {F}}$ the corresponding set of analytic structural hypersequent rules. In some cases (e.g. weakening, contraction axioms), the computed rule(s) may have just a single active component conclusion and hence they correspond to sequent structural rules. We call these sequent axioms, and they belong to the class $\mathcal {N}_2$ in the $(\mathcal {P}_{i}, \mathcal {N}_{i})$ substructural hierarchy.

Theorem 14

Let $\mathcal {F}_{seq}\cup \mathcal {F}$ be a finite set of amenable axioms such that $\mathcal {F}_{seq}$ is a set of sequent axioms with corresponding sequent rules $\mathcal {R}_{seq}$. Also set $\mathcal {F}'=\{\text {Form}(r) |r\in \mathcal {R}_{\mathcal {F}}\}$. For every sequent S, the following are equivalent:

• 1. $\vdash _{\mathbf {FL_{e}}+\mathcal {F}_{seq}+\mathcal {F}} S$

• 2. $\vdash _{\mathbf {FL_{e}}+\mathcal {R}_{seq}}^{cf} \varGamma _{S}\# S$ for a multiset $\varGamma _{S}$ of $g^{\cdot }(S)$-instantiations of elements in $\mathcal {F}'$.

• 3. S has a $(g^{\cdot },\mathcal {F}')$-bounded derivation in $\mathbf {FL_{e}}+\mathcal {R}_{seq}+\mathcal {F}'$.

Proof

(1) $\Rightarrow$ (2). Suppose that $\vdash _{\mathbf {FL_{e}}+\mathcal {F}_{seq}+\mathcal {F}} S$. By Theorem 8: $\vdash ^{cf}_{\mathbf {HFL_{e}}+\mathcal {R}_{\mathcal {F}_{seq}}+\mathcal {R}_{\mathcal {F}}} S$. Let $d_{0}$ be the hypersequent derivation witnessing the latter. Define the rank of a derivation in $\mathbf {HFL_{e}}+\mathcal {R}_{seq}+\mathcal {R}_{\mathcal {F}}$ as the maximum number of $\mathcal {R}_{\mathcal {F}}$-instances on a branch. We successively eliminate all bottommost occurrences of $\mathcal {R}_{\mathcal {F}}$, obtaining a hypersequent derivation of $\varGamma _{S}\# S$ where $\varGamma _{S}$ is an increasing (with each round of elimination/reduction of rank) multiset of $g^{\cdot }(S)$-instantiations of $\mathcal {F}'$.

First observe that since $d_0$ is cut-free, it has the following property:

($*$) every instance of a rule from $\mathcal {R}_{\mathcal {F}}$ instantiates its structure variables with a multiset of elements from $\mathrm {subf}(S)$

Identify the bottommost $\mathcal {R}_{\mathcal {F}}$-instances $\sigma _1(r_{1}),\ldots ,\sigma _n(r_{n})$ in $d_{0}$. Denote the conclusion of $\sigma _i(r_{i})$ by $G|S_{i}^{1}|\ldots |S_{i}^{k_{i}}$. By Theorem 12, $\text {Form}(r_i) =\bigvee _{j\le k_i}\text {Form}(r_i,j)$ is a disjunction form for $r_i$, i.e. a formula built from the structure variables in $r_i$ satisfying (splitting) and (provability) in Definition 5. From ($*$) we establish that each $\widehat{\sigma } _{i}(\text {Form}(r_{i},j))$ is an instantiation of $\text {Form}(r_{i},j)$ by formulas in $g^{\cdot }(S)$.

Set $\delta _{1}:= d_{0}$ and fix an n-tuple $(j_1,\ldots ,j_n)$ satisfying $j_i\le k_i$ ($i\le n$).

for $i=1$ to n do

Use (splitting) to obtain a derivation of $G |\widehat{\sigma } _i(\text {Form}(r_{i},j_i))\# S_i^{j_i}$ using the derivations of the premises of $\widehat{\sigma } _i(r_i)$ in $d_{0}$. Now use $(ew)$ to derive the following.

$$\begin{aligned} G|S^1_i|\ldots |\widehat{\sigma } _i(\text {Form}(r_{i},j_i))\# S_i^{j_i}|\ldots |S^{k_i}_i \end{aligned}$$

(2)

Replace the subderivation (in $\delta _{i}$) of the conclusion $G|S_{i}^{1}|\ldots |S_{i}^{k_{i}}$ of $\sigma _i(r_{i})$ with the above derivation of (2). The result object is not yet a derivation. The following changes are required: when an additive rule or $(ec)$ occurs below (2) (left column below), proceed as in the right column to add the missing formula. Here we are making use of the fact that every $\text {Form}(r_{i},j_i)$ has the form $B\wedge 1$ and hence can be inserted in the LHS using $(1_{L})$ and $(\wedge _{L})$.

The output is a derivation of the hypersequent below left for every $(j_1,\ldots ,j_n)$. Since $\widehat{\sigma } _i(\text {Form}(r_i))=\bigvee _{j\le k_i}\widehat{\sigma } _i(\text {Form}(r_i,j))$, repeatedly apply ($\vee _L$) to this family of derivations to obtain ultimately the derivation $d_{1}$ of below right.

By construction, each $\widehat{\sigma } _{i}(\text {Form}(r_i))$ is a $g^{\cdot }(S)$-instantiation of $\text {Form}(r_{i})$. Derivation $d_{1}$ was obtained from $d_{0}$ (without adding any cuts) by eliminating all bottommost $\mathcal {R}_\mathcal {F}$-instances, without modifying any non-bottommost $\mathcal {R}_\mathcal {F}$-instances. Thus $d_{1}$ is cut-free, has lesser rank than $d_{0}$ and satisfies ($*$).

Identify the bottommost $\mathcal {R}_\mathcal {F}$ instances in $d_{1}$ and repeat the above argument, to obtain ultimately a cut-free derivation $d_{N}$ of $\varGamma _{S}\# S$ in $\mathbf {HFL_{e}}+\mathcal {R}_{seq}+\mathcal {R}_{\mathcal {F}}$ with rank 0, and hence also in $\mathbf {HFL_{e}}+\mathcal {R}_{seq}$. As the derivation contains no rules which act on more than one component in the premise or conclusion, we obtain the cut-free sequent derivation of $\varGamma _{S}\# S$ in $\mathbf {FL_{e}}+\mathcal {R}_{seq}$.

(2) $\Rightarrow$ (3). Given a cut-free derivation of $\{A_{1},\ldots ,A_{n}\}\# S$ in $\mathbf {FL_{e}}+\mathcal {R}_{seq}$ where each $A_{i}$ is a $g^{\cdot }(S)$-instantiations of some element in $\mathcal {F}'$, perform cuts on $A_1,\ldots ,A_n$ to obtain a derivation of S. This derivation is $(g^{\cdot },\mathcal {F}')$-bounded.

(3) $\Rightarrow$ (1). Theorem 12 states that each $\text {Form}(r) \in \mathcal {F}'$ is derivable in $\mathbf {HFL_{e}}+\mathcal {R}_{\mathcal {F}}$. So it follows from (3) that $\vdash _{\mathbf {HFL_{e}}+\mathcal {R}_{seq}+\mathcal {R}_{\mathcal {F}}}^{cf} S$. Then Theorem 8 implies (1). $\blacksquare$

Corollary 15

$\mathbf {FL_{e}}+\mathcal {F}$ has a $(g^{\cdot },\mathcal {F}')$-bounded sequent calculus for every finite set $\mathcal {F}$ of amenable axioms and $\mathcal {F}'=\{\text {Form}(r) |r\in \mathcal {R}_{\mathcal {F}}\}$.

6.1 Application: Decidability and Complexity Of $\mathbf {FL_{ecm}}$ Extensions

The bounded sequent calculi obtained above can be used to give a simple and uniform proof of decidability for every amenable axiomatic extension of $\mathbf {FL_{ecm}}$. Here m is the mingle rule corresponding to the sequent axiom $p \rightarrow p \cdot p$.

Theorem 16

$\mathbf {FL_{ecm}}+\mathcal {F}$ is decidable for each finite set $\mathcal {F}$ of amenable axioms.

Proof

Let $\mathcal {F}':=\{\text {Form}(r) |r\in \mathcal {R}_{\mathcal {F}}\}$. Given a sequent S, let $\varGamma ^{*}$ be the (finite) multiset of all $g^{1\cdot }(S)$-instantiations of $\mathcal {F}'$ without repeats. We claim that

$$\begin{aligned} \vdash _{\mathbf {FL_{ecm}}+\mathcal {F}} S\qquad \text {iff}\qquad \vdash _{\mathbf {FL_{ecm}}} \varGamma ^{*}\#S \end{aligned}$$

The result follows since $\mathbf {FL_{ecm}}$ is decidable [10, 11] and $\varGamma ^{*}$ is computable from S. The direction right to left follows from (2) $\Longrightarrow$ (1) in Theorem 14.

For the other direction, (1) $\Longrightarrow$ (2) in Theorem 14 guarantees the existence of a multiset $\varGamma _{S}$ of $g^{\cdot }(S)$-instantiations of $\mathcal {F}'$ such that $\vdash _{\mathbf {FL_{ecm}}}\varGamma _{S}\# S$. Due to mingle and contraction in $\mathbf {FL_{ecm}}$, we have that $\vdash _{\mathbf {FL_{ecm}}} B\leftrightarrow B^n$ for every formula B and $B^n=B\cdot \ldots \cdot B$ ($n\ge 1$ occurrences). It follows that for every $g^{\cdot }(S)$-instantiation A of a formula in $\mathcal {F}'$, there is a $g^{1\cdot }(S)$-instantiation $A^1$ of the same formula such that $\vdash _{\mathbf {FL_{ecm}}}A^1\Rightarrow A$. By applying cuts with such sequents $A^1\Rightarrow A$ to the proof of $\vdash _{\mathbf {FL_{ecm}}}\varGamma _{S}\# S$, we obtain a derivation of $\varGamma _{S}'\# S$. Applying contractions to this sequent to remove repeated elements in $\varGamma _{S}'$, we obtain a derivation of $\varGamma _{S}''\# S$ such that $\varGamma _{S}''\subseteq \varGamma ^{*}$. Now obtain $\varGamma ^{*}\# S$ by introducing the elements in $\varGamma ^{*}\setminus \varGamma _{S}''$ by $(1_{L})$, $(\wedge _{L})$ and $(\vee _{L})$ (each $A^1\in \varGamma ^{*}$ has the form $(A_1)_{\wedge 1}\vee \ldots \vee (A_n)_{\wedge 1}$).    $\blacksquare$

From the above proof we can also obtain a complexity upper bound. The size of $\varGamma ^{*}$ in the above proof is $O(2^{|S|})$ and this multiset can be computed from S in exponential time. It follows that the decision problem for each amenable extension of $\mathbf {FL_{ecm}}$ is at most exponentially greater than $\mathbf {FL_{ecm}}$.

Deciding if a formula is derivable in $\mathbf {FL_{ecm}}$ is known to be PSPACE-hard [9] but as far as we are aware, no upperbound has been presented in the literature. Let us sketch how to obtain an EXPTIME upperbound using forward proof search. In the presence of contraction and mingle, we can treat the antecedent of a sequent as a set instead of a multiset. In an analytic proof of a sequent S, there are at most $2^{|S|}\cdot |S|$ different sequents (with sets as antecedents) that could appear in the proof. Compute in successive steps which of these sequents is derivable in a proof with depth at most $1,2,3,\ldots ,2^{|S|}\cdot |S|$, terminating if a step does not derive any new sequents. Since each step except perhaps the last derives at least one new sequent, and since no more than $2^{|S|}\cdot |S|$ sequents may be derived, it follows that S is derivable iff S is encountered in one of these steps. Each step takes $O(2^{|S|})$ time so the entire procedure takes $O(2^{|S|})\cdot 2^{|S|}\cdot |S|$ time and the EXPTIME upperbound follows.

In terms of the algebraic semantics [8], Theorem 16 establishes the decidability of the equational theory for the corresponding classes of residuated lattices.

Example 17

Our decidability result applies to a large class of logics including Uninorm Mingle Logic $\mathbf {UML}$ [18] (see [17] for an alternative proof of decidability) axiomatized as $\mathbf {FL_{ecm}}\,+\, (p\rightarrow q)_{\wedge 1}\vee (q \rightarrow p)_{\wedge 1}$, as well as $\mathbf {FL_{ecm}}+ (p \cdot \lnot p) \rightarrow p$ ($\subset \mathbf {LJ}$), and $\mathbf {FL_{ecm}}+(Bwk)$ ($k\ge 2$) where $(Bwk)$ is $\vee _{i=0}^{k} (p_{i}\rightarrow \vee _{j\ne i} {p_{j}})_{\wedge 1}$.

The proof of Theorem 16 also yields the following refinement of Corollary 15.

Lemma 18

$\mathbf {FL_{ecm}}+\mathcal {F}$ has a $(g^{1\cdot },\mathcal {F}')$-bounded calculus for every finite set $\mathcal {F}$ of amenable axioms and $\mathcal {F}'=\{\text {Form}(r) |r\in \mathcal {R}_{\mathcal {F}}\}$.

7 The Methodology Applied to Modal Logics

We shall extract bounded sequent calculi from cut-free hypersequent calculi for three normal modal logics. First, observe that the sequent calculus $\mathbf {S4}$ is obtained by the addition of the rules (T) and (4) to the multi-conclusioned sequent calculus $\mathbf {LK}$ for classical propositional logic. While $\mathbf {S4}$ has cut-elimination, the sequent calculus $\mathbf {S5}=\mathbf {S4}+(5)$ famously fails cut-elimination [20] and, despite much effort, no natural cut-free sequent calculus for the logic has been found.

Let $\mathbf {HS4}$ denote the hypersequent version of the sequent calculus $\mathbf {S4}$. Kurokawa [13] has shown that the hypersequent calculi in the first column below satisfy cut-elimination, and are sound and complete for the corresponding axiomatisations.

The rules (RMS), (MC) and (MS) are given below. The methodology in Sect. 5 has been used to identify the distinguished variables (highlighted in bold). Note: for this purpose we consider a term of the form $\Box \varGamma$ to be a single structure variable. Also let $\widehat{\Box \varGamma }$ denote a propositional variable.

Directly from Definition 9 we obtain:

$$\begin{aligned} \text {Form}(RMS)&=(\lnot (1\cdot (\widehat{\Box \varGamma } \wedge \lnot \widehat{\Box \varDelta })))_{\wedge 1}\vee (\lnot (\widehat{\Box \varDelta } \cdot 1))_{\wedge 1}\\ \text {Form}(MC)&=(\widehat{\Box \varSigma } _1\cdot 1\rightarrow \widehat{\Box \varSigma } _2)_{\wedge 1}\vee (\widehat{\Box \varSigma } _2\cdot 1\rightarrow \widehat{\Box \varSigma } _1)_{\wedge 1}\\ \text {Form}(MS)&=(\lnot (\widehat{\Box \varGamma } \cdot 1))_{\wedge 1}\vee (\widehat{\Box \varGamma } \cdot 1)_{\wedge 1} \end{aligned}$$

The modal case requires the following additional uniform amendments: (i) the $\wedge 1$ in every disjunct is replaced by a leading $\Box$, (ii) the 1 is omitted, (iii) a $\Box$ is introduced in front of every propositional variable $\widehat{\Box \varGamma }$, and (iv) every maximal subformula $\lnot B$ with B not boxed is substituted by $\lnot \Box B$. Let $\text {Form}^{\Box }(r)$ denote the image under these amendments. Then

$$\begin{aligned} \text {Form}^{\Box }(RMS)&=\Box \lnot \Box (\Box \widehat{\Box \varGamma } \wedge \lnot \Box \widehat{\Box \varDelta })\vee \Box \lnot \Box (\Box \widehat{\Box \varDelta })\\ \text {Form}^{\Box }(MC)&=\Box (\Box \widehat{\Box \varSigma } _1\rightarrow \Box \widehat{\Box \varSigma } _2)\vee \Box (\Box \widehat{\Box \varSigma } _2\rightarrow \Box \widehat{\Box \varSigma } _1)\\ \text {Form}^{\Box }(MS)&=\Box \lnot \Box (\Box \widehat{\Box \varGamma })\vee \Box (\Box \widehat{\Box \varGamma }) \end{aligned}$$

The motivation for these amendments is that the analogue of Theorem 12 can now be verified by inspection for $r\in \{RMS,MC,MS\}$ i.e. provability of $\text {Form}^{\Box }(r)$ in $\mathbf {HS4}+r$, and that $\text {Form}^{\Box }(r)$ satisfies splitting in $\mathbf {HS4}$.

For example, here is a derivation of $\text {Form}^{\Box }(RMS)$ in $\mathbf {HS4}+(RMS)$:

For an instantiation $\sigma$ on $(r)$, define the extended instantiation $\widehat{\sigma }$ which maps each $\widehat{\Box \varGamma }$ to the formula $\wedge \Box \sigma (\varGamma )$ (c.f. paragraph following Definition 4). Hence $\Box \sigma (\varGamma )\Rightarrow \widehat{\sigma } (\widehat{\Box \varGamma })$ is derivable. The following witnesses the splitting of $\text {Form}^{\Box }(RMS)$ in $\mathbf {HS4}$.

We can thus obtain the following (the proof is analogous to that for Theorem 14 and the strengthening in Lemma 18).

Theorem 19

The calculus $\mathbf {S4.2_{sc}}$ ($\mathbf {S4.3_{sc}}$, $\mathbf {S5_{sc}}$) has a $(g^{1\wedge },\text {Form}^{\Box }(RMS))$- (resp. $(g^{1\wedge },\text {Form}^{\Box }(MC))$-, $(g^{1\wedge },\text {Form}^{\Box }(MS))$-) bounded sequent calculus.

A New Syntactic Proof of Analyticity for S5

Although cut-elimination fails in $\mathbf {S5}$, Takano [23] gave an intricate syntactic proof of analyticity by establishing that only cuts on subformulas are required. Prior to this, only a semantic argument was known, see Fitting [7].

Although the $(g^{1\wedge },\text {Form}^{\Box }(MS))$-bounded sequent calculus we obtained in Theorem 19 has a finite proof search space and hence is suited for meta-theoretic argument, it is natural to ask if it is possible to modify the methodology of this paper to obtain Takano’s (sharper) result for $\mathbf {S5}$. We are able to answer this in the affirmative. Here is a simple and rather short proof of analyticity for $\mathbf {S5}$.

Theorem 20

The sequent calculus $\mathbf {S5}$ is analytic.

Proof

Cut-free $\mathbf {HS4}+(MS)$ derives exactly the same sequents as $\mathbf {S5_{sc}}$, and the latter is (of course) equivalent to $\mathbf {S5}$. Moreover, any instance of the rule $(MS)$ can be replaced (without introducing cuts) using multiple instances of its single formula version $(MS_{1})$ below, so cut-free $\mathbf {HS4}+(MS_{1})$ derives exactly the same sequents too.

Consider a cut-free derivation d in $\mathbf {HS4}+(MS_{1})$ of a sequent S. For simplicity, suppose that d contains a single instance of $(MS_{1})$ (in the general case, bottommost instances of $(MS_{1})$ are eliminated at each step, c.f. proof of Theorem 14). From this instance, we can obtain the following derivations in $\mathbf {HS4}+(MS_{1})$:

Above left (right), the component $\Box A\Rightarrow \Box A$ (resp. $\Box A,\varDelta \Rightarrow \varPi$) has a $\Box A$ in the RHS (resp. LHS) that was not present in the original derivation d. Proceed downward from each hypersequent following the rules in d, (propagating also these additional $\Box A$ formulas downwards from premise to conclusion).

This is not possible only if $(4)$ is encountered as this rule permits only a single formula in the RHS and the additional $\Box A$ in the RHS would violate this. Solution: use $(5)$ at this point instead of $(4)$. In this way we obtain $(MS_{1})$-free hypersequent derivations (hence in $\mathbf {HS5}$) of $\Box A\# S$ and $S\# \Box A$ (the latter denotes that $\Box A$ is added to the RHS of S). Applying the cut-rule on $\Box A$ on these sequents, we obtain a derivation of S in $\mathbf {HS5}$. Since $\Box A$ occurred in the cut-free derivation d, it is a subformula of S. Finally: every rule in $\mathbf {HS5}$ has one active component, so we can extract an analytic derivation of S in $\mathbf {S5}$.   $\blacksquare$

Concluding Remark: We have investigated what is required in terms of a relaxation of analyticity—represented via a bounding function—in order to trade the extended syntax of the hypersequent calculus for a sequent calculus. This paves the way for a new classification of logics based on their bounding functions. Identifying which functions are amenable to various meta-theoretic arguments (think decidability, interpolation and so on) could lead to the development of a common toolbox of methods applicable over a range of different logics. The immediate corollaries obtained in this paper demonstrate the potential of our approach. Finally, our transformations may provide a means of assessing the logical content of analyticity in the hypersequent calculus (by pegging it to its corresponding bounded sequent calculus), a problem hitherto unstudied.