Interpolation Method for Multicomponent Sequent Calculi

Abstract

The proof-theoretic method of proving the Craig interpolation property was recently extended from sequents to nested sequents and hypersequents. There the notations were formalism-specific, obscuring the underlying common idea, which is presented here in a general form applicable also to other similar formalisms, e.g., prefixed tableaus. It describes requirements sufficient for using the method on a proof system for a logic, as well as additional requirements for certain types of rules. The applicability of the method, however, does not imply its success. We also provide examples from common proof systems to highlight various types of interpolant manipulations that can be employed by the method. The new results are the application of the method to a recent formalism of grafted hypersequents (in their tableau version), the general treatment of external structural rules, including the analytic cut, and the method’s extension to the Lyndon interpolation property.

R. Kuznets—Supported by the Austrian Science Fund (FWF) Lise Meitner grant M 1770-N25.

1 Introduction

Along with decidability and compactness, the Craig interpolation property (CIP) is one of the principal properties desired of any logic. One way of demonstrating it by constructing the interpolant is the so-called proof-theoretic method, which relies on an analytic proof system for the logic. Until recently, the scope of the method has been limited to logics that can be captured by analytic sequent (equivalently, tableau) proof formalisms, as well as by display and resolution calculi, the discussion of which is outside the scope of this paper.

In [6], it was shown how to prove the CIP using nested sequents. In [9], written and accepted before this paper but likely to be published after it, the same principles were successfully applied to hypersequents. An anonymous reviewer of [9] noted that the nested and hypersequent cases are essentially the same. The purpose of this paper, which is based on a talk given at the Logic Colloquium 2015, is to present a general formal method in uniform notation, of which both prior applications are instances. Note that the applicability of the method does not imply that the CIP can be proved using this method or, indeed, at all. For instance, the method is applicable to the hypersequent calculi for S4.3 from [7, 8, 11], but S4.3 does not have the CIP [13].

Let us first outline how general our method is intended to be. We concentrate on internal calculi, which excludes display and labelled sequent calculi. We consider only calculi whose basic unit is what we call a multisequent, i.e., an object that can be viewed as a hierarchy of components with each component containing a(n ordinary) sequent, called a sequent component. Since a sequent is essentially a single-component multisequent, the method for multisequents (partially) subsumes the well-known method for sequents. Following [4], we restrict the type of sequents used to the so-called symmetric sequents, which are best suited for interpolation proofs.

Definition 1

(Symmetric Sequents). Rules of a symmetric sequent system operate on 2-sided sequents with formulas in negation normal form¹ in such a way that formulas never move between the antecedent and the consequent.

The use of symmetric sequent systems is not required by the method (neither of [6, 9] used them). Rather, they are a contrivance used to avoid splitting sequents, first introduced by Maehara in [12] written in Japanese. Splitting a 2-sided sequent results in a rather counter-intuitive 4-sided contraption, whereas splitting a 1-sided sequent is more or less isomorphic to working with a 2-sided symmetric sequent. However, the restriction to symmetric sequents has an unfortunate side-effect: it rules out the application of our method to subclassical logics, which lack De Morgan laws. For such logics, so far we have not been able to use split 2-sided sequents either.

In this paper, by the common language invoked by the more general formulations of the CIP, we understand common propositional variables, with all examples taken from propositional modal logics.

Thus, the proof-theoretic part of our recipe requires a description of a propositional modal logic by a symmetric multisequent proof system. There is one more necessary (for now) ingredient: the modal logic in question needs to have a Kripke semantics (with the standard local interpretation of $\mathbin {\wedge }$ and $\mathbin {\vee }$). Although the algorithm is designed using semantic reasoning (in cases of a successful application of the method), the final algorithm for computing interpolants makes no mention of semantics, remaining fully internal.

2 Sufficient Criteria of Applicability

As discussed in the previous section, we assume that we are given a propositional modal logic $\mathsf{L}$ described by a symmetric multisequent proof system $\mathbf {SL}$ and complete with respect to a class $\mathcal {C}_{\mathsf {L}}$ of Kripke models. The logic $\mathsf{L}$ is formulated in a language $\mathcal {L}$ in negation normal form. Each multisequent is (can be viewed as) a hierarchy of components, each containing some sequent component $\varGamma \Rightarrow \varDelta$, where the antecedent $\varGamma$ and consequent $\varDelta$ are multisets (sets, sequences) of $\mathcal {L}$-formulas that are called antecedent and consequent formulas respectively.

Definition 2

(Craig Interpolation Property). A logic $\mathsf{L}$ has the CIP iff whenever $\mathsf{L}\vdash A \mathbin {\rightarrow }B$, there is an interpolant $C \in \mathcal {L}$ such that each propositional variable of C occurs in both A and B and such that $\mathsf{L}\vdash A \mathbin {\rightarrow }C$ and $\mathsf{L}\vdash C \mathbin {\rightarrow }B$.²

Our method requires relationships among $\mathsf{L}$, $\mathbf {SL}$, and $\mathcal {C}_{\mathsf {L}}$ stronger than completeness. The first requirement is the completeness of $\mathbf {SL}$ w.r.t. implications.

Definition 3

(Singleton Multisequent). A singleton multisequent is a multisequent with exactly one component.

Requirement I

If $\mathsf{L}\vdash A \mathbin {\rightarrow }B$, then $\mathbf {SL}\vdash \mathcal {G}$ for some singleton multisequent $\mathcal {G}$ with sequent component $A \Rightarrow B$.

The second requirement is semantical completeness w.r.t. implications:

Definition 4

(Logical Consequence). For sets (multisets, sequences) $\varGamma$ and $\varDelta$ of $\mathcal {L}$-formulas, $\varGamma \vDash _{\mathcal {C}_{\mathsf {L}}} \varDelta$ if, for each model $\mathcal {M}\in \mathcal {C}_{\mathsf {L}}$ and each world w of $\mathcal {M}$,

$$\begin{aligned} \mathcal {M}, w \Vdash A \text { for each }A\in \varGamma \qquad \Longrightarrow \qquad \mathcal {M}, w \Vdash B \text { for some }B\in \varDelta {.} \end{aligned}$$

