2.1. Rule schemas, rule instances, and sequent calculus

A rule schema consists of some number of premise sequents and a single conclusion sequent, where the antecedent and succedent of each sequent may contain schematic-variables in addition to formulas. A rule schema with no premises is called an initial sequent.

An instance of the rule schema is obtained by the uniform instantiation of schematic-variables for concrete objects of the corresponding type, and the uniform substitution of propositional variables (occurring in formulas) to formulas. It is typical in structural proof theory not to distinguish explicitly between a rule schema and its instance (indeed the word ‘rule’ is used for both), nor distinguish in notation between a schematic-variable and its instantiation. We follow this convention except where an explicit distinction is helpful; in that case an instance of the rule schema r is denoted $\sigma (r)$ where $\sigma $ is a function that maps schematic-variables to concrete objects of the corresponding type. It will be helpful to permit $\sigma $ to be a map also from propositional variables to formulas.

Example 1. Consider the following rule schemas.

Above left, a function $\sigma $ mapping the propositional variables p and q to formulas yields a rule instance $\sigma (lin)$ ; e.g., $\sigma (p)=p\lor q$ and $\sigma (q)=q$ gives the rule instance with no premise and conclusion $\Rightarrow ((p\lor q)\rightarrow q)\lor (q\rightarrow (p\lor q))$ .

Above right, the rule schema is built from multiset schematic-variables $\Gamma,\Delta,\Pi $ and the formula schematic-variable A. For $\sigma (\Gamma )=\{p,p,q\}$ ; $\sigma (\Delta )=\{r,p\}$ ; $\sigma (\Pi )=\emptyset $ ; $\sigma (A)=r\land q$ we obtain the rule instance with premises $p,p,q\Rightarrow r\land q$ and $r\land q,r,p\Rightarrow $ and conclusion $r,p,p,p,q\Rightarrow $ .

A rule schema is single-conclusioned if instantiations are restricted to single-conclusioned sequents. A sequent calculus is a finite set of rule schemas.

2.2. The sequent calculus $\mathbf {FL_{e}}$ and its extensions

The sequent calculus $\mathbf {FL_{e}}$ for the commutative Full Lambek calculus consists of the set of single-conclusioned rules schemas in Figure 1. We observe that no explicit exchange rule is needed for this calculus since sequents are built using multisets.

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

For a set $\mathcal {R}$ of rule schemas, the extension $\mathbf {FL_{e\ast }}+\mathcal {R}$ is simply the set-union $\mathbf {FL_{e\ast }}\cup \mathcal {R}$ . For a set $\mathcal {A}$ of formulas, we write $\mathbf {FL_{e\ast }}+\mathcal {A}$ for the extension of $\mathbf {FL_{e\ast }}$ by the initial sequents $\Rightarrow A$ where $A\in \mathcal {A}$ . Here are some well-known rule schemas: left weakening $(w_l)$ , right weakening $(w_r)$ , contraction $(c)$ , and mingle [Reference Kamide26] $(m)$

Rules schemas containing neither formulas nor propositional/formula schematic-variables will be called structural rules. We add a subscript to $\mathbf {FL_{e}}$ to indicate an extension by one of the rules above, e.g., $\mathbf {FL_{ec}}:= \mathbf {FL_{e}}+\{(c)\}$ . Also, $\mathbf {FL_{e\ast }}$ ( $\mathbf {FL_{ec\ast }}$ ) denotes $\mathbf {FL_{e}}$ ( $\mathbf {FL_{ec}}$ ) extended by a combination of them. Finally, $\mathbf {FL_{ew}}$ is $\mathbf {FL}_{\mathbf {e w_{l}w_{r}}}$ .

2.3. (Cut-free) derivability and subformula property

Let ${\mathcal {C}}$ be any extension of $\mathbf {FL_{e}}$ by rule schemas, and $\mathcal {S}$ a set of sequents. A derivation (or proof) of a sequent S (from $\mathcal {S}$ ) in ${\mathcal {C}}$ is defined in the usual way as a tree of sequents with root S such that every internal node and its children correspond to the conclusion and premises of a rule instance of ${\mathcal {C}}$ , and every leaf of the tree is an instance of an initial sequent from ${\mathcal {C}}$ , or one of the sequents in $\mathcal {S}$ .

A cut-free derivation does not contain any instance of the cut-rule. Let $\mathcal {S}\vdash _{{\mathcal {C}}} S$ ( $\mathcal {S}\vdash ^{cf}_{{\mathcal {C}}}S$ ) denote that the sequent S is derivable (cut-free derivable) from $\mathcal {S}$ in ${\mathcal {C}}$ . If $\mathcal {S}$ is empty we write these as $\vdash _{{\mathcal {C}}} S$ and $\vdash ^{cf}_{{\mathcal {C}}}S$ respectively. A derivation has the subformula property, and is called analytic, if all formulas occurring in it are subformulas of the endsequent.

We say that ${\mathcal {C}}$ is analytic (resp. ${\mathcal {C}}$ has cut-elimination) if every derivable sequent in ${\mathcal {C}}$ has an analytic derivation (resp. every derivation can be transformed into a cut-free derivation). It is well-known that $\mathbf {FL_{e\ast }}$ has cut-elimination and is analytic— its extensions by initial sequents are analytic only in trivial cases.

2.4. Logics and axiomatic extensions

A logic is a set of formulas closed under modus ponens (and necessitation, in the modal case) and the uniform substitution of propositional variables for arbitrary formulas.

For a logic L and a finite set $\mathcal {A}$ of formulas, the axiomatic extension of L by $\mathcal {A}$ (denoted $L+\mathcal {A}$ ) is the smallest logic containing L and all formulas in $\mathcal {A}$ .

Let ${\mathcal {C}}$ be any extension of $\mathbf {FL_{e}}$ by rule schemas. We let $\mathrm {Thm}({\mathcal {C}})$ denote the set of all formulas F such that $\vdash _{{\mathcal {C}}} \,{\Rightarrow }{F}$ . Since the cut-rule subsumes modus ponens, it is easily verified that $\mathrm {Thm}({\mathcal {C}})$ is a logic and that $\mathrm {Thm}({\mathcal {C}}+\mathcal {A})=\mathrm {Thm}({\mathcal {C}})+\mathcal {A}$ . This indicates that axiomatic extensions of the logic $\mathrm {Thm}({\mathcal {C}})$ are captured proof theoretically by the addition of initial sequent rule schemas to ${\mathcal {C}}$ .

We say that ${\mathcal {C}}$ is a calculus for a logic L if $\mathrm {Thm}({\mathcal {C}})=L$ .

Hypersequent calculi generalise sequent calculi by using a multiset of sequents (a hypersequent) rather than a single sequent for the premises and conclusion of the rule schemas. A hypersequent is written $S_1\mid \ldots \mid S_n$ . Each $S_i$ (a sequent) is called a component.

Every sequent calculus $\mathbf S$ can be embedded into a hypersequent calculus $\mathbf {HS}$ : (i) replace each rule schema $(r)$ in $\mathbf S$ with $(Hr)$ (see below) where the hypersequent schematic-variable G can be instantiated with a (possibly empty) hypersequent, and (ii) include the rules of external weakening $(ew)$ and external contraction $(ec)$ (the external exchange).

It is easy to see that a sequent is derivable in $\mathbf {HS}$ iff it is derivable in $\mathbf S$ . This observation will be used several times in this article. The additional expressivity of the hypersequent calculus comes from the use of rule schemas that act on multiple components of the conclusion simultaneously.

Example 2. A sequent calculus for propositional Gödel logic extends $\mathbf {LJ}=\mathbf {FL_{ecw}}$ by the initial sequent $\Rightarrow \mathbf {lin}$ ( $\mathbf {lin}:= (p\rightarrow q)\lor (q\rightarrow p)$ ). The resulting system has neither cut-elimination nor analyticity. A hypersequent calculus with these properties can be obtained [Reference Avron3] by adding to $\mathbf {HLJ}$ the communication rule

