Extensions of $\textsf{K5}$: Proof Theory and Uniform Lyndon Interpolation

Abstract

We introduce a Gentzen-style framework, called layered sequent calculi, for modal logic $\textsf{K5}$ and its extensions $\textsf{KD5}$, $\textsf{K45}$, $\textsf{KD45}$, $\textsf{KB5}$, and $\textsf{S5}$ with the goal to investigate the uniform Lyndon interpolation property (ULIP), which implies both the uniform interpolation property and the Lyndon interpolation property. We obtain complexity-optimal decision procedures for all logics and present a constructive proof of the ULIP for $\textsf{K5}$, which to the best of our knowledge, is the first such syntactic proof. To prove that the interpolant is correct, we use model-theoretic methods, especially bisimulation modulo literals.

I. van der Giessen—Supported by a UKRI Future Leaders Fellowship, ‘Structure vs Invariants in Proofs’, project reference MR/S035540/1.

R. Jalali—Acknowledges the support of the Netherlands Organization for Scientific Research under grant 639.073.807 and the Czech Science Foundation Grant No. 22-06414L.

R. Kuznets—Supported by the Austrian Science Fund (FWF) ByzDEL project (P33600).

1 Introduction

The uniform interpolation property (UIP) is an important property of a logic. It strengthens the Craig interpolation property (CIP) by making interpolants depend on only one formula of an implication, either the premise or conclusion. A lot of work has gone into proving the UIP, and it is shown to be useful in various areas of computer science, including knowledge representation [17] and description logics [25]. Early results on the UIP in modal logic include positive results proved semantically for logics $\textsf{GL}$ and $\textsf{K}$ (independently in [9, 32, 35]) and negative results for logics $\textsf{S4}$ [10] and $\textsf{K4}$ [5]. A proof-theoretic method to prove the UIP was first proposed in [30] for intuitionistic propositional logic and later adapted to modal logics, such as $\textsf{K}$ and $\textsf{T}$ in [5]. A general proof-theoretic method of proving the UIP for many classical and intuitionistic (non-)normal modal logics and substructural (modal) logics based on the form of their sequent-calculi rules was developed in the series of papers [2, 3, 16].

Apart from the UIP, we are also interested in the uniform Lyndon interpolation property (ULIP) that is a strengthening of the UIP in the sense that interpolants must respect the polarities of the propositional variables involved. Kurahashi [18] first introduced this property and proved it for several normal modal logics, by employing a semantic method using layered bisimulations. A sequent-based proof-theoretic method was used in [1] to show the ULIP for several non-normal modal logics and conditional logics.

Our long-term goal is to provide a general proof-theoretic method to (re)prove the UIP for modal logics via multisequent calculi (i.e., nested sequents, hypersequents, labelled hypersequents, etc.). Unlike many other ways of proving interpolation, the proof-theoretic treatment is constructive in that it additionally yields an algorithm for constructing uniform interpolants. Towards this goal, we build on the modular treatment of multicomponent calculi to prove the CIP for modal and intermediate logics in [8, 19, 21, 23, 24]. First steps have been made by reproving the UIP for modal logics $\textsf{K}$, $\textsf{D}$, and $\textsf{T}$ via nested sequents [12] and for $\textsf{S5}$ via hypersequents [11, 13], the first time this is proved proof-theoretically for $\textsf{S5}$.

In this paper, we focus on logics $\textsf{K5}$, $\textsf{KD5}$, $\textsf{K45}$, $\textsf{KD45}$, $\textsf{KB5}$, and $\textsf{S5}$. The ULIP for these logics was derived in [18, Prop. 3] from the logics’ local tabularity [28] and Lyndon interpolation property (LIP) [20].

Towards a modular proof-theoretic treatment, we introduce a new form of multisequent calculi for these logics that we call layered sequent calculi, the structure of which is inspired by the structure of the Kripke frames for the concerned logics from [27]. For $\textsf{S5}$, this results in standard hypersequents [4, 26, 31]. For $\textsf{K5}$ and $\textsf{KD5}$, the presented calculi are similar to grafted hypersequent calculi in [22] but without explicit weakening. Other, less related, proof systems include analytic cut-free sequent systems for $\textsf{K5}$ and $\textsf{KD5}$ [34], cut-free sequent calculi for $\textsf{K45}$ and $\textsf{KD45}$ [33], and nested sequent calculi for modal logics [7].

The layered sequent calculi introduced in this paper adopt a strong version of termination that only relies on a local loop-check based on saturation. For all concerned logics, this yields a decision procedure that runs in co-NP time, which is, therefore, optimal [15]. We provide a semantic completeness proof via a countermodel construction from failed proof search.

Finally, layered sequents are used to provide the first proof-theoretic proof of the ULIP for $\textsf{K5}$. The method is adapted from [11, 13] in which the UIP is proved for $\textsf{S5}$ based on hypersequents. We provide an algorithm to construct uniform Lyndon interpolants purely by syntactic means using the termination strategy of the proof search. To show the correctness of the constructed interpolants, we use model-theoretic techniques inspired by bisimulation quantification in the setting of uniform Lyndon interpolation [18].

An extended version of the paper with more detailed proofs is found in [14].

2 Preliminaries

The language of modal logics consists of a set $\textsf{Pr}$ of countably many (propositional) atoms $p, q, \ldots$, their negations $\overline{p}, \overline{q}, \ldots$, propositional connectives $\wedge$ and $\vee$, boolean constants $\top$ and $\bot$, and modal operators $\Box$ and $\Diamond$. A literal $\ell$ is either an atom or its negation, and the set of all literals is denoted by $\textsf{Lit}$. We define modal formulas in the usual way and denote them by lowercase Greek letters $\varphi , \psi , \ldots$. We define $\overline{\varphi }$ using the usual De Morgan laws to push the negation inwards (in particular, $\overline{\overline{p}} := p$) and $\varphi \rightarrow \psi :=\overline{\varphi } \vee \psi$. We use uppercase Greek letters $\varGamma , \varDelta , \ldots$ to refer to finite multisets of formulas. We write $\varGamma ,\varDelta$ to mean $\varGamma \cup \varDelta$ and $\varGamma , \varphi$ to mean $\varGamma \cup \{ \varphi \}$. The set of literals of a formula $\varphi$, denoted $\textsf{Lit}(\varphi )$, is defined recursively: $\textsf{Lit}(\top )=\textsf{Lit}(\bot )=\varnothing$, $\textsf{Lit}(\ell )=\ell$ for $\ell \in \textsf{Lit}$, $\textsf{Lit}(\varphi \wedge \psi )= \textsf{Lit}(\varphi \vee \psi )= \textsf{Lit}(\varphi ) \cup \textsf{Lit}(\psi )$, and $\textsf{Lit}(\Box \varphi )= \textsf{Lit}(\Diamond \varphi )=\textsf{Lit}(\varphi )$.

Table 1. Modal axioms and their corresponding frame conditions.

We consider extensions of $\textsf{K5}$ with any combination of axioms $\textsf{4}$, $\textsf{d}$, $\textsf{b}$, and $\textsf{t}$ (Table 1). Several of the 16 combinations coincide, resulting in 6 logics: $\textsf{K5}$, $\textsf{KD5}$, $\textsf{K45}$, $\textsf{KD45}$, $\textsf{KB5}$, and $\textsf{S5}$ (Table 2). Throughout the paper, we assume $\textsf{L}\in \{\textsf{K5}, \textsf{KD5}, \textsf{K45}, \textsf{KD45}, \textsf{KB5}, \textsf{S5}\}$ and write $\vdash _\textsf{L}\varphi$ iff $\varphi \in \textsf{L}$.

Definition 1

(Logic $\textsf{K5}$). Modal logic $\textsf{K5}$ is axiomatized by the classical tautologies, axioms $\mathsf k$ and $\mathsf 5$, and rules modus ponens (from $\varphi$ and $\varphi \rightarrow \psi$ infer $\psi )$ and necessitation (from $\varphi$ infer $\Box \varphi )$.

Throughout the paper we employ the semantics of Kripke frames and models.

Definition 2

(Kripke semantics). A Kripke frame is a pair (W, R) where W is a nonempty set of worlds and $R \subseteq W \times W$ a binary relation. A Kripke model is a triple (W, R, V) where (W, R) is a Kripke frame and $V:\textsf{Pr} \rightarrow \mathcal {P}(W)$ is a valuation function. A formula $\varphi$ is defined to be true at a world w in a model $\mathcal {M}=(W,R,V)$, denoted $\mathcal {M}, w \vDash \varphi$, as follows: $\mathcal {M},w\vDash \top$, $\mathcal {M},w\nvDash \bot$ and

Formula $\varphi$ is valid in $\mathcal {M}= (W,R,V)$, denoted $\mathcal {M}\vDash \varphi$, iff for all $w \in W$, $\mathcal {M},w \vDash \varphi$. We call $\varnothing \ne C \subseteq W$ a cluster (in $\mathcal {M})$ iff $C \times C \subseteq R$, i.e., the relation R is total on C. We write wRC iff wRv for all $v \in C$.

Table 2. Semantics for extensions of $\textsf{K5}$ (see [27, 29]). Everywhere not $\rho R \rho$ for the root $\rho$, set C is a finite cluster, and $\sqcup$ denotes disjoint union.

We work with specific classes of Kripke models sound and complete w.r.t. the logics. The respective frame conditions for the logic $\textsf{L}$, called $\textsf{L}$-frames, are defined in Table 2. A model (W, R, V) is an $\mathsf L$-model iff (W, R) is an $\textsf{L}$-frame. Table 2 is a refinement of Theorem 3, particularly shown for $\textsf{K45}$, $\textsf{KD45}$, and $\textsf{KB5}$ in [29]. More precisely, we consider rooted frames and completeness w.r.t. the root, i.e., $\vdash _\textsf{L}\varphi$ iff for all $\textsf{L}$-models $\mathcal {M}$ with root $\rho$, $\mathcal {M}, \rho \vDash \varphi$ (we often denote the if-condition as $\vDash _\textsf{L}\varphi$). For each logic, this follows from easy bisimulation arguments.