Requirement II

If $A \vDash _{\mathcal {C}_{\mathsf {L}}} B$, then $\mathsf{L}\vdash A \mathbin {\rightarrow }B$.

Formulating the next requirement requires preparation. The idea of our method is to consider maps f from the components of a given multisequent $\mathcal {G}$ to the worlds of a given model $\mathcal {M}\in \mathcal {C}_{\mathsf {L}}$ and to evaluate formulas from a component $\alpha$ of $\mathcal {G}$ (i.e., formulas from the sequent component $\varGamma \Rightarrow \varDelta$ contained at $\alpha$) at the world $f(\alpha )\in \mathcal {M}$. To faithfully represent the component hierarchy peculiar to the multisequent system $\mathbf {SL}$, however, we need to restrict these maps. For each multisequent type and each class of models considered, we require that the notion of good map be defined for each pair of a multisequent and a model. After we formulate what is needed from such maps, we give examples of good maps for nested sequents and hypersequents.

Remark 5

By a slight abuse of notation, we write $f :\mathcal {G}\rightarrow \mathcal {M}$ for a mapping from the components of $\mathcal {G}$ to the worlds of $\mathcal {M}$. In the same vein, we write $\alpha \in \mathcal {G}$ to state that $\alpha$ is a component of $\mathcal {G}$ and $w \in \mathcal {M}$ to state that w is a world in $\mathcal {M}$.

Requirement III

If $\mathbf {SL}\vdash \mathcal {G}$, then for each model $\mathcal {M}\in \mathcal {C}_{\mathsf {L}}$ and for each good map $f :\mathcal {G}\rightarrow \mathcal {M}$, there exists a component $\alpha \in \mathcal {G}$ containing $\varGamma \Rightarrow \varDelta$ such that

$$\begin{aligned} \mathcal {M}, f(\alpha ) \nVdash A \text { for some }A \in \varGamma \qquad \text {or}\qquad \mathcal {M}, f(\alpha ) \Vdash B \text { for some }B \in \varDelta {.} \end{aligned}$$

In other words, we understand a multisequent as a multiworld disjunction of its sequent components and require this disjunction to be valid with respect to all good maps, which direct where each sequent component is to be evaluated.

Example 6

(Nested sequents). Nested sequents are often described as trees of sequents (and are sometimes called tree hypersequents). To transfer this tree hierarchy of components into models, we define good maps from a given nested sequent $\mathcal {G}$ to a given model $\mathcal {M}= (W, R, V)$ to be those that satisfy the following condition: if $\beta$ is a child of $\alpha$ in $\mathcal {G}$ , then $f(\alpha ) R f(\beta )$. It has been shown in [6] that Req. III is satisfied for all such maps.

Example 7

(Hypersequents). The standard formula interpretation of a hypersequent $\varGamma _1 \Rightarrow \varDelta _1 \mid \dots \mid \varGamma _n \Rightarrow \varDelta _n$ as $\bigvee \limits _{i=1}^n \Box \left( \bigwedge \varGamma _i \mathbin {\rightarrow }\bigvee \varDelta _i\right)$ suggests that good maps send all components to worlds accessible from a single root: good maps from a given hypersequent $\mathcal {G}$ to a given model $\mathcal {M}= (W, R, V)$ are all maps satisfying the following condition: there exists $w \in W$ such that $w R f(\alpha )$ for all $\alpha \in \mathcal {G}$. For some classes of models, this formulation can be simplified, e.g., if R is an equivalence relation for all models from $\mathcal {C}_{\mathsf {L}}$ (as in the case of S5), it is sufficient³ to require that $f(\alpha ) R f(\beta )$ for all $\alpha , \beta \in \mathcal {G}$.

Remark 8

Note that good maps are defined on components rather than on sequent components. This means that we must notationally distinguish occurrences of the same sequent component. The linear notation for hypersequents masks the problems when hypersequents are sets or multisets of sequents. We assume that in any multisequent system there is a way of distinguishing sequent components and rely on this, but we do not specify the details, which could involve converting sets/multisets to sequences as the underlying data structure for multisequent components and adding appropriate exchange rules or using explicit labels for sequent components.

Requirement IV

For each singleton multisequent with component $\alpha$, each model $\mathcal {M}\in \mathcal {C}_{\mathsf {L}}$, and each world $w \in \mathcal {M}$, the map $\{(\alpha , w)\}$ must be a good map.

3 Reducing the CIP to the Componentwise Interpolation

Our aim is to generalize the CIP to multiple components. In particular, interpolants are to be evaluated via good maps and, hence, cannot be mere formulas.

Definition 9

(Uniformula). A uniformula is obtained from a multisequent $\mathcal {G}$ by replacing all sequent components in $\mathcal {G}$ with such multisets of formulas that the union of these multisets contains exactly one formula.

In other words, a uniformula is a single formula C placed at a particular component $\alpha$ of a given multisequent $\mathcal {G}$. We call C the formula contained in the uniformula and the component $\alpha$ the active component of the uniformula. Let $\mathcal {G}(\underbrace{\varGamma _1\Rightarrow \varDelta _1}_{\alpha _1};\dots ;\underbrace{\varGamma _n\Rightarrow \varDelta _n}_{\alpha _n})$ for $n\ge 0$ denote a multisequent with displayed components $\alpha _i$ containing sequents $\varGamma _i \Rightarrow \varDelta _i$. By $\mathcal {G}^\circ (\alpha _1;\dots ;\alpha _n)$ we denote the result of removing all sequent components from $\mathcal {G}(\varGamma _1\Rightarrow \varDelta _1;\dots ;\varGamma _n\Rightarrow \varDelta _n)$ but keeping its components with the hierarchy intact. Further, we allow to insert new objects, such as formulas, into a displayed component $\alpha _i$. Thus, each uniformula has the form $\mathcal {G}^\circ (C)$ for some multisequent $\mathcal {G}(\varGamma \Rightarrow \varDelta )$ and some formula C.

Definition 10