A cut-free hypersequent calculus for modal logic $\mathbf {S5}$ with the subformula property is obtained by extending the hypersequent calculus $\mathbf {HS4}$ for $\mathbf {S4}$ with Avron’s modalized splitting rule [Reference Avron, Hodges, Hyland, Steinhorn and Truss4]:

In the above examples, the hypersequent schematic-variable G is called the context. The remaining components are called the active components of the rule.

Notations and terminologies introduced for sequent calculi apply to hypersequent calculi in the obvious way.

3.1. Subformula property compared to $\psi $ -analytic sequent calculus

For sequent calculus with the subformula property, every derivable sequent ${\Rightarrow } F$ has a derivation such that

$$ \begin{align*} \text{every formula is a subformula of}\ F. \end{align*} $$

Meanwhile in a $\psi $ -analytic derivation of ${\Rightarrow } F$ in $\mathbf {FL_{e\ast }}+\mathcal {A}$ , every cut-formula and every initial sequent $\Rightarrow A$ belong to $\psi (\mathcal {A},F)$ . In such a derivation

$$ \begin{align*} \text{every formula is a subformula of}\ F\ \text{or of some}\ A\in \psi (\mathcal {A},F). \end{align*} $$

Therefore, a $\psi $ -analytic sequent calculus is a generalisation of a sequent calculus with the subformula property that preserves its original motivation: the restriction of the proof search space. This is especially the case when $\psi $ has a finite image. In the following sections we shall see that this generalisation is precisely what is needed to capture logics that do not satisfy the subformula property in the sequent calculus.

4.1. Disjunction form of a structural hypersequent rule

Convention. For a multiset $\mathcal {A}$ of formulas, let ${\odot }\mathcal {A}$ denote the fusion of all formulas in $\mathcal {A}$ , and $1$ if $\mathcal {A}$ is empty. When working in calculi which have weakening and contraction, we identify $1$ and $\top $ , $0$ and $\bot $ , as well as $\cdot $ and $\land $ .

The disjunction form is defined with respect to a rule schema (and not to a particular rule instance). Consequently, the disjunction form will represent all of its rule instances. Consider a structural hypersequent rule schema $(r)$

Here the $T_i$ ’s are the active components of the premise, and the $S_i$ ’s are the active components of the conclusion. Let $\{\Gamma _i\mid i\in I\}$ be the multiset schematic-variables from which the active components are built, and associate with each $\Gamma _{i}$ a propositional variable $\widehat {\Gamma }_{i}$ . Given an instantiation $\sigma $ on $(r)$ , we can then define the substitution $\widehat {\sigma }$ which maps each $\widehat {\Gamma }_{i}$ to the formula ${\odot }\sigma (\Gamma _{i})$ .

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})$ is cut-free derivable from the premises of the rule without using $(r)$ . This can be depicted as follows:

By (provability), we assure that the disjunction form is not too strong, i.e., it must be a theorem of the logic under consideration.

Example 11. $(\widehat {\Gamma }_2\rightarrow \widehat {\Gamma }_1)\lor (\widehat {\Gamma }_1\rightarrow \widehat {\Gamma }_2)$ is a disjunction form of

over $\mathbf {HLJ}$ (cf. Example 2 and the case study in the introduction). ⊣

4.2. Multiset-axiomatisations/analyticity via the disjunction form

We are ready to prove the main result of this section.

Proof. First observe that (ii) and (iii) are equivalent by Lemma 8.

To prove (i) and (iii) we make use of the following claim.

( $\dagger $ ) Every analytic $\mathbf {H}\mathbf {FL_{e\ast }}+\mathcal {R}$ -derivation $\delta $ of ${\Rightarrow } F$ can be transformed into a $\mathbf {FL_{e\ast }}$ -derivation of $B_1,\ldots,B_m\Rightarrow F$ where $B_i\in \psi _{ms}(\mathcal {A},F)$ for every $i\leq m$ .

Indeed: $\mathrm {Thm}(\mathbf {H}\mathbf {FL_{e\ast }}+\mathcal {R})\supseteq \mathrm {Thm}(\mathbf {FL_{e\ast }}+\mathcal {A})$ by the (provability) property of disjunction forms, and the reverse inclusion $\mathrm {Thm}(\mathbf {H}\mathbf {FL_{e\ast }}+\mathcal {R})\subseteq \mathrm {Thm}(\mathbf {FL_{e\ast }}+\mathcal {A})$ is a consequence of $(\dagger )$ , so (i) follows.

Also, $\mathrm {Thm}(\mathbf {FL_{e\ast }})+\mathcal {A}=\mathrm {Thm}(\mathbf {FL_{e\ast }}+\mathcal {A})$ and this is $\mathrm {Thm}(\mathbf {H}\mathbf {FL_{e\ast }}+\mathcal {R})$ by (i). Therefore $F\in \mathrm {Thm}(\mathbf {FL_{e\ast }})+\mathcal {A}$ implies—using $(\dagger )$ —that some $B_1\cdot \ldots \cdot B_m\rightarrow F\in \mathrm {Thm}(\mathbf {FL_{e\ast }})$ with each $B_{i}\in \psi _{ms}(\mathcal {A},F)$ . So (iii) follows.

It remains to prove the claim ( $\dagger $ ).

We generalize the procedure illustrated in Section 1 for $\mathbf {HLJ}+(com)$ . To deal with derivations containing more than one application of $\mathcal {R}$ -rules we first transform $\delta $ into an intermediary derivation of $B_1, \dots, B_m \Rightarrow F$ in $\mathbf {H}\mathbf {FL_{e\ast }}$ . Moreover, as the elimination of each $\mathcal {R}$ -rule entails a duplication of parts of the derivation and hence might introduce new instances of rules in $\mathcal {R}$ , we eliminate all lowermost $\mathcal {R}$ -rules in $\delta $ simultaneously. In doing so, we ensure that after each reduction step, the maximal number of $\mathcal {R}$ -instances on a branch in the proof—henceforth called the $\mathcal {R}$ -rank of the derivation—decreases, and hence the whole procedure terminates.

Let $\sigma _1(r_{1}),\ldots,\sigma _k(r_k)$ the lowermost $\mathcal {R}$ -instances in $\delta $ . Assume $\sigma _i(r_i)$ is:

(1)

By assumption, there is a disjunction form $A_i=A^i_1\lor \cdots \lor A^i_{n_i}\in \mathcal {A}$ for $r_i$ . Recall that $A_i$ is built from variables $\widehat {\Gamma }$ where $\Gamma $ is a multiset schematic-variable in the rule $r_i$ , and that the substitution $\widehat {\sigma }_i$ is defined by setting $\widehat {\sigma }_i(\widehat {\Gamma }):= {\odot }\sigma _i(\Gamma )$ .

From the subformula property of the derivation $\delta $ it follows that:

( $\ast $ ) every instance of an $\mathcal {R}$ -rule instantiates its multiset schematic-variables with a multiset of elements from $\mathrm {subf}(F)$ ,

and consequently, $\widehat {\sigma }_i(A_i)\in \psi _{ms}(\mathcal {A},F)$ . By the (splitting) property of the disjunction form we can eliminate the instance $\sigma _i(r_i)$ by introducing a formula $\widehat {\sigma }_i(A^i_j)$ to the antecedent of the j-active component in the conclusion ( $j \leq n_i$ ). This gives us $n_i$ ways of eliminating $\sigma _i(r_i)$ .

Hence, in order to eliminate all lowermost instances $\sigma _1(r_1),\ldots,\sigma _k(r_k)$ , we have to make $n_1\cdot \ldots \cdot n_k$ many choices. We may encode every such combined choice by a function in the set