Theorem 3

([27]). Any normal modal logic containing $\textsf{K5}$ is sound and complete w.r.t. a class of finite Euclidean Kripke frames (W, R) of one of the following forms: (a) $W = \{\rho \}$ consists of a singleton root and $R=\varnothing$, (b) the whole W is a cluster (any world can be considered its root), or (c) $W \backslash \{\rho \}$ is a cluster for a (unique) root $\rho \in W$ such that $\rho R w$ for some $w \in W \backslash \{\rho \}$ while not $\rho R \rho$.

Definition 4

(UIP and ULIP). A logic $\textsf{L}$ has the uniform interpolation property (UIP) iff for any formula $\varphi$ and $p \in \textsf{Pr}$ there is a formula $\forall p \varphi$ such that

• (1) $\textsf{Lit}(\forall p \varphi ) \subseteq \textsf{Lit}(\varphi ) \setminus \{ p, \overline{p} \}$,

• (2) $\vdash _\textsf{L}\forall p \varphi \rightarrow \varphi$, and

• (3) $\vdash _\textsf{L}\psi \rightarrow \varphi \text { implies } \vdash _\textsf{L}\psi \rightarrow \forall p \varphi$ for any formula $\psi$ with $p,\overline{p} \notin \textsf{Lit}(\psi )$.

A logic $\textsf{L}$ has the uniform Lyndon interpolation property (ULIP)  [1, 18] iff for any formula $\varphi$ and $\ell \in \textsf{Lit}$, there is a formula $\forall \ell \varphi$ such that

• (i) $\textsf{Lit}(\forall \ell \varphi ) \subseteq \textsf{Lit}(\varphi ) \setminus \{ \ell \}$,

• (ii) $\vdash _\textsf{L}\forall \ell \varphi \rightarrow \varphi$, and

• (iii) $\vdash _\textsf{L}\psi \rightarrow \varphi \text { implies } \vdash _\textsf{L}\psi \rightarrow \forall \ell \varphi$ for any formula $\psi$ with $\ell \notin \textsf{Lit}(\psi )$.

We call $\forall p \varphi$ $(\forall \ell \varphi )$ the uniform (Lyndon) interpolant of $\varphi$ w.r.t. atom p (literal $\ell$).

These are often called pre-interpolants as opposed to their dual post-interpolants that, in classical logic, can be defined as $\exists p \varphi = \overline{\forall p \overline{\varphi }}$ and $\exists \ell \varphi = \overline{\forall \overline{\ell } \overline{\varphi }}$ (see, e.g., [1, 5, 11, 18] for more explanations).

Theorem 5

If a logic $\textsf{L}$ has the ULIP, then it also has the UIP.

Proof

We define a uniform interpolant of $\varphi$ w.r.t. atom p as a uniform Lyndon interpolant $\forall p \forall \overline{p} \varphi$ of $\forall \overline{p} \varphi$ w.r.t. literal p. We need to demonstrate conditions LIP(1)–(3) from Definition 4. First, it follows from ULIP(i) that $\textsf{Lit}(\forall p \forall \overline{p} \varphi ) \subseteq \textsf{Lit}(\forall \overline{p} \varphi ) \setminus \{p\} \subseteq \textsf{Lit}(\varphi ) \setminus \{p, \overline{p}\}$. Second, $\vdash _{\textsf{L}} \forall p \forall \overline{p} \varphi \rightarrow \forall \overline{p} \varphi$ and $\vdash _{\textsf{L}} \forall \overline{p} \varphi \rightarrow \varphi$ by ULIP(ii), hence, $\vdash _{\textsf{L}} \forall p \forall \overline{p} \varphi \rightarrow \varphi$. Finally, if $\vdash _{\textsf{L}} \psi \rightarrow \varphi$ where $p, \overline{p} \notin \textsf{Lit}(\psi )$, then by ULIP(iii), $\vdash _{\textsf{L}} \psi \rightarrow \forall \overline{p} \varphi$ as $\overline{p} \notin \textsf{Lit}(\psi )$ and $\vdash _{\textsf{L}} \psi \rightarrow \forall p \forall \overline{p} \varphi$ as $p \notin \textsf{Lit}(\psi )$.    $\square$

Table 3. Layered sequent calculi $\mathsf{L.L}$: in addition to explicitly stated rules, all $\mathsf{L.L}$ have axioms $\mathsf {id_P}$ and $\mathsf {id_{\top }}$ and rules $\vee$, $\wedge$, $\Diamond _c$, and $\textsf{t}$ (see Fig. 1). Note that the rules of system $\mathsf{L.L}$ may only be applied to $\textsf{L}$-sequents.

3 Layered Sequents

Definition 6

(Layered sequents). A layered sequent is a generalized one-sided sequent of the form

$$\begin{aligned} \mathcal {G}= \varGamma _1, \ldots , \varGamma _n, [\varSigma _1], \ldots , [\varSigma _m], [[\Pi _1]] , \ldots , [[\Pi _k]] \end{aligned}$$

(1)

where $\varGamma _i, \varSigma _i, \Pi _i$ are finite multisets of formulas, $n,m,k \ge 0$, and if $k\ge 1$, then $m \ge 1$. A layered sequent is an $\textsf{L}$-sequent iff it satisfies the conditions in the rightmost column of Table 3. Each $\varSigma _i$, each $\Pi _i$, and $\bigcup _i \varGamma _i$ is called a sequent component of $\mathcal {G}$. The formula interpretation of a layered sequent $\mathcal {G}$ above is:

$$ \iota (\mathcal {G}) = \bigvee \nolimits _{i=1}^n \big (\bigvee \varGamma _i\big ) \vee \bigvee \nolimits _{i=1}^m \Box \big (\bigvee \varSigma _i\big ) \vee \bigvee \nolimits _{i=1}^k \Box \Box \big (\bigvee \Pi _i\big ). $$

Layered sequents are denoted by $\mathcal {G}$ and $\mathcal {H}$. The structure of a layered sequent can be viewed as at most two layers of hypersequents ($[]$-components $\varSigma _i$ and $[[]]$-components $\Pi _i$ forming the first and second layer respectively) possibly nested on top of the sequent component $\bigcup _i \varGamma _i$ as the root. Following the arboreal terminology from [22], the root is called the trunk while $[]$- and $[[]]$-components form the crown. Analogously to nested sequents representing tree-like Kripke models, the structure of $\textsf{L}$-sequents is in line with the structure of $\textsf{L}$-models introduced in Sect. 2. We view sequents components as freely permutable, e.g., $[[\Pi _1]], \varGamma _1, [\varSigma _1], \varGamma _2$ and $\varGamma _1, \varGamma _2, [\varSigma _1], [[\Pi _1]]$ represent the same layered sequent.

Remark 7

The layered calculi presented here generalize grafted hypersequents of [22] and, hence, similarly combine features of hypersequents and nested sequents. In particular, layered sequents are generally neither pure hypersequents (except for the case of $\textsf{S5}$) nor bounded-depth nested sequents. The latter is due to the fact that the defining property of nested sequents is the tree structure of the sequent components, whereas the crown components of a layered sequent form a cluster. Although formally grafted hypersequents are defined with one layer only, this syntactic choice is more of a syntactic sugar than a real distinction. Indeed, the close relationship of one-layer grafted hypersequents for $\textsf{K5}$ and $\textsf{KD5}$ in [22] to the two-layer layered sequents presented here clearly manifests itself when translating grafted hypersequents into the prefixed-tableau format (see grafted tableau system for $\textsf{K5}$ [22, Sect. 6]). There prefixes for the crown are separated into two types, limbs and twigs, which match the separation into $[]$- and $[[]]$-components.

Fig. 1.

Layered sequent rules: brackets $\llbracket \rrbracket$ and $\llparenthesis \rrparenthesis$ range over both $[]$ and $[[]]$.

For a layered sequent (1), we assign labels to the components as follows: the trunk is labeled $\bullet$, $[ ]$-components get distinct labels $\bullet 1, \bullet 2, \dots$, and $[[ ]]$-components get distinct labels $1,2, \dots$. We let $\sigma , \tau , \dots$ range over these labels. The set of labels is denoted $Lab (\mathcal {G})$ and $\sigma \in \mathcal {G}$ means $\sigma \in Lab (\mathcal {G})$. We write $\sigma : \varphi \in \mathcal {G}$ (or $\sigma : \varphi$ if no confusion occurs) when a formula $\varphi$ occurs in a sequent component of $\mathcal {G}$ labeled by $\sigma$.

Example 8

$\mathcal {G}= \varphi , \psi , [\chi ], [\xi ], [[\theta ]]$ is a layered sequent with the trunk and three crown components: two $[]$-components and one $[[]]$-component. Since it has both the trunk and a $[[ ]]$-component, it can only be a $\textsf{K5}$- or $\textsf{KD5}$-sequent. A corresponding labeled sequent is $\mathcal {G}= \varphi _\bullet , \psi _\bullet , [\chi ]_{\bullet 1}, [\xi ]_{\bullet 2}, [[\theta ]]_1$, with the set $Lab (\mathcal {G}) = \{\bullet , \bullet 1, \bullet 2, 1\}$ of four labels. Similarly, for the $\textsf{KB5}$/$\textsf{S5}$-sequent $\mathcal H= [\sigma ], [\delta ]$, a corresponding labeled sequent is $\mathcal {H}= [\sigma ]_{\bullet 1}, [\delta ]_{\bullet 2}$ with $Lab (\mathcal {H}) = \{\bullet 1, \bullet 2\}$.