(Multiformula). A multiformula $\mho$ with structure $\mho ^\circ$ is defined as follows. Each uniformula $\mathcal {G}^\circ (A)$ is a multiformula with structure $\mathcal {G}^{\circ }(\alpha )$. If $\mho _1$ and $\mho _2$ are multiformulas with $\mho _1^\circ = \mho _2^\circ$, then and are also multiformulas with the same structure.

To be able to formulate a generalized interpolation statement, we need to define a satisfaction relation between good maps and multiformulas, which are used as interpolants. For any two multisequents/multiformulas with the same structure, there is a unique way of transferring a good map from one onto the other.

Definition 11

( $\Vdash$ on Multiformulas). Let $f :\mathcal {G}^\circ (\alpha ) \rightarrow \mathcal {M}$. For a uniformula $\mathcal {G}^\circ (C)$, we say that $f \Vdash \mathcal {G}^\circ (C)$ iff $\mathcal {M}, f(\alpha ) \Vdash C$.

If is defined, then $\mho _1^\circ =\mho _2^\circ$. Let f be a map from this structure to a model $\mathcal {M}$. iff $f \Vdash \mho _i$ for some (each) $i=1,2$.

In other words, a uniformula is forced by a map if the formula contained in it is forced at the world to which the active component is mapped. The external conjunction  and disjunction  on multiformulas behave classically.

To define the Componentwise Interpolation Property, we use abbreviations:

Definition 12

For a good map f from a multisequent $\mathcal {G}$ to a model $\mathcal {M}$, we write $f\vDash \mathsf {Ant}(\mathcal {G})$ if $\mathcal {M}, f(\alpha ) \Vdash A$ for each component $\alpha \in \mathcal {G}$ and each antecedent formula A contained in $\alpha$. We write $f\vDash \mathsf {Cons}(\mathcal {G})$ if $\mathcal {M}, f(\beta ) \Vdash B$ for some component $\beta \in \mathcal {G}$ and some consequent formula B contained in $\beta$.

Definition 13

(Componentwise Interpolation Property, or CWIP). A multiformula $\mho$ is a (componentwise) interpolant of a multisequent $\mathcal {G}$, written $\mathcal {G}\longleftarrow \mho$, if $\mho ^\circ =\mathcal {G}^\circ$ and the following two conditions hold:

• 1. if a propositional variable occurs in $\mho$, it must occur both in some antecedent formula of $\mathcal {G}$ and in some consequent formula of $\mathcal {G}$ ;

• 2. for each model $\mathcal {M}\in \mathcal {C}_{\mathsf {L}}$ and each good map $f:\mathcal {G}\rightarrow \mathcal {M}$,

  $$\begin{aligned} f \vDash \mathsf {Ant}(\mathcal {G}) \quad \Longrightarrow \quad f \Vdash \mho \qquad \text {and}\qquad f \Vdash \mho \quad \Longrightarrow \quad f \vDash \mathsf {Cons}(\mathcal {G}) {.} \end{aligned}$$

  (1)

A multisequent proof system $\mathbf {SL}$ has the CWIP iff every derivable multisequent has an interpolant.

The CIP can be reduced to the CWIP if Reqs. I–IV are satisfied. The proof of the reduction requires another small piece of notation.

Definition 14

(Componentwise Equivalence). Multiformulas $\mho _1$ and $\mho _2$ are called componentwise equivalent, written $\mho _1 \equiv \mho _2$, provided $\mho _1^\circ = \mho _2^\circ$ and $f \Vdash \mho _1 \Longleftrightarrow f \Vdash \mho _2$ for any good map f on the common structure of $\mho _1$ and $\mho _2$.

Remark 15

The classical reading of  and  implies that each multiformula can be transformed to a componentwise equivalent multiformula both in the DNF and in the CNF. This will be used for some of the rules in the following section.

Lemma 16

For singleton sequents, multiformulas and uniformulas are equiexpressive, i.e., for each multiformula $\mho$ with a structure $\mathcal {G}^\circ (\alpha )$ where $\alpha$ is the only component, there exists a uniformula $\mathcal {G}^\circ (C)$ such that $\mathcal {G}^\circ (C)\equiv \mho$ and it has the same propositional variables as $\mho$.

Proof

By induction on the construction of $\mho$. The case when $\mho$ is a uniformula is trivial. Let $\mho _1 \equiv \mathcal {G}^\circ (C_1)$ and $\mho _2 \equiv \mathcal {G}^\circ (C_2)$ for some structure $\mathcal {G}^\circ (\alpha )$. Then it is easy to see that and and that the condition on propositional variables is also satisfied.    $\square$

Theorem 17

(Reduction of CIP to CWIP). Let a logic $\mathsf{L}$, a multisequent proof system $\mathbf {SL}$, and a class of Kripke models $\mathcal {C}_{\mathsf {L}}$ satisfy all Reqs. I–IV. If $\mathbf {SL}$ enjoys the CWIP, then $\mathsf{L}$ enjoys the CIP.

Proof

Assume that $\mathbf {SL}$ satisfies the CWIP and that $\mathsf{L}\vdash A \mathbin {\rightarrow }B$. Then, by Req. I, $\mathbf {SL}\vdash \mathcal {G}(A \Rightarrow B)$ for some singleton multisequent $\mathcal {G}(A \Rightarrow B)$, which has a componentwise interpolant $\mho$ by the CWIP. By Lemma 16, $\mathcal {G}(A \Rightarrow B) \longleftarrow \mathcal {G}^\circ (C)$ for some uniformula $\mathcal {G}^\circ (C)$. Since A is the only antecedent and B is the only consequent formula of $\mathcal {G}(A \Rightarrow B)$, each propositional variable of C must occur in both A and B. For any model $\mathcal {M}\in \mathcal {C}_{\mathsf {L}}$ and any world $w \in \mathcal {M}$, by Req. IV, $f := \{(\alpha , w)\}$ is a good map on $\mathcal {G}(A \Rightarrow B)$. In particular, $f \vDash \mathsf {Ant}(\mathcal {G}(A \Rightarrow B))$ implies $f \Vdash \mathcal {G}^\circ (C)$, i.e., $\mathcal {M}, w \Vdash A$ implies $\mathcal {M}, w \Vdash C$. Given the arbitrariness of $\mathcal {M}$ and w, we conclude that $A \vDash _{\mathcal {C}_{\mathsf {L}}} C$. It now follows from Req. II that $\mathsf{L}\vdash A \mathbin {\rightarrow }C$. The proof of $\mathsf{L}\vdash C \mathbin {\rightarrow }B$ is analogous.    $\square$

