11institutetext: University of Birmingham, UK, 11email:
<EMAIL_ADDRESS>22institutetext: Utrecht University, Netherlands
and Czech Academy of Sciences, Prague, Czechia, 22email:
<EMAIL_ADDRESS>33institutetext: TU Wien, Austria, 33email:
<EMAIL_ADDRESS>
# Extensions of ${\sf K5}$: Proof Theory and
Uniform Lyndon Interpolation

Iris van der Giessen Supported by a UKRI Future Leaders Fellowship, ‘Structure
vs Invariants in Proofs’, project reference MR/S035540/1.11 Raheleh 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.22 0000-0002-3321-8087 Roman Kuznets Supported by the Austrian
Science Fund (FWF) ByzDEL project (P33600).33 0000-0001-5894-8724

###### Abstract

We introduce a Gentzen-style framework, called _layered sequent calculi_ , for
modal logic ${\sf K5}$ and its extensions ${\sf KD5}$, ${\sf K45}$, ${\sf
KD45}$, ${\sf KB5}$, and ${\sf 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 ${\sf 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.

##  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 [16] and description logics [24]. Early results on the UIP in
modal logic include positive results proved semantically for logics
$\mathsf{GL}$ and $\mathsf{K}$ (independently in [31, 9, 34]) and negative
results for logics ${\sf S4}$ [10] and ${\sf K4}$ [5]. A proof-theoretic
method to prove the UIP was first proposed in [29] for intuitionistic
propositional logic and later adapted to modal logics, such as $\mathsf{K}$
and $\mathsf{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 [15, 3, 2].

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 [17] 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, 18, 20, 22, 23].
First steps have been made by reproving the UIP for modal logics ${\sf K}$,
${\sf D}$, and ${\sf T}$ via nested sequents [12] and for ${\sf S5}$ via
hypersequents [13, 11], the first time this is proved proof-theoretically for
${\sf S5}$.

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

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 [26]. For ${\sf S5}$, this results in standard
hypersequents [25, 30, 4]. For ${\sf K5}$ and ${\sf KD5}$, the presented
calculi are similar to grafted hypersequent calculi in [21] but without
explicit weakening. Other, less related, proof systems include analytic cut-
free sequent systems for ${\sf K5}$ and ${\sf KD5}$ [33], cut-free sequent
calculi for ${\sf K45}$ and ${\sf KD45}$ [32], 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 [14]. 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 ${\sf K5}$. The method is adapted from [11, 13] in which the
UIP is proved for ${\sf 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
[17].

##  2 Preliminaries

The language of modal logics consists of a set $\mathsf{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 ${\sf 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}}\colonequals p$) and
$\varphi\to\psi\colonequals\overline{\varphi}\vee\psi$. We use uppercase Greek
letters $\Gamma,\Delta,\ldots$ to refer to finite _multisets_ of formulas. We
write $\Gamma,\Delta$ to mean $\Gamma\cup\Delta$ and $\Gamma,\varphi$ to mean
$\Gamma\cup\\{\varphi\\}$. The set of literals of a formula $\varphi$, denoted
${\sf Lit}(\varphi)$, is defined recursively: ${\sf Lit}(\top)={\sf
Lit}(\bot)=\varnothing$, ${\sf Lit}(\ell)=\ell$ for $\ell\in{\sf Lit}$, ${\sf
Lit}(\varphi\wedge\psi)={\sf Lit}(\varphi\vee\psi)={\sf Lit}(\varphi)\cup{\sf
Lit}(\psi)$, and ${\sf Lit}(\Box\varphi)={\sf Lit}(\Diamond\varphi)={\sf
Lit}(\varphi)$.

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

######  Definition 1 (Logic ${\sf K5}$)

_Modal logic ${\sf K5}$_ is axiomatized by the classical tautologies, axioms
$\sf k$ and $\sf 5$, and rules modus ponens $($from $\varphi$ and
$\varphi\to\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\colon\mathsf{Pr}\to\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

$\mathcal{M},w\vDash p$ | iff | $w\in V(p)$
---|---|---
$\mathcal{M},w\vDash\overline{p}$ | iff | $w\notin V(p)$
$\mathcal{M},w\vDash\varphi\land\psi$ | iff |  $\mathcal{M},w\vDash\varphi$ and $\mathcal{M},w\vDash\psi$
$\mathcal{M},w\vDash\varphi\lor\psi$ | iff |  $\mathcal{M},w\vDash\varphi$ or $\mathcal{M},w\vDash\psi$
$\mathcal{M},w\vDash\Box\varphi$ | iff | for all $v\in W$ such that $wRv$, $\mathcal{M},v\vDash\varphi$
$\mathcal{M},w\vDash\Diamond\varphi$ | iff | there exists $v\in W$ such that $wRv$ and $\mathcal{M},v\vDash\varphi$.

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\neq 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$.

Axiom | Formula | Frame condition
---|---|---
$\sf k$ | $\Box(\varphi\to\psi)\to(\Box\varphi\to\Box\psi)$ | none
$\sf 5$ | $\Diamond\varphi\to\Box\Diamond\varphi$ |  Euclidean: $wRv\wedge wRu\Rightarrow vRu$
$\sf 4$ | $\Box\varphi\to\Box\Box\varphi$ |  transitive: $wRv\wedge vRu\Rightarrow wRu$
$\sf d$ | $\Box\varphi\to\Diamond\varphi$ |  serial: $\forall w\exists v(wRv)$
$\sf b$ | $\varphi\to\Box\Diamond\varphi$ |  symmetric: $wRv\Rightarrow vRw$
$\sf t$ | $\Box\varphi\to\varphi$ |  reflexive: $\forall w(wRw)$
Table 1: Modal axioms and their corresponding frame conditions.

Logic L | Axiomatization |  Class of L-frames $(W,R)$
---|---|---
${\sf K5}$ |  Definition 1 |  $W=\\{\rho\\}$ or $W=\\{\rho\\}\sqcup C$
${\sf KD5}$ | ${\sf K5}+\sf d$ | $W=\\{\rho\\}\sqcup C$
${\sf K45}$ | ${\sf K5}+\sf 4$ |  $W=\\{\rho\\}$ or ($W=\\{\rho\\}\sqcup C$ and $\rho RC$)
${\sf KD45}$ | ${\sf K5}+\sf d+\sf 4$ |  $W=\\{\rho\\}\sqcup C$ and $\rho RC$
${\sf KB5}$ | ${\sf K5}+\sf b$ |  $W=\\{\rho\\}$ or $W=C$
${\sf S5}$ | ${\sf K5}+\sf t$ | $W=C$

Table 2: Semantics for extensions of ${\sf K5}$ (see [26, 28]). 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 ${\sf L}$, called _${\sf
L}$ -frames_, are defined in Table 2. A model $(W,R,V)$ is an _$\sf L$ -model_
iff $(W,R)$ is an $\sf{L}$-frame. Table 2 is a refinement of Theorem 2.1,
particularly shown for ${\sf K45}$, ${\sf KD45}$, and ${\sf KB5}$ in [28].
More precisely, we consider rooted frames and completeness w.r.t. the root,
i.e., $\vdash_{\sf L}\varphi$ iff for all ${\sf L}$-models $\mathcal{M}$ with
root $\rho$, $\mathcal{M},\rho\vDash\varphi$ (we often denote the if-condition
as $\vDash_{\sf L}\varphi$). For each logic, this follows from easy
bisimulation arguments.

######  Theorem 2.1 ([26])

Any normal modal logic containing ${\sf 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 Rw$ for some $w\in W\backslash\\{\rho\\}$ while not $\rho R\rho$.

######  Definition 3 (UIP and ULIP)

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

  1. (1)

${\sf Lit}(\forall p\varphi)\subseteq{\sf
Lit}(\varphi)\setminus\\{p,\overline{p}\\}$,

  2. (2)

$\vdash_{\sf L}\forall p\varphi\to\varphi$, and

  3. (3)

$\vdash_{\sf L}\psi\rightarrow\varphi\text{ implies }\vdash_{\sf
L}\psi\rightarrow\forall p\varphi$ for any formula $\psi$ with
$p,\overline{p}\notin{\sf Lit}(\psi)$.

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

  1. (i)

${\sf Lit}(\forall\ell\varphi)\subseteq{\sf Lit}(\varphi)\setminus\\{\ell\\}$,

  2. (ii)

$\vdash_{\sf L}\forall\ell\varphi\to\varphi$, and

  3. (iii)

$\vdash_{\sf L}\psi\rightarrow\varphi\text{ implies }\vdash_{\sf
L}\psi\rightarrow\forall\ell\varphi$ for any formula $\psi$ with
$\ell\notin{\sf 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, 17] for more explanations).

###### Theorem 2.2

If a logic ${\sf 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 Def. 3. First, it follows from ULIP(i) that ${\sf
Lit}(\forall p\forall\overline{p}\varphi)\subseteq{\sf
Lit}(\forall\overline{p}\varphi)\setminus\\{p\\}\subseteq{\sf
Lit}(\varphi)\setminus\\{p,\overline{p}\\}$. Second, $\vdash_{{\sf L}}\forall
p\forall\overline{p}\varphi\to\forall\overline{p}\varphi$ and $\vdash_{{\sf
L}}\forall\overline{p}\varphi\to\varphi$ by ULIP(ii), hence, $\vdash_{{\sf
L}}\forall p\forall\overline{p}\varphi\to\varphi$. Finally, if $\vdash_{{\sf
L}}\psi\to\varphi$ where $p,\overline{p}\notin{\sf Lit}(\psi)$, then by
ULIP(iii), $\vdash_{{\sf L}}\psi\to\forall\overline{p}\varphi$ as
$\overline{p}\notin{\sf Lit}(\psi)$ and $\vdash_{{\sf L}}\psi\to\forall
p\forall\overline{p}\varphi$ as $p\notin{\sf Lit}(\psi)$. ∎

##  3 Layered Sequents

######  Definition 4 (Layered sequents)

A _layered sequent_ is a generalized one-sided sequent of the form

$\mathcal{G}=\Gamma_{1},\ldots,\Gamma_{n},[\Sigma_{1}],\ldots,[\Sigma_{m}],[[\Pi_{1}]],\ldots,[[\Pi_{k}]]$
(1)

where $\Gamma_{i},\Sigma_{i},\Pi_{i}$ are finite multisets of formulas,
$n,m,k\geq 0$, and if $k\geq 1$, then $m\geq 1$. A layered sequent is an ${\sf
L}$-sequent iff it satisfies the conditions in the rightmost column of Table
3. Each $\Sigma_{i}$, each $\Pi_{i}$, and $\bigcup_{i}\Gamma_{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\Gamma_{i}\big{)}\vee\bigvee\nolimits_{i=1}^{m}\Box\big{(}\bigvee\Sigma_{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
(_$[\enspace]$ -components_ $\Sigma_{i}$ and _$[[\enspace]]$ -components_
$\Pi_{i}$ forming the first and second layer respectively) possibly nested on
top of the sequent component $\bigcup_{i}\Gamma_{i}$ as the root. Following
the arboreal terminology from [21], the root is called the _trunk_ while
$[\enspace]$\- and $[[\enspace]]$-components form the _crown_. Analogously to
nested sequents representing tree-like Kripke models, the structure of ${\sf
L}$-sequents is in line with the structure of ${\sf L}$-models introduced in
Sect. 2. We view sequents components as freely permutable, e.g.,
$[[\Pi_{1}]],\Gamma_{1},[\Sigma_{1}],\Gamma_{2}$ and
$\Gamma_{1},\Gamma_{2},[\Sigma_{1}],[[\Pi_{1}]]$ represent the same layered
sequent.

Calculus | Sequent rules | Conditions on layered sequents
---|---|---
${\sf L.K5}$ |  $\Box_{t}$ |  | $\Diamond_{t}$ |  | $\Box_{c^{\prime}}$ |  |  |  | $n\geq 1,\;m,k\geq 0$
${\sf L.KD5}$ |  $\Box_{t}$ |  | $\Diamond_{t}$ |  | $\Box_{c^{\prime}}$ | ${\sf d}_{t}$ |  | ${\sf d}_{c^{\prime}}$ | $n\geq 1,\;m,k\geq 0$
${\sf L.K45}$ |  $\Box_{t}$ |  | $\Diamond_{t}$ | $\Box_{c}$ |  |  |  |  | $n\geq 1,\;m\geq 0,\;k=0$
${\sf L.KD45}$ |  $\Box_{t}$ |  | $\Diamond_{t}$ | $\Box_{c}$ |  | ${\sf d}_{t}$ | ${\sf d}_{c}$ |  | $n\geq 1,\;m\geq 0,\;k=0$
${\sf L.KB5}$ |  |  $\Box_{t^{\prime}}$ |  | $\Box_{c}$ |  |  |  |  |  $n=0,m\geq 2,k=0\;$ or $\;n=1,m=0,k=0$
${\sf L.S5}$ |  |  |  | $\Box_{c}$ |  |  |  |  | $n=0,\;m\geq 1,\;k=0$
Table 3: Layered sequent calculi ${\sf L.L}$: in addition to explicitly stated
rules, all ${\sf L.L}$ have axioms $\mathsf{id_{P}}$ and $\mathsf{id_{\top}}$
and rules $\vee$, $\wedge$, $\Diamond_{c}$, and ${\sf t}$ (see Fig. 1). Note
that the rules of system ${\sf L.L}$ may only be applied to ${\sf
L}$-sequents.

$\scriptstyle\mathsf{id_{P}}\;$ $\mathcal{G}{\\{p,\overline{p}\\}}$
$\scriptstyle\mathsf{id_{\top}}\;$ $\mathcal{G}{\\{\top\\}}$
$\mathcal{G}{\\{\varphi\land\psi,\varphi\\}}$$\mathcal{G}{\\{\varphi\land\psi,\psi\\}}$
$\scriptstyle\land\;$ $\mathcal{G}{\\{\varphi\land\psi\\}}$
$\mathcal{G}{\\{\varphi\lor\psi,\varphi,\psi\\}}$ $\scriptstyle\lor\;$
$\mathcal{G}{\\{\varphi\lor\psi\\}}$ $\mathcal{G},\Box\varphi,[\varphi]$
$\scriptstyle\Box_{t}\;$ $\mathcal{G},\Box\varphi$
$[\Sigma,\Box\varphi],[\varphi]$ $\scriptstyle\Box_{t^{\prime}}\;$
$\Sigma,\Box\varphi$ $\mathcal{G},\Diamond\varphi,[\Sigma,\varphi]$
$\scriptstyle\Diamond_{t}\;$ $\mathcal{G},\Diamond\varphi,[\Sigma]$
$\mathcal{G},\llbracket\Sigma,\Box\varphi\rrbracket,[\varphi]$
$\scriptstyle\Box_{c}\;$ $\mathcal{G},\llbracket\Sigma,\Box\varphi\rrbracket$
$\mathcal{G},\llbracket\Sigma,\Box\varphi\rrbracket,[[\varphi]]$
$\scriptstyle\Box_{c^{\prime}}\;$
$\mathcal{G},\llbracket\Sigma,\Box\varphi\rrbracket$
$\mathcal{G},\llbracket\Sigma,\Diamond\varphi\rrbracket,\llparenthesis\Pi,\varphi\rrparenthesis$
$\scriptstyle\Diamond_{c}\;$
$\mathcal{G},\llbracket\Sigma,\Diamond\varphi\rrbracket,\llparenthesis\Pi\rrparenthesis$
$\mathcal{G},\Diamond\varphi,[\varphi]$ $\scriptstyle{\sf d}_{t}\;$
$\mathcal{G},\Diamond\varphi$
$\mathcal{G},\llbracket\Sigma,\Diamond\varphi\rrbracket,[\varphi]$
$\scriptstyle{\sf d}_{c}\;$
$\mathcal{G},\llbracket\Sigma,\Diamond\varphi\rrbracket$
$\mathcal{G},\llbracket\Sigma,\Diamond\varphi\rrbracket,[[\varphi]]$
$\scriptstyle{\sf d}_{c^{\prime}}\;$
$\mathcal{G},\llbracket\Sigma,\Diamond\varphi\rrbracket$
$\mathcal{G},\llbracket\Sigma,\Diamond\varphi,\varphi\rrbracket$
$\scriptstyle{\sf t}\;$
$\mathcal{G},\llbracket\Sigma,\Diamond\varphi\rrbracket$

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

###### Remark 1

The layered calculi presented here generalize grafted hypersequents of [21]
and, hence, similarly combine features of hypersequents and nested sequents.
In particular, layered sequents are generally neither pure hypersequents
(except for the case of ${\sf 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 ${\sf K5}$ and ${\sf KD5}$ in [21] 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 ${\sf K5}$ [21, Sect. 6]). There prefixes for the crown are
separated into two types, limbs and twigs, which match the separation into
$[\enspace]$\- and $[[\enspace]]$-components.

For a layered sequent (1), we assign labels to the components as follows: the
trunk is labeled $\bullet$, $[\enspace]$-components get distinct labels
$\bullet 1,\bullet 2,\dots$, and $[[\enspace]]$-components get distinct labels
$1,2,\dots$. We let $\sigma,\tau,\dots$ range over these labels. The set of
labels is denoted $\mathit{Lab}(\mathcal{G})$ and $\sigma\in\mathcal{G}$ means
$\sigma\in\mathit{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 1

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

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

Using Fig. 1 and the middle column of Table 3, we define layered sequent
calculi ${\sf L.K5}$, ${\sf L.KD5}$, ${\sf L.K45}$, ${\sf L.KD45}$, ${\sf
L.KB5}$, and ${\sf L.S5}$, where ${\sf L.L}$ is the calculus for the logic
${\sf L}$. Following the terminology from [21], 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_{\sf
L.L}\mathcal{G}$ iff $\mathcal{G}$ is derivable in ${\sf L.L}$.

######  Definition 5 (Saturation)

Labeled formula $\sigma:\varphi\in\mathcal{G}$ is _saturated for ${\sf 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^{\prime}$, the unique rule applicable to
$\sigma:\Box\varphi^{\prime}$ in ${\sf L.L}$ is either $\Box_{t}$ or
$\Box_{c}$ $($i.e., a rule creating a $[\enspace]$-component$)$, and $\bullet
i:\varphi^{\prime}\in\mathcal{G}$ for some $i$;

  * •

$\varphi=\Box\varphi^{\prime}$, the unique rule applicable to
$\sigma:\Box\varphi^{\prime}$ in ${\sf L.L}$ is $\Box_{c^{\prime}}$ $($i.e., a
rule creating a $[[\enspace]]$-component$)$, and
$i:\varphi^{\prime}\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\mathit{Lab}(\mathcal{G})$;

  * •

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

  * •

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

  * •

$\sigma:\Diamond\varphi$ is _${\sf d}_{t}$ -saturated_ iff $\sigma\neq\bullet$
or $\bullet i:\varphi\in\mathcal{G}$ for some $i$;

  * •

$\sigma:\Diamond\varphi$ is _${\sf d}_{c}$ -saturated_ iff $\sigma=\bullet$ or
$\bullet i:\varphi\in\mathcal{G}$ for some $i$;

  * •

$\sigma:\Diamond\varphi$ is _${\sf d}^{\prime}_{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}$. ${\sf L}$-sequent
$\mathcal{G}$ is _${\sf L}$ -saturated_ iff $a)$ each non-$\Diamond$ formula
is saturated, $b)$ each $\sigma:\Diamond\varphi$ is saturated w.r.t. every
label in $\mathit{Lab}(\mathcal{G})$, $c)$ each $\sigma:\Diamond\varphi$ is
${\sf d}$-saturated whenever ${\sf d}\in{\sf L.L}\cap\\{{\sf d}_{t},{\sf
d}_{c},{\sf d}_{c^{\prime}}\\}$, and $d)$ $\mathcal{G}$ is not of the from
$\mathcal{H}\\{\top\\}$ or $\mathcal{H}\\{q,\overline{q}\\}$ for some
$q\in{\sf Pr}$.

###### Theorem 3.1

Proof search in ${{\sf 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.∎

######  Definition 6 (Interpretations)

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

  1. 1.

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

  2. 2.

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

  3. 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 $\mathit{Lab}(\mathcal{G})$;

  4. 4.

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

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

######  Definition 7 (Sequent semantics)

For any given interpretation $\mathcal{I}$ of an ${\sf L}$-sequent
$\mathcal{G}$ into an ${\sf L}$-model $\mathcal{M}$,

$\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}.$

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

The proof of the following theorem is based on a countermodel construction
(with more standard parts of the proof relegated to the Appendix):

######  Theorem 3.2 (Soundness and completeness)

For any ${\sf L}$-sequent $\mathcal{G}$,

$\vdash_{\sf L.L}\mathcal{G}\qquad\Longleftrightarrow\qquad\vDash_{\sf
L}\iota(\mathcal{G})\qquad\Longleftrightarrow\qquad\vDash_{\sf L}\mathcal{G}.$

###### Proof

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

For the middle-to-right implication, i.e., $\vDash_{\sf
L}\iota(\mathcal{G})\Longrightarrow\ \vDash_{\sf 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}\Gamma_{i}$, for each $1\leq i\leq m$ we
have $\mathcal{I}(\bullet i)\nvDash\psi$ for all $\psi\in\Sigma_{i}$, and for
each $1\leq i\leq k$ we have $\mathcal{I}(i)\nvDash\chi$ for all
$\chi\in\Pi_{i}$. By Def. 6, in case $k\geq 1$ label $\bullet 1$ is in
$\mathcal{G}$ and $\mathcal{I}(\bullet)R\mathcal{I}(\bullet 1)R\mathcal{I}(i)$
for each $1\leq i\leq 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 ${\sf L}$-model refuting $\mathcal{G}$ from (1). In a failed
proof-search tree (Theorem 3.1), since $\nvdash_{\sf L.L}\mathcal{G}$, at
least one saturated leaf

$\mathcal{G}^{\prime}=\Gamma^{\prime},[\Sigma^{\prime}_{1}],\ldots,[\Sigma^{\prime}_{m}],[\Sigma^{\prime\prime}_{1}],\ldots,[\Sigma^{\prime\prime}_{m^{\prime}}],[[\Pi^{\prime}_{1}]],\ldots,[[\Pi^{\prime}_{k}]],[[\Pi^{\prime\prime}_{1}]],\ldots,[[\Pi^{\prime\prime}_{k^{\prime}}]],\vspace{-0.15em}$

is such that $\bigcup_{i}\Gamma_{i}\subseteq\Gamma^{\prime}$,
$\Sigma_{i}\subseteq\Sigma^{\prime}_{i}$, and
$\Pi_{i}\subseteq\Pi^{\prime}_{i}$ (or for ${\sf KB5}$, if
$\mathcal{G}=\Gamma$, then $\mathcal{G}^{\prime}=\Gamma^{\prime}$ for
$\Gamma\subseteq\Gamma^{\prime}$ or $[\Sigma],[\Sigma_{1}],\dots,[\Sigma_{m}]$
with $\Gamma\subseteq\Sigma$). Define $\mathcal{M}=(W,R,V)$:

$\displaystyle W=\mathit{Lab}(\mathcal{G}^{\prime}),\qquad\qquad
V(p)=\\{\sigma\mid\sigma:\overline{p}\in\mathcal{G}^{\prime}\\},$
$\displaystyle R=\\{(\bullet,\bullet i)\mid\bullet
i\in\mathit{Lab}(\mathcal{G}^{\prime})\\}\cup\\{(\sigma,\tau)\mid\sigma,\tau\in\mathit{Lab}(\mathcal{G}^{\prime}),\sigma,\tau\neq\bullet\\}.$

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

##  4 Uniform Lyndon Interpolation

######  Definition 8 (Multiformulas)

The grammar

$\mho\coloncolonequals\sigma:\varphi\mid(\mho\mathbin{\varowedge}\mho)\mid(\mho\mathbin{\varovee}\mho)$

defines _multiformulas_ , where $\sigma:\varphi$ is a labeled formula.
$\mathit{Lab}(\mho)$ denotes the set of labels of $\mho$. An _interpretation
$\mathcal{I}$_ of a layered sequent $\cal G$ into a model $\mathcal{M}$ is
called an _interpretation of a multiformula $\mho$ into $\mathcal{M}$_ iff
$\mathit{Lab}(\mho)\subseteq\mathit{Lab}(\mathcal{G})$. If $\mathcal{I}$ is an
interpretation of $\mho$ into $\mathcal{M}$, we define
$\mathcal{M},\mathcal{I}\vDash\mho$ as follows:
compactenum  $\mathcal{M},\mathcal{I}\vDash\sigma:\varphi$ iff
$\mathcal{M},\mathcal{I}(\sigma)\vDash\varphi$,
$\mathcal{M},\mathcal{I}\vDash\mho_{1}\mathbin{\varowedge}\mho_{2}$ iff
$\mathcal{M},\mathcal{I}\vDash\mho_{1}$ and
$\mathcal{M},\mathcal{I}\vDash\mho_{2}$,
$\mathcal{M},\mathcal{I}\vDash\mho_{1}\mathbin{\varovee}\mho_{2}$ iff
$\mathcal{M},\mathcal{I}\vDash\mho_{i}$ for at least one $i=1,2$.
Multiformulas $\mho_{1}$ and $\mho_{2}$ are said to be _equivalent_ , denoted
$\mho_{1}\equiv_{\sf 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
${\sf L}$-model $\mathcal{M}$.

######  Lemma 1 ([20])

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

######  Definition 9 (Bisimilarity)

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

literalsℓ.

if $wZw^{\prime}$, then $a)$ $\mathcal{M},w\vDash q$ iff
$\mathcal{M}^{\prime},w^{\prime}\vDash q$ for all atoms
$q\notin\\{\ell,\overline{\ell}\\}$ and
$b)$ if $\mathcal{M}^{\prime},w^{\prime}\vDash\ell$, then
$\mathcal{M},w\vDash\ell$;

forth.

if $wZw^{\prime}$ and $wRv$, then there exists $v^{\prime}\in W^{\prime}$ such
that $vZv^{\prime}$ and $w^{\prime}R^{\prime}v^{\prime}$;

back.

if $wZw^{\prime}$ and $w^{\prime}R^{\prime}v^{\prime}$, then there exists
$v\in W$ such that $vZv^{\prime}$ and $wRv$.

$\mathcal{M}$ and $\mathcal{M}^{\prime}$ are _bisimilar_ , denoted
$\mathcal{M}\sim\mathcal{M}^{\prime}$, iff there is a relation
$Z\neq\varnothing$ satisfying forth and back, as well as part $a)$ of
literalsℓ for any $p\in{\sf Pr}$, in which case $Z$ is called a
_bisimulation_. We write $($similarly for $\sim$ instead of $\leq_{\ell})$:

  * •

$(\mathcal{M}^{\prime},w^{\prime})\leq_{\ell}(\mathcal{M},w)$ iff there is an
$\ell$-bisimulation $Z$, such that $wZw^{\prime}$;

  * •

$(\mathcal{M}^{\prime},\mathcal{I}^{\prime})\leq_{\ell}(\mathcal{M},\mathcal{I})$
for functions $\mathcal{I}:X\to W$ and $\mathcal{I}^{\prime}:X\to W^{\prime}$
iff there is an $\ell$-bisimulation $Z$ such that
$\mathcal{I}(\sigma)\,Z\,\mathcal{I}^{\prime}(\sigma)$ for each $\sigma\in X$.

Note that $\leq_{\ell}$ is a preorder and we have
$\mathcal{M}^{\prime}\leq_{\ell}\mathcal{M}$ iff
$\mathcal{M}\leq_{\overline{\ell}}\mathcal{M}^{\prime}$. By analogy with [6,
Theorem 2.20], we have the following immediate observation, which additionally
holds for multiformulas $\mho$ (see the Appendix for a proof):

######  Lemma 2 ()

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

  1. 1.

Let $\ell\notin{\sf Lit}(\mathcal{G})$. If
$(\mathcal{M}^{\prime},\mathcal{I}^{\prime})\leq_{\ell}(\mathcal{M},\mathcal{I})$,
then $\mathcal{M},\mathcal{I}\vDash\mathcal{G}$ implies
$\mathcal{M}^{\prime},\mathcal{I}^{\prime}\vDash\mathcal{G}$.

  2. 2.

If $(\mathcal{M},\mathcal{I})\sim(\mathcal{M}^{\prime},\mathcal{I}^{\prime})$,
then $\mathcal{M},\mathcal{I}\vDash\mathcal{G}$ iff
$\mathcal{M}^{\prime},\mathcal{I}^{\prime}\vDash\mathcal{G}$.

######  Definition 10 (BLUIP)

Logic ${\sf L}$ is said to have the _bisimulation layered-sequent uniform
interpolation property (BLUIP)_ iff for every literal $\ell$ and every ${\sf
L}$-sequent $\mathcal{G}$, there is a multiformula $A_{\ell}(\mathcal{G})$,
called _BLU interpolant_ , such that:

  1. (i)

${\sf Lit}\bigl{(}A_{\ell}(\cal G)\bigr{)}\subseteq{\sf Lit}(\cal
G)\setminus$$\\{\ell\\}$ and $\mathit{Lab}\bigl{(}A_{\ell}(\cal
G)\bigr{)}\subseteq\mathit{Lab}(\cal G)$;

  2. (ii)

for each interpretation $\mathcal{I}$ of $\cal G$ into an ${\sf L}$-model
$\mathcal{M}$,

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

  3. (iii)

for each ${\sf L}$-model $\mathcal{M}$ and interpretation $\mathcal{I}$ of
$\cal G$ into $\mathcal{M}$, if $\mathcal{M},\mathcal{I}\nvDash A_{\ell}(\cal
G)$, then there is an ${\sf L}$-model $\mathcal{M}^{\prime}$ and
interpretation $\mathcal{I}^{\prime}$ of $\cal G$ into $\mathcal{M}^{\prime}$
such that

$(\mathcal{M}^{\prime},\mathcal{I}^{\prime})\leq_{\ell}(\mathcal{M},\mathcal{I})\;\text{and}\;\mathcal{M}^{\prime},\mathcal{I}^{\prime}\nvDash\cal
G.$

###### Lemma 3

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

###### Proof

Let $\forall\ell\varphi=A_{\ell}(\varphi)$. We prove the properties of Def. 3.
Variable property is immediate. For Property (ii), assume $\nvdash_{\sf
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 ${\sf L}$-model $\mathcal{M}$ with
root $\rho$. As $\rho$ is the root, it can be considered as an interpretation
by Def. 6. By condition (ii) from Def. 10 we get a contradiction. For (iii),
let $\psi$ be a formula such that $\ell\notin{\sf Lit}(\psi)$ and suppose
$\nvdash_{\sf L}\psi\rightarrow A_{\ell}(\varphi)$. So there is an ${\sf
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 Def. 10,
there is an ${\sf L}$-model $\mathcal{M}^{\prime}$ with root $\rho^{\prime}$
such that $(\mathcal{M}^{\prime},\rho^{\prime})\leq_{\ell}(\mathcal{M},\rho)$
and $\mathcal{M}^{\prime},\rho^{\prime}\nvDash\varphi$. By Lemma 2,
$\mathcal{M}^{\prime},\rho^{\prime}\vDash\psi$, hence $\nvdash_{\sf
L}\psi\rightarrow\varphi$ as desired.∎

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

######  Definition 11 (Copying)

Let $\mathcal{M}=(W,R,V)$ be a ${\sf K5}$-model with root $\rho$ and cluster
$C$. Model $\mathcal{N}^{\prime}=(W\sqcup\\{w_{c}\\},R^{\prime},V^{\prime})$
is obtained by _copying $w\in C$_ iff $R^{\prime}=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^{\prime}(p)=V(p)\sqcup\\{w_{c}\mid w\in
V(p)\\}$ for any $p\in{\sf Pr}$. Model
$\mathcal{N}^{\prime\prime}=(W\sqcup\\{w_{c}\\},R^{\prime\prime},V^{\prime})$
is obtained by _copying $w$ away from the root_ iff
$R^{\prime\prime}=R^{\prime}\setminus\\{(\rho,w_{c})\\}$.

###### Lemma 4

Let model $\mathcal{N}$ be obtained by copying a world $w$ from a ${\sf
K5}$-model $\mathcal{M}$ (away from the root). Let $\mathcal{I}\colon
X\to\mathcal{M}$ and $\mathcal{I}^{\prime}\colon X\to\mathcal{N}$ be
interpretations such that for each $x\in X$, either
$\mathcal{I}(x)=\mathcal{I}^{\prime}(x)$ or $\mathcal{I}(x)=w$ while
$\mathcal{I}^{\prime}(x)=w_{c}$. Then, $\mathcal{N}$ is a ${\sf K5}$-model and
$(\mathcal{M},\mathcal{I})\sim(\mathcal{N},\mathcal{I}^{\prime})$.

In the construction of interpolants, we use the following rules ${\sf
d}_{t}^{\prime}$ and ${\sf dd}$ and sets $\mathcal{G}_{c}$ and
$\Box\Diamond\mathcal{G}_{c}$ of formulas from the crown of $\mathcal{G}$:

$\mathcal{G}_{c}=\\{\varphi\mid\sigma:\varphi\in\mathcal{G},\sigma\neq\bullet\\}\qquad\Box\Diamond\mathcal{G}_{c}=\\{\Box\varphi\mid\Box\varphi\in\mathcal{G}_{c}\\}\sqcup\\{\Diamond\varphi\mid\Diamond\varphi\in\mathcal{G}_{c}\\}$

$\Gamma,\bigl{[}\\{\psi\mid\Diamond\psi\in\Gamma\\}\bigr{]}$$\Gamma,\Diamond\top$
$\scriptstyle{\sf d}_{t}^{\prime}\;$ $\Gamma$ and
$\mathcal{G},\bigl{[}\\{\psi\mid\Diamond\psi\in\mathcal{G}\\}\bigr{]},\bigl{[}\bigl{[}\\{\chi\mid\Diamond\chi\in\mathcal{G}_{c}\\}\bigr{]}\bigr{]}$
$\scriptstyle{\sf dd}\;$ $\mathcal{G}$

Rule ${\sf d}_{t}^{\prime}$ shows similarities with rule ${\sf d}_{t}$ from
logics ${\sf KD5}$ and ${\sf KD45}$, but is only applied in the absence of the
crown. Rule ${\sf d}_{t}^{\prime}$ is sound for ${\sf 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\Gamma$. The label of this crown component is always $\bullet
1$. Rule ${\sf 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 ${\sf
dd}$ using special placeholder labels $\bullet{\sf d}$ and ${\sf 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
${\sf dd}$.

|  $\mathcal{G}$ matches |  $A_{\ell}(t,\Sigma_{c};\mathcal{G})$ equals
---|---|---
1. | $\mathcal{G}^{\prime}{\\{\top\\}}_{\sigma}$ | $\sigma:\top$
2. | $\mathcal{G}^{\prime}{\\{q,\overline{q}\\}}_{\sigma}$ | $\sigma:\top$
3. | $\mathcal{G}^{\prime}{\\{\varphi\lor\psi\\}}$ | $A_{\ell}\bigl{(}t,\Sigma_{c};\mathcal{G}^{\prime}{\\{\varphi\lor\psi,\varphi,\psi\\}}\bigr{)}$
4. | $\mathcal{G}^{\prime}{\\{\varphi\land\psi\\}}$ | $A_{\ell}\bigl{(}t,\Sigma_{c};\mathcal{G}^{\prime}{\\{\varphi\land\psi,\varphi\\}}\bigr{)}\mathbin{\varowedge}A_{\ell}\bigl{(}t,\Sigma_{c};\mathcal{G}^{\prime}{\\{\varphi\land\psi,\psi\\}}\bigr{)}$
5. | $\mathcal{G}^{\prime},\Box\varphi$ | $\mathop{{{{{\varowedge}}}}}\limits_{i=1}^{h}\left(\bullet:\Box\delta_{i}\mathbin{\varovee}\mathop{{{{{\varovee}}}}}\limits_{\tau\in\mathcal{G}}\tau:\gamma_{i,\tau}\right)$
|  | where $j$ is the smallest integer such that $\bullet j\notin\mathcal{G}$ and the SCNF
|  | of $A_{\ell}\bigl{(}t,\Sigma_{c};\mathcal{G}^{\prime},\Box\varphi,[\varphi]_{\bullet j}\bigr{)}$ is $\mathop{{{{{\varowedge}}}}}\limits_{i=1}^{h}\left(\bullet j:\delta_{i}\mathbin{\varovee}\mathop{{{{{\varovee}}}}}\limits_{\tau\in\mathcal{G}}\tau:\gamma_{i,\tau}\right)$,
6. | $\mathcal{G}^{\prime},\llbracket\Sigma,\Box\varphi\rrbracket_{\sigma}$ | $\mathop{{{{{\varowedge}}}}}\limits_{i=1}^{h}\left(\sigma:\Box\delta_{i}\mathbin{\varovee}\mathop{{{{{\varovee}}}}}\limits_{\tau\in\mathcal{G}}\tau:\gamma_{i,\tau}\right)$
|  | where $j$ is the smallest integer such that $j\notin\mathcal{G}$ and the SCNF
|  | of $A_{\ell}\bigl{(}t,\Sigma_{c};\mathcal{G}^{\prime}$, $\llbracket\Sigma,\Box\varphi\rrbracket_{\sigma},[[\varphi]]_{j}\bigr{)}$ is $\mathop{{{{{\varowedge}}}}}\limits_{i=1}^{h}\left(j:\delta_{i}\mathbin{\varovee}\mathop{{{{{\varovee}}}}}\limits_{\tau\in\mathcal{G}}\tau:\gamma_{i,\tau}\right)$,
7. | $\mathcal{G}^{\prime},\Diamond\varphi,[\Sigma]$ | $A_{\ell}\bigl{(}t,\Sigma_{c};\mathcal{G}^{\prime},\Diamond\varphi,[\Sigma,\varphi]\bigr{)}$
8. | $\mathcal{G}^{\prime},\llbracket\Sigma,\Diamond\varphi\rrbracket$ | $A_{\ell}\bigl{(}t,\Sigma_{c};\mathcal{G}^{\prime},\llbracket\Sigma,\Diamond\varphi,\varphi\rrbracket\bigr{)}$
9. | $\mathcal{G}^{\prime},\llbracket\Sigma,\Diamond\varphi\rrbracket,\llparenthesis\Pi\rrparenthesis$ | $A_{\ell}\bigl{(}t,\Sigma_{c};\mathcal{G}^{\prime},\llbracket\Sigma,\Diamond\varphi\rrbracket,\llparenthesis\Pi,\varphi\rrparenthesis\bigr{)}$
Table 4: Recursive construction of $A_{\ell}(t,\Sigma_{c};\mathcal{G})$ for
$\mathcal{G}$ that are not ${\sf 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,\Sigma_{c};\mathcal{G})$ with three
parameters we present below. The main parameter is a ${\sf 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 ${\sf dd}$ has been
applied at least once for the case when $\mathcal{G}$ contains diamond
formulas; $\Sigma_{c}\subseteq\Box\Diamond\mathcal{G}_{c}$ is a set of modal
formulas that provides a bookkeeping strategy to prevent redundant
applications of rule ${\sf dd}$.

To calculate $A_{\ell}(t,\Sigma_{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. 1.

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

  2. 2.

If some formula $\varphi\lor\psi$ (resp. $\varphi\land\psi$) from
$\mathcal{G}$ is not saturated, compute $A_{\ell}(t,\Sigma_{c};\mathcal{G})$
according to row 3 (resp. 4) applied to this formula.

  3. 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,\Sigma_{c};\mathcal{G})$
according to the unique respective row among 5–9 applicable to this formula
(w.r.t. $\sigma$).

  4. 4.

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

    1. (a)

if $\mathcal{G}$ has no $\Diamond$-formulas, stop and return
$A_{\ell}(t,\Sigma_{c};\mathcal{G})={\sf LitDis}_{\ell}(\mathcal{G})$ where

${\sf
LitDis}_{\ell}(\mathcal{G})=\mathop{{{{{\varovee}}}}}\limits_{\sigma:\ell^{\prime}\in\mathcal{G},\ell^{\prime}\in{\sf
Lit}\setminus\\{\ell\\}}\sigma:\ell^{\prime}$ (2)

    2. (b)

else, if $\mathcal{G}=\Gamma$ consists of the trunk only, apply rule ${\sf
d}_{t}^{\prime}$ as follows:

$\vspace{-10pt}A_{\ell}(t,\Sigma_{c};\Gamma)=\\\
\Bigl{(}\bullet:\Box\bot\mathbin{\varovee}\mathop{{{{{\varovee}}}}}\limits_{i=1}^{h}\big{(}\bullet:\Diamond\delta_{i}\mathbin{\varowedge}\bullet:\gamma_{i}\big{)}\Bigr{)}\mathbin{\varowedge}\bigl{(}\bullet:\Diamond\top\mathbin{\varovee}{\sf
LitDis}_{\ell}(\Gamma)\bigr{)}$ (3)

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

$\mathop{{{{{\varovee}}}}}\limits_{i=1}^{h}\Bigl{(}\bullet
1:\delta_{i}\mathbin{\varowedge}\bullet:\gamma_{i}\Bigr{)}$ (4)

    3. (c)

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

    4. (d)

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

$A_{\ell}(t,\Sigma_{c};\mathcal{G})=\mathop{{{{{\varovee}}}}}\limits_{i=1}^{h}\left(\bullet:\Diamond\delta_{i}\mathbin{\varowedge}\bullet
1:\Diamond\delta^{\prime}_{i}\mathbin{\varowedge}\mathop{{{{{\varowedge}}}}}\limits_{\tau\in\mathcal{G}}\tau:\gamma_{i,\tau}\right)$
(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{\sf
d}},\>\bigl{[}\bigl{[}\\{\chi\mid\Diamond\chi\in\mathcal{G}_{c}\\}\bigr{]}\bigr{]}_{{\sf
d}}\Bigr{)}$ is

$\mathop{{{{{\varovee}}}}}\limits_{i=1}^{h}\left(\bullet{\sf
d}:\delta_{i}\mathbin{\varowedge}{\sf
d}:\delta^{\prime}_{i}\mathbin{\varowedge}\mathop{{{{{\varowedge}}}}}\limits_{\tau\in\mathcal{G}}\tau:\gamma_{i,\tau}\right)$
(6)

The computation of the algorithm can be seen as a proof search tree (extended
with rules ${\sf d}_{t}^{\prime}$ and ${\sf dd}$). In this proof search, call
$A_{\ell}(t,\Sigma_{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,\Sigma_{c};\mathcal{H})$. In this case,
$A_{\ell}(1,\Sigma_{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 2

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,\Sigma_{c})$ to the left of each line,
according to the algorithm, using the following abbreviations
$\Gamma=\varphi,\overline{p},\Diamond\Diamond(p\vee q)$ and
$\Sigma_{1}=\Diamond(p\vee q),p\vee q,p,q$:

$(1,\\{\Diamond(p\vee q)\\})\ \ \ {\Gamma,[\Sigma_{1}]_{\bullet
1},[\Diamond(p\vee q),p\vee q,p,q]_{\bullet{\sf d}},[[p\vee q,p,q]]_{{\sf
d}}}$ $\vee$ $(1,\\{\Diamond(p\vee q)\\})\ \ \ \Gamma,[\Sigma_{1}]_{\bullet
1},[\Diamond(p\vee q),p\vee q]_{\bullet{\sf d}},[[p\vee q]]_{{\sf d}}$ ${\sf
dd}$ $(0,\varnothing)\ \ \ \Gamma,[\Diamond(p\vee q),p\vee q,p,q]_{\bullet 1}$
$\vee$ $(0,\varnothing)\ \ \ \Gamma,[\Diamond(p\vee q),p\vee q]_{\bullet 1}$
${\sf t}$ $(0,\varnothing)\ \ \ \Gamma,[\Diamond(p\vee q)]_{\bullet 1}$
$\Gamma,\Diamond\top$ ${\sf d}_{t}^{\prime}$ $(0,\varnothing)\ \ \
\varphi,\overline{p},\Diamond\Diamond(p\vee q)$ $\vee$ $(0,\varnothing)\ \ \
\overline{p}\vee\Diamond\Diamond(p\vee 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{\sf
d}},[[p\vee q,p,q]]_{{\sf 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)\\}=\Sigma_{c}$. Hence, by Step 4c,

$A_{p}(1,\\{\Diamond(p\vee
q)\\};\mathcal{H})\quad=\quad\bullet:\overline{p}\,\mathbin{\varovee}\,\bullet
1:q\,\mathbin{\varovee}\,\bullet{\sf d}:q\,\mathbin{\varovee}\ {\sf d}:q.$ (7)

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

$\Bigl{(}\bullet:\overline{p}\mathbin{\varowedge}\mathop{{{{{\varowedge}}}}}\limits_{\sigma\in\\{\bullet
1,\bullet{\sf d},{\sf
d}\\}}\sigma:\top\Bigr{)}\mathbin{\varovee}\mathop{{{{{\varovee}}}}}\limits_{\tau\in\\{\bullet
1,\bullet{\sf d},{\sf
d}\\}}\Bigl{(}\tau:q\mathbin{\varowedge}\mathop{{{{{\varowedge}}}}}\limits_{\sigma\in\\{\bullet,\bullet
1,\bullet{\sf d},{\sf d}\\}\setminus\\{\tau\\}}\sigma:\top\Bigr{)}.$

Now, by Step 4d, and converting into a new SDNF, we get
$A_{p}(0,\varnothing;\Gamma,[\Sigma_{1}]_{\bullet 1})\equiv{}$

$\displaystyle\big{(}\bullet:(\overline{p}\wedge\Diamond\top)\mathbin{\varowedge}\bullet
1:(\top\wedge\Diamond\top)\big{)}\mathbin{\varovee}\big{(}\bullet:(\top\wedge\Diamond\top)\mathbin{\varowedge}\bullet
1:(q\wedge\Diamond\top)\big{)}\mathbin{\varovee}$
$\displaystyle\big{(}\bullet:(\top\wedge\Diamond q)\mathbin{\varowedge}\bullet
1:(\top\wedge\Diamond\top)\big{)}\mathbin{\varovee}\big{(}\bullet:(\top\wedge\Diamond\top)\mathbin{\varowedge}\bullet
1:(\top\wedge\Diamond q)\big{)}\hbox
to0.0pt{.\hss}\phantom{\mathbin{\varovee}}$

Further applications of $\vee$ and ${\sf t}$ keep this interpolant intact.
Note that the application of ${\sf d}^{\prime}_{t}$ does not require to
continue proof search for the right branch. Instead, Step 4b prescribes that
$A_{p}(0,\varnothing;\varphi,\overline{p},\Diamond\Diamond(p\vee
q))\equiv\bigl{(}\bullet:\overline{p}\mathbin{\varovee}\bullet:\Diamond\top\bigr{)}\mathbin{\varowedge}$

$\displaystyle\Bigl{(}\big{(}\bullet:(\overline{p}\wedge\Diamond\top\wedge\Diamond(\top\wedge\Diamond\top))\big{)}\mathbin{\varovee}\big{(}\bullet:(\top\wedge\Diamond\top\wedge\Diamond(q\wedge\Diamond\top))\big{)}\mathbin{\varovee}\phantom{\bullet:\Box\bot\Bigr{)}}$
$\displaystyle\phantom{\Bigl{(}}\big{(}\bullet:(\top\wedge\Diamond
q\wedge\Diamond(\top\wedge\Diamond\top))\big{)}\mathbin{\varovee}\big{(}\bullet:(\top\wedge\Diamond\top\wedge\Diamond(\top\wedge\Diamond
q))\big{)}\mathbin{\varovee}\bullet:\Box\bot\Bigr{)}\hbox to0.0pt{.\hss}$

Simplifying, we finally obtain

$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).$ (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 Def.
10. 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 ${\sf K5}$-model
$\mathcal{M}=(W,R,V)$, then, by Defs. 8 and 6,
$\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}^{\prime},\mathcal{I})\leq_{\ell}(\mathcal{M},\mathcal{I})$ for
$\mathcal{M}^{\prime}=(W,R,V^{\prime})$ with $V^{\prime}(p)=\\{\rho\\}$ and
$V^{\prime}(r)=V(r)$ for $r\neq p$ since $\mathbf{literals}_{p}$ allows to
turn $p$ from true to false. It is easy to see that
$\mathcal{M}^{\prime},\rho\nvDash\overline{p}\vee\Diamond\Diamond(p\vee q)$.
Thus, $\mathcal{M}^{\prime},\mathcal{I}\nvDash\bullet:\varphi$.

The following properties of the algorithm are proved in the Appendix.

######  Lemma 5 ()

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

  1. 1.

The algorithm is terminating.

  2. 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. 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},[\Theta]_{\bullet{\sf
d}},[[\Phi]]_{{\sf d}})$ of one of the following types:

    1. (a)

sufficient and final when calculated via Step 1;

    2. (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;

    3. (c)

insufficient and saturated when calculated via Step 4c.

######  Theorem 4.1 ()

Logic ${\sf 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,\Sigma_{c};\mathcal{G})$ in the proof search returns a BLU
interpolant for a ${\sf 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, relegating most to the Appendix
and omitting simple ones, e.g., BLUIP(i), altogether.

BLUIP(ii)

We show that $\mathcal{M},\mathcal{I}\vDash
A_{\ell}(t,\Sigma_{c};\mathcal{G})$ implies
$\mathcal{M},\mathcal{I}\vDash\mathcal{G}$ for any interpretation
$\mathcal{I}$ of $\mathcal{G}$ into any ${\sf 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}^{\prime},\Box\varphi$ and
$\mathcal{M},\mathcal{I}\vDash
A_{\ell}(t,\Sigma_{c};\mathcal{G}^{\prime},\Box\varphi)$ for

$A_{\ell}(t,\Sigma_{c};\quad\mathcal{G}^{\prime},\Box\varphi)\quad=\quad\mathop{{{{{\varowedge}}}}}\limits_{i=1}^{h}\left(\bullet:\Box\delta_{i}\mathbin{\varovee}\mathop{{{{{\varovee}}}}}\limits_{\tau\in\mathcal{G}}\tau:\gamma_{i,\tau}\right),$
(9)

i.e., for each $1\leq i\leq 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 Rv$ 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}^{\prime},\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\leq i\leq
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,\Sigma_{c};\mathcal{G}^{\prime},\Box\varphi,[\varphi]_{\bullet
j}\bigr{)}$ for

$A_{\ell}\bigl{(}t,\Sigma_{c};\quad\mathcal{G}^{\prime},\Box\varphi,[\varphi]_{\bullet
j}\bigr{)}\quad\equiv\quad\mathop{{{{{\varowedge}}}}}\limits_{i=1}^{h}\left(\bullet
j:\delta_{i}\mathbin{\varovee}\mathop{{{{{\varovee}}}}}\limits_{\tau\in\mathcal{G}}\tau:\gamma_{i,\tau}\right).$
(10)

By IH,
$\mathcal{M},\mathcal{I}_{v}\vDash\mathcal{G}^{\prime},\Box\varphi,[\varphi]_{\bullet
j}$ whenever $\rho Rv$. 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
Rv$. For it, $\mathcal{M},\mathcal{I}_{v}\vDash\mathcal{G}^{\prime}$, 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,\Sigma_{c};\mathcal{G})$ for
$A_{\ell}(t,\Sigma_{c};\mathcal{G})$ from (5), i.e., for some $1\leq i\leq h$
we have $\mathcal{M},\rho\vDash\Diamond\delta_{i}$, and
$\mathcal{M},\mathcal{I}(\bullet 1)\vDash\Diamond\delta^{\prime}_{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^{\prime}_{i}$ for some
$\mathcal{I}(\bullet 1)Ru$. Let $\mathcal{M}^{\prime}$ be obtained by copying
$u$ into $u^{\prime}$ away from the root in $\mathcal{M}$ and let
$\mathcal{J}=\mathcal{I}\sqcup\\{(\bullet{\sf d},v),({\sf d},u^{\prime})\\}$
be a well-defined interpretation. $\mathcal{M}^{\prime},\mathcal{J}\vDash
A_{\ell}(1,\Box\Diamond\mathcal{G}_{c};\mathcal{G},[\\{\psi\mid\Diamond\psi\in\mathcal{G}\\}]_{\bullet{\sf
d}},[[\\{\chi\mid\Diamond\chi\in\mathcal{G}_{c}\\}]]_{{\sf d}})$, as (6) is
true for $\mathcal{M}^{\prime}$ and $\mathcal{J}$. By IH,
$\mathcal{M}^{\prime},\mathcal{J}\vDash\mathcal{G},[\\{\psi\mid\Diamond\psi\in\mathcal{G}\\}]_{\bullet{\sf
d}},[[\\{\chi\mid\Diamond\chi\in\mathcal{G}_{c}\\}]]_{{\sf d}}$. If
$\mathcal{M}^{\prime},v\vDash\psi$ for some $\Diamond\psi\in\mathcal{G}$ or
$\mathcal{M}^{\prime},u^{\prime}\vDash\chi$ for some
$\Diamond\chi\in\mathcal{G}_{c}$, then
$\mathcal{M}^{\prime},\mathcal{J}\vDash\mathcal{G}$ because of $\Diamond\psi$
or $\Diamond\chi$ respectively. Otherwise, also
$\mathcal{M}^{\prime},\mathcal{J}\vDash\mathcal{G}$. Since we have
$(\mathcal{M},\mathcal{I})\sim(\mathcal{M}^{\prime},\mathcal{J})$ by Lemma 4,
we have $\mathcal{M},\mathcal{I}\vDash\mathcal{G}$ by Lemma 2(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,\Sigma_{c};\mathcal{G})$, then
$\mathcal{M}^{\prime},\mathcal{J}^{\prime}\nvDash\mathcal{G}$ for some
interpretation $\mathcal{J}^{\prime}$ of $\mathcal{G}$ into another ${\sf
K5}$-model $\mathcal{M}^{\prime}$ such that
$(\mathcal{M}^{\prime},\mathcal{J}^{\prime})\leq_{\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 5.
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,\Sigma_{c};\mathcal{G})$ for
$A_{\ell}(t,\Sigma_{c};\mathcal{G})$ from (5).

We first modify $\mathcal{M}$ and $\mathcal{I}$ to obtain an injective
interpretation $\mathcal{I}^{\prime}$ into a ${\sf K5}$-model
$\mathcal{N}^{\prime}=(W^{\prime},R^{\prime},V^{\prime})$ such that
$W^{\prime}\setminus\mathit{Range}(\mathcal{I}^{\prime})$ is not empty and
partitioned into pairs $(v,u)$ with $\mathcal{I}^{\prime}(\bullet)Rv$ and not
$\mathcal{I}^{\prime}(\bullet)Ru$. To this end we employ copying as per Def.
11, 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. 1.

If $\mathcal{I}_{i}(\tau_{1})=\mathcal{I}_{i}(\tau_{2})$ for
$\tau_{1}\neq\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. 2.

If $\mathcal{I}_{K-1}$ is injective but
$W_{K-1}\setminus\mathit{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\mathit{Range}(\mathcal{I}_{K})\neq\varnothing$.

  3. 3.

Finally, define the two sets $Y=\\{y\in
W_{K}\setminus\mathit{Range}(\mathcal{I}_{K})\mid\mathcal{I}_{K}(\bullet)R_{K}y\\}$
and $Z=\\{z\in W_{K}\setminus\mathit{Range}(\mathcal{I}_{K})\mid\text{not
}\mathcal{I}_{K}(\bullet)R_{K}z\\}$ and obtain $\mathcal{N}^{\prime}$ 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}^{\prime}=\mathcal{I}_{K}$ is an injective interpretation of
$\mathcal{G}$ into $\mathcal{N}^{\prime}$.

Note that $W^{\prime}\setminus\mathit{Range}(\mathcal{I}^{\prime})=Y\sqcup
Z\sqcup\\{y_{2}\mid y\in Y\\}\sqcup\\{z_{1}\mid z\in Z\\}\neq\varnothing$.
Further, $\mathcal{I}^{\prime}(\bullet)R^{\prime}y$ for all $y\in Y$, and not
$\mathcal{I}^{\prime}(\bullet)R^{\prime}y_{2}$ for all $y\in Y$, and
$\mathcal{I}^{\prime}(\bullet)R^{\prime}z_{1}$ for all $z\in Z$, and not
$\mathcal{I}^{\prime}(\bullet)R^{\prime}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\\}\neq\varnothing$ of the non-empty
$W^{\prime}\setminus\mathit{Range}(\mathcal{I}^{\prime})$.

It is clear that
$(\mathcal{N}^{\prime},\mathcal{I}^{\prime})\sim(\mathcal{M},\mathcal{I})$. So
$\mathcal{N}^{\prime},\mathcal{I}^{\prime}\nvDash
A_{\ell}(t,\Sigma_{c};\mathcal{G})$ by Lemma 2, i.e., for each $1\leq i\leq h$
we have $\mathcal{N}^{\prime},\rho\nvDash\Diamond\delta_{i}$ for
$\rho=\mathcal{I}^{\prime}(\bullet)$, or
$\mathcal{N}^{\prime},\mathcal{I}^{\prime}(\bullet
1)\nvDash\Diamond\delta^{\prime}_{i}$, or
$\mathcal{N}^{\prime},\mathcal{I}^{\prime}(\tau)\nvDash\gamma_{i,\tau}$ for
some $\tau\in\mathcal{G}$. Thus, for any $(v,u)\in P$ and each $1\leq i\leq
h$, we have $\mathcal{N}^{\prime},v\nvDash\delta_{i}$, or
$\mathcal{N}^{\prime},u\nvDash\delta^{\prime}_{i}$, or
$\mathcal{N}^{\prime},\mathcal{I}^{\prime}(\tau)\nvDash\gamma_{i,\tau}$ for
some $\tau\in\mathcal{G}$. Hence, (6) is false under injective interpretation
$\mathcal{J}_{v,u}=\mathcal{I}^{\prime}\sqcup\\{(\bullet{\sf d},v),({\sf
d},u)\\}$ into $\mathcal{N}^{\prime}$, i.e., abbreviating
$\Theta=\\{\psi\mid\Diamond\psi\in\mathcal{G}\\}$ and
$\Phi=\\{\chi\mid\Diamond\chi\in\mathcal{G}_{c}\\}$, we get
$\mathcal{N}^{\prime},\mathcal{J}_{v,u}\nvDash
A_{\ell}(1,\Box\Diamond\mathcal{G}_{c};\mathcal{G},[\Theta]_{\bullet{\sf
d}},[[\Phi]]_{{\sf 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 5(3) is
that every branch going up from (6) leads to a call of the form

$A_{\ell}(1,\Box\Diamond\mathcal{G}_{c};\quad\mathcal{G},[\Theta_{j}]_{\bullet{\sf
d}},[[\Phi_{j}]]_{{\sf d}}),$ (11)

where $\Theta_{j}\supseteq\Theta$ and $\Phi_{j}\supseteq\Phi$, that returns
multiformula $\mho_{j}$ and is either sufficient or insufficient but
saturated. Let $\Xi$ 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.,
$A_{\ell}(1,\Box\Diamond\mathcal{G}_{c};\mathcal{G},[\Theta]_{\bullet{\sf
d}},[[\Phi]]_{{\sf
d}})\equiv\mathop{{{{{\varowedge}}}}}\limits\nolimits_{\mho_{j}\in\Xi}\mho_{j}$.
Collecting all this together, we conclude that for each pair $(v,u)\in P$
there is some $\mho_{v,u}\in\Xi$ such that

$\mathcal{N}^{\prime},\mathcal{J}_{v,u}\nvDash\mho_{v,u}.$ (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},[\Theta_{v,u}]_{\bullet{\sf
d}},[[\Phi_{v,u}]]_{{\sf d}})$ satisfying (12). By IH for this $\mho_{v,u}$
there is an interpretation $\mathcal{J}_{0}^{\prime}$ into a ${\sf K5}$-model
$\mathcal{M}^{\prime}$ such that
$(\mathcal{M}^{\prime},\mathcal{J}_{0}^{\prime})\leq_{\ell}(\mathcal{N}^{\prime},\mathcal{J}_{v,u})$
and
$\mathcal{M}^{\prime},\mathcal{J}_{0}^{\prime}\nvDash\mathcal{G},[\Theta_{v,u}]_{\bullet{\sf
d}},[[\Phi_{v,u}]]_{{\sf d}}$. Thus,
$\mathcal{M}^{\prime},\mathcal{J}^{\prime}\nvDash\mathcal{G}$ for
$\mathcal{J}^{\prime}=\mathcal{J}_{0}^{\prime}\\!\upharpoonright\\!\mathit{Lab}(\mathcal{G})$.
Finally, by restricting to labels of $\mathcal{G}$, we can see that

$(\mathcal{M}^{\prime},\mathcal{J}^{\prime})\quad\leq_{\ell}\quad(\mathcal{N}^{\prime},\mathcal{I}^{\prime})\quad\sim\quad(\mathcal{M},\mathcal{I}).$
(13)

Otherwise, (12) does not hold for any pair $(v,u)\in P$ and any sufficient
$\mho_{v,u}\in\Xi$. In this case,
$\mathcal{N}^{\prime},\mathcal{J}_{v,u}\nvDash\mathop{{{{{\varowedge}}}}}\limits\nolimits_{\mho_{j}\in\Xi}\mho_{j}$
guarantees the existence of an insufficient $\mho_{v,u}\in\Xi$ 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}^{\prime}$
and $\mathcal{J}^{\prime}$ directly by changing $\ell$ from true to false if
needed based on $\mathcal{G}$ within $\mathit{Range}(\mathcal{I}^{\prime})$
and based on $\mho_{v,u}$’s outside of this range. Thanks to
$\mathcal{I}^{\prime}$ 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
$\mathit{Range}(\mathcal{I}^{\prime})$. Let
$\mathcal{M}^{\prime}=(W^{\prime},R^{\prime},U^{\prime})$ be
$\mathcal{N}^{\prime}$ with $V^{\prime}$ changed into $U^{\prime}$. We define
${V^{\prime}}\mathord{\downarrow}_{\ell}{T}$ as the valuation that makes
$\ell$ false in all worlds from $T\subseteq W^{\prime}$, i.e.,
$({V^{\prime}}\mathord{\downarrow}_{\ell}{T})(q)=V^{\prime}(q)$ for all
$q\notin\\{\ell,\overline{\ell}\\}$, while

$({V^{\prime}}\mathord{\downarrow}_{\ell}{T})(p)=\begin{cases}V^{\prime}(p)\setminus
T&\text{if $\ell=p$},\\\ V^{\prime}(p)\cup T&\text{if
$\ell=\overline{p}$}\end{cases}$

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

$T_{\mathcal{G}}=\\{\mathcal{I}^{\prime}(\sigma)\mid\sigma:\ell\in\mathcal{G}\\}\sqcup\\{v\mid(v,u)\in
P\text{ and }\bullet{\sf d}:\ell\in\mho_{v,u}\\}\sqcup\\\ \\{u\mid(v,u)\in
P\text{ and }{\sf d}:\ell\in\mho_{v,u}\\}.$ (14)

Finally, $\mathcal{J}^{\prime}=\mathcal{I}^{\prime}$. It is clear that (13)
holds for these $\mathcal{M}^{\prime}$ and $\mathcal{J}^{\prime}$.

It remains to show that
$\mathcal{M}^{\prime},\mathcal{J}^{\prime}\nvDash\mathcal{G}$. This is done by
mutual induction on the construction of formula $\varphi$ for the following
three induction statements

$\displaystyle\sigma:\varphi\in\mathcal{G}$
$\displaystyle\Longrightarrow\mathcal{M}^{\prime},\mathcal{I}^{\prime}(\sigma)\nvDash\varphi,$
(15) $\displaystyle\bullet{\sf d}:\varphi\in\mho_{v,u}$
$\displaystyle\Longrightarrow\mathcal{M}^{\prime},v\nvDash\varphi,$ (16)
$\displaystyle{\sf d}:\varphi\in\mho_{v,u}$
$\displaystyle\Longrightarrow\mathcal{M}^{\prime},u\nvDash\varphi.$ (17)

Case $\varphi=\ell^{\prime}\in{\sf Lit}\setminus\\{\ell,\overline{\ell}\\}$.

By Lemma 5(3), all $\mho_{v,u}$ are computed by Step 4c due to their
insufficiency, i.e., $\mho_{v,u}={\sf
LitDis}_{\ell}(\mathcal{G},[\Theta_{v,u}]_{\bullet{\sf
d}},[[\Phi_{v,u}]]_{{\sf d}})$. (16) and (17) follow from (12) and (2) because
$\mathcal{M}^{\prime}$ agrees with $\mathcal{N}^{\prime}$ on
$\ell^{\prime}\notin\\{\ell,\overline{\ell}\\}$. Similarly, since
$\mathcal{J}_{v,u}$ agrees with $\mathcal{J}^{\prime}=\mathcal{I}^{\prime}$ on
$\mathit{Lab}(\mathcal{G})$, (15) follows by using $\mho_{v,u}$ for any
$(v,u)\in P\neq\varnothing$.

Case $\varphi=\overline{\ell}$

is analogous to the previous one. The only difference is the reason why
$\mathcal{M}^{\prime}$ agrees with $\mathcal{N}^{\prime}$ 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}^{\prime}(\sigma)\notin T_{\mathcal{G}}$ by
the injectivity of $\mathcal{I}^{\prime}$, and $\overline{\ell}$ was not made
true in $\mathcal{I}^{\prime}(\sigma)$, ensuring (15). The argument for (16)
and (17) is similar, except $\bullet{\sf d}/{\sf 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}^{\prime}(\sigma)R^{\prime}\mathcal{I}^{\prime}(\tau)$: if
$\sigma=\bullet$, then $\tau=\bullet j$ for some $j$, while if
$\sigma\neq\bullet$, then $\tau\neq\bullet$. By IH(15),
$\mathcal{M}^{\prime},\mathcal{I}^{\prime}(\tau)\nvDash\xi$, and
$\mathcal{M}^{\prime},\mathcal{I}^{\prime}(\sigma)\nvDash\Box\xi$.

If $\bullet{\sf d}/{\sf 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\neq\bullet$ such that $\tau:\xi\in\mathcal{G}$. Since $v$, $u$, and
$\mathcal{I}^{\prime}(\tau)$ are all in the cluster $C$ of
$\mathcal{M}^{\prime}$, we have $vR^{\prime}\mathcal{I}^{\prime}(\tau)$ and
$uR^{\prime}\mathcal{I}^{\prime}(\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}^{\prime}(\bullet)=\rho$ is the root, $\rho R^{\prime}w$ implies
either $w=\mathcal{I}^{\prime}(\bullet j)$ for some $j$ or
$w\notin\mathit{Range}(\mathcal{I}^{\prime})$. In the former case, $\bullet
j:\xi\in\mathcal{G}$ by saturation of $\mathcal{G}$, so
$\mathcal{M}^{\prime},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},[\Theta_{w,u}]_{\bullet{\sf
d}},[[\Phi_{w,u}]]_{{\sf d}})$ that we have
$\Theta_{w,u}\supseteq\Theta=\\{\psi\mid\Diamond\psi\in\mathcal{G}\\}\ni\xi$.
Hence, $\bullet{\sf d}:\xi\in\mho_{w,u}$ and
$\mathcal{M}^{\prime},w\nvDash\xi$ by IH(16). Since
$\mathcal{M}^{\prime},w\nvDash\xi$ for all $\mathcal{I}^{\prime}(\bullet)=\rho
R^{\prime}w$, we conclude
$\mathcal{M}^{\prime},\mathcal{I}^{\prime}(\bullet)\nvDash\Diamond\xi$.

If $\sigma\neq\bullet$ and $\sigma:\Diamond\xi\in\mathcal{G}$, the argument is
similar. But additionally we may have $w=\mathcal{I}^{\prime}(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}^{\prime},w\nvDash\xi$ by IH(15).
In the latter case,
$\Phi_{v,w}\supseteq\Phi=\\{\chi\mid\Diamond\chi\in\mathcal{G}_{c}\\}\ni\xi$.
Hence, ${\sf d}:\xi\in\mho_{v,w}$ and $\mathcal{M}^{\prime},w\nvDash\xi$ by
IH(17). Since $\mathcal{M}^{\prime},w\nvDash\xi$ for all
$\mathcal{I}^{\prime}(\sigma)R^{\prime}w$, we conclude
$\mathcal{M}^{\prime},\mathcal{I}^{\prime}(\sigma)\nvDash\Diamond\xi$.

If $\bullet{\sf d}/{\sf 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}\neq\bullet$. Then $\tau:\xi\in\mathcal{G}$ for all
$\tau\neq\bullet$ by saturation of $\mathcal{G}$. Thus,
$\mathcal{M}^{\prime},\mathcal{I}^{\prime}(\tau)\nvDash\xi$ for all
$\tau\neq\bullet$ by IH(15). For each
$y\notin\mathit{Range}(\mathcal{I}^{\prime})$ such that $\rho R^{\prime}y$,
there is $x$ such that $(y,x)\in P$ and $\bullet{\sf d}:\xi\in\mho_{y,x}$
because $\Theta_{y,x}\supseteq\Theta\ni\xi$. Hence,
$\mathcal{M}^{\prime},y\nvDash\xi$ by IH(16). Finally, for each
$x\notin\mathit{Range}(\mathcal{I}^{\prime})$ such that not $\rho
R^{\prime}x$, there is $y$ such that $(y,x)\in P$ and ${\sf
d}:\xi\in\mho_{y,x}$ because $\Phi_{y,x}\supseteq\Phi\ni\xi$. Hence,
$\mathcal{M}^{\prime},x\nvDash\xi$ by IH(17). We have shown that
$\mathcal{M}^{\prime},w\nvDash\xi$ whenever $vR^{\prime}w$ ($uR^{\prime}w$).
Thus, $\mathcal{M}^{\prime},v\nvDash\Diamond\xi$ and
$\mathcal{M}^{\prime},u\nvDash\Diamond\xi$. ∎

##  5 Conclusion

We presented layered sequent calculi for several extensions of modal logic
${\sf K5}$: namely, ${\sf K5}$ itself, ${\sf KD5}$, ${\sf K45}$, ${\sf KD45}$,
${\sf KB5}$, and ${\sf 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 ${\sf K5}$ to obtain the first syntactic (and, hence, constructive) proof
of the uniform Lyndon interpolation property for ${\sf K5}$.

Due to the proof being technically involved, space considerations prevented us
from extending the syntactic proof of ULIP to ${\sf KD5}$, ${\sf K45}$, ${\sf
KD45}$, ${\sf KB5}$, and ${\sf S5}$. For ${\sf 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 ${\sf KD5}$, ${\sf
K45}$, ${\sf KD45}$, and ${\sf KB5}$, the idea is to modify the method
presented here for ${\sf K5}$ by using the layered sequent calculus for the
respective logic and making other necessary modifications, e.g., to rule ${\sf
dd}$, to fit the specific structure of the layers. We conjecture that the
proof for ${\sf K45}$, ${\sf KD45}$, and ${\sf KB5}$ would be similar to that
for ${\sf S5}$, whereas ${\sf KD5}$ would more closely resemble ${\sf K5}$.

#### Acknowledgments.

Iris van der Giessen and Raheleh Jalali are grateful for the productive and
exciting four-week research visit to the Embedded Computing Systems Group at
TU Wien. The authors thank the anonymous reviewers for their useful comments.

## References

  * [1] Akbar Tabatabai, A., Iemhoff, R., Jalali, R.: Uniform Lyndon interpolation for basic non-normal modal and conditional logics. Eprint 2208.05202, arXiv (2022). https://doi.org/10.48550/arXiv.2208.05202
  * [2] Akbar Tabatabai, A., Iemhoff, R., Jalali, R.: Uniform Lyndon interpolation for intuitionistic monotone modal logic. Eprint 2208.04607, arXiv (2022). https://doi.org/10.48550/arXiv.2208.04607
  * [3] Akbar Tabatabai, A., Jalali, R.: Universal proof theory: Semi-analytic rules and uniform interpolation. E-print 1808.06258, arXiv (2018). https://doi.org/10.48550/arXiv.1808.06258
  * [4] Avron, A.: The method of hypersequents in the proof theory of propositional non-classical logics. In: Hodges, W., Hyland, M., Steinhorn, C., Truss, J. (eds.) Logic: from foundations to Applications: European Logic Colloquium, pp. 1–32. Clarendon Press (1996)
  * [5] Bílková, M.: Interpolation in Modal Logics. Ph.D. thesis, Charles University Prague (2006), https://dspace.cuni.cz/handle/20.500.11956/15732
  * [6] Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic, Cambridge Tracts in Theoretical Computer Science, vol. 53. Cambridge University Press (2001). https://doi.org/10.1017/CBO9781107050884
  * [7] Brünnler, K.: Deep sequent systems for modal logic. Archive for Mathematical Logic 48, 551–577 (2009). https://doi.org/10.1007/s00153-009-0137-3
  * [8] Fitting, M., Kuznets, R.: Modal interpolation via nested sequents. Annals of Pure and Applied Logic 166, 274–305 (2015). https://doi.org/10.1016/j.apal.2014.11.002
  * [9] Ghilardi, S.: An algebraic theory of normal forms. Annals of Pure and Applied Logic 71, 189–245 (1995). https://doi.org/10.1016/0168-0072(93)E0084-2
  * [10] Ghilardi, S., Zawadowski, M.: Undefinability of propositional quantifiers in the modal system S4. Studia Logica 55, 259–271 (1995). https://doi.org/10.1007/BF01061237
  * [11] van der Giessen, I.: Uniform Interpolation and Admissible Rules. Proof-theoretic investigations into (intuitionistic) modal logics. Ph.D. thesis, Utrecht University (2022). https://doi.org/10.33540/1486
  * [12] van der Giessen, I., Jalali, R., Kuznets, R.: Uniform interpolation via nested sequents. In: Silva, A., Wassermann, R., de Queiroz, R. (eds.) Logic, Language, Information, and Computation: 27th International Workshop, WoLLIC 2021, Virtual Event, October 5–8, 2021, Proceedings, Lecture Notes in Computer Science, vol. 13038, pp. 337–354. Springer (2021). https://doi.org/10.1007/978-3-030-88853-4_21
  * [13] van der Giessen, I., Jalali, R., Kuznets, R.: Uniform interpolation via nested sequents and hypersequents. E-print 2105.10930, arXiv (2021). https://doi.org/10.48550/arXiv.2105.10930
  * [14] Halpern, J.Y., Rêgo, L.C.: Characterizing the NP–PSPACE gap in the satisfiability problem for modal logic. Journal of Logic and Computation 17, 795–806 (2007). https://doi.org/10.1093/logcom/exm029
  * [15] Iemhoff, R.: Uniform interpolation and the existence of sequent calculi. Annals of Pure and Applied Logic 170, 102711 (2019). https://doi.org/10.1016/j.apal.2019.05.008
  * [16] Koopmann, P.: Practical Uniform Interpolation for Expressive Description Logics. Ph.D. thesis, University of Manchester (2015), https://www.research.manchester.ac.uk/portal/files/54574261/FULL_TEXT.PDF
  * [17] Kurahashi, T.: Uniform Lyndon interpolation property in propositional modal logics. Archive for Mathematical Logic 59, 659–678 (2020). https://doi.org/10.1007/s00153-020-00713-y
  * [18] Kuznets, R.: Craig interpolation via hypersequents. In: Probst, D., Schuster, P. (eds.) Concepts of Proof in Mathematics, Philosophy, and Computer Science, Ontos Mathematical Logic, vol. 6, pp. 193–214. De Gruyter (2016). https://doi.org/10.1515/9781501502620-012
  * [19] Kuznets, R.: Proving Craig and Lyndon interpolation using labelled sequent calculi. In: Michael, L., Kakas, A. (eds.) Logics in Artificial Intelligence: 15th European Conference, JELIA 2016, Larnaca, Cyprus, November 9–11, 2016, Proceedings, pp. 320–335. Springer (2016). https://doi.org/10.1007/978-3-319-48758-8_21
  * [20] Kuznets, R.: Multicomponent proof-theoretic method for proving interpolation properties. Annals of Pure and Applied Logic 169, 1369 – 1418 (2018). https://doi.org/10.1016/j.apal.2018.08.007
  * [21] Kuznets, R., Lellmann, B.: Grafting hypersequents onto nested sequents. Logic Journal of the IGPL 24, 375–423 (2016). https://doi.org/10.1093/jigpal/jzw005
  * [22] Kuznets, R., Lellmann, B.: Interpolation for intermediate logics via hyper- and linear nested sequents. In: Advances in Modal Logic, vol. 12, pp. 473–492. College Publications (2018), http://www.aiml.net/volumes/volume12/Kuznets-Lellmann.pdf
  * [23] Kuznets, R., Lellmann, B.: Interpolation for intermediate logics via injective nested sequents. Journal of Logic and Computation 31, 797–831 (2021). https://doi.org/10.1093/logcom/exab015
  * [24] Lutz, C., Wolter, F.: Foundations for uniform interpolation and forgetting in expressive description logics. In: Walsh, T. (ed.) IJCAI-11. vol. 2, pp. 989–995. AAAI Press (2011), https://www.ijcai.org/Proceedings/11/Papers/170.pdf
  * [25] Minc, G.E.: On some calculi of modal logic. In: Orevkov, V.P. (ed.) The Calculi of Symbolic Logic. I, Proceedings of the Steklov Institute of Mathematics, vol. 98 (1968), pp. 97–124. AMS (1971)
  * [26] Nagle, M.C.: The decidability of normal K5 logics. Journal of Symbolic Logic 46, 319–328 (1981). https://doi.org/10.2307/2273624
  * [27] Nagle, M.C., Thomason, S.K.: The extensions of the modal logic K5. Journal of Symbolic Logic 50, 102–109 (1985). https://doi.org/10.2307/2273793
  * [28] Pietruszczak, A., Klonowski, M., Petrukhin, Y.: Simplified Kripke-style semantics for some normal modal logics. Studia Logica 108, 451–476 (2020). https://doi.org/10.1007/s11225-019-09849-2
  * [29] Pitts, A.M.: On an interpretation of second order quantification in first order intuitionistic propositional logic. Journal of Symbolic Logic 57, 33–52 (1992). https://doi.org/10.2307/2275175
  * [30] Pottinger, G.: Uniform, cut-free formulations of $T$, $S_{4}$, and $S_{5}$. Journal of Symbolic Logic 48, 900 (1983). https://doi.org/10.2307/2273495, abstract
  * [31] Shavrukov, V.Y.: Subalgebras of diagonalizable algebras of theories containing arithmetic, Dissertationes Mathematicae, vol. 323. Institute of Mathematics, Polish Academy of Sciences (1993), http://matwbn.icm.edu.pl/ksiazki/rm/rm323/rm32301.pdf
  * [32] Shvarts, G.F.: Gentzen style systems for K45 and K45D. In: Meyer, A.R., Taitslin, M.A. (eds.) Logic at Botik ’89: Symposium on Logical Foundations of Computer Science, Pereslavl-Zalessky, USSR, July 1989, Proceedings, Lecture Notes in Computer Science, vol. 363, pp. 245–256. Springer (1989). https://doi.org/10.1007/3-540-51237-3_20
  * [33] Takano, M.: A modified subformula property for the modal logics K5 and K5D. Bulletin of the Section of Logic 30(2), 115–122 (2001)
  * [34] Visser, A.: Uniform interpolation and layered bisimulation. In: Hájek, P. (ed.) Gödel ’96: Logical Foundations of Mathematics, Computer Science and Physics — Kurt Gödel’s Legacy, Lecture Notes in Logic, vol. 6, pp. 139–164. ASL (1996). https://doi.org/10.1017/9781316716939.010

##  Appendix 0.A Appendix

In this Appendix we provide and elaborate on the proofs that could not be
included into the main part because of space considerations.

See 3.2

###### Proof

We prove a cycle of implications: from the left statement to the middle one,
from the middle one to the right one, and, finally, from the right to the left
one. Most of the proof can be found in the main text. Here we elaborate only
on the left-to-middle implication and the argument why the constructed
countermodel is an ${\sf L}$-model due to $\mathcal{G}^{\prime}$ being
saturated in the right-to-left implication.

For the left-to-middle implication, i.e., $\vdash_{\sf
L.L}\mathcal{G}\quad\Longrightarrow\quad\vDash_{\sf L}\iota(\mathcal{G})$,
which is proved by induction on an ${\sf L.L}$-derivation of $\mathcal{G}$, we
show the case of $\Diamond_{c}$, a rule of all considered calculi. Of the many
flavors of $\Diamond_{c}$, depending on what brackets
$\llbracket\enspace\rrbracket$ and $\llparenthesis\enspace\rrparenthesis$
represent, we show the following application for ${\sf K5}$ and ${\sf KD5}$:

$\mathcal{G},[[\Sigma,\Diamond\varphi]],[\Pi,\varphi]$
$\scriptstyle\Diamond_{c}\;$ $\mathcal{G},[[\Sigma,\Diamond\varphi]],[\Pi]$

Let $\mathcal{M}$ be an ${\sf L}$-model with root $\rho$ with
$\mathcal{M},\rho\vDash\iota(\mathcal{G})\vee\Box\Box(\bigvee\Sigma\vee\Diamond\varphi)\vee\Box(\bigvee\Pi\vee\varphi)$.
If $\mathcal{M},\rho\vDash\iota(\mathcal{G})$,
$\mathcal{M},\rho\vDash\Box\Box(\bigvee\Sigma\vee\Diamond\varphi)$, or
$\mathcal{M},\rho\vDash\Box(\bigvee\Pi)$, we are done. If not, there is a $v$
such that $\rho Rv$ and $\mathcal{M},v\vDash\varphi$. By the form of the
models, indeed, $\mathcal{M},\rho\vDash\Box\Box\Diamond\varphi$, hence
$\mathcal{M},\rho\vDash\Box\Box(\bigvee\Sigma\vee\Diamond\varphi)$. Therefore,
we have $\vDash_{\sf
L}\iota(\mathcal{G})\vee\Box\Box(\bigvee\Sigma\vee\Diamond\varphi)\vee\Box(\bigvee\Pi)$.

To prove that the countermodel $\mathcal{M}$ constructed for the
contraposition of the right-to-left implication is an ${\sf L}$-model, we use
the saturation of $\mathcal{G}^{\prime}$. For example, in case of ${\sf KD5}$,
the root has a successor because of ${\sf d}_{t}$-saturation. By induction on
$\varphi$, for each $\sigma:\varphi\in\mathcal{G}^{\prime}$ we have
$\mathcal{M},\sigma\nvDash\varphi$, using the saturation of
$\mathcal{G}^{\prime}$. Taking $\mathcal{I}$ of $\mathcal{G}$ into
$\mathcal{M}$ as the identity function (or $\mathcal{I}(\bullet)=1$ in case of
${\sf KB5}$), we have $\mathcal{M},\mathcal{I}\nvDash\mathcal{G}$ as desired.
∎

See 2

###### Proof

From $\mathcal{M},\mathcal{I}\vDash\mathcal{G}$, it follows that
$\mathcal{M},\mathcal{I}(\sigma)\vDash\varphi$ for some
$\sigma:\varphi\in\mathcal{G}$. Let us examine 1, where $Z$ is the
bisimulation underlying $\leq_{\ell}$. As
$\mathcal{I}(\sigma)Z\mathcal{I}^{\prime}(\sigma)$, it is sufficient to show
by induction on $\varphi$, that $\mathcal{M},w\vDash\varphi$ implies
$\mathcal{M}^{\prime},w^{\prime}\vDash\varphi$ for every $wZw^{\prime}$. We
treat some cases. If $\varphi=\overline{\ell}$, i.e.,
$\mathcal{M},w\nvDash\ell$, it follows from part b) of literalsℓ (Def. 9) that
$\mathcal{M}^{\prime},w^{\prime}\nvDash\ell$, hence
$\mathcal{M}^{\prime},w^{\prime}\vDash\overline{\ell}$. If
$\varphi=\Diamond\psi$, there is a $v$ such that $wRv$ and
$\mathcal{M},v\vDash\psi$. By forth, there exists $v^{\prime}$ such that
$w^{\prime}Rv^{\prime}$ and $vZv^{\prime}$. So by IH,
$\mathcal{M}^{\prime},v^{\prime}\vDash\psi$ and therefore
$\mathcal{M}^{\prime},w^{\prime}\vDash\Diamond\psi$. For $\varphi=\Box\psi$,
let $w^{\prime}Rv^{\prime}$. By back, there exists $v$ such that
$vZv^{\prime}$ and $wRv$. So, $\mathcal{M},v\vDash\psi$ and by IH we have
$\mathcal{M}^{\prime},v^{\prime}\vDash\psi$ as desired.∎

See 5

###### Proof

For (1), note that Steps 1–3 are terminating by termination of the rules
modulo saturation by Theorem 3.1. In addition, the algorithm stops in Step 4a
or 4c by definition. When $A_{\ell}(t,\Sigma_{c};\mathcal{G})$ is calculated
by Step 4b, $\mathcal{G}$ must consist only of the trunk, and after that the
algorithm continues on layered sequents that contain the crown, meaning we
will never encounter Step 4b again.

In particular, to prove property (2), note that each branch going up from Step
4b will either stop in Step 1, or will be calculated in Step 4. In the latter
case, note that Steps 4a–4c do not apply resulting in Step 4d. In particular,
$t$ is set to $0$ in Step 4b and will not change in any Steps 2–3 which
excludes Step 4c.

Finally, continuing proof of (1), there is a bound on the number of
applications of Step 4d. Indeed, for each branch of the algorithm the
annotations $\Sigma_{c}\subseteq\mathcal{G}_{c}$ of the multiformulas
$A_{\ell}(t,\Sigma_{c};\mathcal{G})$ form a non-decreasing sequence of sets.
These sets grow in Step 4d, because there
$\Box\Diamond\mathcal{G}_{c}\not\subseteq\Sigma_{c}$ (otherwise Step 4c would
apply). Also, all formulas in these annotations are subformulas of the layered
sequent at the root. So, if a branch of the algorithm did not stop earlier by
Step 1, one would reach, after finitely many applications of Step 4d, a
multiformula $A_{\ell}(t,\Sigma_{c};\mathcal{G})$ for which
$\Box\Diamond\mathcal{G}_{c}\subseteq\Sigma_{c}$ that stops the algorithm in
Step 4c.

Property 3 says something more refined than we just observed. The form of
$A_{\ell}(1,\Box\Diamond\mathcal{G}_{c};\mathcal{G},[\Theta],[[\Phi]])$ is
justified by the rules in Steps 4d, 1, and 2. If it is calculated by Step 1,
then this leaf is sufficient by definition. Otherwise, applications of Steps 1
and 2 propositionally saturate the layered sequent. There are two cases.
Either,
$\Box\Diamond(\mathcal{G},[\Theta],[[\Phi]])_{c}\not\subseteq\Box\Diamond\mathcal{G}_{c}$.
Then any saturation of it will contain new modal formulas in the crown and
will trigger Step 4d, if not stopped earlier in Step 1. Hence, in this case,
$A_{\ell}(1,\Box\Diamond\mathcal{G}_{c};\mathcal{G},[\Theta],[[\Phi]])$ will
be sufficient. Or,
$\Box\Diamond(\mathcal{G},[\Theta],[[\Phi]])_{c}\subseteq\Box\Diamond\mathcal{G}_{c}$.
We will now show that it will not be saturated only propositionally, but in
fact fully saturated. Each $\sigma:\Box\varphi\in\mathcal{G}$ is saturated
because $\mathcal{G}$ is. If $\Box\varphi\in\Theta$ or $\Box\varphi\in\Phi$,
then also $\Box\varphi\in\mathcal{G}_{c}$ by assumption and so in both cases
these occurrences are saturated by the saturation of $\mathcal{G}$. For
$\sigma:\Diamond\varphi\in\mathcal{G}$, note that it is saturated for each
corresponding component in $\mathcal{G}$ by saturation and
$\Theta\supseteq\\{\psi\mid\Diamond\psi\in\mathcal{G}\\}$ and
$\Phi\supseteq\\{\chi\mid\Diamond\chi\in\mathcal{G}_{c}\\}$, making it also
saturated w.r.t. components $\Theta$ and $\Phi$ (the latter is only needed if
$\Diamond\varphi\in\mathcal{G}_{c}$). For $\Diamond\varphi\in\Theta$ and
$\Diamond\varphi\in\Phi$ the same argument applies as
$\Diamond\varphi\in\mathcal{G}_{c}$ by assumption. Now, as
$A_{\ell}(1,\Box\Diamond\mathcal{G}_{c};\mathcal{G},[\Theta],[[\Phi]])$ is
saturated and
$\Box\Diamond(\mathcal{G},[\Theta],[[\Phi]])_{c}\subseteq\Box\Diamond\mathcal{G}_{c}$,
we apply Step 4c to it which makes it insufficient. ∎

See 4.1

###### Proof

In addition to the cases provided in the proof in the main text, here we show
additional representative cases:

### BLUIP(ii), some of the cases from Steps 1–3.

row 2 of Table 4:

$\mathcal{G}=\mathcal{G}^{\prime}$${\\{q,\overline{q}\\}}_{\sigma}$. Then
either $\mathcal{M},\mathcal{I}(\sigma)\vDash q$ or
$\mathcal{M},\mathcal{I}(\sigma)\vDash\overline{q}$, hence
$\mathcal{M},\mathcal{I}\vDash\mathcal{G}$.

row 4 of Table 4:

If $\mathcal{G}=\mathcal{G}^{\prime}{\\{\varphi\land\psi\\}}_{\sigma}$, then

$\displaystyle
A_{\ell}(t,\Sigma_{c};\mathcal{G})={A_{\ell}\bigl{(}t,\Sigma_{c};\cal
G^{\prime}{\\{\varphi\land\psi,\varphi\\}}_{\sigma}\bigr{)}}\mathbin{\varowedge}{A_{\ell}\bigl{(}t,\Sigma_{c};\mathcal{G}^{\prime}{\\{\varphi\land\psi,\psi\\}}_{\sigma}\bigr{)}}.$
(18)

Since
$\mathcal{M},\mathcal{I}\vDash{A_{\ell}\bigl{(}t,\Sigma_{c};\mathcal{G}^{\prime}{\\{\varphi\land\psi,\varphi\\}}\bigr{)}}$
and
$\mathcal{M},\mathcal{I}\vDash{A_{\ell}\bigl{(}t,\Sigma_{c};\mathcal{G}^{\prime}{\\{\varphi\land\psi,\psi\\}}\bigr{)}}$,
by IH, $\mathcal{M},\mathcal{I}\vDash\cal
G^{\prime}{\\{\varphi\land\psi,\varphi\\}}$ and
$\mathcal{M},\mathcal{I}\vDash\mathcal{G}^{\prime}{\\{\varphi\land\psi,\psi\\}}$.
If $\mathcal{M},\mathcal{I}(\sigma)\vDash\varphi\land\psi$ we are done. If
not, $\mathcal{M},\mathcal{I}(\sigma)\nvDash\varphi$ or
$\mathcal{M},\mathcal{I}(\sigma)\nvDash\psi$. Therefore,
$\mathcal{M},\mathcal{I}\vDash\mathcal{G}$.

row 9 of Table 4:

Suppose
$\mathcal{G}=\mathcal{G}^{\prime},\llbracket\Sigma,\Diamond\varphi\rrbracket_{\sigma},\llparenthesis\Pi\rrparenthesis_{\tau}$.
We have

$A_{\ell}(t,\Sigma_{c};\mathcal{G})=A_{\ell}\bigl{(}t,\Sigma_{c};\mathcal{G}^{\prime},\llbracket\Sigma,\Diamond\varphi\rrbracket_{\sigma},\llparenthesis\Pi,\varphi\rrparenthesis_{\tau}\bigr{)}$

By IH,
$\mathcal{M},\mathcal{I}\vDash\mathcal{G}^{\prime},\llbracket\Sigma,\Diamond\varphi\rrbracket_{\sigma},\llparenthesis\Pi,\varphi\rrparenthesis_{\tau}$.
Note that $\mathcal{I}(\sigma)R\mathcal{I}(\tau)$ meaning that
$\mathcal{M},\mathcal{I}(\tau)\vDash\varphi$ implies
$\mathcal{M},\mathcal{I}(\sigma)\vDash\Diamond\varphi$. Hence
$\mathcal{M},\mathcal{I}\vDash\mathcal{G}$.

### BLUIP(ii), remaining cases from Step 4.

Steps 4a and 4c.

We can treat them simultaneously because both are calculated according to (2).
This case is easy as the truth of the interpolant implies that some literal in
$\mathcal{G}$ is true.

Step 4b.

Suppose $\mathcal{M},\mathcal{I}\vDash A_{\ell}(0,\Sigma_{c};\Gamma)$ for the
multiformula presented in (3)

$A_{\ell}(0,\Sigma_{c};\Gamma)=\Bigl{(}\bullet:\Box\bot\mathbin{\varovee}\mathop{{{{{\varovee}}}}}\limits_{i=1}^{h}\big{(}\bullet:\Diamond\delta_{i}\mathbin{\varowedge}\bullet:\gamma_{i}\big{)}\Bigr{)}\mathbin{\varowedge}\bigl{(}\bullet:\Diamond\top\mathbin{\varovee}{\sf
LitDis}_{\ell}(\Gamma)\bigr{)}.$ (19)

Obviously, either $\mathcal{M},\rho\nvDash\Box\bot$ or
$\mathcal{M},\rho\nvDash\Diamond\top$. In the latter case, it follows from the
right conjunct of (19) that some literal in $\Gamma$ is true, resulting in
$\mathcal{M},\mathcal{I}\vDash\Gamma$. In the former case, based on the left
conjunct of (19), there is an $1\leq i\leq h$ such that
$\mathcal{M},\rho\vDash\Diamond\delta_{i}\wedge\gamma_{i}$. In particular,
$\mathcal{M},v\vDash\delta_{i}$ for some $v$ such that $\rho Rv$. It follows
that

$\mathcal{M},\mathcal{J}\vDash\mathop{{{{{\varovee}}}}}\limits_{i=1}^{h}\Bigl{(}\bullet
1:\delta_{i}\mathbin{\varowedge}\bullet:\gamma_{i}\Bigr{)}$

for $\mathcal{J}=\mathcal{I}\sqcup\\{(\bullet 1,v)\\}$, i.e.,
$\mathcal{M},\mathcal{J}\vDash
A_{\ell}(0,\Sigma_{c};\Gamma,[\\{\psi\mid\Diamond\psi\in\Gamma\\}]_{\bullet
1})$. By IH,
$\mathcal{M},\mathcal{J}\vDash\Gamma,[\\{\psi\mid\Diamond\psi\in\Gamma\\}]_{\bullet
1}$. If $\mathcal{M},v\vDash\psi$ for some $\Diamond\psi\in\Gamma$, then
$\mathcal{M},\rho\vDash\Diamond\psi$, and
$\mathcal{M},\mathcal{I}\vDash\Gamma$. Otherwise,
$\mathcal{M},\mathcal{J}\vDash\Gamma$, so again
$\mathcal{M},\mathcal{I}\vDash\Gamma$.

### BLUIP(iii), some of the cases from Steps 1–3.

Let us start with the induction steps in which $\mathcal{G}$ is not saturated
and $A_{\ell}(t,\Sigma_{c};\mathcal{G})$ is calculated according to a row in
Table 4 (one of Steps 1–3 in the algorithm):

row 2 of Table 4:

$\mathcal{G}$ cannot be of the form
$\mathcal{G}^{\prime}{\\{q,\overline{q}\\}}_{\sigma}$ since
$A_{\ell}(t,\Sigma_{c};\mathcal{G})=\sigma:\top$ and we assumed
$\mathcal{M},\mathcal{I}\nvDash A_{\ell}(t,\Sigma_{c};\mathcal{G})$.

row 4 of Table 4:

If $\mathcal{G}=\mathcal{G}^{\prime}{\\{\varphi\land\psi\\}}_{\sigma}$, then
$A_{\ell}(t,\Sigma_{c};\mathcal{G})$ is defined in (18). So either
$\mathcal{M},\mathcal{I}\nvDash A_{\ell}\bigl{(}t,\Sigma_{c};\cal
G^{\prime}{\\{\varphi\land\psi,\varphi\\}}_{\sigma}\bigr{)}$ or
$\mathcal{M},\mathcal{I}\nvDash
A_{\ell}\bigl{(}t,\Sigma_{c};\mathcal{G}^{\prime}{\\{\varphi\land\psi,\psi\\}}_{\sigma}\bigr{)}$.
The cases are symmetric, so let us only treat the former. By assumption,
$\mathcal{G}$ is a sufficient layered sequent and thus so is
$\mathcal{G}^{\prime}{\\{\varphi\land\psi,\varphi\\}}_{\sigma}$ by definition.
So we can apply the IH and get a model $\mathcal{M}^{\prime}$ and
interpretation $\mathcal{I}^{\prime}$, such that
$(\mathcal{M}^{\prime},\mathcal{I}^{\prime})\leq_{\ell}(\mathcal{M},\mathcal{I})$
and
$\mathcal{M}^{\prime},\mathcal{I}^{\prime}\nvDash\mathcal{G}^{\prime}{\\{\varphi\land\psi,\varphi\\}}_{\sigma}$.
So, in particular,
$\mathcal{M}^{\prime},\mathcal{I}^{\prime}\nvDash\mathcal{G}$.

row 5 of Table 4:

If $\mathcal{G}=\mathcal{G}^{\prime},\Box\varphi$, then
$A_{\ell}(t,\Sigma_{c};\mathcal{G})$ is defined in (9) using the SCNF of
$A_{\ell}\bigl{(}t,\Sigma_{c};\mathcal{G}^{\prime},\Box\varphi,[\varphi]_{\bullet
j}\bigr{)}$ as defined in (10). From $\mathcal{M},\mathcal{I}\nvDash
A_{\ell}(t,\Sigma_{c};\mathcal{G})$ it follows that for some $1\leq i\leq h$,
both $\mathcal{M},\mathcal{I}(\bullet)\nvDash\Box\delta_{i}$ and also for all
$\tau\in\mathcal{G}$, $\mathcal{M},\mathcal{I}(\tau)\nvDash\gamma_{i,\tau}$.
From the former it follows that there is $v$ such that
$\mathcal{I}(\bullet)Rv$ and $\mathcal{M},v\nvDash\delta_{i}$. Define a new
interpretation $\mathcal{J}=\mathcal{I}\sqcup\\{(\bullet j,v)\\}$. By
inspection of (10) we can easily see that $\mathcal{M},\mathcal{J}\nvDash
A_{\ell}\bigl{(}t,\Sigma_{c};\mathcal{G}^{\prime},\Box\varphi,[\varphi]_{\bullet
j}\bigr{)}$. Note that $\mathcal{G}^{\prime},\Box\varphi,[\varphi]_{\bullet
j}$ is a sufficient layered sequent, and by IH there are
$\mathcal{M}^{\prime}$ and $\mathcal{J}^{\prime}$ such that
$(\mathcal{M}^{\prime},\mathcal{J}^{\prime})\leq_{\ell}(\mathcal{M},\mathcal{J})$
and
$\mathcal{M}^{\prime},\mathcal{J}^{\prime}\nvDash\mathcal{G}^{\prime},\Box\varphi,[\varphi]_{\bullet
j}$. Now define $\mathcal{I}^{\prime}=\mathcal{J}^{\prime}\upharpoonright
Dom(\mathcal{I})$. Clearly,
$(\mathcal{M}^{\prime},\mathcal{I}^{\prime})\leq_{\ell}(\mathcal{M},\mathcal{I})$
and $\mathcal{M},\mathcal{I}\nvDash\mathcal{G}$.

row 9 of Table 4:

If
$\mathcal{G}=\mathcal{G}^{\prime},\llbracket\Sigma,\Diamond\varphi\rrbracket_{\sigma},\llparenthesis\Pi\rrparenthesis_{\tau}$,
then $A_{\ell}(t,\Sigma_{c};\mathcal{G})$ is obtained from a sufficient
layered sequent as
$A_{\ell}\bigl{(}t,\Sigma_{c};\mathcal{G}^{\prime},\llbracket\Sigma,\Diamond\varphi\rrbracket_{\sigma},\llparenthesis\Pi,\varphi\rrparenthesis_{\tau}\bigr{)}$.
By IH, there is
$(\mathcal{M}^{\prime},\mathcal{I}^{\prime})\leq_{\ell}(\mathcal{M},\mathcal{I})$
such that
$\mathcal{M}^{\prime},\mathcal{I}^{\prime}\nvDash\mathcal{G}^{\prime},\llbracket\Sigma,\Diamond\varphi\rrbracket_{\sigma},\llparenthesis\Pi,\varphi\rrparenthesis_{\tau}$.
In particular, $\mathcal{M}^{\prime},\mathcal{I}^{\prime}\nvDash\mathcal{G}$.

### BLUIP(iii), Step 4a.

Here $\mathcal{G}$ has no diamond formulas and
$A_{\ell}(t,\Sigma_{c};\mathcal{G})$ is calculated according to (2). Since
$\mathcal{M},\mathcal{I}\nvDash A_{\ell}(t,\Sigma_{c};\mathcal{G})$, we have
by inspection of (2) that for all $\sigma:\ell^{\prime}\in\mathcal{G}$ where
$\ell^{\prime}\in{\sf Lit}\setminus\\{\ell\\}$,

$\displaystyle\mathcal{M},\mathcal{I}(\sigma)\nvDash\ell^{\prime}.$ (20)

We construct an $\ell$-bisimilar model $\mathcal{M}^{\prime}$ with
interpretation $\mathcal{I}^{\prime}$ such that each occurrence of $\ell$ in
$\mathcal{G}$ is still falsified in the corresponding world in
$\mathcal{M}^{\prime}$ according to $\mathcal{I}^{\prime}$. We proceed in two
steps. Informally speaking, we first copy worlds to make an injective
interpretation $\mathcal{I}^{\prime}$ and after that we modify the valuation
of $p\in\\{\ell,\overline{\ell}\\}$, as desired.

  1. 1.

Divide the domain of $\mathcal{I}$ into equivalence classes such that $\sigma$
and $\tau$ belong to the same class if and only if
$\mathcal{I}(\sigma)=\mathcal{I}(\tau)$. One could say that each class is
represented by a world in $\mathcal{M}$. For each equivalence class with $n>1$
elements, make $n-1$ copies of the corresponding world and call this model
$\mathcal{N}=(W^{\prime},R^{\prime},V_{\mathcal{N}})$. Define
$\mathcal{I}^{\prime}$ to be the interpretation assigning different labels in
an equivalence class to copies of the worlds in such a way that
$\mathcal{I}^{\prime}$ is injective and, by Lemma 4,
$(\mathcal{N},\mathcal{I}^{\prime})\sim(\mathcal{M},\mathcal{I})$.

  2. 2.

Define $\mathcal{M}^{\prime}=(W^{\prime},R^{\prime},V^{\prime})$ to be the
same as $\mathcal{N}$ except for valuations of $p$:

$V^{\prime}(p)=\begin{cases}V_{\mathcal{N}}(p)\setminus\\{w\mid\sigma:p\in\mathcal{G},w=\mathcal{I}(\sigma)\\}&\text{
if }\ell=p.\\\
V_{\mathcal{N}}(p)\cup\\{w\mid\sigma:\overline{p}\in\mathcal{G},w=\mathcal{I}(\sigma)\\}&\text{
if }\ell=\overline{p}.\end{cases}$

Indeed, by Definition 9,
$(\mathcal{M}^{\prime},\mathcal{I}^{\prime})\leq_{\ell}(\mathcal{M},\mathcal{I})$
as desired.

Now we check that the constructed model $\mathcal{M}^{\prime}$ with
interpretation $\mathcal{I}^{\prime}$ falsifies $\mathcal{G}$. We prove that
$\mathcal{M}^{\prime},\mathcal{I}^{\prime}(\sigma)\nvDash\varphi$ whenever
$\sigma:\varphi\in\mathcal{G}$ by induction on the structure of $\varphi$.
Recall that $\mathcal{G}$ does not contain formulas of the form
$\Diamond\psi$.

  * •

If $\sigma:\ell\in\mathcal{G}$, then $\mathcal{I}(\sigma)\notin V^{\prime}(p)$
in case $\ell=p$ and $\mathcal{I}(\sigma)\in V^{\prime}(p)$ in case
$\ell=\overline{p}$. In both cases,
$\mathcal{M}^{\prime},\mathcal{I}^{\prime}(\sigma)\nvDash\ell$.

  * •

If $\sigma:\overline{\ell}\in\mathcal{G}$, then
$\mathcal{M},\mathcal{I}(\sigma)\nvDash\overline{\ell}$ by (20). If $\ell=p$,
then $\mathcal{I}(\sigma)\in V^{\prime}(p)$. By construction, also
$\mathcal{I}^{\prime}(\sigma)\in V_{\mathcal{N}}(p)$. Note that
$\sigma:p\notin\mathcal{G}$, otherwise Step 1 would have been applied.
Therefore $\mathcal{I}^{\prime}(\sigma)\in V^{\prime}(p)$ and thus
$\mathcal{M}^{\prime},\mathcal{I}^{\prime}\nvDash\overline{p}$. We leave the
case that $\ell=\overline{p}$ to the reader.

  * •

If $\sigma:\ell^{\prime}\in\mathcal{G}$ with $\ell^{\prime}\in{\sf
Lit}\setminus\\{\ell,\overline{\ell}\\}$, then
$\mathcal{M},\mathcal{I}(\sigma)\nvDash\ell^{\prime}$ by (20), which
immediately transfers to $\mathcal{M}^{\prime}$ and $\mathcal{I}^{\prime}$ by
construction.

  * •

The cases for $\land$ and $\lor$ easily follow by saturation of $\mathcal{G}$.

  * •

If $\sigma:\Box\psi\in\mathcal{G}$, we use the fact that $\mathcal{G}$ is
saturated to see that $\tau:\psi\in\mathcal{G}$ for some $\tau$ such that
$\mathcal{I}^{\prime}(\sigma)R\mathcal{I}^{\prime}(\tau)$. By induction
hypothesis, $\mathcal{M}^{\prime},\mathcal{I}^{\prime}(\tau)\nvDash\psi$ and
therefore $\mathcal{M}^{\prime},\mathcal{I}^{\prime}(\sigma)\nvDash\Box\psi$.

### BLUIP(iii), Step 4b.

Now suppose $A_{\ell}(0,\Sigma_{c};\Gamma)$ is obtained by Step 4b, i.e., the
sequent consists of only the trunk and contains at least one diamond formula.
Multiformula $A_{\ell}(0,\Sigma_{c};\Gamma)$ is calculated as in (3) making
use of the SDNF of
$A_{\ell}(0,\Sigma_{c};\Gamma,[\\{\psi\mid\Diamond\psi\in\Gamma\\}]_{\bullet
1})$ presented in (4). By $\mathcal{M},\mathcal{I}\nvDash
A_{\ell}(0,\Sigma_{c};\Gamma)$, we know from (3) that

$\mathcal{M},\mathcal{I}\nvDash\mathop{{{{{\varovee}}}}}\limits_{i=1}^{h}\big{(}\bullet:\Diamond\delta_{i}\mathbin{\varowedge}\bullet:\gamma_{i}\big{)}\mathbin{\varovee}\bullet:\Box\bot$
or
$\mathcal{M},\mathcal{I}\nvDash\mathop{{{{{\varovee}}}}}\limits_{\bullet:\ell^{\prime}\in\Gamma,\ell^{\prime}\in{\sf
Lit}\setminus\\{\ell\\}}\bullet:\ell^{\prime}\mathbin{\varovee}\bullet:\Diamond\top$

In the latter case, $\mathcal{M}$ is a one-world (irreflexive) model. We only
need to define a new valuation on $\mathcal{M}$ to define
$\mathcal{M}^{\prime}$ as in Step 2 and the proof proceeds the same way and is
left to the reader. In particular, note that $\Gamma$ has no boxed formulas as
it only consists of the trunk.

For the former case, $\mathcal{M}$ consists of more than one world. In
particular, for each $1\leq i\leq h$, either
$\mathcal{M},\mathcal{I}(\bullet)\nvDash\gamma_{i}$ or for all worlds $v$ such
that $\mathcal{I}(\bullet)Rv$ we have $\mathcal{M},v\nvDash\delta_{i}$. For
all such $v$, consider the interpretation $\mathcal{J}_{v}:\\{\bullet,\bullet
1\\}\rightarrow\mathcal{M}$ defined by mapping label $\bullet 1$ to world $v$.
By inspection of (4), observe that for all such $v$ we have
$\mathcal{M},\mathcal{J}_{v}\nvDash
A_{\ell}(0,\Sigma_{c};\Gamma,[\\{\psi\mid\Diamond\psi\in\Gamma\\}]_{\bullet
1})$. It will be sufficient to fix such a $v$. Since
$A_{\ell}(0,\Sigma_{c};\Gamma,[\\{\psi\mid\Diamond\psi\in\Gamma\\}]_{\bullet
1})$ is sufficient by Lemma 5(2), we can apply the induction hypothesis to
obtain
$(\mathcal{M}^{\prime},\mathcal{J}^{\prime})\leq_{\ell}(\mathcal{M},\mathcal{J}_{v})$
such that
$\mathcal{M}^{\prime},\mathcal{J}^{\prime}\nvDash\Gamma,[\\{\psi\mid\Diamond\psi\in\Gamma\\}]_{\bullet
1}$. Now let $\mathcal{I}^{\prime}$ be $\mathcal{J}^{\prime}$ restricted to
the domain $\\{\bullet\\}$. Hence,
$\mathcal{M}^{\prime},\mathcal{I}^{\prime}\nvDash\mathcal{G}$. ∎