We sometimes use unary contexts, i.e., layered sequents with exactly one hole, denoted $\{ \}$. Such contexts are denoted by $\mathcal {G}\{ \}$. The insertion $\mathcal {G}\{\varGamma \}$ of a finite multiset $\varGamma$ into $\mathcal {G}\{ \}$ is obtained by replacing $\{ \}$ with $\varGamma$. The hole $\{ \}$ in a component $\sigma$ can also be labeled $\mathcal {G}\{ \}_\sigma$. We use the notations $\llbracket \rrbracket$ and $\llparenthesis \rrparenthesis$ to refer to either of $[]$ or $[[]]$.

Using Fig. 1 and the middle column of Table 3, we define layered sequent calculi $\mathsf{L.K5}$, $\mathsf{L.KD5}$, $\mathsf{L.K45}$, $\mathsf{L.KD45}$, $\mathsf{L.KB5}$, and $\mathsf{L.S5}$, where $\mathsf{L.L}$ is the calculus for the logic $\textsf{L}$. Following the terminology from [22], we split all modal rules into trunk rules (subscript t) and crown rules (subscript c) depending on the position of the principal formula. We write $\vdash _\mathsf{L.L}\mathcal {G}$ iff $\mathcal {G}$ is derivable in $\mathsf{L.L}$.

Definition 9

(Saturation). Labeled formula $\sigma : \varphi \in \mathcal {G}$ is saturated for $\mathsf{L.L}$ iff

• $\varphi$ equals p or $\overline{p}$ for an atom p, or equals $\bot$, or equals $\top$;

• $\varphi = \varphi _1 \wedge \varphi _2$ and $\sigma : \varphi _i \in \mathcal {G}$ for some i;

• $\varphi = \varphi _1 \vee \varphi _2$ and both $\sigma : \varphi _1 \in \mathcal {G}$ and $\sigma : \varphi _2 \in \mathcal {G}$;

• $\varphi =\Box \varphi '$, the unique rule applicable to $\sigma : \Box \varphi '$ in $\mathsf{L.L}$ is either $\Box _t$ or $\Box _c$ (i.e., a rule creating a $[]$-component), and $\bullet i : \varphi ' \in \mathcal {G}$ for some i;

• $\varphi =\Box \varphi '$, the unique rule applicable to $\sigma : \Box \varphi '$ in $\mathsf{L.L}$ is $\Box _{c'}$ (i.e., a rule creating a $[[]]$-component), and $i : \varphi ' \in \mathcal {G}$ for some i.

In addition, we define for any label $\sigma$ and formula $\varphi$:

• $\sigma : \Diamond \varphi$ is saturated w.r.t. $\bullet \in Lab (\mathcal {G})$;

• $\sigma : \Diamond \varphi$ is saturated w.r.t. a label $\bullet i \in Lab (\mathcal {G})$ iff $\bullet i : \varphi \in \mathcal {G}$;

• $\sigma : \Diamond \varphi$ is saturated w.r.t. a label $i\in Lab (\mathcal {G})$ iff $\sigma = \bullet$ or $i : \varphi \in \mathcal {G}$;

• $\sigma : \Diamond \varphi$ is $\textsf{d}_t$-saturated iff $\sigma \ne \bullet$ or $\bullet i : \varphi \in \mathcal {G}$ for some i;

• $\sigma : \Diamond \varphi$ is $\textsf{d}_c$-saturated iff $\sigma = \bullet$ or $\bullet i : \varphi \in \mathcal {G}$ for some i;

• $\sigma : \Diamond \varphi$ is $\textsf{d}'_c$-saturated iff $\sigma = \bullet$ or $i: \varphi \in \mathcal {G}$ for some i.

$\mathcal {G}$ is propositionally saturated iff all $\vee$- and $\wedge$-formulas are saturated in $\mathcal {G}$. $\textsf{L}$-sequent $\mathcal {G}$ is $\textsf{L}$-saturated iff a) each non-$\Diamond$ formula is saturated, b) each $\sigma : \Diamond \varphi$ is saturated w.r.t. every label in $Lab (\mathcal {G})$, c) each $\sigma : \Diamond \varphi$ is $\textsf{d}$-saturated whenever $\textsf{d} \in \mathsf{L.L}\cap \{\textsf{d}_t, \textsf{d}_c, \textsf{d}_{c'} \}$, and d) $\mathcal {G}$ is not of the from $\mathcal {H}\{\top \}$ or $\mathcal {H}\{q, \overline{q}\}$ for some $q \in \textsf{Pr}$.

Theorem 10

Proof search in ${\mathsf{L.L}}$ modulo saturation terminates and provides an optimal-complexity decision algorithm, i.e., runs in co-NP time.

Proof

Given a proof search of layered sequent $\mathcal {G}$, for each layered sequent $\mathcal {H}$ in this proof search, consider its labeled formulas as a set $F_\mathcal {H}=\{\sigma : \varphi \mid \sigma : \varphi \in \mathcal {H}\}$. Let s be the number of subformulas occurring in $\mathcal {G}$ and N be the number of sequent components in $\mathcal {G}$. Since we only apply rules (that do not equal $\mathsf {id_P}$ or $\mathsf {id_{\top }}$) to non-saturated sequents, sets $F_\mathcal {H}$ will grow for each premise. Going bottom-up in the proof search, at most s labels of the form $\bullet i$ and at most s labels of the form i can be created, and each label can have at most s formulas. Therefore, the cardinality of sets $F_\mathcal {H}$ are bounded by $s(N+s + s)$, which is polynomial in the size of $F_\mathcal {G}$. Hence, the proof search terminates modulo saturation. Moreover, since each added labeled formula is linear in the size $F_\mathcal {G}$ and the non-deterministic branching in the proof search is bounded by $(N+s+s)s(N+s+s)$, again a polynomial in the size of $F_\mathcal {G}$, this algorithm is co-NP, i.e., provides an optimal decision procedure for the logic.   $\square$

Definition 11

(Interpretations). An interpretation of an $\textsf{L}$-sequent $\mathcal {G}$ into an $\textsf{L}$-model $\mathcal {M}= (W,R,V)$ is a function $\mathcal {I}: Lab (\mathcal {G}) \rightarrow W$ such that the following conditions apply whenever the respective type of labels exists in $\mathcal {G}$:

• 1. $\mathcal {I}(\bullet ) = \rho$, where $\rho$ is the root of $\mathcal {M}$;

• 2. $\mathcal {I}(\bullet )R\;\mathcal {I}(\bullet i)$ for each label of the form $\bullet i \in Lab (\mathcal {G})$;

• 3. $\mathcal {I}(\bullet i) R\; \mathcal {I}(j)$ and $\mathcal {I}(j) R\; \mathcal {I}(\bullet i)$ for all labels of the form $\bullet i$ and j in $Lab (\mathcal {G})$;

• 4. Not $\mathcal {I}(\bullet ) R\; \mathcal {I}(j)$ for any label of the form $j \in Lab (\mathcal {G})$.

Note that none of the conditions (1)–(4) apply to layered $\textsf{S5}$-sequents.

Definition 12

(Sequent semantics). For any given interpretation $\mathcal {I}$ of an $\textsf{L}$-sequent $\mathcal {G}$ into an $\textsf{L}$-model $\mathcal {M}$,

$$\begin{aligned} \mathcal {M}, \mathcal {I}\vDash \mathcal {G}\qquad \text { if{f} }\qquad \mathcal {M}, \mathcal {I}(\sigma ) \vDash \varphi \text { for some } \sigma : \varphi \in \mathcal {G}. \end{aligned}$$

$\mathcal {G}$ is valid in $\textsf{L}$, denoted $\vDash _\textsf{L}\mathcal {G}$, iff $\mathcal {M}, \mathcal {I}\vDash \mathcal {G}$ for all $\textsf{L}$-models $\mathcal {M}$ and interpretations $\mathcal {I}$ of $\mathcal {G}$ into $\mathcal {M}$. We omit $\textsf{L}$ and $\mathcal M$ when clear from the context.

The proof of the following theorem is based on a countermodel construction (for more standard parts of the proof we refer to the Appendix of [14]):

Theorem 13

(Soundness and completeness). For any $\textsf{L}$-sequent $\mathcal {G}$,

$$ \vdash _\mathsf{L.L}\mathcal {G}\qquad \Longleftrightarrow \qquad \vDash _\textsf{L}\iota (\mathcal {G}) \qquad \Longleftrightarrow \qquad \vDash _\textsf{L}\mathcal {G}. $$

Proof

We show a cycle of implications. The left-to-middle implication, i.e., that $\vdash _\mathsf{L.L}\mathcal {G}\Longrightarrow \ \vDash _\textsf{L}\iota (\mathcal {G})$, can be proved by induction on the $\mathsf{L.L}$-derivation of $\mathcal {G}$.

For the middle-to-right implication, i.e., $\vDash _\textsf{L}\iota (\mathcal {G}) \Longrightarrow \ \vDash _\textsf{L}\mathcal {G}$, let $\mathcal {G}$ be a sequent of form (1). We prove that $\mathcal {M}, \mathcal {I}\nvDash \mathcal {G}$ implies $\mathcal {M}, \mathcal {I}(\bullet ) \nvDash \iota (\mathcal {G})$ (if $n=0$, use 1 in place of $\bullet$). By definition, $\mathcal {I}(\bullet )$ is the root of $\mathcal {M}$. If $\mathcal {M}, \mathcal {I}\nvDash \mathcal {G}$, then $\mathcal {I}(\bullet ) \nvDash \varphi$ for all $\varphi \in \bigcup \nolimits _{i=1}^n \varGamma _i$, for each $1 \le i \le m$ we have $\mathcal {I}(\bullet i) \nvDash \psi$ for all $\psi \in \varSigma _i$, and for each $1 \le i \le k$ we have $\mathcal {I}(i) \nvDash \chi$ for all $\chi \in \Pi _i$. By Definition 11, in case $k \ge 1$ label $\bullet 1$ is in $\mathcal {G}$ and $\mathcal {I}(\bullet )R\mathcal {I}(\bullet 1)R\mathcal {I}(i)$ for each $1 \le i \le k$. Therefore $\mathcal {M}, \mathcal {I}(\bullet ) \nvDash \iota (\mathcal {G})$.

Finally, we prove the right-to-left implication by contraposition using a countermodel construction: from a failed proof search of $\mathcal {G}$, construct an $\textsf{L}$-model refuting $\mathcal {G}$ from (1). In a failed proof-search tree (Theorem 10), since $\nvdash _\mathsf{L.L}\mathcal {G}$, at least one saturated leaf

$$ \mathcal {G}'=\varGamma ', [\varSigma '_1], \ldots , [\varSigma '_m], [\varSigma ''_1], \ldots , [\varSigma ''_{m'}],[[\Pi '_1]] , \ldots , [[\Pi '_k]], [[\Pi ''_{1}]] , \ldots , [[\Pi ''_{k'}]], $$

is such that $\bigcup _i \varGamma _i \subseteq \varGamma '$, $\varSigma _i \subseteq \varSigma '_i$, and $\Pi _i \subseteq \Pi '_i$ (or for $\textsf{KB5}$, if $\mathcal {G}= \varGamma$, then $\mathcal {G}' = \varGamma '$ for $\varGamma \subseteq \varGamma '$ or $[\varSigma ], [\varSigma _1], \dots , [\varSigma _m]$ with $\varGamma \subseteq \varSigma$). Define $\mathcal {M}= (W,R,V)$:

$$\begin{aligned}\begin{gathered} W = Lab (\mathcal {G}'),\qquad \qquad V(p) = \{ \sigma \mid \sigma : \overline{p} \in \mathcal {G}' \},\\ R = \{ (\bullet , \bullet i) \mid \bullet i \in Lab (\mathcal {G}')\} \cup \{ (\sigma , \tau ) \mid \sigma , \tau \in Lab (\mathcal {G}'), \sigma , \tau \ne \bullet \}. \end{gathered}\end{aligned}$$

Since $\mathcal {G}'$ is saturated, $\mathcal {M}$ is an $\textsf{L}$-model. Taking $\mathcal {I}$ of $\mathcal {G}$ into $\mathcal {M}$ as the identity function (or $\mathcal {I}(\bullet ) = 1$ in case of $\textsf{KB5}$), we have $\mathcal {M}, \mathcal {I}\nvDash \mathcal {G}$ as desired.    $\square$

4 Uniform Lyndon Interpolation

Definition 14

(Multiformulas). The grammar

defines multiformulas, where $\sigma : \varphi$ is a labeled formula. $Lab (\mho )$ denotes the set of labels of $\mho$. An interpretation $\mathcal {I}$ of a layered sequent $\mathcal G$ into a model $\mathcal {M}$ is called an interpretation of a multiformula $\mho$ into $\mathcal {M}$ iff $Lab (\mho ) \subseteq Lab (\mathcal {G})$. If $\mathcal {I}$ is an interpretation of $\mho$ into $\mathcal {M}$, we define $\mathcal {M}, \mathcal {I}\vDash \mho$ as follows:

Multiformulas $\mho _1$ and $\mho _2$ are said to be equivalent, denoted $\mho _1 \equiv _\textsf{L}\mho _2$, or simply $\mho _1 \equiv \mho _2$, iff $\mathcal {M},\mathcal {I}\vDash \mho _1 \Leftrightarrow \mathcal {M}, \mathcal {I}\vDash \mho _2$ for any interpretation $\mathcal {I}$ of both $\mho _1$ and $\mho _2$ into an $\textsf{L}$-model $\mathcal {M}$.

Lemma 15

([21]). Any multiformula $\mho$ can be transformed into an equivalent one in SDNF (SCNF) as a -disjunction -conjunction) of -conjunctions -disjunctions) of labeled formulas $\sigma : \varphi$ such that each label of $\mho$ occurs exactly once per conjunct (disjunct).

Definition 16 (Bisimilarity)

. Let $\mathcal {M}=(W,R,V)$ and $\mathcal {M}'=(W',R',V')$ be models and $\ell \in \textsf{Lit}$. We say $\mathcal M'$ is $\ell$-bisimilar to $\mathcal M$, denoted $\mathcal {M'} \le _{\ell } \mathcal {M}$ iff there is a nonempty binary relation $Z \subseteq W \times W'$, called an $\ell$-bisimulation between $\mathcal {M}$ and $\mathcal {M'}$, such that the following hold for every $w \in W$ and $w' \in W'$:

• literals$_{\ell }$. if $w Z w'$, then a) $\mathcal {M}, w \vDash q$ iff $\mathcal {M}', w' \vDash q$ for all atoms $q \notin \{\ell , \overline{\ell }\}$ and

  b) if $\mathcal {M}', w' \vDash \ell$, then $\mathcal {M}, w \vDash \ell$;

• forth. if $w Z w'$ and wRv, then there exists $v'\in W'$ such that $v Zv'$ and $w' R' v'$;

• back. if $w Z w'$ and $w' R' v'$, then there exists $v \in W$ such that $v Zv'$ and wRv.

$\mathcal {M}$ and $\mathcal {M}'$ are bisimilar, denoted $\mathcal {M}\sim \mathcal {M}'$, iff there is a relation $Z \ne \varnothing$ satisfying forth and back, as well as part a) of literals$_{\ell }$ for any $p\in \textsf{Pr}$, in which case Z is called a bisimulation. We write (similarly for $\sim$ instead of $\le _{\ell })$:

• $(\mathcal {M}', w') \le _{\ell } (\mathcal {M},w)$ iff there is an $\ell$-bisimulation Z, such that $wZw'$;

• $(\mathcal {M}', \mathcal {I}') \le _{\ell } (\mathcal {M},\mathcal {I})$ for functions $\mathcal {I}: X \rightarrow W$ and $\mathcal {I}' : X \rightarrow W'$ iff there is an $\ell$-bisimulation Z such that $\mathcal {I}(\sigma )\, Z\, \mathcal {I}'(\sigma )$ for each $\sigma \in X$.

Note that $\le _{\ell }$ is a preorder and we have $\mathcal {M}' \le _\ell \mathcal {M}$ iff $\mathcal {M}\le _{\overline{\ell }} \mathcal {M}'$. By analogy with [6, Theorem 2.20], we have the following immediate observation, which additionally holds for multiformulas $\mho$ (we provide a proof in [14]):

Lemma 17

Let $\mathcal {I}$ and $\mathcal {I}'$ be interpretations of a layered sequent $\mathcal {G}$ into models $\mathcal {M}$ and $\mathcal {M}'$ respectively.

• 1. Let $\ell \notin \textsf{Lit}(\mathcal {G})$. If $(\mathcal {M}', \mathcal {I}') \le _\ell (\mathcal {M}, \mathcal {I})$, then $\mathcal {M}, \mathcal {I}\vDash \mathcal {G}$ implies $\mathcal {M}', \mathcal {I}' \vDash \mathcal {G}$.

• 2. If $(\mathcal {M}, \mathcal {I}) \sim (\mathcal {M}', \mathcal {I}')$, then $\mathcal {M}, \mathcal {I}\vDash \mathcal {G}$ iff $\mathcal {M}', \mathcal {I}' \vDash \mathcal {G}$.

Definition 18

(BLUIP). Logic $\textsf{L}$ is said to have the bisimulation layered-sequent uniform interpolation property (BLUIP) iff for every literal $\ell$ and every $\textsf{L}$-sequent $\mathcal {G}$, there is a multiformula $A_\ell (\mathcal {G})$, called BLU interpolant, such that:

• (i) $\textsf{Lit}\bigl (A_\ell (\mathcal G)\bigr ) \subseteq \textsf{Lit}(\mathcal G) \setminus$ $\{\ell \}$ and $Lab \bigl (A_\ell (\mathcal G)\bigr ) \subseteq Lab\mathcal (\mathcal G)$;

• (ii) for each interpretation $\mathcal {I}$ of $\mathcal G$ into an $\textsf{L}$-model $\mathcal {M}$,

  $$ \mathcal {M}, \mathcal {I}\vDash A_\ell (\mathcal G) \quad \text {implies}\quad \mathcal {M}, \mathcal {I}\vDash \mathcal G; $$

• (iii) for each $\textsf{L}$-model $\mathcal {M}$ and interpretation $\mathcal {I}$ of $\mathcal G$ into $\mathcal {M}$, if $\mathcal {M}, \mathcal {I}\nvDash A_\ell (\mathcal G)$, then there is an $\textsf{L}$-model $\mathcal {M}'$ and interpretation $\mathcal {I}'$ of $\mathcal G$ into $\mathcal {M}'$ such that

  $$(\mathcal {M}',\mathcal {I}') \le _\ell (\mathcal {M}, \mathcal {I}) \; \text {and} \; \mathcal {M}', \mathcal {I}' \nvDash \mathcal G.$$

Lemma 19

The BLUIP for $\textsf{L}$ implies the ULIP for $\textsf{L}$.

Proof

Let $\forall \ell \varphi = A_\ell (\varphi )$. We prove the properties of Definition 4. Variable property is immediate. For Property (ii), assume $\nvdash _\textsf{L}A_\ell (\varphi ) \rightarrow \varphi$. By completeness, we have $\mathcal {M}, \rho \vDash A_\ell (\varphi )$ and $\mathcal {M},\rho \nvDash \varphi$ for some $\textsf{L}$-model $\mathcal {M}$ with root $\rho$. As $\rho$ is the root, it can be considered as an interpretation by Definition 11. By condition (ii) from Definition 18 we get a contradiction. For (iii), let $\psi$ be a formula such that $\ell \notin \textsf{Lit}(\psi )$ and suppose $\nvdash _\textsf{L}\psi \rightarrow A_\ell (\varphi )$. So there is an $\textsf{L}$-model $\mathcal {M}$ with root $\rho$ such that $\mathcal {M}, \rho \vDash \psi$ and $\mathcal {M}, \rho \nvDash A_\ell (\varphi )$. Again, $\rho$ is treated as an interpretation, and by (iii) from Definition 18, there is an $\textsf{L}$-model $\mathcal {M}'$ with root $\rho '$ such that $(\mathcal {M}',\rho ') \le _\ell (\mathcal {M},\rho )$ and $\mathcal {M}',\rho ' \nvDash \varphi$. By Lemma 17, $\mathcal {M}', \rho ' \vDash \psi$, hence $\nvdash _\textsf{L}\psi \rightarrow \varphi$ as desired.    $\square$