Remark 18

An attentive reader would notice the absence of Req. III, the most complex one, from the proof of Theorem 17. While the reduction does not rely on Req. III, its violation renders the reduction vacuous by denying the possibility of the CWIP for $\mathbf {SL}$. Indeed, if Req. III is violated, i.e., $\mathbf {SL}\vdash \mathcal {G}$ and $f \vDash \mathsf {Ant}(\mathcal {G})$ but $f \nvDash \mathsf {Cons}(\mathcal {G})$ for some $\mathcal {M}\in \mathcal {C}_{\mathsf {L}}$ and some good map $f :\mathcal {G}\rightarrow \mathcal {M}$, then no multiformula $\mho$ could satisfy (1) for this f.

4 Demonstrating the CWIP

In this section, strategies for proving the CWIP for various types of multisequent rules are described. For many common types of rules, a general (but not universal) recipe for handling them is presented. Thus, every statement in this section is implicitly prefaced by the qualifier “normally”.

Initial Sequents are interpolated by uniformulas. It is easy to see that the following are interpolants for the most popular initial sequents:

$$\begin{aligned} \mathcal {G}(\varGamma , A \Rightarrow A, \varDelta )&\longleftarrow \mathcal {G}^\circ (A)&\mathcal {G}(\varGamma \Rightarrow A, \overline{A},\varDelta )&\longleftarrow \mathcal {G}^\circ (\top ) \\ \mathcal {G}(\varGamma , \overline{A} \Rightarrow \overline{A}, \varDelta )&\longleftarrow \mathcal {G}^\circ (\overline{A})&\mathcal {G}(\varGamma , \bot \Rightarrow \varDelta )&\longleftarrow \mathcal {G}^\circ (\bot ) \\ \mathcal {G}(\varGamma , A, \overline{A} \Rightarrow \varDelta )&\longleftarrow \mathcal {G}^\circ (\bot )&\mathcal {G}(\varGamma \Rightarrow \top , \varDelta )&\longleftarrow \mathcal {G}^\circ (\top ) \end{aligned}$$

Single-Premise Local Rules. By a local rule we mean a rule that does not affect the components and affects the sequent components mildly enough to use the same map for the conclusion and the premise(s) (cf. component-shifting rules on p. 13). (Normally,) single-premise local rules require no change to the interpolant. We formulate sufficient criteria for reusing the interpolant and then list common rules satisfying them.

Lemma 19

Consider a single-premise rule such that $\mathcal {G}^\circ = \mathcal {H}^\circ$ and such that no antecedent and no consequent propositional variable from $\mathcal {G}$ disappears in $\mathcal {H}$. If for any good map f on the common structure of $\mathcal {G}$ and $\mathcal {H}$,

$$\begin{aligned} f \vDash \mathsf {Ant}(\mathcal {H}) \,\Longrightarrow \, f \vDash \mathsf {Ant}(\mathcal {G}) \qquad \text {and}\qquad f \vDash \mathsf {Cons}(\mathcal {G}) \,\Longrightarrow \, f \vDash \mathsf {Cons}(\mathcal {H}) {,} \end{aligned}$$

then $\mathcal {H}\longleftarrow \mho$ whenever $\mathcal {G}\longleftarrow \mho$ .

Proof

Follows directly from the definition of componentwise interpolation.    $\square$

This almost trivial observation captures most of the common single-premise propositional rules, both logical and internal structural. We only provide a non-exhaustive list, leaving the proof to the reader: internal weakening IW, internal contraction IC, internal exchange IEx, and both internal-context sharing and splitting versions of the left conjunction and right disjunction rules; some modal rules can also be treated this way: e.g., the multisequent T rules for reflexive models or the multisequent (local) D rules for serial models; an example of such a rule with multiple active components is the hypersequent rule $\mathsf \Box \mathrm{L}^{s}$ from [14] and its symmetric version $\mathsf \Diamond \mathrm{L}^{s}$ for equivalence models with good maps from Example 7 (see Fig. 1). The variants of these logical rules with embedded internal contraction are also local.

Fig. 1.

Rules not requiring changes to the interpolant by Lemma 19

Multi-premise Local Rules are those for which any good map on the conclusion can be applied to any of the premises. It follows directly from the definition of CWIP:

Lemma 20

(Conjunctive Rules). Consider a rule such that $\mathcal {G}_1^\circ = \dots = \mathcal {G}_n^\circ = \mathcal {H}^\circ$ and such that no antecedent and no consequent propositional variable from any $\mathcal {G}_i$ disappears in $\mathcal {H}$. If for any good map f on the common structure of $\mathcal {G}_i$’s and $\mathcal {H}$,

$$\begin{aligned} f \vDash \mathsf {Ant}(\mathcal {H}) \,\Longrightarrow \, (\forall i) \bigl (f \vDash \mathsf {Ant}(\mathcal {G}_i)\bigr ) \quad \!\text {and}\quad \! (\forall i) \bigl (f \vDash \mathsf {Cons}(\mathcal {G}_i)\bigr ) \,\Longrightarrow \, f \vDash \mathsf {Cons}(\mathcal {H}), \end{aligned}$$

then whenever $\mathcal {G}_i \longleftarrow \mho _i$ for each $i=1,\dots ,n$ .

Lemma 21

(Disjunctive Rules). Consider a rule such that $\mathcal {H}^\circ = \mathcal {G}_1^\circ = \dots = \mathcal {G}_n^\circ$ and such that no antecedent and no consequent propositional variable from any $\mathcal {G}_i$ disappears in $\mathcal {H}$. If for any good map f on the common structure of $\mathcal {G}_i$’s and $\mathcal {H}$,