$$ \begin{align*} \Omega:= \{f:\{1,\ldots,k\}\rightarrow\mathbb{N}\mid \forall i \; (f(i) \leq n_i)\}. \end{align*} $$

We fix one $f\in \Omega $ and formally describe a transformation $f(\delta )$ of the original proof $\delta $ which ‘for all $i\leq k$ eliminate $\sigma _i(r_i)$ by adding $\widehat {\sigma }_i(A^i_{f(i)})$ ’. Indeed we simultaneously replace all instances $\sigma _{i}(r_{i})$ (cf. (1) above) in $\delta $ , for $i\leq k$ , by

Here, the dotted line indicates the $\mathbf {FL_{e\ast }}$ -derivation guaranteed by the (splitting) property; the side hypersequent $\sigma _i(G)$ can simply be appended to all sequents in this derivation. In words, the rule instance $\sigma _{i}(r_{i})$ in $\delta $ has been replaced by a derivation (in $\mathbf {H}\mathbf {FL_{e\ast }}$ ) of the conclusion of $\sigma _{i}(r_{i})$ from its premises where the formula $\widehat {\sigma }_i(A_{i,f(i)})$ has been appended to the antecedent of the component $\sigma _i(S_{f(i)})$ . Next, the formula $\widehat {\sigma }_i(A_{i,f(i)})$ is added to the corresponding antecedents of all hypersequents from the denoted $(ew)$ down to the endsequent ${\Rightarrow } F$ . When propagating $\widehat {\sigma }_i(A_{i,f(i)})$ downwards from the premise to the conclusion of a binary additive rule, it is necessary to supply a copy of $\widehat {\sigma }_i(A_{i,f(i)})$ to the antecedent of corresponding component in the other premise. This can be done using the rule $(w_l)$ , if it is present in $\mathbf {FL_{e\ast }}$ . Otherwise, the effect of $(w_l)$ can be simulated as follows, using the fact that $\widehat {\sigma }_i(A_{i,f(i)})$ is weakenable (which is guaranteed by the (weakening) property of disjunction forms):

Now having propagated all the $\widehat {\sigma }_i(A^i_{f(i)})$ ’s ( $i\leq k$ ) down to the endsequent, we obtain a derivation of

$$ \begin{align*} \widehat{\sigma}_1(A^1_{f(1)}),\ldots,\widehat{\sigma}_k(A^k_{f(k)})\Rightarrow F. \end{align*} $$

Call this derivation $f(\delta )$ , and note that its $\mathcal {R}$ -rank is smaller than that of $\delta $ . Recall that each disjunction form $A_i=A^i_1\lor \cdots \lor A^i_{n_i}$ . To get the proof $\Omega (\delta )$ of

$$ \begin{align*} \widehat{\sigma}_1(A_1),\ldots,\widehat{\sigma}_k(A_k)\Rightarrow F, \end{align*} $$

we connect all the proofs $f(\delta )$ for every $f\in \Omega $ by repeatedly applying the $(\lor _L)$ -rule to their conclusion. We already remarked that $\widehat {\sigma }_i(A_i) \in \psi _{ms}(\mathcal {A},F)$ . Furthermore, $\Omega (\delta )$ still satisfies ( $\ast $ ) because no new $\mathcal {R}$ -instances have been introduced and every $\mathcal {R}$ -instance of $\delta $ has either been eliminated or left unchanged. Lastly, the $\mathcal {R}$ -rank of $\Omega (\delta )$ equals the maximal $\mathcal {R}$ -rank of one of the $f(\delta )$ ’s, and therefore is smaller than the $\mathcal {R}$ -rank of $\delta $ . It follows that we can repeat the above transformation to eventually obtain an $\mathcal {R}$ -free derivation $\Omega ^\ast (\delta )$ of

$$ \begin{align*} B_1,\ldots,B_m\Rightarrow F \mbox{ where each } B_i\in \psi_{ms}(\mathcal{A},F). \end{align*} $$

Since this is a derivation in $\mathbf {H}\mathbf {FL_{e\ast }}$ and since this calculus contains no rule schemas that act on multiple components of the conclusion simultaneously, $\Omega ^\ast (\delta )$ can be reduced to an $\mathbf {FL_{e\ast }}$ -proof by pruning components and branches. This concludes the proof of $(\dagger )$ , and hence the proof of the theorem. ⊣

5.1. Analytic structural hypersequent rules

Analytic structural hypersequent rules (analytic rules, for short) are structural hypersequent rules that have exactly one active component in each premise and satisfy the following properties:

• (linear conclusion) Every schematic-variable that occurs in the conclusion occurs exactly once there.

• (separation) No multiset schematic-variable occurs in an antecedent position and in a succedent position.

• (coupling) For each conclusion component with a multiset schematic-variable $\Pi $ as succedent, there is a multiset schematic-variable $\Sigma $ in the antecedent of the same component such that the pair $(\Sigma,\Pi )$ always occur together in the premises, and when $\Sigma $ occurs in a premise it occurs exactly once.

• (subformula property) Each schematic-variable that occurs in the premise also occurs in the conclusion.

The addition of analytic rules to $\mathbf {HFL_{e}}$ leads to cut-free hypersequent calculi with the subformula property for many substructural logics. These rules can be computed for a large class of axiomatic extensions of $\mathrm {Thm}(\mathbf {FL_{e}})$ in a uniform and systematic way. This result is based on the following syntactic classification of Hilbert axioms in the language of $\mathbf {FL_{e}}$ . Let $\mathcal {P}_{0}=\mathcal {N}_{0}$ be the set $\mathbf {Var}$ of propositional variables, and define

$$ \begin{align*} &\mathcal{P}_{n+1} := 1 \,\,|\,\, \bot \,\,|\,\, \mathcal{N}_{n} \,\,|\,\, \mathcal{P}_{n+1}\lor\mathcal{P}_{n+}\,\,|\,\, \mathcal{P}_{n+1}\cdot \mathcal{P}_{n+1}, \\ &\mathcal{N}_{n+1} := 0 \,\,|\,\, \top \,\,|\,\, \mathcal{P}_{n} \,\,|\,\, \mathcal{N}_{n+1}\land\mathcal{N}_{n+}\,\,|\,\, \mathcal{P}_{n+1}\rightarrow \mathcal{N}_{n+1}. \end{align*} $$

Observe that $U_{i}\subset V_{i+1}$ ( $U,V\in \{\mathcal {P},\mathcal {N}\}$ ). For axiomatic extensions of $\mathbf {FL_{ew}}$ every formula in $\mathcal {P}_3$ can be transformed into analytic rules. In absence of weakening, only formulas in $\mathcal {P}_{3}'\subset \mathcal {P}_{3}$ that are acyclic (i.e., those that do not lead the transformation into cycles) can be transformed into analytic rules. Here $\mathcal {P}_{3}'$ is defined by the grammar $1\,\,|\,\, \bot \,\,|\,\, \mathcal {N}_{2}\land 1 \,\,|\,\, \mathcal {P}_{3}'\cdot \mathcal {P}_{3}' \,\,|\,\, \mathcal {P}_{3}'\lor \mathcal {P}_{3}'$ .