To show that calculus $\mathsf{L.K5}$ enjoys the BLUIP for $\textsf{K5}$, we need two important ingredients: some model modifications that are closed under bisimulation and an algorithm to compute uniform Lyndon interpolants.

Definition 20

(Copying). Let $\mathcal {M}=(W,R,V)$ be a $\textsf{K5}$-model with root $\rho$ and cluster C. Model $\mathcal {N}' = (W \sqcup \{w_c \},R',V')$ is obtained by copying $w\in C$ iff $R' = R \sqcup (\{w_c\}\times C) \sqcup (C \times \{w_c\}) \sqcup \{(\rho ,w_c) \mid (\rho ,w) \in R \} \sqcup \{(w_c,w_c) \}$, and $V'(p)= V(p) \sqcup \{w_c \mid w \in V(p) \}$ for any $p \in \textsf{Pr}$. Model $\mathcal {N}'' = (W \sqcup \{w_c \},R'',V')$ is obtained by copying w away from the root iff $R'' = R' \setminus \{(\rho , w_c)\}$.

Lemma 21

Let model $\mathcal {N}$ be obtained by copying a world w from a $\textsf{K5}$-model $\mathcal {M}$ (away from the root). Let $\mathcal {I}:X \rightarrow \mathcal {M}$ and $\mathcal {I}':X \rightarrow \mathcal {N}$ be interpretations such that for each $x \in X$, either $\mathcal {I}(x) = \mathcal {I}'(x)$ or $\mathcal {I}(x)=w$ while $\mathcal {I}'(x)= w_c$. Then, $\mathcal {N}$ is a $\textsf{K5}$-model and $(\mathcal {M},\mathcal {I}) \sim (\mathcal {N},\mathcal {I}')$.

In the construction of interpolants, we use the following rules $\textsf{d}_t'$ and $\textsf{dd}$ and sets $\mathcal {G}_c$ and $\Box \Diamond \mathcal {G}_c$ of formulas from the crown of $\mathcal {G}$:

Rule $\textsf{d}_t'$ shows similarities with rule $\textsf{d}_t$ from logics $\textsf{KD5}$ and $\textsf{KD45}$, but is only applied in the absence of the crown. Rule $\textsf{d}_t'$ is sound for $\textsf{K5}$ because it can be viewed as a composition of an (admissible) cut on $\Box \bot$ and $\Diamond \top$ in the trunk, followed by $\Box _t$ in the left premise on $\Box \bot$ that creates the first crown component (though $\bot$ is dropped from it), which is populated using several $\Diamond _t$-rules for $\Diamond \psi \in \varGamma$. The label of this crown component is always $\bullet 1$. Rule $\textsf{dd}$ provides extra information in the calculation of the uniform interpolant and is needed primarily for technical reasons. We highlight the two new sequent components created by the last instance of $\textsf{dd}$ using special placeholder labels $\bullet \textsf{d}$ and $\textsf{d}$ for the respective brackets. These labels are purely for readability purposes and revert to the standard $\bullet j$ and k labels after the next instance of $\textsf{dd}$.

Table 4. Recursive construction of $A_\ell (t, \varSigma _c; \mathcal {G})$ for $\mathcal {G}$ that are not $\textsf{K5}$-saturated.

To compute a uniform Lyndon interpolant $\forall \ell \xi$ for a formula $\xi$, we first compute a BLU interpolant $A_\ell (0,\varnothing ; \xi _\bullet )$ by using the recursive function $A_\ell (t,\varSigma _c ; \mathcal {G})$ with three parameters we present below. The main parameter is a $\textsf{K5}$-sequent $\mathcal {G}$, while the other two parameters are auxiliary: $t \in \{0,1\}$ is a boolean variable such that $t=1$ guarantees that rule $\textsf{dd}$ has been applied at least once for the case when $\mathcal {G}$ contains diamond formulas; $\varSigma _c \subseteq \Box \Diamond \mathcal {G}_c$ is a set of modal formulas that provides a bookkeeping strategy to prevent redundant applications of rule $\textsf{dd}$.

To calculate $A_\ell (t,\varSigma _c ; \mathcal {G})$ our algorithm makes a choice of which row from Table 4 to apply by trying each of the following steps in the specified order:

• 1. If possible, apply rows 1–2, i.e., stop and return $A_\ell (t, \varSigma _c;\mathcal {G}) =\sigma : \top$.

• 2. If some formula $\varphi \vee \psi$ (resp. $\varphi \wedge \psi$) from $\mathcal {G}$ is not saturated, compute $A_\ell (t, \varSigma _c;\mathcal {G})$ according to row 3 (resp. 4) applied to this formula.

• 3. If some formula $\Box \varphi \in \mathcal {G}$ is not saturated (resp. $\Diamond \varphi \in \mathcal {G}$ is not saturated w.r.t. $\sigma \in \mathcal {G}$), compute $A_\ell (t, \varSigma _c;\mathcal {G})$ according to the unique respective row among 5–9 applicable to this formula (w.r.t. $\sigma$).

• 4. If Steps 1–3 do not apply, i.e., $\mathcal {G}$ is saturated, proceed as follows:

  • (a) if $\mathcal {G}$ has no $\Diamond$-formulas, stop and return $A_\ell (t, \varSigma _c;\mathcal {G}) = \textsf{LitDis}_\ell (\mathcal {G})$ where

    

    (2)

  • (b) else, if $\mathcal {G}=\varGamma$ consists of the trunk only, apply rule $\textsf{d}_t'$ as follows:

    

    (3)

    where the SDNF of $A_\ell \Bigl (0, \varSigma _c ;\quad \varGamma , \bigl [\{\psi \mid \Diamond \psi \in \varGamma \}\bigr ]_{ \bullet 1}\Bigr )$ is

    

    (4)

  • (c) else, if $t=1$ and $\Box \Diamond \mathcal {G}_c \subseteq \varSigma _c$, stop and return $A_\ell (t, \varSigma _c;\mathcal {G}) = \textsf{LitDis}_\ell (\mathcal {G})$.

  • (d) else, apply the rule $\textsf{dd}$ as follows (where w.l.o.g. $\bullet 1 \in \mathcal {G})$:

    

    (5)

    where SDNF of $A_\ell \Bigl (1, \Box \Diamond \mathcal {G}_c;\,\, \mathcal {G}, \bigl [\{\psi \mid \Diamond \psi \in \mathcal {G}\}\bigr ]_{\bullet \textsf{d}},\, \bigl [\bigl [ \{ \chi \mid \Diamond \chi \in \mathcal {G}_c\} \bigr ]\bigr ]_{\textsf{d}}\Bigr )$ is

    

    (6)