$$\begin{aligned} f \vDash \mathsf {Ant}(\mathcal {H}) \,\Longrightarrow \, (\exists i) \bigl (f \vDash \mathsf {Ant}(\mathcal {G}_i)\bigr ) \quad \!\text {and}\quad \! (\exists i) \bigl (f \vDash \mathsf {Cons}(\mathcal {G}_i)\bigr ) \,\Longrightarrow \, f \vDash \mathsf {Cons}(\mathcal {H}) {,} \end{aligned}$$

then whenever $\mathcal {G}_i \longleftarrow \mho _i$ for each $i=1,\dots ,n$ .

The remaining propositional rules fall under the scope of these two lemmas: it is easy to see that both the internal-context splitting and sharing versions of the right conjunction rule $\Rightarrow \mathbin {\wedge }$ (see Fig. 2) are conjunctive and both versions of the left disjunction rule $\mathbin {\vee }\Rightarrow$ (see Fig. 3) are disjunctive rules in this sense.

Fig. 2.

Propositional conjunctive rules in the sense of Lemma 20

Fig. 3.

Propositional disjunctive rules in the sense of Lemma 21

Analytic Cut. Another common local rule is cut. While the general cut rule is problematic even in the sequent case, it is well known that analytic cuts can be handled (see [4]). To extend this handling to the external-context sharing and internal-context splitting cuts on multisequents (see Fig. 4), we impose a condition that is both stronger and weaker than analyticity. While A need not appear as a subformula in the conclusion as long as all its propositional variables occur there, these propositional variables must be on the same side of $\Rightarrow$ as in A or $\overline{A}$ displayed in the premises. This condition is necessary to use the interpolants of both premises and the formula $\overline{A}$ in constructing the interpolant for the conclusion.

Lemma 22

(Analytic Cut). For the cut rules from Fig. 4, if no antecedent and no consequent propositional variable from any premise disappears in the conclusion, then $(\mathrm {Cut}\Rightarrow )$ and $(\Rightarrow \mathrm {Cut})$ are a disjunctive and conjunctive rule respectively and can be treated according to Lemmas 21 or 20 respectively. For the $(\mathrm {C}\overset{\mathrm {u}}{\Rightarrow }\mathrm {t})$ rule, we have whenever $\mathcal {G}(\varGamma _1 \Rightarrow A, \varDelta _1) \longleftarrow \mho _1$ and $\mathcal {G}(\varGamma _2, A \Rightarrow \varDelta _2) \longleftarrow \mho _2$.

Proof

The common language requirement is clearly satisfied. Consider an arbitrary good map f from the common structure of the premises and the conclusion of $(\mathrm {C}\overset{\text {u}}{\Rightarrow }\text {t})$ to some $\mathcal {M}\in \mathcal {C}_{\mathsf {L}}$. Assume first that $f \vDash \mathsf {Ant}\bigl (\mathcal {G}(\varGamma _1, \varGamma _2 \Rightarrow \varDelta _1, \varDelta _2)\bigr )$. It is immediate that $f \vDash \mathsf {Ant}\bigl (\mathcal {G}(\varGamma _1 \Rightarrow A, \varDelta _1)\bigr )$ and, hence, $f \Vdash \mho _1$. Further, either $\mathcal {M}, f(\alpha ) \Vdash A$ or $\mathcal {M}, f(\alpha ) \nVdash A$ for the active component $\alpha$. In the latter case, $f \Vdash \mathcal {G}^\circ (\overline{A})$.⁴ In the former case, $f\vDash \mathsf {Ant}\bigl (\mathcal {G}(\varGamma _2, A \Rightarrow \varDelta _2)\bigr )$ implying $f \Vdash \mho _2$. In either case, for the second conjunct of the proposed interpolant.

Assume now that . It follows from $f \Vdash \mho _1$ that $f \vDash \mathsf {Cons}\bigl (\mathcal {G}(\varGamma _1 \Rightarrow A, \varDelta _1)\bigr )$. If one of the forced formulas is not the displayed A, then $f \vDash \mathsf {Cons}\bigl (\mathcal {G}(\varGamma _1, \varGamma _2 \Rightarrow \varDelta _1, \varDelta _2)\bigr )$, which is the desired result. Otherwise, we have $\mathcal {M}, f(\alpha ) \Vdash A$. In this case, $f \nVdash \mathcal {G}^\circ (\overline{A})$ implying $f \Vdash \mho _2$. This, in turn, implies $f \vDash \mathsf {Cons}\bigl (\mathcal {G}(\varGamma _2, A \Rightarrow \varDelta _2)\bigr )$ and $f \vDash \mathsf {Cons}\bigl (\mathcal {G}(\varGamma _1, \varGamma _2 \Rightarrow \varDelta _1, \varDelta _2)\bigr )$ again.   $\square$

Remark 23

Lemma 22 also applies to one-to-one multicut rules allowing multiple copies of the cut formula in both premises in Fig. 4.

External Structural Rules. From now on, interpolants for most rules rely on the specifics of goodness conditions. The guiding principle is that any good map on the conclusion of the rule needs to be transformed in some natural and general way into a good map on the premise(s). We start with rule types that are reasonably common across various sequent types: external weakening EW, external contraction EC, external mix, and external exchange EEx.

Fig. 4.

Cut rules

Fig. 5.

External structural rules EW and mix

External weakening. By external weakening rules we understand rules EW from Fig. 5 where the conclusion is obtained by adding new components in such a way that all the sequent components already present in the premise, along with the hierarchical relationships among their components, remain intact.

Requirement V

(For EW ). For each instance of EW from Fig. 5 and each good map f on its conclusion, the restriction $f \!\upharpoonright \!\mathcal {G}()$ of f onto the components of $\mathcal {G}()$ must be a good map on the premise.

Lemma 24

(External Weakening). Let $\mathcal {G}() \longleftarrow \mho$ for an instance of EW from Fig. 5 and $\mho '$ be the result of adding empty components $\alpha _1,\dots ,\alpha _n$ to each uniformula in $\mho$ in the same way they are added in the rule. Then Req. V implies $\mathcal {G}(\varGamma _1 \Rightarrow \varDelta _1;\dots ;\varGamma _n \Rightarrow \varDelta _n) \longleftarrow \mho '$.

Proof