Theorem 16(i) in this paper is Theorem 5.6 in [Reference Ciabattoni, Galatos and Terui12]. The proof in the latter relies on expressing every $\mathcal {P}_{3}'$ axiomatic extension of $\mathbf {FL_{e}}$ as an axiomatic extension by disjunctions of $\mathcal {N}_{2} \wedge 1$ formulas (see [Reference Ciabattoni, Galatos and Terui12, Lemma 3.5]). The latter proof is incomplete as it does not cover cases like $((\mathcal {P}_{3}'\lor \mathcal {P}_{3}')\cdot (\mathcal {P}_{3}'\lor \mathcal {P}_{3}'))\lor ((\mathcal {P}_{3}'\lor \mathcal {P}_{3}')\cdot (\mathcal {P}_{3}'\lor \mathcal {P}_{3}'))$ . Nevertheless the result stands. An algebraic argument can be found in [Reference Ciabattoni, Galatos and Terui13, Lemma 4.5]. Here is an alternative argument. By induction on the structure of A we have $\mathbf {FL_{e}}\vdash A\Rightarrow 1$ , and thus $\mathbf {FL_{e}}\vdash A,B\Rightarrow B$ , for every $A,B\in \mathcal {P}_{3}'$ . Making use of the latter it can be seen that for every extension L of $\mathbf {FL_{e}}$ and $A,B,C\in \mathcal {P}_{3}'$ : $\mathrm {Thm}(L+A\cdot B)=\mathrm {Thm}(L+A+B)$ and $\mathrm {Thm}(L+(A\lor (B\cdot C)))=\mathrm {Thm}(L+A\lor B+A\lor C)$ . Repeatedly apply the latter two equalities to express a $\mathcal {P}_{3}'$ axiomatic extension as a disjunctions of $\mathcal {N}_{2} \wedge 1$ formulas.

5.2. Computing the disjunction form of an analytic rule

We now describe an algorithm which turns an analytic rule into a disjunction form. We occasionally write $A_{\land 1}$ for $A\land 1$ for brevity.

As the first step, select exactly one multiset schematic-variable occurrence in the active component of each premise (‘distinguished variable occurrence’) of the analytic rule. This induces an association of the distinguished variable (and the premise it is contained in) to the unique conclusion component containing this variable. For premises with a multiset schematic-variable $\Pi $ as succedent, we will choose as distinguished variable occurrence the multiset schematic-variable $\Sigma $ to which it is coupled (i.e., the coupling $(\Sigma,\Pi )$ in the definition of analytic rule).

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

• – A multiset schematic-variable declared as distinguished in a premise whose active component has empty succedent may appear in a conclusion component with or without empty succedent.

• – Distinct premises may be associated with the same conclusion component due to the same or different distinguished variables.

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

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

Figure 2 Association form. ${\mathcal {S}},{\mathcal {T}},{\mathcal {U}},{\mathcal {V}},{\mathcal {W}}$ denote multisets of multiset schematic-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.

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

Definition 19 ( $\text {Form}(r,i)$ )

For a rule $(r)$ in association form $($ Figure 2 $)$ , let

$$ \begin{align*} &\text{Form}(r,i) := \left({\odot}{\widehat{{\mathcal{V}}}}_{i}\cdot{\odot}\left\{\widehat{\Gamma}_{ij}\land(\lnot\bigvee_{l\in M_{ij}}{} {\odot}{\widehat{{\mathcal{T}}}}_{ijl}) \mid j\leq r_i\right\} \rightarrow\bigvee_{j\in J_i}{}{\odot}{\widehat{{\mathcal{S}}}}_{ij}\right)_{\!\!\!\!\land 1} && (i\in I), \\ &\text{Form}(r,i) := \left(\lnot\left({\odot}{\widehat{{\mathcal{W}}}}_{i}\cdot{\odot}\left\{\widehat{\Delta}_{ij}\land(\lnot\bigvee_{l\in N_{ij}}{}{\odot}{\widehat{{\mathcal{U}}}}_{ijl}) \mid j\leq s_i\right\}\right)\right)_{\!\!\!\!\land 1} && (i\in L). \end{align*} $$

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

Example 20. Here are association forms of three well-known structural rules. In (com), the choice of distinguished variables $\Sigma _{1}$ and $\Sigma _{2}$ is forced since the coupled variable in the antecedent is always chosen. In (lq), the $\Gamma $ could have been chosen as distinguished instead of $\Delta $ . In (wc), the second occurrence of $\Delta $ could have been chosen as distinguished instead.

• – Pattern-matching the $(com)$ rule with Figure 2 we obtain:

  
  $I=\{1,2\}$ , $L=\emptyset $ , ${\mathcal {V}}_1=\{\Gamma _2\}$ , ${\mathcal {V}}_2=\{\Gamma _1\}$ , $J_1=J_2=\{1\}$ , ${\mathcal {S}}_{11}=\{\Gamma _1\}$ , ${\mathcal {S}}_{21}=\{\Gamma _2\}$ , $r_1=r_2=0$ , and therefore:
  
  In the above, we have written to indicate that the term evaluates to $1$ . (Recall that in $\mathbf {H}\mathbf {FL_{e\ast }}$ , ${\odot }\mathcal {A}$ denotes the fusion of all formulas in $\mathcal {A}$ , and $1$ if $\mathcal {A}$ is empty.) So $ \text {Form}(com)=(\widehat {\Gamma }_2\cdot 1\rightarrow \widehat {\Gamma }_1)_{\land 1}\lor (\widehat {\Gamma }_1\cdot 1\rightarrow \widehat {\Gamma }_2)_{\land 1}. $

• – Pattern-matching the $(lq)$ rule with Figure 2 we obtain:

  
  $I=\emptyset $ , $L=\{1,2\}$ , $s_1=1$ , $s_2=0$ , $\mathcal {N}_{11}=\{1\}$ , ${\mathcal {W}}_1=\emptyset $ , ${\mathcal {W}}_2={\mathcal {U}}_{111}=\Gamma $ , $\Delta _{11}=\Delta $ , and therefore:
  
  So $\text {Form}(lq)=(\lnot (1\cdot (\widehat {\Delta }\land \lnot \widehat {\Gamma })))_{\land 1}\lor (\lnot (\widehat {\Gamma }\cdot 1))_{\land 1}$ .

• – Similarly, for $(wc)$ one obtains $\text {Form}(wc)=(\lnot (1\cdot (\widehat {\Delta }\land \lnot \widehat {\Delta })))_{\land 1}$ .⊣

Proof. Given an analytic rule $(r)$ , obtain $\text {Form}(r)$ from its association form. We require (cf. Definition 10) (i) provability, i.e., $\vdash _{\mathbf {HFL_{e}}+(r)} \Rightarrow \text {Form}(r)$ , and (ii) splitting. Weakening is satisfied by construction.

(i) First repeatedly apply to $\Rightarrow \text {Form}(r)$ the rules $(ec)$ and $(\lor _{R})$ to obtain the hypersequent $\Rightarrow \text {Form}(r,i) \mid \dots \mid \Rightarrow \text {Form}(r,l)$ , for all $i \in I$ and $l \in L$ . Then apply the invertible rules $(\lor _{L})$ , $(\rightarrow _{R})$ , $(\cdot _{L})$ backwards from each component to get the hypersequent below. The instantiation $\sigma $ making this hypersequent the conclusion of an instance $\sigma (r)$ of $(r)$ in association form (cf. Figure 2) is obtained by pattern-matching (refer to variables shown above the hypersequents),

$$ \begin{align*} &\left[{\widehat{{\mathcal{V}}}}_{i},\{\overbrace{\widehat{\Gamma}_{ij}\land(\lnot\bigvee_{l\in M_{ij}}{}{\odot}{\widehat{{\mathcal{T}}}}_{ijl})}^{\Gamma_{ij}\hspace{2.4cm}\Sigma_{i}\,\emptyset\hspace{-3.1cm}} \mid j\leq r_i \}\Rightarrow \overbrace{\bigvee_{j\in J_i}{}{\odot}{\widehat{{\mathcal{S}}}}_{ij}}^{\Pi_{i}}\right]_{i\in I} |\\ & \quad \times \left[{\widehat{{\mathcal{W}}}}_{i},\{\overbrace{\widehat{\Delta}_{ij}\land(\lnot\bigvee_{l\in N_{ij}}{}{\odot}{\widehat{{\mathcal{U}}}}_{ijl})}^{\Delta_{ij}} \mid j\leq s_i\}\Rightarrow\right]_{i\in L}. \end{align*} $$