The computation of the algorithm can be seen as a proof search tree (extended with rules $\textsf{d}_t'$ and $\textsf{dd}$). In this proof search, call $A_\ell (t,\varSigma _c ; \mathcal {G})$ is sufficient (to be a BLU interpolant for $\mathcal {G}$) if each branch going up from it either stops in Steps 1 or 4a or continues via Steps 4b or 4d. Otherwise, it is insufficient, if one of the branches stops in Step 4c, say, calculating $A_\ell (1,\varSigma _c ; \mathcal {H})$. In this case, $A_\ell (1,\varSigma _c ; \mathcal {H})$ is not generally a BLU interpolant for $\mathcal {H}$, but these leaves provide enough information to find a BLU interpolant from some sequent down the proof search tree.

Example 22

Consider the layered sequent $\mathcal {G}= \varphi$ for $\varphi =\overline{p} \vee \Diamond \Diamond (p \vee q)$. We show how to construct $A_\ell (0, \varnothing ;\varphi )$ for $\ell =p$. First, we compute the proof search tree decorated with $(t, \varSigma _c)$ to the left of each line, according to the algorithm, using the following abbreviations $\varGamma = \varphi , \overline{p}, \Diamond \Diamond (p \vee q)$ and $\varSigma _1 = \Diamond (p \vee q), p \vee q, p, q$:

$\mathcal {H}=\varphi , \overline{p}, \Diamond \Diamond (p \vee q), [\Diamond (p \vee q), p \vee q, p, q]_{\bullet 1}, [\Diamond (p \vee q), p \vee q, p, q]_{\bullet \textsf{d}}, [[p \vee q, p, q]]_{\textsf{d}}$ in the left leaf is a saturated sequent with $\Diamond$-formulas, crown components, $t=1$, and $\Box \Diamond \mathcal {H}_c = \{\Diamond (p \vee q)\} \subseteq \{\Diamond (p \vee q)\}=\varSigma _c$. Hence, by Step 4c,

(7)

Applications of rule $\vee$ do not change the interpolant (Step 2, row 3). To compute $A_p(0,\varnothing ; \varGamma , [\varSigma _1]_{\bullet 1})$ for the conclusion of $\textsf{dd}$, we convert (7) into an SDNF

Now, by Step (d), and converting into a new SDNF, we get $A_p(0, \varnothing ; \varGamma , [\varSigma _1]_{\bullet 1})\equiv {}$

Further applications of $\vee$ and $\textsf{t}$ keep this interpolant intact. Note that the application of $\textsf{d}'_t$ does not require to continue proof search for the right branch. Instead, Step 4b prescribes that

Simplifying, we finally obtain

$$\begin{aligned} A_p(0, \varnothing ; \varphi ) \equiv \bullet : \Bigl ((\overline{p} \vee \Diamond \top ) \wedge \bigl ((\overline{p} \wedge \Diamond \top ) \vee \Diamond q \vee \Diamond \Diamond q \vee \Box \bot \bigr ) \Bigr ) \equiv \bullet : (\overline{p} \vee \Diamond \Diamond q) . \end{aligned}$$

(8)

To check that $\overline{p} \vee \Diamond \Diamond q$ is a uniform Lyndon interpolant for $\varphi$ w.r.t. literal p, it is sufficient to verify that (8) is a BLU interpolant for $\mathcal {G}$ by checking the conditions in Definition 18. We only check BLUIP(iii) as the least trivial. If $\mathcal {M},\mathcal {I}\nvDash \bullet : (\overline{p} \vee \Diamond \Diamond q)$ for an interpretation $\mathcal {I}$ into a $\textsf{K5}$-model $\mathcal {M}=(W,R,V)$, then, by Definitions 14 and 11, $\mathcal {M}, \rho \nvDash \overline{p} \vee \Diamond \Diamond q$ for the root $\rho$ of $\mathcal {M}$. For $\ell =p$, we have an $\ell$-bisimulation $(\mathcal {M}',\mathcal {I}) \le _\ell (\mathcal {M},\mathcal {I})$ for $\mathcal {M}'=(W,R,V')$ with $V'(p) = \{\rho \}$ and $V'(r) = V(r)$ for $r\ne p$ since $\textbf{literals}_p$ allows to turn p from true to false. It is easy to see that $\mathcal {M}',\rho \nvDash \overline{p} \vee \Diamond \Diamond (p \vee q)$. Thus, $\mathcal {M}', \mathcal {I}\nvDash \bullet : \varphi$.

We have the following properties of the algorithm (we provide a proof in [14]).

Lemma 23

All recursive calls $A_\ell (t,\varSigma _c; \mathcal {G})$ in a proof search tree of $A_\ell (0,\varnothing ; \varphi )$ have the following properties:

• 1. The algorithm is terminating.

• 2. When Step 4b is applied, $t=0$ and every branch going up from it consists of Steps 2–3 followed by either final Step 1 or continuation via Step 4d.

• 3. After Step 4d is applied, every branch going up from it consists of Steps 2 followed by a call $A_\ell (1,\Box \Diamond \mathcal {G}_c;\mathcal {G}, [\varTheta ]_{\bullet \textsf{d}}, [[\varPhi ]]_{\textsf{d}})$ of one of the following types:

  • (a) sufficient and final when calculated via Step 1;

  • (b) sufficient and propositionally saturated when calculated via Step 3, with every branch going up from there consisting of more Steps 2–3, followed by either final Step 1 or continuation via Step 4d;

  • (c) insufficient and saturated when calculated via Step 4c.

Theorem 24

Logic $\textsf{K5}$ has the BLUIP and, hence, the ULIP.

Proof

It is sufficient to prove that, once the algorithm starts on $A_\ell (0,\varnothing ; \varphi )$, then every sufficient call $A_\ell (t,\varSigma _c;\mathcal {G})$ in the proof search returns a BLU interpolant for a $\textsf{K5}$-sequent $\mathcal {G}$. Because the induction on the proof-search is quite technical and involves multiple cases, we demonstrate only a few representative cases and omitting simple ones, e.g., BLUIP(i), altogether. We present more cases in the Appendix of [14].

• BLUIP(ii) We show that $\mathcal {M}, \mathcal {I}\vDash A_\ell (t, \varSigma _c;\mathcal {G})$ implies $\mathcal {M}, \mathcal {I}\vDash \mathcal {G}$ for any interpretation $\mathcal {I}$ of $\mathcal {G}$ into any $\textsf{K5}$-model $\mathcal {M}=(W,R,V)$. The hardest among Steps 1–3 is Step 3 using row 5 in Table 4. Let $\mathcal {G}=\mathcal {G}', \Box \varphi$ and $\mathcal {M}, \mathcal {I}\vDash A_\ell (t, \varSigma _c;\mathcal {G}', \Box \varphi )$ for

  

  (9)

  i.e., for each $1\le i \le h$ either $\mathcal {M}, \rho \vDash \Box \delta _i$ or $\mathcal {M},\mathcal {I}(\tau ) \vDash \gamma _{i,\tau }$ for some $\tau \in \mathcal {G}$. For an arbitrary v such that $\rho R v$ and the the smallest j such that $\bullet j \notin \mathcal {G}$, clearly $\mathcal {I}_v = \mathcal {I}\sqcup \{(\bullet j, v )\}$ is an interpretation of $\mathcal {G}', \Box \varphi , [\varphi ]_{\bullet j}$ into $\mathcal {M}$. Since $\mathcal {M}, \mathcal {I}_v(\bullet j)\vDash \delta _i$ whenever $\mathcal {M}, \rho \vDash \Box \delta _i$, it follows that for each $1\le i \le h$ either $\mathcal {M}, \mathcal {I}_v(\bullet j) \vDash \delta _i$ or $\mathcal {M},\mathcal {I}_v(\tau ) \vDash \gamma _{i,\tau }$ for some $\tau \in \mathcal {G}$, i.e., $\mathcal {M}, \mathcal {I}_v \vDash A_\ell \bigl (t, \varSigma _c ; \mathcal {G}', \Box \varphi , [\varphi ]_{\bullet j}\bigr )$ for

  

  (10)

  By IH, $\mathcal {M}, \mathcal {I}_v \vDash \mathcal {G}', \Box \varphi , [\varphi ]_{\bullet j}$ whenever $\rho R v$. If $\mathcal {M}, \rho \vDash \Box \varphi$, then $\mathcal {M}, \mathcal {I}\vDash \mathcal {G}$. Otherwise, $\mathcal {M}, \mathcal {I}_v(\bullet j) \nvDash \varphi$ for some v with $\rho R v$. For it, $\mathcal {M}, \mathcal {I}_v \vDash \mathcal {G}'$, hence, $\mathcal {M}, \mathcal {I}\vDash \mathcal {G}$.

  The only other case we consider (here) is Step 4d. Let $\mathcal {M}, \mathcal {I}\vDash A_\ell (t, \varSigma _c; \mathcal {G})$ for $A_\ell (t, \varSigma _c; \mathcal {G})$ from (5), i.e., for some $1 \le i \le h$ we have $\mathcal {M}, \rho \vDash \Diamond \delta _i$, and $\mathcal {M}, \mathcal {I}(\bullet 1)\vDash \Diamond \delta '_i$, and $\mathcal {M}, \mathcal {I}(\tau ) \vDash \gamma _{i,\tau }$ for all $\tau \in \mathcal {G}$. In particular, $\mathcal {M}, v \vDash \delta _i$ for some $\rho Rv$ and $\mathcal {M}, u \vDash \delta '_i$ for some $\mathcal {I}(\bullet 1)Ru$. Let $\mathcal {M}'$ be obtained by copying u into $u'$ away from the root in $\mathcal {M}$ and let $\mathcal {J}= \mathcal {I}\sqcup \{(\bullet \textsf{d},v), (\textsf{d}, u')\}$ be a well-defined interpretation. $\mathcal {M}',\mathcal {J}\vDash A_\ell (1, \Box \Diamond \mathcal {G}_c ; \mathcal {G}, [\{\psi \mid \Diamond \psi \in \mathcal {G}\}]_{\bullet \textsf{d}}, [[ \{ \chi \mid \Diamond \chi \in \mathcal {G}_c\} ]]_{\textsf{d}})$, as (6) is true for $\mathcal {M}'$ and $\mathcal {J}$. By IH, $\mathcal {M}',\mathcal {J}\vDash \mathcal {G}, [\{\psi \mid \Diamond \psi \in \mathcal {G}\}]_{\bullet \textsf{d}}, [[ \{ \chi \mid \Diamond \chi \in \mathcal {G}_c\} ]]_{\textsf{d}}$. If $\mathcal {M}', v \vDash \psi$ for some $\Diamond \psi \in \mathcal {G}$ or $\mathcal {M}', u' \vDash \chi$ for some $\Diamond \chi \in \mathcal {G}_c$, then $\mathcal {M}', \mathcal {J}\vDash \mathcal {G}$ because of $\Diamond \psi$ or $\Diamond \chi$ respectively. Otherwise, also $\mathcal {M}',\mathcal {J}\vDash \mathcal {G}$. Since we have $(\mathcal {M}, \mathcal {I}) \sim (\mathcal {M}',\mathcal {J})$ by Lemma 21, we have $\mathcal {M}, \mathcal {I}\vDash \mathcal {G}$ by Lemma 17(2) in all cases.

• BLUIP(iii) We show the following statement by induction restricted to sufficient calls: if $\mathcal {M}, \mathcal {I}\nvDash A_\ell (t, \varSigma _c ; \mathcal {G})$, then $\mathcal {M}', \mathcal {J}' \nvDash \mathcal {G}$ for some interpretation $\mathcal {J}'$ of $\mathcal {G}$ into another $\textsf{K5}$-model $\mathcal {M}'$ such that $(\mathcal {M}',\mathcal {J}') \le _\ell (\mathcal {M},\mathcal {I})$. Here we only consider Step 4 as the other steps are sufficiently similar to K and S5 covered in [12, 13]. Among the four subcases, Step 4a is tedious but conceptually transparent. Step 4c is trivial because the induction statement is only for sufficient calls while Step 4c calls are insufficient by Lemma 23. Out of remaining two steps we only have space for Step 4d, which is conceptually the most interesting because its recursive call may be insufficient, precluding the use of IH for it. Let $\mathcal {M}, \mathcal {I}\nvDash A_\ell (t, \varSigma _c; \mathcal {G})$ for $A_\ell (t, \varSigma _c; \mathcal {G})$ from (5).

  We first modify $\mathcal {M}$ and $\mathcal {I}$ to obtain an injective interpretation $\mathcal {I}'$ into a $\textsf{K5}$-model $\mathcal {N}'=(W',R',V')$ such that $W' \setminus Range (\mathcal {I}')$ is not empty and partitioned into pairs (v, u) with $\mathcal {I}'(\bullet ) R v$ and not $\mathcal {I}'(\bullet ) Ru$. To this end we employ copying as per Definition 20, constructing a sequence of interpretations $\mathcal {I}_i$ from $\mathcal {G}$ into models $\mathcal {N}_i=(W_i,R_i,V_i)$ starting from $\mathcal {N}_0=\mathcal {M}$ and $\mathcal {I}_0 = \mathcal {I}$ as follows:

  • 1. If $\mathcal {I}_i(\tau _1)=\mathcal {I}_i(\tau _2)$ for $\tau _1 \ne \tau _2$, obtain $\mathcal {N}_{i+1}$ by copying $\mathcal {I}_i(\tau _2)$ to a new world w and redirect $\tau _2$ to this new world, i.e., $\mathcal {I}_{i+1}= \mathcal {I}_i \sqcup \{(\tau _2,w)\} \setminus \{(\tau _2,\mathcal {I}_i(\tau _2))\}$.

  • 2. If $\mathcal {I}_{K-1}$ is injective but $W_{K-1} \setminus Range (\mathcal {I}_{K-1})=\varnothing$, obtain $\mathcal {N}_{K}$ by copying $\mathcal {I}_{K-1}(\bullet 1)$ to a new world y. Set $\mathcal {I}_{K} = \mathcal {I}_{K-1}$. Now $W_{K} \setminus Range (\mathcal {I}_{K})\ne \varnothing$.

  • 3. Finally, define the two sets $Y = \{y \in W_{K} \setminus Range (\mathcal {I}_{K}) \mid \mathcal {I}_{K}(\bullet ) R_{K} y\}$ and $Z = \{z \in W_K \setminus Range (\mathcal {I}_K) \mid \text {not }\mathcal {I}_K(\bullet ) R_K z\}$ and obtain $\mathcal {N}'$ by copying:

    • for each $y \in Y$, copy $\mathcal {I}_K(\bullet 1)$ away from the root to a new world $y_2$;

    • for each $z \in Z$, copy $\mathcal {I}_K(\bullet 1)$ to a new world $z_1$.

    Then $\mathcal {I}' = \mathcal {I}_K$ is an injective interpretation of $\mathcal {G}$ into $\mathcal {N}'$.

  Note that $W' \setminus Range (\mathcal {I}')=Y \sqcup Z \sqcup \{y_2 \mid y \in Y\} \sqcup \{z_1 \mid z \in Z\} \ne \varnothing$. Further, $\mathcal {I}'(\bullet ) R' y$ for all $y \in Y$, and not $\mathcal {I}'(\bullet ) R' y_2$ for all $y \in Y$, and $\mathcal {I}'(\bullet ) R' z_1$ for all $z \in Z$, and not $\mathcal {I}'(\bullet ) R' z$ for all $z \in Z$. Thus, we obtain the requisite partition $P=\{(y,y_2)\mid y \in Y\}\sqcup \{(z_1,z)\mid z \in Z\}\ne \varnothing$ of the non-empty $W' \setminus Range (\mathcal {I}')$. It is clear that $(\mathcal {N}',\mathcal {I}') \sim (\mathcal {M}, \mathcal {I})$. So $\mathcal {N}', \mathcal {I}' \nvDash A_\ell (t, \varSigma _c ; \mathcal {G})$ by Lemma 17, i.e., for each $1 \le i \le h$ we have $\mathcal {N}', \rho \nvDash \Diamond \delta _i$ for $\rho = \mathcal {I}'(\bullet )$, or $\mathcal {N}', \mathcal {I}'(\bullet 1)\nvDash \Diamond \delta '_i$, or $\mathcal {N}', \mathcal {I}'(\tau ) \nvDash \gamma _{i,\tau }$ for some $\tau \in \mathcal {G}$. Thus, for any $(v,u)\in P$ and each $1 \le i \le h$, we have $\mathcal {N}', v \nvDash \delta _i$, or $\mathcal {N}', u\nvDash \delta '_i$, or $\mathcal {N}', \mathcal {I}'(\tau ) \nvDash \gamma _{i,\tau }$ for some $\tau \in \mathcal {G}$. Hence, (6) is false under injective interpretation $\mathcal {J}_{v,u} = \mathcal {I}' \sqcup \{(\bullet \textsf{d}, v), (\textsf{d}, u)\}$ into $\mathcal {N}'$, i.e., abbreviating $\varTheta = \{\psi \mid \Diamond \psi \in \mathcal {G}\}$ and $\varPhi = \{ \chi \mid \Diamond \chi \in \mathcal {G}_c\}$, we get $\mathcal {N}', \mathcal {J}_{v,u} \nvDash A_\ell (1, \Box \Diamond \mathcal {G}_c; \mathcal {G}, [\varTheta ]_{\bullet \textsf{d}}, [[ \varPhi ]]_{\textsf{d}}).$ Ordinarily, here we would use IH, but this is only possible for sufficient calls, which, alas, is not guaranteed for (6). What is known by Lemma 23(3) is that every branch going up from (6) leads to a call of the form

  $$\begin{aligned} A_\ell (1, \Box \Diamond \mathcal {G}_c ;\quad \mathcal {G}, [\varTheta _j]_{\bullet \textsf{d}}, [[ \varPhi _j ]]_{\textsf{d}}), \end{aligned}$$

  (11)

  where $\varTheta _j \supseteq \varTheta$ and $\varPhi _j \supseteq \varPhi$, that returns multiformula $\mho _j$ and is either sufficient or insufficient but saturated. Let $\varXi$ denote the multiset of these multiformulas $\mho _j$ returned by all these calls. Since Step 2 is the only one used between that call and all the calls comprising (11), it is clear that (6) is their conjunction, i.e., . Collecting all this together, we conclude that for each pair $(v,u) \in P$ there is some $\mho _{v,u} \in \varXi$ such that

  $$\begin{aligned} \mathcal {N}', \mathcal {J}_{v,u} \nvDash \mho _{v,u}. \end{aligned}$$

  (12)

  We distinguish between two cases. First, suppose for at least one pair $(v,u) \in P$ there is a sufficient $\mho _{v,u}= A_\ell (1, \Box \Diamond \mathcal {G}_c ; \mathcal {G}, [\varTheta _{v,u}]_{\bullet \textsf{d}}, [[ \varPhi _{v,u} ]]_{\textsf{d}})$ satisfying (12). By IH for this $\mho _{v,u}$ there is an interpretation $\mathcal {J}_0'$ into a $\textsf{K5}$-model $\mathcal {M}'$ such that $(\mathcal {M}', \mathcal {J}_0') \le _\ell (\mathcal {N}', \mathcal {J}_{v,u})$ and $\mathcal {M}', \mathcal {J}_0' \nvDash \mathcal {G}, [\varTheta _{v,u}]_{\bullet \textsf{d}}, [[ \varPhi _{v,u} ]]_{\textsf{d}}$. Thus, $\mathcal {M}', \mathcal {J}' \nvDash \mathcal {G}$ for $\mathcal {J}' = \mathcal {J}_0'\! \upharpoonright \! Lab (\mathcal {G})$. Finally, by restricting to labels of $\mathcal {G}$, we can see that

  $$\begin{aligned} (\mathcal {M}',\mathcal {J}')\quad \le _\ell \quad (\mathcal {N}', \mathcal {I}')\quad \sim \quad (\mathcal {M}, \mathcal {I}). \end{aligned}$$

  (13)

  Otherwise, (12) does not hold for any pair $(v,u)\in P$ and any sufficient $\mho _{v,u} \in \varXi$. In this case, guarantees the existence of an insufficient $\mho _{v,u}\in \varXi$ for each pair $(v,u) \in P$ such that (12) holds. Since all these $\mho _{v,u}$ are insufficient, we cannot use IH. Instead, we construct $\mathcal {M}'$ and $\mathcal {J}'$ directly by changing $\ell$ from true to false if needed based on $\mathcal {G}$ within $Range (\mathcal {I}')$ and based on $\mho _{v,u}$’s outside of this range. Thanks to $\mathcal {I}'$ being injective, we do not need to worry about conflicting requirements from different components of $\mathcal {G}$. Similarly, P being a partition prevents conflicts outside $Range (\mathcal {I}')$. Let $\mathcal {M}' = (W',R',U')$ be $\mathcal {N}'$ with $V'$ changed into $U'$. We define ${V'}\mathord {\downarrow }_{\ell }{T}$ as the valuation that makes $\ell$ false in all worlds from $T \subseteq W'$, i.e., $({V'}\mathord {\downarrow }_{\ell }{T}) (q)= V'(q)$ for all $q\notin \{\ell ,\overline{\ell }\}$, while

  $$ ({V'}\mathord {\downarrow }_{\ell }{T})(p) = {\left\{ \begin{array}{ll} V'(p) \setminus T &{} \text {if }\ell =p, \\ V'(p) \cup T &{} \text {if }\ell =\overline{p} \end{array}\right. } $$

  for $p \in \{\ell ,\overline{\ell }\}$. Using this notation, we define $U' = {V'}\mathord {\downarrow }_{\ell }{T_\mathcal {G}}$ where

  $$\begin{aligned}&T_\mathcal {G}= \{ \mathcal {I}'(\sigma ) \mid \sigma : \ell \in \mathcal {G}\} \sqcup \{ v \mid (v,u) \in P\text { and }\bullet \textsf{d}: \ell \in \mho _{v,u} \} \sqcup \nonumber \\&\qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \,\,\,\, \{u \mid (v,u) \in P \text { and } \textsf{d}:\ell \in \mho _{v,u}\}. \end{aligned}$$

  (14)

  Finally, $\mathcal {J}' = \mathcal {I}'$. It is clear that (13) holds for these $\mathcal {M}'$ and $\mathcal {J}'$. It remains to show that $\mathcal {M}',\mathcal {J}' \nvDash \mathcal {G}$. This is done by mutual induction on the construction of formula $\varphi$ for the following three induction statements

  $$\begin{aligned} \sigma : \varphi \in \mathcal {G}&\Longrightarrow \mathcal {M}', \mathcal {I}'(\sigma ) \nvDash \varphi ,\end{aligned}$$

  (15)
  $$\begin{aligned} \bullet \textsf{d}:\varphi \in \mho _{v,u}&\Longrightarrow \mathcal {M}', v \nvDash \varphi ,\end{aligned}$$

  (16)
  $$\begin{aligned} \textsf{d}: \varphi \in \mho _{v,u}&\Longrightarrow \mathcal {M}', u \nvDash \varphi . \end{aligned}$$

  (17)

  • Case $\varphi = \ell '\in \textsf{Lit}\setminus \{\ell , \overline{\ell }\}$. By Lemma 23(3), all $\mho _{v,u}$ are computed by Step 4c due to their insufficiency, i.e., $\mho _{v,u}=\textsf{LitDis}_\ell (\mathcal {G}, [\varTheta _{v,u}]_{\bullet \textsf{d}}, [[ \varPhi _{v,u} ]]_{\textsf{d}})$. (16) and (17) follow from (12) and (2) because $\mathcal {M}'$ agrees with $\mathcal {N}'$ on $\ell ' \notin \{\ell ,\overline{\ell }\}$. Similarly, since $\mathcal {J}_{v,u}$ agrees with $\mathcal {J}'=\mathcal {I}'$ on $Lab (\mathcal {G})$, (15) follows by using $\mho _{v,u}$ for any $(v,u) \in P \ne \varnothing$.

  • Case $\varphi = \overline{\ell }$ is analogous to the previous one. The only difference is the reason why $\mathcal {M}'$ agrees with $\mathcal {N}'$ on $\overline{\ell }$. Here, $\sigma : \overline{\ell }\in \mathcal {G}$ implies $\sigma : \ell \notin \mathcal {G}$ because $\mathcal {G}$ was processed by Step 4d not Step 1. Therefore, $\mathcal {I}'(\sigma ) \notin T_\mathcal {G}$ by the injectivity of $\mathcal {I}'$, and $\overline{\ell }$ was not made true in $\mathcal {I}'(\sigma )$, ensuring (15). The argument for (16) and (17) is similar, except $\bullet \textsf{d}/\textsf{d}: \overline{\ell }$ is taken from $\mho _{v,u}$ processed by Step 4c not Step 1.

  • Case $\varphi = \ell$. All of (15)–(17) follow from (14).

  • Cases $\varphi = \varphi _1 \wedge \varphi _2$ and $\varphi = \varphi _1 \vee \varphi _2$ are standard and follow by IH due to saturation of $\mathcal {G}$ for (15) and $\mho _{v,u}$ for (16) and (17).

  • Case $\varphi =\Box \xi$. If $\sigma : \Box \xi \in \mathcal {G}$, then by saturation of $\mathcal {G}$, there is a $\tau$ such that $\tau : \xi \in \mathcal {G}$ and $\mathcal {I}'(\sigma )R'\mathcal {I}'(\tau )$: if $\sigma = \bullet$, then $\tau = \bullet j$ for some j, while if $\sigma \ne \bullet$, then $\tau \ne \bullet$. By IH(15), $\mathcal {M}',\mathcal {I}'(\tau ) \nvDash \xi$, and $\mathcal {M}', \mathcal {I}'(\sigma ) \nvDash \Box \xi$.

    If $\bullet \textsf{d}/\textsf{d}: \Box \xi \in \mho _{v,u}$, then $\Box \xi \in \Box \Diamond \mathcal {G}_c$ by conditions of Step 4c due to (11), i.e., $\Box \xi \in \mathcal {G}_c$. By saturation of $\mathcal {G}$, there is a $\tau \ne \bullet$ such that $\tau : \xi \in \mathcal {G}$. Since v, u, and $\mathcal {I}'(\tau )$ are all in the cluster C of $\mathcal {M}'$, we have $vR'\mathcal {I}'(\tau )$ and $uR'\mathcal {I}'(\tau )$. It remains to use IH(16) and IH(17).

  • Case $\varphi =\Diamond \xi$. First consider $\sigma = \bullet$ and $\bullet : \Diamond \xi \in \mathcal {G}$. Since $\mathcal {I}'(\bullet )=\rho$ is the root, $\rho R' w$ implies either $w = \mathcal {I}'(\bullet j)$ for some j or $w \notin Range (\mathcal {I}')$. In the former case, $\bullet j : \xi \in \mathcal {G}$ by saturation of $\mathcal {G}$, so $\mathcal {M}', w \nvDash \xi$ by IH(15). In the latter case, $(w,u) \in P$ for some u. Recall for $A_\ell (1, \Box \Diamond \mathcal {G}_c ; \mathcal {G}, [\varTheta _{w,u}]_{\bullet \textsf{d}}, [[ \varPhi _{w,u} ]]_{\textsf{d}})$ that we have $\varTheta _{w,u} \supseteq \varTheta = \{ \psi \mid \Diamond \psi \in \mathcal {G}\} \ni \xi$. Hence, $\bullet \textsf{d}: \xi \in \mho _{w,u}$ and $\mathcal {M}', w \nvDash \xi$ by IH(16). Since $\mathcal {M}', w \nvDash \xi$ for all $\mathcal {I}'(\bullet )=\rho R' w$, we conclude $\mathcal {M}', \mathcal {I}'(\bullet ) \nvDash \Diamond \xi$.

    If $\sigma \ne \bullet$ and $\sigma : \Diamond \xi \in \mathcal {G}$, the argument is similar. But additionally we may have $w = \mathcal {I}'(k)$ for some k or $(v,w) \in P$ for some v. In the former case, $k : \xi \in \mathcal {G}$ by saturation of $\mathcal {G}$, so $\mathcal {M}', w \nvDash \xi$ by IH(15). In the latter case, $\varPhi _{v,w} \supseteq \varPhi = \{ \chi \mid \Diamond \chi \in \mathcal {G}_c\} \ni \xi$. Hence, $\textsf{d}: \xi \in \mho _{v,w}$ and $\mathcal {M}', w \nvDash \xi$ by IH(17). Since $\mathcal {M}', w \nvDash \xi$ for all $\mathcal {I}'(\sigma ) R' w$, we conclude $\mathcal {M}', \mathcal {I}'(\sigma ) \nvDash \Diamond \xi$.

    If $\bullet \textsf{d}/\textsf{d}: \Diamond \xi \in \mho _{v,u}$, then, similar to the analogous subcase of $\Box \xi$, conditions of Step 4c imply that $\Diamond \xi \in \mathcal {G}_c$, i.e., $\tau _0 : \Diamond \xi \in \mathcal {G}$ for some $\tau _0 \ne \bullet$. Then $\tau : \xi \in \mathcal {G}$ for all $\tau \ne \bullet$ by saturation of $\mathcal {G}$. Thus, $\mathcal {M}',\mathcal {I}'(\tau )\nvDash \xi$ for all $\tau \ne \bullet$ by IH(15). For each $y\notin Range (\mathcal {I}')$ such that $\rho R' y$, there is x such that $(y,x) \in P$ and $\bullet \textsf{d}: \xi \in \mho _{y,x}$ because $\varTheta _{y,x} \supseteq \varTheta \ni \xi$. Hence, $\mathcal {M}', y \nvDash \xi$ by IH(16). Finally, for each $x\notin Range (\mathcal {I}')$ such that not $\rho R' x$, there is y such that $(y,x) \in P$ and $\textsf{d}: \xi \in \mho _{y,x}$ because $\varPhi _{y,x} \supseteq \varPhi \ni \xi$. Hence, $\mathcal {M}', x \nvDash \xi$ by IH(17). We have shown that $\mathcal {M}', w \nvDash \xi$ whenever $v R' w$ ($u R' w$). Thus, $\mathcal {M}', v \nvDash \Diamond \xi$ and $\mathcal {M}', u \nvDash \Diamond \xi$.    $\square$

5 Conclusion

We presented layered sequent calculi for several extensions of modal logic $\textsf{K5}$: namely, $\textsf{K5}$ itself, $\textsf{KD5}$, $\textsf{K45}$, $\textsf{KD45}$, $\textsf{KB5}$, and $\textsf{S5}$. By leveraging the simplicity of Kripke models for these logics, we were able to formulate these calculi in a modular way and obtain optimal complexity upper bounds for proof search. We used the calculus for $\textsf{K5}$ to obtain the first syntactic (and, hence, constructive) proof of the uniform Lyndon interpolation property for $\textsf{K5}$.

Due to the proof being technically involved, space considerations prevented us from extending the syntactic proof of ULIP to $\textsf{KD5}$, $\textsf{K45}$, $\textsf{KD45}$, $\textsf{KB5}$, and $\textsf{S5}$. For $\textsf{S5}$, layered sequents coincide with hypersequents, and we plan to upgrade the hypersequent-based syntactic proof of UIP from [11] to ULIP (see also [13]). As for $\textsf{KD5}$, $\textsf{K45}$, $\textsf{KD45}$, and $\textsf{KB5}$, the idea is to modify the method presented here for $\textsf{K5}$ by using the layered sequent calculus for the respective logic and making other necessary modifications, e.g., to rule $\textsf{dd}$, to fit the specific structure of the layers. We conjecture that the proof for $\textsf{K45}$, $\textsf{KD45}$, and $\textsf{KB5}$ would be similar to that for $\textsf{S5}$, whereas $\textsf{KD5}$ would more closely resemble $\textsf{K5}$.