For a good map $f :\mathcal {G}(\varGamma _1 \Rightarrow \varDelta _1;\dots ;\varGamma _n \Rightarrow \varDelta _n) \rightarrow \mathcal {M}$, the map $f \!\upharpoonright \!\mathcal {G}()$ is good by Req. V. If $f \vDash \mathsf {Ant}\bigl (\mathcal {G}(\varGamma _1 \Rightarrow \varDelta _1;\dots ;\varGamma _n \Rightarrow \varDelta _n)\bigr )$, then $f\!\upharpoonright \!\mathcal {G}() \vDash \mathsf {Ant}\bigl (\mathcal {G}()\bigr )$. Thus, $f\!\upharpoonright \!\mathcal {G}() \Vdash \mho$. It is easy to show by induction on the construction of $\mho$ that $f \Vdash \mho '$ iff $f\!\upharpoonright \!\mathcal {G}() \Vdash \mho$. Thus, $f \Vdash \mho '$. The argument for the consequents is similar. The common language condition is also clearly fulfilled.   $\square$

The external weakening rules of both hypersequents and nested sequents are covered by this lemma w.r.t. good maps from Examples 7 and 6 respectively.

Example 25

Consider symmetric nested sequents written in a hybrid Brünnler–Poggiolesi notation (a similar notation has been used in [5]). By Lemma 24,

Mix and external contraction rules. By mix rules we understand rules mix from Fig. 5 where the conclusion is obtained by transferring all antecedent and consequent formulas contained in each $\beta _i$, $i=1,\dots ,n$, to the antecedent and consequent respectively of $\alpha _i$ and removing the emptied components $\beta _i$.

Requirement VI

(For mix and EC ). For each instance of mix from Fig. 5 and each good map f on its conclusion, $f[\mathbf {\alpha }\Rrightarrow \mathbf {\beta }] \! := \! f \cup \{(\beta _1, f(\alpha _1)), \dots , (\beta _n, f(\alpha _n))\}$ must be a good map on the premise.

Lemma 26

(Mix). Let $\mathcal {G}(\varGamma _1 \Rightarrow \varDelta _1; \varPi _1 \Rightarrow \varSigma _1; \dots ;\varGamma _n \Rightarrow \varDelta _n; \varPi _n \Rightarrow \varSigma _n ) \longleftarrow \mho$ for an instance of mix from Fig. 5. Let $\mho '$ be the result of moving each formula within each $\beta _i$ to $\alpha _i$, leaving formulas contained in components other than $\beta _i$ intact, and removing the emptied $\beta _i$’s from each uniformula in $\mho$. Then $\mathcal {G}(\varGamma _1, \varPi _1 \Rightarrow \varDelta _1, \varSigma _1;\dots ;\varGamma _n, \varPi _n \Rightarrow \varDelta _n, \varSigma _n) \longleftarrow \mho '$ whenever Req. VI is fulfilled.

Proof

If $f :\mathcal {G}(\varGamma _1, \varPi _1 \Rightarrow \varDelta _1, \varSigma _1;\dots ;\varGamma _n, \varPi _n \Rightarrow \varDelta _n, \varSigma _n) \rightarrow \mathcal {M}$ is good, so is $f[\mathbf {\alpha }\Rrightarrow \mathbf {\beta }]$ by Req. VI. $f \vDash \mathsf {Ant}\bigl (\mathcal {G}(\varGamma _1, \varPi _1 \Rightarrow \varDelta _1, \varSigma _1;\dots ;\varGamma _n, \varPi _n \Rightarrow \varDelta _n, \varSigma _n) \bigr )$ implies $f[\mathbf {\alpha }\Rrightarrow \mathbf {\beta }] \vDash \mathsf {Ant}\bigl (\mathcal {G}(\varGamma _1 \Rightarrow \varDelta _1;\dots ;\varGamma _n \Rightarrow \varDelta _n;\quad \varPi _1 \Rightarrow \varSigma _1; \dots ; \varPi _n \Rightarrow \varSigma _n)\bigr )$ because formulas from each $\varPi _i$ are evaluated at $f[\mathbf {\alpha }\Rrightarrow \mathbf {\beta }](\beta _i) = f(\alpha _i)$, same as in f. Thus, $f[\mathbf {\alpha }\Rrightarrow \mathbf {\beta }] \Vdash \mho$. It is easy to show by induction on the construction of $\mho$ that $f \Vdash \mho '$ iff $f[\mathbf {\alpha }\Rrightarrow \mathbf {\beta }]\Vdash \mho$. Thus, $f \Vdash \mho '$. The argument for the consequents is similar. The common language condition is also fulfilled.   $\square$

For set-based sequent components, the external contraction EC is simply an instance of mix with $\varGamma _i = \varPi _i$ and $\varDelta _i = \varSigma _i$ for each $i=1,\dots ,n$. For multiset- and sequence-based ones, EC can be obtained from mix by internal contraction IC and internal exchange IEx. Since the definition of CWIP is not sensitive to multiplicities of formulas or their positions within the antecedent (consequent), Lemma 26 is equally applicable to EC (cf. also the application of Lemma 19 to IC and IEx).

Remark 27

Requirement VI does not yet guarantee that mix from Fig. 5 is a proper mix rule or that its variant with $\varGamma _i=\varPi _i$ and $\varDelta _i =\varSigma _i$ is a proper contraction rule: that requires the $\alpha$-components to have the same hierarchical relations as the $\beta$-components, both among themselves and as related to the rest of the multisequent. But this is not a problem of interpolation.

The external contraction rules of both hypersequents and nested sequents are covered by Lemma 26 w.r.t. good maps from Examples 7 and 6 respectively.

Example 28

An example of a nontrivial mix rule is medial from [2], represented here in the original nested-sequent notation: , with brackets used to represent the tree structure on the components. Thus, the root component of $\varDelta _1$ is mixed with that of $\varDelta _2$ and each child component of either root becomes a child of the mixed component. Below we present an example of the use of Lemma 26, where $C \Rightarrow D$ is mixed with $A \Rightarrow A$ :

Clearly, Req. VI is satisfied for $\mathsf{med}$ w.r.t. the good maps from Example 6.