$$ \begin{align*} &\text{-- For}\ i\in I\!\!:\qquad \qquad \sigma(G) := \emptyset \qquad \qquad \sigma(\Sigma_i):= \emptyset \qquad \sigma(\Pi_i):= \bigvee_{j\in J_i}{\odot}({\widehat{{\mathcal{S}}}}_{ij}),\\ &\text{for every}~{{\mathcal{V}}}_{i}=\{Q_{1},\ldots,Q_{n}\},\ \text{set}\ \sigma(Q_{s}):= \widehat{Q}_{s}, \\ &\text{finally, set }\sigma(\mathbf{\Gamma}_{ij}):= \widehat{\mathbf{\Gamma}}_{ij}\land\lnot\bigvee_{l\in M_{ij}}{\odot}({\widehat{{\mathcal{T}}}}_{ijl})\quad (j\leq r_i, l\in M_{ij}). \\ &\text{-- For}\ i\in L\!\!:\ \text{for every}~{{\mathcal{W}}}_{i}=\{Q_{1},\ldots,Q_{n}\},\ \text{set}\ \sigma(Q_{s}):= \widehat{Q}_{s},\\ &\text{finally, set }\sigma(\mathbf{\Delta}_{ij}):= \widehat{\mathbf{\Delta}}_{ij}\land\lnot\bigvee_{l\in N_{ij}}{\odot}({\widehat{{\mathcal{S}}}}_{ijl})\quad (j\leq s_i, l\in N_{ij}). \end{align*} $$

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