Fig. 6.

Modal K rules

External Exchange. These are the rules that change the structure of the multisequent without changing a single sequent component. For them, it is sufficient to change the structures of each uniformula in the interpolant in the same way. It is required that good maps on the conclusion could be transferred to the premise without changing where each formula is evaluated.

Component-Removing Rules are modal rules that remove a component from the premise multisequent. Such rules can be highly logic-specific. We consider two most common ones that rely on the connection between the modality and the Kripke semantics and are likely to be present in one form or another in virtually every multisequent system. For these rules, the argument is almost the same as the one given in [6] for nested sequents. Hence, we only provide the proof for one. It should be noted that, to the best of our knowledge, these rules require the interpolant of the premise to be in the DNF or CNF, depending on the rule. We have not been able to extend the construction to arbitrary interpolants. For both rules in Fig. 6, the conclusion is obtained by removing the component $\beta$ with a single formula and transferring this formula, prefaced with an appropriate modality, to the component $\alpha$ (as usual, copying the modalized formula to the premise makes no difference).

Requirement VII

(For K Rules). For each instance of each rule from Fig. 6 and each good map f from its conclusion to a model $\mathcal {M}= (W, R, V)$, it is required that $f \cup \{(\beta , w)\}$ be a good map on the premise of the rule whenever $f(\alpha ) R w$.

Lemma 29

( K Rules). Consider an instance of $(\mathsf{K} \Rightarrow )$ from Fig. 6 and let

(2)

where $\beta$ is not the active component of any uniformula $\mho _{ij}(X_{ij}; \varnothing )$. Then

(3)

wherever Req. VII is fulfilled. Similarly, for the $(\Rightarrow \mathsf{K})$ rule, if

then, in the presence of Req. VII,

Proof

We prove the statement for the $(\mathsf{K} \Rightarrow )$ rule. Let $f \vDash \mathsf {Ant}\bigl (\mathcal {G}(\varGamma , \Diamond A \Rightarrow \varDelta )\bigr )$ for some good map $f :\mathcal {G}(\varGamma , \Diamond A \Rightarrow \varDelta ) \rightarrow \mathcal {M}$, where $\mathcal {M}= (W, R, V)$. Then $\mathcal {M}, f(\alpha ) \Vdash \Diamond A$, so that there exists a world $w \in W$ such that $f(\alpha ) R w$ and $\mathcal {M}, w \Vdash A$. By Req. VII, the good map $f\cup \{(\beta , w)\} \vDash \mathsf {Ant}\bigl (\mathcal {G}(\varGamma \Rightarrow \varDelta ; A \Rightarrow \;)\bigr )$. Assuming (2), the interpolant given there in the DNF is forced by $f\cup \{(\beta , w)\}$, i.e., for some i, the map $f\cup \{(\beta , w)\}$ forces one of the disjuncts of the DNF: in particular, $\mathcal {M}, w \Vdash C_{ik}$ for all $k=1,\dots , l_i$ for this i. Given that $f(\alpha ) R w$, we see that $\mathcal {M}, f(\alpha ) \Vdash \Diamond \bigwedge _{k=1}^{l_i} C_{ik}$.⁵ The removal of the empty $\beta$ component from the remaining $\mho _{ij}(X_{ij}; \varnothing )$ works the same way as for mix in Lemma 26. Thus, after the removal, all these uniformulas remain forced by f for this i. It follows that f forces the interpolant from (3). The argument for the consequents is analogous.

It is crucial that only one diamond formula has to be satisfied. This is used to find one world to extend the good map with. To single out such diamond formulas, the interpolant of the premise needs to be in the DNF.    $\square$

Composite Rules can be viewed as combinations of other rule types.

Component-shifting rules. Some rules seem local because the structure of the multisequent is unchanged, whereas in reality a new component is added to replace an old one. An example is the hypersequent $\mathsf \Box \mathrm{R}$ rule from [14], which can be obtained from EW and ($\Rightarrow \mathsf{K}$) (see Fig. 7), necessitating both Reqs. V and VII.

Seriality rules. It was shown in [6] that of the modal nested rules from [2], only the basic K rules (Fig. 6) and the seriality D rules require changing interpolants, with changes for the D rules obtained from those for the K rules by swapping the antecedent and consequent versions. An explanation is depicted in Fig. 8. The $\mathbin {\lnot }$ rules do not fit into our paradigm: they are from split sequents. But in this example the second $\mathbin {\lnot }$ cancels the problem created by the first one. Thus, a transformation can be guessed and then proved to be correct independently.

Fig. 7.

A rule that looks local but should be treated as composite

Fig. 8.

A composite component-removing rule with illegal transitions.

Multicut rule. Unlike in Rem. 23, the multi-to-one multicut rule is external-context splitting and, hence, not local. In addition, one component is juxtaposed against many in the other premise. Fortunately, it can always be represented as a combination of local one-to-one multicuts and rules EW, making our method directly applicable. For the lack of space, we leave the details to the reader.

5 Grafted Hypersequents

To show the versatility of our general method, we apply it to the prefixed-tableau version of a new type of multisequents called grafted hypersequents, introduced in [10]. A grafted hypersequent itself is a (possibly empty) hypersequent with an additional trunk component, separated from the others by $\parallel$. The formula interpretation for a hypersequent $\varGamma \Rightarrow \varDelta \parallel \varPi _1 \Rightarrow \varSigma _1 \mid \dots \mid \varPi _n \Rightarrow \varSigma _n$ is $\bigwedge \varGamma \mathbin {\rightarrow }\bigvee \varDelta \mathbin {\vee }\bigvee _{i=1}^n \Box (\bigwedge \varPi _i \mathbin {\rightarrow }\bigvee \varSigma _i)$. In [10], a prefixed tableau version equivalent to grafted hypersequents is developed for K5 and KD5. This system operates with signed prefixed formulas $\ell :\mathsf {S} A$, where the sign $\mathsf {S}\in \{\mathsf{T}, \mathsf{F}\}$ and the prefixes can be of three types: the trunk prefix $\bullet$, countably many limb prefixes $\mathbb {{1}}, \mathbb {{2}}, \dots$ and countably many twig prefixes $1, 2, \dots$. Twig prefixes do not appear in initial tableaus: they can only be introduced by tableau rules. Each branch of a tableau is considered to be a multisequent with each prefix $\ell$ on the branch determining the component $\ell$ that contains $\varGamma _\ell \Rightarrow \varDelta _\ell$ where $\varGamma _\ell := \{ A \mid \ell :\mathsf{T} A \text { occurs on the branch}\}$ and $\varDelta _\ell := \{ A \mid \ell :\mathsf{F} A \text { occurs on the branch}\}$. Since the prefix $\bullet$ is always present, the singleton multisequents contain no limb or twig prefixes. The interpolant is constructed beginning from a closed tableau and working backwards through the stages of the tableau derivation until the starting tableau whose only branch contains $\bullet :\mathsf{T} A$ and $\bullet :\mathsf{F} B$ is reached.

Example 30

(Grafted tableaus). A map from the prefixes occurring on a branch to worlds in a model $\mathcal {M}= (W, R, V)$ is called good if $f(\bullet ) R f(\mathbb {{n}})$ for any limb prefix $\mathbb {{n}}$ and $f(\bullet ) R^k f(m)$ for some $k>0$ for any twig prefix m.

Requirements I and II easily follow from the results of [10].⁶ Given the formula interpretation of grafted hypersequents, Req. III follows from the equivalence of grafted tableaus and grafted hypersequents ([10]), from Def. 30, and from the fact that twig components do not occur in initial tableaus. Req. IV is also trivial.

Fig. 9.

Grafted tableau rules for K5, where c and $\mathsf{c}'$ are either limb or twig prefixes

The propositional logical and all structural rules fall into the categories discussed above. The cut rule is eliminable. Thus, to demonstrate the CIP for K5, it is sufficient to consider the modal rules from [10] and their symmetric variants, as presented in Fig. 9. Written in our general notation, R2 and R6 coincide with $\mathsf{\Box L^s}$ while R4 and R8 coincide with $\mathsf \Diamond L^s$ from Fig. 1. The locality of the rules R2 and R4 directly follows from Def. 30 as $f(\bullet ) R f(\mathbb {{n}})$ for any good map. The locality of the rules R6 and R8 relies on the fact that $f(\bullet ) R^k f(\mathsf{c})$ and $f(\bullet ) R^l f(\mathsf{c}')$ for $k,l>0$ implies $f(\mathsf{c}) R f(\mathsf{c}')$ in Euclidean models. The rules R1 and R5 are variants of the $(\Rightarrow \mathsf{K})$ rule with the principal modal formula preserved in the premise, whereas R3 and R7 are such variants of the $(\mathsf{K}\Rightarrow )$ rule. Req. VII directly follows from Def. 30 for all four rules.

Fig. 10.

Grafted tableau rules for $\mathsf{KT}_\Box$, where c is either a limb or twig prefix

For the logic $\mathsf{KT}_\Box$ of shift reflexivity, the grafted hypersequents from [10] can be translated into grafted tableaus by replacing the modal rules R5–R8 from Fig. 9 with the modal rules S5–S8 from Fig. 10. Instead of Euclideanity, the semantic condition of shift reflexivity is imposed: w R w whenever v R w for some v. To prove the CIP for $\mathsf{KT}_\Box$, it is sufficient to note that S7 and S8 are local rules because $f(\bullet ) R^k f(\mathsf{c})$ for some $k>0$. Further, S5 and S6 can be represented as $(\Rightarrow \mathsf{K})$ and $(\mathsf{K}\Rightarrow )$ respectively, followed by a series of $\mathsf \Box L^s$ and $\mathsf \Diamond L^s$ rules. Req. VII is clearly fulfilled by Def. 30. Moreover, since the $\mathsf \Box L^s$ and $\mathsf \Diamond L^s$ rules are performed in one block with a K rule, we can assume $f(\mathsf{c}) R f(m)$ ensuring their locality. Note that Euclideanity was not used for the rules R1–R4 in K5.

Since the additional tableau rule for KD5 from [10] can be extended to $\mathsf{SDL}^+$ and since both the rule and its symmetric version are variants of $(\mathsf{D} \Rightarrow )$ and $(\Rightarrow \mathsf{D})$ with embedded contraction, they can be dealt with in the manner described in Sect. 7.

Theorem 31

The Craig interpolation property for K5, KD5, the logic of shift reflexivity $\mathsf{KT}_\Box$, and the extended standard deontic logic $\mathsf{SDL}^+$ can be proved constructively using grafted tableau systems, based on [10].

6 Lyndon Interpolation

The CIP is often strengthened to the Lyndon interpolation property (LIP). Up to now, p and $\overline{p}$ have represented the same propositional variable. By contrast, for the LIP they are distinct: p ($\overline{p}$) can occur in the interpolant iff p ($\overline{p}$) occurs in both antecedent and consequent formulas. Thanks to the use of symmetric-type sequents, the interpolants constructed for the CIP can also be used to demonstrate the LIP for all the rules considered, with the exception of the analytic cut, which requires a strengthening of the condition on preservation of p and $\overline{p}$. The main condition for using our method to prove the LIP for custom-made rules is that no propositional letter, positive or negative, antecedent or consequent, disappears on the way from initial sequents to the endsequent.

Corollary 32

The LIP for all 15 logics of the modal cube can be proved constructively using nested sequents from [2]. The LIP for S5 can be proved constructively using the hypersequent system from [1]. The LIP for K5, KD5, $\mathsf{KT}_\Box$, and $\mathsf{SDL}^+$ can be proved constructively using grafted tableaus based on [10].

7 Conclusion and Future Work

We have presented a general description of the constructive proof of Craig and Lyndon interpolation for hypersequents, nested sequents, and other multicomponent sequent formalisms such as grafted tableaus. This general description explains already existing results and facilitates the extension of the method to new rules, e.g., the analytic cut rule and the generalizations of the mix rule. We also provide a general formalism-independent treatment of external weakening and contraction rules. The natural next step is to apply this framework to new multisequent formalisms and to semantics other than Kripke models.