We illustrate with the premise $G\mid {{\mathcal {S}}}_{ij},\mathbf {\Sigma }_{i}\Rightarrow \Pi _{i}$ of $(r)$ ( $i\in I$ , $j\in J_{i}$ ). In $\sigma (r)$ , since $\sigma (\Sigma _{i})=\emptyset =\sigma (G)$ this becomes $\sigma ({{\mathcal {S}}}_{ij})\Rightarrow \bigvee _{j'\in J_{i}}{\odot }({\widehat {{\mathcal {S}}}}_{ij'})$ . Obtain $\sigma ({{\mathcal {S}}}_{ij})\Rightarrow {\odot }(\vec {\widehat {{\mathcal {S}}}}_{ij})$ using $(\lor _{R})$ . Let $\vec {{\mathcal {S}}}_{ij}=\{P_1,\ldots,P_n\}$ (each $P_{s}$ is a multiset schematic-variable). Applying $(\cdot _{R})$ backwards to the latter sequent we obtain $\sigma (P_{s})\Rightarrow \widehat {P}_{s}$ ( $1\leq s\leq n$ ). It remains to verify derivability of the latter. Since $P_{s}$ occurs in the premise in the antecedent, it must occur in the conclusion (subformula property) in the antecedent (separation). Additionally it cannot be a $\Sigma $ variable since coupled variables occur only as indicated in Figure 2 by the (coupling) condition. Therefore either $P_{s}\in {{\mathcal {V}}}_i$ , $P_{s}\in \vec {{\mathcal {W}}}_i$ , $P_{s}=\Gamma _{uv}$ , or $P_{s}=\Delta _{uv}$ . In the first two cases, due to the definition of $\sigma (\vec {{\mathcal {V}}}_i)$ and $\sigma (\vec {{\mathcal {W}}}_i)$ , we have the assignment $\sigma (P_{s}):= \widehat {P}_{s}$ and hence derivability. In the latter two cases we get $\widehat {\mathbf {\Gamma }}_{uv}\land \lnot \bigvee _{l\in M_{uv}}{\odot }({\widehat {{\mathcal {T}}}}_{uvl})\Rightarrow \widehat {\Gamma }_{uv}$ and $\widehat {\mathbf {\Delta }}_{uv}\land \lnot \bigvee _{l\in N_{uv}}{\odot }({\widehat {{\mathcal {S}}}}_{uvl})\Rightarrow \widehat {\Delta }_{uv}$ respectively. Applying $(\land _{L})$ backwards we get $\widehat {\Gamma }_{uv}\Rightarrow \widehat {\Gamma }_{uv}$ and $\widehat {\Delta }_{uv}\Rightarrow \widehat {\Delta }_{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 $i\in I\cup L$ , $\sigma (\widehat {\sigma }( \text {Form}(r,i))\# S_i)$ is derivable from the active components of the premises in $\sigma (\mathcal {H})$ in $\mathbf {FL_{e\ast }}$ . We illustrate the case $i\in I$ . The sequent $\sigma (\widehat {\sigma }(\text {Form}(r,i))\# S_i)$ is

(2) $$ \begin{align} \widehat{\sigma}(\text{Form}(r,i)), \sigma({{\mathcal{V}}}_{i}),\sigma(\Gamma_{i1}),\ldots,\sigma(\Gamma_{ir_i}),\sigma(\Sigma_i)\Rightarrow\sigma(\Pi_i). \end{align} $$

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

$$ \begin{align*} \left({\odot}\sigma({{\mathcal{V}}}_{i})\cdot{\odot}\left\{\sigma(\Gamma_{ij})\land\left(\lnot\bigvee_{l\in M_{ij}}{\odot}\sigma(\vec{{\mathcal{T}}}_{ijl})\right) \mid j\leq r_i\right\} \rightarrow\bigvee_{j\in J_i}{\odot}\sigma({{\mathcal{S}}}_{ij})\right)_{\land 1}. \end{align*} $$

Applying the logical rules backwards to suitably decompose the formula $\widehat {\sigma }(\text {Form}(r,i))$ , one obtains a proof of (2) from the active components of $(r)$ . ⊣

5.3. Multiset-axiomatisations/analyticity for substructural logics

6.1. Set-axiomatisations

Multiset-axiomatisations imply set-axiomatisations whenever the structural rules of contraction and mingle (or weakening) are present.

An embedding of a logic L into a logic K is a function $\rho $ on formulas such that $F\in L\leftrightarrow \rho (F)\in K$ . The embedding is PTIME (EXPTIME) if the function is computable in PTIME (EXPTIME).

Proof. 1. By the definition of set-axiomatisable, $F\in \mathrm {Thm}(\mathbf {FL_{ec\ast }}+\mathcal {A})$ iff

(*) $$ \begin{align} \exists A_{1},\ldots,A_{n}\in \psi_s(\mathcal{A},F)\text{ such that } \vdash_{\mathbf{FL_{ec\ast}}} A_{1},\ldots,A_{n}\Rightarrow F. \end{align} $$

Since $\psi _s(\mathcal {A},F)$ is a finite set, we have that (*) is equivalent to the following (contraction is needed in the left-to-right direction of the equivalence since a formula $A\in \psi _s(\mathcal {A},F)$ might appear multiple times in the list $A_1,\ldots,A_n$ ).

$$ \begin{align*} \vdash_{\mathbf{FL_{ec\ast}}}{\odot}\{A\land 1\mid A\in \psi_s(\mathcal{A},F)\}\Rightarrow F. \end{align*} $$

Therefore the following is an embedding of $\mathrm {Thm}(\mathbf {FL_{ec\ast }}+\mathcal {A})$ into $\mathrm {Thm}(\mathbf {FL_{ec\ast }})$ .

$$ \begin{align*} F \quad\mapsto\quad {\odot}\{A\land 1\mid A\in \psi_s(\mathcal{A},F)\}\rightarrow F. \end{align*} $$

The time to compute values of this function is polynomial in the size of the set $\psi _s(\mathcal {A},F)$ and that is exponential in F.

2. Arguing as in 1., we see that the following function is an embedding of $\mathrm {Thm}(\mathbf {FL_{ec\ast }}+\mathcal {A})$ into $\mathrm {Thm}(\mathbf {FL_{ec\ast }})$ .

$$ \begin{align*} F \quad\mapsto\quad {\odot}\{A\land 1\mid A\in \psi_f(\mathcal{A},F)\}\rightarrow F. \end{align*} $$

It is computable in PTIME because the size of $\psi _f(\mathcal {A},F)$ is polynomial in F. ⊣

We obtain the following uniform decidability and complexity upper bound.

In terms of the algebraic semantics [Reference Galatos, Jipsen, Kowalski and Ono18], the corollary above applies to the equational theory of the corresponding classes of residuated lattices.

A 2EXPTIME upper bound for ${\mathbf {FL_{ecm}}}$ already appears in [Reference St John44]. The following improves on this bound. A PSPACE lower bound for this logic was given in [Reference Horcík and Terui21].

Proof. Since $\vdash _{{\mathbf {FL_{ecm}}}}^{cf} \Gamma \Rightarrow A$ iff $\vdash _{{\mathbf {FL_{ecm}}}}^{cf} \Rightarrow {\odot }\Gamma \rightarrow A$ , it suffices to decide derivability of a formula. Let ${\mathbf {FL_{ecm}^s}}$ be the calculus whose rule figures are the same as those of ${\mathbf {FL_{ecm}}}$ , but whose sequents have the form $X\Rightarrow A$ where X is a set of formulas (instead of a multiset as in ${\mathbf {FL_{ecm}}}$ ). Since $\vdash _{{\mathbf {FL_{ecm}}}}^{cf} A\leftrightarrow A\cdot A$ , the claim below follows from a standard induction on the height of the derivation.

$$ \begin{align*} \text{For every formula}~A\!\!:\ \vdash_{{\mathbf{FL_{ecm}}}}^{cf} \Rightarrow A\ \text{iff}\ \vdash_{{\mathbf{FL_{ecm}^s}}}^{cf}\Rightarrow A. \end{align*} $$

It suffices therefore to search for a proof of $\Rightarrow A$ in ${\mathbf {FL_{ecm}^s}}$ . In a cut-free derivation in ${\mathbf {FL_{ecm}^s}}$ of $\Rightarrow A$ , each antecedent is a subset of $\mathrm {subf}(A)$ . Since $|\mathrm {subf}(A)|\leq |A|$ , there are at most $2^{|A|}$ such subsets, and at most $|A|$ possibilities for the succedent. There are thus at most $K:= 2^{|A|}\cdot |A|$ sequents that can occur in a cut-free proof of $\Rightarrow A$ . Using forward proof search, we can decide in exponential timeFootnote ³ if $\Rightarrow A$ is derivable as follows.

First, write down on a tape of the Turing Machine, each of the K sequents that can occur in the proof (this takes time polynomial in K). Mark each initial sequent in this list as proved. Now consider the following algorithm:

1. 1. For each triple of sequents $(S_{1},S_{2},S_{3})$ such that $S_{1}$ and $S_{2}$ are marked proved and $S_{3}$ is unmarked, if there is a binary rule instance in ${\mathbf {FL_{ecm}^s}}$ with premises $S_{1}$ and $S_{2}$ and conclusion $S_{3}$ , then mark $S_{3}$ as newly proved. Proceed similarly with the unary rules of ${\mathbf {FL_{ecm}^s}}$ using a tuple.

2. 2. If none of the sequents is marked newly proved after Step 1 then terminate. Otherwise, replace every newly proved mark with proved, and go to Step 1.

It is easily verified that $\Rightarrow A$ is derivable iff $\Rightarrow A$ is marked proved at termination. Step 1 takes time polynomial in K for each triple, and there are at most $K^{3}$ different triples ( $K^{2}$ different tuples). At each iteration, by Step 2, the algorithm terminates unless the number of sequents marked proved increases. Hence the algorithm must terminate after at most K iterations. It follows that the algorithm has a runtime that is polynomial in K, and thus exponential in $|A|$ .

6.2. Formula and variable boundedness

The previous subsection made use of contraction and mingle to obtain set-axiomatisations. Replacing mingle with weakening, and hence considering the $\mathbf {LJ}$ calculus for intuitionistic logic, opens the door to even sharper results. Here we present two sufficient conditions for a multiset-axiomatisation of $\mathbf {LJ}$ to imply a formula-axiomatisation. Adding a further condition implies a variable-axiomatisation and regains the sufficient condition for the simple substitution property presented in [Reference Hosoi23]. Recall that $A \wedge 1 \leftrightarrow A$ holds in the presence of weakening, and hence all references to the constant $1$ are omitted in this section.

Let $A(B/p)$ denote the formula obtained from A by substituting every occurrence of the propositional variable p in A with the formula B.

Definition 30 ( $\Omega $ -propagation property)

Formula A has the $\Omega $ -propagation property for a set $\Omega $ of binary connectives if for variables $p,q,r$ and every $\diamond \in C$ ,

(*) $$ \begin{align} \vdash_{\mathbf{LJ}} A(q/p),A(r/p)\Rightarrow A(q\diamond r/p). \end{align} $$

Note that this condition is trivial for variables p not occurring in A.

Determining if an axiom has the $\{\land \}$ -propagation property can be tedious, e.g., try checking this property for the $Bc_k$ axiom (Kripke models with k worlds) $p_0\lor (p_0{\rightarrow } p_1)\lor \cdots \lor (p_0\land \cdots \land p_{k-1}{\rightarrow } p_k)$ .

We now introduce an inductive criterion to simplify this check.

In the following, let $p\in \mathbf {Var}$ be an arbitrary propositional variable, and let $A(B)$ abbreviate $A(B/p)$ . Let $U_p$ denote the set of formulas that possess the $\{\land \}$ -propagation property with respect to the variable p:

$$ \begin{align*} U_p = \{A\mid \forall q,r\in \mathbf{Var}.\vdash_{\mathbf{LJ}} A(q),A(r)\Rightarrow A(q\land r)\}. \end{align*} $$

The following is immediate.

Recall that an occurrence of a propositional variable p is negative (positive) in a formula A if it occurs on the left hand side of an odd (resp. even) number of implications. Define the following sets of formulas:

$$ \begin{align*} U_p^\ast =& \{A\mid\forall q,r\in \mathbf{Var}.\vdash_{\mathbf{LJ}} A(q)\Rightarrow A(q\land r)\}; \\ D_p =& \{A\mid\forall q,r\in \mathbf{Var}.\vdash_{\mathbf{LJ}} A(q\land r)\Rightarrow A(q) \,\&\, \vdash_{\mathbf{LJ}}A(q\land r)\Rightarrow A(r)\};\\ N_p =& \{A\mid\ p \text{occurs only negatively in}~A\}. \end{align*} $$

As a mnemonic, U stands for ‘upwards propagation’ (going from simple instances up to conjunctive instances), $U^\ast $ for ‘strong upwards propagation’, D stands for ‘downwards propagation’ (going from conjunctive instances down to simple instances), and of course N stands for negative. For sets $M,N$ of formulas and a binary connective $\diamond $ , define $M\diamond N$ to be the set $\{ A\diamond B\mid A\in M,B\in N\}$ .

Proof. (1) Since $\vdash _{\mathbf {LJ}} q,r\Rightarrow q\land r$ . (2) holds trivially. (3) Let $A\in N_p$ , and let $\delta $ be the standard proof of $A(q)\Rightarrow A(q)$ . Start constructing a proof $\delta '$ of $A(q)\Rightarrow A(q\land r)$ bottom up by imitating the proof steps in $\delta $ . Whenever the formula $q\land r$ appears isolated in $\delta '$ , then this is on the left hand side of a sequent because $A\in N_p$ . We can thus apply a cut with $q\land r\Rightarrow q$ to (again, reading the proof bottom up) replace $q\land r$ with q. Then copy the remaining steps of $\delta $ . (4) Let $A\in D_p$ and $ B\in U_p$ , and consider the following derivation showing that $ A{\rightarrow } B\in U_p$ :

(5) Let $A\in U_p^\ast $ and $B\in U_p$ . Start constructing a proof of $(A\lor B)(q),(A\lor B)(r)\Rightarrow (A\lor B)(q\land r)$ by applying the rule $(\lor _L)$ twice. We then have to check provability of the following four sequents:

1. (i) $A(q),A(r)\Rightarrow (A\lor B)(q\land r);$

2. (ii) $A(q),B(r)\Rightarrow (A\lor B)(q\land r);$

3. (iii) $B(q),A(r)\Rightarrow (A\lor B)(q\land r);$

4. (iv) $B(q),B(r)\Rightarrow (A\lor B)(q\land r).$

Now (i)–(iii) are provable since $A\in U_p^{\ast }$ . Also (iv) is provable since $B\in U_p$ . ⊣

Together, Lemmas 32 and 33 provide a convenient sufficient condition for the $\{\land \}$ -propagation property. Here are two examples.

6.3. Variable-axiomatisations

Variable-axiomatisations in intermediate logics were investigated in [Reference Hosoi23, Reference Sasaki40–Reference Sasaki42] as the simple substitution property.

It is important to note that this is a property of a specific axiomatisation rather than a property of the logic, i.e., alternative axiomatisations of the same logic may not have the property. For example, the standard axiomatisation $\mathbf {LJ}+(p\rightarrow q)\lor (q\rightarrow p)$ for Gödel logic is not a variable-axiomatisation. The formula $\lnot p\lor \lnot \lnot p$ is a counterexample since it is a theorem of Gödel logic and $\mathbf {LJ}$ does not prove $(p{\rightarrow } p)\lor (p{\rightarrow } p)\Rightarrow \lnot p\lor \lnot \lnot p$ . As shown in [Reference Sasaki40], a variable-axiomatisation of Gödel logic is $\mathbf {LJ}+(p{\rightarrow } q)\lor ((p{\rightarrow } q){\rightarrow } p)+(\lnot p\lor \lnot \lnot p).$

A simple sufficient criterion for a variable-axiomatisation is presented in [Reference Hosoi23] using a propagation property. We reformulate that proof in our setting.

Observe that Lemma 36 applies to arbitrary extensions of $\mathbf {LJ}$ but Lemma 31 requires a multiset-axiomatisation. This is because an arbitrary formula instance $A'$ of $\mathcal {A}$ cannot be transformed to an element of $\mathcal {A}[\psi _f(F)]$ by variable renaming. In contrast, an arbitrary variable instance $A'$ of $\mathcal {A}$ is transformable to an element in $\mathcal {A}[\psi _v(F)]$ via variable renaming. Lemma 36 is used in [Reference Hosoi23] to show that classical logic $\mathbf {LJ}+(\lnot p\lor p)$ and $\mathbf {LQ}=\mathbf {LJ}+(\lnot p\lor \lnot \lnot p)$ are variable-axiomatisations.

A logic L has the Craig interpolation property if $A\rightarrow B\in L$ implies the existence of a formula I with $(A\rightarrow I)\land (I\rightarrow B)\in L$ and $\mathbf {Var}(I)\subseteq \mathbf {Var}(A)\cap \mathbf {Var}(B)$ . We reproduce below the elegant argument from [Reference Sasaki40] where the Craig interpolation property for $\mathbf {LQ}$ is induced from $\mathbf {LJ}$ by using a variable-axiomatisation. An analogous argument applies to classical logic.

In [Reference Sasaki41] it is shown that classical logic and $\mathbf {LQ}$ are the only consistent variable-axiomatisable logics over $\mathbf {LJ}$ that are axiomatisable by a single-variable formula. The same paper shows that all finite-valued Gödel logics are variable-axiomatisable over $\mathbf {LJ}$ . We remark that these results have been generalised in [Reference Sasaki42] using algebraic methods to establish necessary and sufficient criterion for variable-axiomatisable intermediate logics on a finite slice (see [Reference Hosoi22]).

7.1. Formula-axiomatisation of $\mathbf {S4.2}$

Throughout, a formula is called boxed if it has the form $\Box A$ .

The modal logic $\mathbf {S4}$ of pre-ordered (reflexive and transitive) Kripke frames is obtained by the addition of the following two rules to the standard multi-conclusion sequent calculus $\mathbf {LK}$ for classical propositional logic.

The modal logic $\mathbf {S4.2}$ extends $\mathbf {S4}$ by the axiom $\Diamond \Box p{\rightarrow }\Box \Diamond p$ . This logic is characterised semantically as the logic of directed pre-ordered Kripke frames. A cut-free hypersequent calculus $\mathbf {HS4.2}$ for $\mathbf {S4.2}$ is obtained (see [Reference Kurokawa, Nakano, Satoh and Bekki28]) by lifting $\mathbf {S4}$ to a hypersequent calculus $\mathbf {HS4}$ and then adding the modal rule

Paralleling the argument in Section 4.2, we now transform cut-free $\mathbf {HS4.2}$ -proofs into bounded analytic sequent calculus proofs. First, using the rules $(ec)$ and $(w_l)$ it is easy to see that any instance of $(RMS)$ can be replaced by multiple applications of its single formula variant

As a disjunction form for $(RMS_1)$ , we choose the formula $\Box \lnot \Box \Box p\lor \Box \lnot \Box \lnot \Box p$ (the formal computation of the modal disjunction form is explained in Section 7.2). This is equivalent to the axiom instance $\Diamond \Box (\Box p){\rightarrow }\Box \Diamond (\Box p)$ and hence the provability property is satisfied. The following two derivations show the splitting property for $\sigma (p)=A$ :

We can then eliminate applications of $(RMS_1)$ in proofs of ${\Rightarrow } F$ by adding the formula $\Box \lnot \Box \Box A$ or the formula $\Box \lnot \Box \lnot \Box A$ into the corresponding antecedent of the rule conclusion. We then propagate these formulas downwards in each of the two derivations. Crucially, since both formulas are boxed, adding them to the antecedent of applications of $(4)$ yields a legal instance of $(4)$ .

Finally, combine the two derivations by a disjunction introduction to obtain a proof of $\Box \lnot \Box \Box A\lor \Box \lnot \Box \lnot \Box A\Rightarrow F$ . As $\Box A$ appeared in the cut-free hypersequent calculus proof, it must be a subformula of F. Eliminate all instances of $(RMS_1)$ and reduce the resulting $\mathbf {HS4}$ proof into a sequent calculus proof.

We obtain formula-axiomatisations—as opposed to set-axiomatisations—because we replaced $\Box \Gamma $ in $(RMS)$ with $\Box A$ in $(RMS_{1})$ .

7.2. Bounded-analytic sequent calculi for simple frame properties

Bounded-analytic sequent calculi for modal logics—extending the methodology for substructural logics—can be obtained from a uniform presentation of the hypersequent rules. We illustrate using the rules in [Reference Lahav29] for extensions of $\mathbf {S4}$ .

Let n be a positive natural number and $S=\{ (S_{R}^{i},S_{=}^{i}) \}_{i\in I}$ for some finite index set I such that every $S_{R}^{i}$ and $S_{=}^{i}$ is a subset of $\{1,\dots,n\}$ and every $S_{R}^{i} \cup S_{=}^{i}$ is non-empty. This is what is called a “normal description of an n-simple $\mathcal {L}_{1}$ -formula” [Reference Lahav29, Definition 4]. Any such description defines a first-order formula

$$ \begin{align*} \forall w_{1}\ldots\forall w_{n}\exists u\bigvee_{i\in I}\left(\bigwedge_{i\in S_{R}^{i}} w_{i}Ru \land \bigwedge_{i\in S_{=}^{i}} w_{i}=u\right) .\end{align*} $$

This gives rise to the class of Kripke frames satisfying this formula. The modal logic of S is defined as the set of formulas valid on this class of frames. For each such logic, an analytic hypersequent calculus is obtained in [Reference Lahav29] by computing the following hypersequent rule “induced by S for transitive modal logics”

$\Box \Gamma _{i}$ and $\boxtimes \Gamma _{i}$ are standard notation for multiset schematic-variables that are instantiable by sets $\{\Box A_{1},\ldots,\Box A_{k}\}$ and $\{A_{1},\Box A_{1},\ldots,A_{k},\Box A_{k}\}$ respectively.

We shall obtain the following analogue of Theorem 13 for the function $\text {Form}^{\Box }$ defined below that maps an analytic hypersequent rule to a modal formula.

Proof. Let the normal description $S=\{ (S_{R}^{i},S_{=}^{i}) \}_{i\in I}$ be given.

In order to compute the disjunction form for the hypersequent rule induced by S, we first rewrite the rule as follows:

In the above, we have partitioned $I=I_{1}\sqcup I_{2}$ such that $S_{=}^{i} = \emptyset $ iff $i\in I_{2}$ . For the purpose of obtaining an association form as done in Section 5.2 we begin by reading $\Box \Gamma _{j}'$ and $\boxtimes \Gamma _{j}'$ as the same multiset schematic-variable. Following that algorithm, the distinguished variable occurrences of each active component in the premises are: some $\Sigma _{j}$ ( $j\in S_{=}^{i}$ ) for $i\in I_{1}$ , and some $\boxtimes \Gamma _{j}'$ ( $j\in S_{R}^{i}$ ) for $i\in I_{2}$ . Associating $\Box \Gamma _{j}'$ and $\boxtimes \Gamma _{j}'$ to the same propositional variable, construct $\text {Form}(r(S))$ from the association form (Definition 19). The required formula ${{\text {Form}^{\Box }(r(S))}}$ is obtained by amending $\text {Form}(r(S))$ as follows:

1. (i) Replace every leading disjunct $B\land 1$ by B (if B is boxed) or $\Box B$ (otherwise).

2. (ii) A $\Box $ is placed in front of every propositional variable.

Now follow the proof for $\text {Form}(r(S))$ (Theorem 21) to prove that ${{\text {Form}^{\Box }(r(S))}}$ is a disjunction formula (provability, weakening, and splitting property). Regarding the amendments, observe that these can be emulated by applying the appropriate modal rules: for (i), use (4) to introduce a leading $\Box $ ; for (ii), start with $\Box p\Rightarrow \Box p$ rather than $p\Rightarrow p$ . We do have to account for our reading of $\Box \Gamma _{j}'$ and $\boxtimes \Gamma _{j}'$ as the same variable despite these multiset schematic-variables having different instantiations (the former permits instantiation only by $\{\Box A_{1},\ldots,\Box A_{k}\}$ and the latter only by $\{A_{1},\Box A_{1},\ldots,A_{k},\Box A_{k}\}$ ). It turns out that this is not problematic because every instantiation of “strong box variable $\Rightarrow $ its box variable” and “box variable $\Rightarrow $ its strong box variable” is derivable in $\mathbf {S4}$ .

To obtain a multiset-axiomatisation we follow the proof of Theorem 13. The only thing to check is that each disjunct in the disjunction form can be permuted downwards, i.e., adding this formula to the antecedents of the premise(s) and conclusion of a rule instance should not invalidate the rule instance. This holds for the instances of the $(4)$ rule because this formula is boxed due to (i), and it is immediate for the other rules. Finally, a set-axiomatisation follows from the presence of contraction and weakening, refer to Lemma 24. ⊣

The above proof relies on the presence of the $(T)$ and $(4)$ rules. In particular, if the $(4)$ rule was replaced by the standard modal rule for $\mathbf {K}$ , then the addition of a boxed formula to the premise and conclusion of the latter would invalidate the rule instance. This is why the theorem is framed with respect to $\mathbf {S4}$ .

Example 41. Consider $r(S_{lin})$ in Example 39. Read $\Box \Gamma _{1}'$ and $\boxtimes \Gamma _{1}'$ as the same variable, and read $\Box \Gamma _{2}'$ and $\boxtimes \Gamma _{2}'$ as the same variable to obtain the association form. Associating $\Box \Gamma _{1}'$ and $\boxtimes \Gamma _{1}'$ with the propositional variable p, and $\Box \Gamma _{2}'$ and $\boxtimes \Gamma _{2}'$ with the propositional variable q, we obtain

$$ \begin{align*} \text{Form}(r(S_{lin})):= ((p\rightarrow q){\land 1})\lor ((q\rightarrow p){\land 1}). \end{align*} $$

Applying (i) we get $\Box (p\rightarrow q)\lor \Box (q\rightarrow p)$ . After (ii) we obtain

$$ \begin{align*} {{\text{Form}^{\Box}(r(S_{lin}))}}:= \Box (\Box p\rightarrow \Box q)\lor \Box (\Box q\rightarrow \Box p). \end{align*} $$

Let us prove that $\Box (\Box p\rightarrow \Box q)\lor \Box (\Box q\rightarrow \Box p)$ is a disjunction form of $r(S_{lin})$ . The following derivation in $\mathbf {HS4}$ witnesses one half of the splitting property (the other derivation is analogous).

Observe that the instance of the right disjunct of the disjunction formula above is obtained by the substitution $q\mapsto \land \Box \Gamma _{2}'$ and $p\mapsto \land \Box \Gamma _{1}'$ , analogous to the substructural case. The following establishes the provability property.

7.3. A new syntactic proof of analyticity for $\mathbf {S5}$

A sequent calculus for $\mathbf {S5}$ is obtained by the addition of the rules $(T)$ and $(5)$ to the sequent calculus $\mathbf {LK}$ for classical propositional logic:

In response to the failure of cut-elimination for this calculus, Takano [Reference Takano45] gave an intricate syntactic proof of analyticity, establishing that only cuts on subformulas are required. Prior to that, only a semantic argument had been shown, see [Reference Fitting17].

A formula-axiomatisation for $\mathbf {S5}$ can be established along the lines of Theorem 38. Is it possible to tweak the methodology of this paper to obtain Takano’s (stronger) analyticity result? The answer is affirmative, as shown below.

Proof. Our starting point is a cut-free hypersequent calculus for $\mathbf {S5}$ presented in [Reference Kurokawa, Nakano, Satoh and Bekki28]. It extends $\mathbf {HS4}$ by the rule

This is a special case of Avron’s rule $(MS_{Av})$ (cf. Example 2). Cut-free $\mathbf {HS4}+{(MS)}$ derives exactly the same sequents as the sequent calculus for $\mathbf {S5}$ . Moreover, any instance of the rule ${(MS)}$ can be simulated using $(ec)$ , $(w_l)$ , and using multiple instances of its single formula version ${(MS_1)}$ below:

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, refer to the proof of Theorem 13). 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,\Gamma \Rightarrow \Pi $ ) has a $\Box A$ in the succedent (resp. antecedent) that was not present in the original derivation d. Proceed downward from each hypersequent mimicking the rules in d. Although these hypersequents each contain an additional occurrence of $\Box A$ that needs to be propagated downwards, the same rule can be used for this purpose provided it is not $(4)$ . The issue with $(4)$ is that it permits only a single formula in the succedent and the additional $\Box A$ in the succedent would violate this. The solution is to use $(5)$ instead. 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 succedent 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. Since every rule in $\mathbf {HS5}$ has one active component, we can extract an analytic derivation of S in the sequent calculus for $\mathbf {S5}$ .⊣