Institut für Logic and Computation, Technische Universität Wien, Austria and
<EMAIL_ADDRESS>by the
European Union Horizon 2020 Marie Skłodowska-Curie grant No 689176 and FWF
projects I 2982, Y544-N2, and W1255-N23. Research School of Computer Science,
The Australian National University, Australia Research School of Computer
Science, The Australian National University, Australia Research School of
Computer Science, The Australian National University, Australia Tim Lyon and
Alwen Tiu and Rajeev Góre and Ranald Clouston[100]Theory of Computation Proof
Theory [100]Theory of Computation Automated ReasoningMaribel Fernández and
Anca Muscholl 2 28th EACSL Annual Conference on Computer Science Logic (CSL
2020) CSL 2020 CSL 2020 January 13–16, 2020 Barcelona, Spain 152 28

# Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via
Nested Sequents

Tim Lyon  Alwen Tiu  Rajeev Goré  Ranald Clouston

###### Abstract

We provide a direct method for proving Craig interpolation for a range of
modal and intuitionistic logics, including those containing a “converse”
modality. We demonstrate this method for classical tense logic, its extensions
with path axioms, and for bi-intuitionistic logic. These logics do not have
straightforward formalisations in the traditional Gentzen-style sequent
calculus, but have all been shown to have cut-free nested sequent calculi. The
proof of the interpolation theorem uses these calculi and is purely syntactic,
without resorting to embeddings, semantic arguments, or interpreted
connectives external to the underlying logical language. A novel feature of
our proof includes an orthogonality condition for defining duality between
interpolants.

###### keywords:

Bi-intuitionistic logic, Interpolation, Nested calculi, Proof theory,
Sequents, Tense logics

###### category:

##  1 Introduction

The Craig interpolation property for a logic $\mathbf{L}$ states that if
$A\Rightarrow B\in\mathbf{L}$, then there exists a formula $C$ in the language
of $\mathbf{L}$ such that $A\Rightarrow C\in\mathbf{L}$ and $C\Rightarrow
B\in\mathbf{L}$, and every propositional variable appearing in $C$ appears in
$A$ and $B$. This property has many useful applications: it can be used to
prove Beth definability [11]; in computer-aided verification it can be used to
split a large problem involving $A\Rightarrow B$ into smaller problems
involving $A\Rightarrow C$ and $C\Rightarrow B$ [17]; and in knowledge
representation (uniform) interpolation can be used to conceal or forget
irrelevant or confidential information in ontology querying [15]. Therefore,
demonstrating that a logic possesses the Craig interpolation property is of
practical value.

Interpolation can be proved semantically or syntactically. In the semantic
method, $\mathbf{L}$ is the set of valid formulae, thereby requiring a
semantics for $\mathbf{L}$. In the syntactic method, often known as Maehara’s
method [16], $\mathbf{L}$ is the set of theorems, thereby requiring a proof-
calculus. The syntactic approach constructs the interpolant $C$ by induction
on the (usually cut-free) derivation of $A\Rightarrow B$, and usually also
provides derivations witnessing $A\Rightarrow C$ and $C\Rightarrow B$.

Over the past forty years, Gentzen’s original sequent calculus has been
extended in many different ways to handle a plethora of logics. The four main
extensions are hypersequent calculi [2], display calculi [7], nested sequent
calculi [1, 10, 20], and labelled calculi [18]. Various interpolation results
have been found using these calculi but the only general methodology that we
know of is the recent work of Kuznets [13] with Lellman [14]. Although they
use extended sequent calculi, binary-relational Kripke semantical arguments
are crucial for their methodology, and extending their method to other
semantics is left as further work. They also construct the interpolants using
a language containing (interpreted) meta-level connectives which are external
to the logic at hand, and do not handle logics containing converse modalities
such as tense logic. Finally, their method does not yield derivations
witnessing $A\Rightarrow C$ and $C\Rightarrow B$.

We give a general, purely syntactic, methodology for proving Craig
interpolation using nested sequent calculi for a variety of propositional,
non-classical logics including normal tense logics, their extensions with path
axioms, and bi-intuitionistic logic. Our methodology does not utilise
semantics, does not embed one logic into another, and does not utilise logical
connectives which are external to the underlying logical language.

The first novelty of our approach is a generalisation of the notion of
interpolant from formulas to sets of sequents. The second is a notion of
orthogonality which gives rise to a notion of duality via cut: if two
interpolants are orthogonal, then the empty sequent is derivable from the
sequents in the interpolants using only the cut and the contraction rules.
This duality via cut allows us to relate our more general notion of
interpolants (as sets of sequents) to the usual notion of interpolants (as
formulas). Moreover, given a derivation of $A\Rightarrow B$, our orthogonality
condition not only allows us to construct the interpolant $C$, but also the
derivations witnessing $A\Rightarrow C$ and $C\Rightarrow B$. This fact shows
that our approach possesses a distinct complexity-theoretic advantage over the
semantic approach: to verify that $C$ is indeed the interpolant of
$A\Rightarrow B$, one need only check the derivations of $A\Rightarrow C$ and
$C\Rightarrow B$, which is a PTIME process. In the semantic approach, to
verify that $A\Rightarrow C$ and $C\Rightarrow B$ are indeed valid (and that
$C$ is in fact an interpolant of $A\Rightarrow B$) one must construct proofs
of the implications, which is generally much harder (e.g., finding a proof of
a validity in one of the tense logics presented in Sec. 3 is PSPACE complete).

Related work. Interpolation has been heavily investigated in the description
logic community, where it is used to hide or forget information [22]. In this
setting, the logic ALC is a syntactic variant of the multimodal normal modal
logic Kn while its extension with inverse roles, ALCI, is a variant of the
multimodal normal tense logic Ktn. Cate et al [22] utilise a complexity-
optimal tableau algorithm to prove interpolation for ALC via Maehara’s method.
They then embed ALCI into ALC and extend their interpolation result to ALCI.

By contrast, our methodology is direct: we obtain interpolation for the normal
tense logic Kt, and can then extract interpolation for the normal modal logic
K by simply observing that our nested sequent calculus obeys the separation
property: if the end-sequent $\vdash A\rightarrow B$ contains no occurrences
of the black (converse) modalities, then neither does the interpolant.

As mentioned earlier, the work of Kuznets et al. [6, 13, 14] on interpolation
for modal logics in nested sequent calculi is closest to ours. Our
construction of interpolants for tense logics shares some similarity with
theirs. One crucial difference is that our interpolants are justified purely
through syntactic and proof-theoretic means, whereas their interpolants are
justified via semantic arguments. Another important difference is that our
method extends to the bi-modal case and also (bi-)intuitionistic case, and it
is straightforward to adapt our work to the multi-modal case, e.g., using
nested sequent calculi as in [23]. Kowalski and Ono [12] showed interpolation
for bi-intuitionistic logic using a sequent calculus with analytic cut. In
contrast, our proof is based on a cut-free nested sequent calculus [8].

Outline of the paper. In Sec. 2 we give a brief overview of a typical
interpolation proof using the traditional sequent calculus, and highlight some
issues of extending it to nested sequent calculi, which motivates the
generalisation of the interpolation theorem we adopt in this paper. In Sec. 3
we show how the generalised notion of interpolants can be used to prove the
Craig interpolation theorem for classical tense logic and its extensions with
path axioms [9], covering all logics in the modal cube and more. We then show
how our approach can be extended to bi-intuitionistic logic in Sec. 4. In Sec.
5 we conclude and discuss future work.

##  2 Overview of our approach

We analyze a typical syntactic interpolation proof for Gentzen sequents,
highlight the issues of extending it to nested sequents, and motivate our
syntactic approach for interpolation.

Consider, for example, a two-sided sequent calculus for classical logic such
as G3c [24]. Interpolation holds when we can prove that for all
$\Gamma_{1},\Gamma_{2},\Delta_{1},\Delta_{2}$, if
${\Gamma_{1},\Gamma_{2}}\vdash{\Delta_{1},\Delta_{2}}$ is provable in G3c,
then so are both ${\Gamma_{1}}\vdash{\Delta_{1},C}$ and
${C,\Gamma_{2}}\vdash{\Delta_{2}}$, for some $C$ containing only propositional
variables common to both $\Gamma_{1},\Delta_{1}$ and $\Gamma_{2},\Delta_{2}$.

The inductive construction of $C$ can be encoded via inference rules over more
expressive sequents that specify the splitting of the contexts and the
interpolant constructed thus far. In G3c, we write
${\Gamma_{1}\mid\Gamma_{2}}\vdash{\Delta_{1}\mid\Delta_{2}}\mathrel{\|}{C}$ to
denote the sequent ${\Gamma_{1},\Gamma_{2}}\vdash{\Delta_{1},\Delta_{2}}$ with
its context split into $\Gamma_{1}\vdash\Delta_{1}$ and
$\Gamma_{2}\vdash\Delta_{2}$, and with $C$ the interpolant. Inference rules
for this extended sequent are similar to the usual ones, with variations
encoding the different ways the contexts may be split. For example, the
initial rule ${\Gamma,p}\vdash{p,\Delta}$ has the following four variants
corresponding to the four splittings of where $p$ can occur (with four
different interpolants!):

${\Gamma_{1},p\mid\Gamma_{2}}\vdash{p,\Delta_{1}\mid\Delta_{2}}\mathrel{\|}{\bot}\qquad{\Gamma_{1},p\mid\Gamma_{2}}\vdash{\Delta_{1}\mid
p,\Delta_{2}}\mathrel{\|}{p}$
${\Gamma_{1}\mid\Gamma_{2},p}\vdash{p,\Delta_{1}\mid\Delta_{2}}\mathrel{\|}{\neg
p}\qquad{\Gamma_{1}\mid\Gamma_{2},p}\vdash{\Delta_{1}\mid
p,\Delta_{2}}\mathrel{\|}{\top}$

Branching rules, such as the right-introduction rule for $\land$, split into
two variants, depending on whether the principal formula is in the first or
the second partition of the context:

${\Gamma_{1}\mid\Gamma_{2}}\vdash{A\land
B,\Delta_{1}\mid\Delta_{2}}\mathrel{\|}{C\lor
D}\lx@proof@logical@and{\Gamma_{1}\mid\Gamma_{2}}\vdash{A,\Delta_{1}\mid\Delta_{2}}\mathrel{\|}{C}{\Gamma_{1}\mid\Gamma_{2}}\vdash{B,\Delta_{1}\mid\Delta_{2}}\mathrel{\|}{D}$
${\Gamma_{1}\mid\Gamma_{2}}\vdash{\Delta_{1}\mid\Delta_{2},A\land
B}\mathrel{\|}{C\land
D}\lx@proof@logical@and{\Gamma_{1}\mid\Gamma_{2}}\vdash{\Delta_{1}\mid\Delta_{2},A}\mathrel{\|}{C}{\Gamma_{1}\mid\Gamma_{2}}\vdash{\Delta_{1}\mid\Delta_{2},B}\mathrel{\|}{D}$

Observe that the interpolants of the conclusion sequents are composed from the
interpolants of the premises, but with the main connectives dual to one
another: a disjunction in the $\land_{R_{1}}$ rule and a conjunction in the
$\land_{R_{2}}$ rule. These observations also apply for the other rules of
G3c, with a slight subtlety for the implication-left rule: see [24].
Interpolation for G3c can then be proved by a straightforward induction on the
height of proofs.

Below we discuss some issues with extending this approach to proving
interpolation for modal/tense logics and bi-intuitionistic logic using nested
sequent calculi, and how these issues lead to the generalisation of the
intermediate lemmas we need to prove (which amounts to an interpolation
theorem for sequents, rather than formulae).

### Classical modal and tense logics

A nested sequent [10] can be seen as a tree of traditional Gentzen-style
sequents. For classical modal logics, single-sided sequents suffice, so a
nested sequent in this case can be seen as a nested multiset: i.e. a multiset
whose elements can be formulae or multisets. Following the notation in [9], a
sequent nested inside another sequent is prefixed with a $\circ$, which is the
structural proxy for the $\Box$ modal operator. For example, the nested
sequent below first left, with two sub-sequents $\\{c,d\\}$ and $\\{e,f\\}$,
represents the formula shown second left:

${}\vdash{\\{a,b,\circ\\{c,d\\},\circ\\{e,f\\}\\}}\qquad a\lor
b\lor\square(c\lor d)\lor\square(e\lor f)\qquad{}\vdash{\Gamma,\lozenge
A,\circ\\{\Delta\\}}{}\vdash{\Gamma,\circ\\{A,\Delta\\}}\qquad{}\vdash{\lozenge\neg
p,\lozenge p,\circ\\{q\\}}{}\vdash{\lozenge\neg p,\circ\\{p,q\\}}$

Nested sequent calculi for modal logics [1, 9, 10] typically contain the
propagation rule for diamond shown third left above which “propagates” the $A$
into the scope of $\circ$, when read upwards. Propagation rules complicate the
adaptation of the interpolation proof from traditional Gentzen sequent
calculi. In particular, it is not sufficient to partition a context into two
disjoint multisets. That is, suppose a nested sequent
${}\vdash{\Gamma,\Delta}$ is provable, and we would like to construct an
interpolant $C$ such that ${}\vdash{\Gamma,C}$ and
${}\vdash{\overline{C},\Delta}$ are provable, where $\overline{C}$ is the
negation normal form of $\neg C$. Suppose the proof of
${}\vdash{\Gamma,\Delta}$ ends with a propagation rule, e.g., when
$\Gamma=\lozenge\neg p,\lozenge p$ and $\Delta=\circ\\{q\\}$ as shown above
far right. In this case, by induction, we can construct an interpolant $D$
such that the splittings ${}\vdash{\lozenge\neg p,D}$ and
${}\vdash{\overline{D},\circ\\{p,q\\}}$ of the premiss are provable, but it is
in general not obvious how to construct the desired interpolant $C$ for the
conclusion ${}\vdash{\lozenge\neg p,\circ\\{p,q\\}}$ from $D$. For this
example,$D$ should be $\square p$, $C$ should be $\square\bot$, which does not
mention $p$ at all.

The above issue with propagation rules suggests that we need to strengthen the
induction hypothesis to construct interpolants, i.e., by considering splitting
the sequent context at every sub-sequent in the nested sequent. For example,
the nested sequent ${}\vdash{\lozenge\neg p,\circ\\{p,q\\}}$ above should be
split into ${}\vdash{\lozenge\neg p,\circ\\{p\\}}$ and
${}\vdash{\circ\\{q\\}}$ when applying the induction hypothesis. Then,
$D=C=\square\bot$ is indeed an interpolant: both ${}\vdash{\lozenge\neg
p,\circ\\{p\\},\square\bot}$ and ${}\vdash{\lozenge\top,\circ\\{q\\}}$ are
provable. Nevertheless, employing a formula interpolant is not enough to push
through the inductive argument in general. Consider, for example, the nested
sequent ${}\vdash{\circ\\{p,\neg p\\}}$, which is provable with an identity
rule, and its partition ${}\vdash{\circ\\{p\\}}$ and ${}\vdash{\circ\\{\neg
p\\}}$. There is no formula $C$ such that both ${}\vdash{\circ\\{p\\},C}$ and
${}\vdash{\overline{C},\circ\\{\neg p\\}}$ are provable. One solution to this
problem is to generalise the interpolation statement to consider a nested
sequent as an interpolant: If a nested sequent ${}\vdash{\Gamma}$ is provable,
then for every ‘partitioning’ of ${}\vdash{\Gamma}$ into
${}\vdash{\Gamma_{1}}$ and ${}\vdash{\Gamma_{2}}$ (where the partitioning
applies to every sub-sequent in a nested sequent; the precise definition will
be given in subsequent sections), there exists ${}\vdash{\Delta}$ (the
interpolant), ${}\vdash{\Gamma_{1}^{\prime}}$ and
${}\vdash{\Gamma_{2}^{\prime}}$ such that

  1. 1.

The propositional variables occuring in ${}\vdash{\Delta}$ are in both
${}\vdash{\Gamma_{1}}$ and ${}\vdash{\Gamma_{2}}$,

  2. 2.

${}\vdash{\Gamma_{1}^{\prime}}$ splits into ${}\vdash{\Gamma_{1}}$ and
${}\vdash{\Delta}$, and ${}\vdash{\Gamma_{2}^{\prime}}$ splits into
${}\vdash{\Gamma_{2}}$ and ${}\vdash{\overline{\Delta}}$, where
${}\vdash{\overline{\Delta}}$ denotes the nested sequent ${}\vdash{\Delta}$
with all formula occurrences replaced with their negations, and

  3. 3.

Both ${}\vdash{\Gamma_{1}^{\prime}}$ and ${}\vdash{\Gamma_{2}^{\prime}}$ are
provable.

For example, the nested sequent ${}\vdash{\circ\\{p,\neg p\\}}$, with
partitions ${}\vdash{\circ\\{p\\}}$ and ${}\vdash{\circ\\{\neg p\\}}$, has the
interpolant ${}\vdash{\Delta}={}\vdash{\circ\\{\neg p\\}}$ (hence
${}\vdash{\overline{\Delta}}={}\vdash{\circ\\{p\\}}$), and
${}\vdash{\Gamma_{1}^{\prime}}={}\vdash{\Gamma_{2}^{\prime}}={}\vdash{\circ\\{p,\neg
p\\}}.$

One remaining issue is that, since we now use a nested sequent as an
interpolant, the composition of interpolants needs to be adjusted as well.
Recall that in the construction of interpolants for G3c above, in the case
involving the right-introduction for $\land$, we constructed either $C\lor D$
or $C\land D$ as the interpolant for the conclusion. If $C$ and $D$ are nested
sequents, the expression $C\lor D$ or $C\land D$ would not be well-formed. To
solve this remaining issue, we generalise the interpolant further to be a set
of nested sequents.

Fitting and Kuznets [6] similarly generalise the notion of interpolants, but
instead of generalising interpolants to a set of (nested) sequents, they
introduce ‘meta’ connectives for conjunction and disjunction, applicable only
to interpolants, and justified semantically. Our notion of interpolants
requires no new logical operators or semantical notions.

### Propositional bi-intuionistic logic

Bi-intuitionistic logic is obtained from intuitionistic logic by adding a
subtraction (or exclusion) connective $-\\!\\!\\!<$ that is dual to
implication. Its introduction rules are the mirror images of those for
implication; in the traditional sequent calculus, these take the form:

${A-\\!\\!\\!<B}\vdash{\Delta}{A}\vdash{B,\Delta}\qquad{\Gamma}\vdash{\Delta,A-\\!\\!\\!<B}\lx@proof@logical@and{\Gamma}\vdash{\Delta,A}{\Gamma,B}\vdash{\Delta}$

However, as shown in [19], the cut rule cannot be entirely eliminated in a
sequent calculus featuring these rules, although they can be restricted to
analytic cuts [12]. In [8], Postniece et al. show how bi-intuitionistic logic
can be formalised in a nested sequent calculus. Although interpolation holds
for intuitionistic logic, it does not generalise straightforwardly to bi-
intuitionistic logic, and only very recently has interpolation for bi-
intuitionistic logic been shown [12]. The proof for the interpolation theorem
for intuitionistic logic is very similar to the proof of the same theorem for
classical logic; one simply needs to restrict the partitioning of the sequent
to the form ${\Gamma_{1}\mid\Gamma_{2}}\vdash{\Delta_{1}\mid\Delta_{2}}$ where
$\Delta_{1}$ is empty and $\Delta_{2}$ contains at most one formula
occurrence. Since the (nested) sequent calculus for bi-intuitionistic logic
uses multiple-conclusion (nested) sequents, the proof for intuitionistic logic
cannot be adapted to the bi-intutionistic case. The problem already shows up
in the very simple case involving the identity rule: suppose we have a proof
of the initial sequent ${p}\vdash{p}$ and we want to partition the sequent as
${\cdot\mid p}\vdash{p\mid\cdot}$. It is not possible to find an interpolant
$C$ such that ${\cdot}\vdash{p,C}$ and ${C,p}\vdash{\cdot}$ (otherwise, one
would be able to prove the excluded middle $p\lor(p\supset\bot)$, which is not
valid in bi-intuitionistic logic, using the cut formula $p\lor C$). In
general, the inductive construction of the interpolant for $A\supset B$ may
involve finding an interpolant $C$ for the problematic partition of the form
${\cdot\mid\Gamma}\vdash{\Delta\mid\cdot}$, where $\Delta$ is non-empty. This
case does not arise in the interpolation proof for intuitionistic logic in
[24], due to the restriction to single-conclusion sequents.

We show that the above issue with bi-intutionistic logic can be solved using
the same approach as in modal logic: simply extend the interpolant to a set of
nested sequents. In particular, for ${\cdot\mid p}\vdash{p\mid\cdot}$, the
generalised interpolation statement only requires finding an interpolating
sequent ${\Gamma}\vdash{\Delta}$ and its ‘dual’
${\Gamma^{\prime}}\vdash{\Delta^{\prime}}$ (see below) such that both
${\Gamma}\vdash{p,\Delta}$ and ${\Gamma^{\prime},p}\vdash{\Delta^{\prime}}$
are provable, which is achieved by letting $\Gamma=\\{p\\}$,
$\Delta=\\{\leavevmode\nobreak\ \\}$, $\Gamma^{\prime}=\\{\leavevmode\nobreak\
\\}$ and $\Delta^{\prime}=\\{p\\}.$

### Interpolating sequents and orthogonality

In a simplified form (e.g., sequent calculus), the generalised interpolation
result we show can be roughly summarised as follows: given a provable sequent
${\Gamma_{1},\Gamma_{2}}\vdash{\Delta_{1},\Delta_{2}}$, there exist two sets
of sequents $\mathcal{I}$ and $\mathcal{I}^{\prime}$ such that

  1. 1.

For every sequent $({\Sigma}\vdash{\Theta})\in\mathcal{I}$, the sequent
${\Gamma_{1},\Sigma}\vdash{\Delta_{1},\Theta}$ is provable,

  2. 2.

For every sequent
$({\Sigma^{\prime}}\vdash{\Theta^{\prime}})\in\mathcal{I}^{\prime}$, the
sequent ${\Gamma_{2},\Sigma^{\prime}}\vdash{\Delta_{2},\Theta^{\prime}}$ is
provable,

  3. 3.

The propositional variables in $\mathcal{I}$ and $\mathcal{I}^{\prime}$ occur
in both ${\Gamma_{1}}\vdash{\Delta_{1}}$ and ${\Gamma_{2}}\vdash{\Delta_{2}}$,
and

  4. 4.

The sequents in $\mathcal{I}$ and $\mathcal{I}^{\prime}$ are orthogonal to
each other, that is, the empty sequent ${}\vdash{}$ is derivable from all
sequents in $\mathcal{I}\cup{\mathcal{I}^{\prime}}$ using only the cut rule
and possibly structural rules (contraction and/or weakening).

The set $\mathcal{I}$ is taken to be the (sequent) interpolant.

Last, the orthogonality condition, can be seen as a generalisation of duality.
To see how this is the case, consider a degenerate case where
${\Gamma_{1},\Gamma_{2}}\vdash{\Delta_{1},\Delta_{2}}$ is a classical sequent
(e.g., in G3c). We show how one can convert a formula interpolant in the usual
definition (i.e., formula $C$ s.t. ${\Gamma_{1}}\vdash{C,\Delta_{1}}$ and
${\Gamma_{2},C}\vdash{\Delta_{2}}$ are provable) to a sequent interpolant
satisfying the four conditions above, and vice-versa. For the forward
direction, simply let $\mathcal{I}=\\{{}\vdash{C}\\}$ and
$\mathcal{I}^{\prime}=\\{{C}\vdash{}\\}$. It is easy to see that $\mathcal{I}$
is orthogonal to $\mathcal{I}^{\prime}.$ For the converse direction, suppose
we have a sequent interpolant $\mathcal{I}$ and its orthogonal
$\mathcal{I}^{\prime}$. We illustrate how one can construct a formula
interpolant $C$. To simplify the discussion, let us assume that

$\mathcal{I}=\\{({p,q}\vdash{r,s})\\}\quad{\mathcal{I}^{\prime}}=\\{({}\vdash{p}),\leavevmode\nobreak\
({}\vdash{q}),\leavevmode\nobreak\ ({r}\vdash{})\leavevmode\nobreak\
,({s}\vdash{\leavevmode\nobreak\ })\\}$

and that the following sequents are provable:

$(1)\leavevmode\nobreak\
{\Gamma_{1},p,q}\vdash{r,s,\Delta_{1}}\quad(2)\leavevmode\nobreak\
{\Gamma_{2}}\vdash{\Delta_{2},p}\quad(3)\leavevmode\nobreak\
{\Gamma_{2}}\vdash{\Delta_{2},q}\quad(4)\leavevmode\nobreak\
{\Gamma_{2},r}\vdash{\Delta_{2}}\quad(5)\leavevmode\nobreak\
{\Gamma_{2},s}\vdash{\Delta_{2}}$

Let $C=(p\land q)\supset(r\lor s).$ Then it is easy to see that
${\Gamma_{1}}\vdash{\Delta_{1},C}$ is provable given (1), and
${\Gamma_{2},C}\vdash{\Delta_{2}}$ is provable given (2) - (5). The formal
statement and the proof of the generalised interpolation theorem will be
discussed in detail in the next two sections.

### A note on notation

In what follows, we adopt a representation of nested sequents using restricted
labelled sequents where we use the labels and relational atoms to encode the
tree structure of a nested sequent. To clarify what we mean, consider the
following nested sequent for tense logic [9]:

$A,B,\circ\\{C,D\\},\circ\\{E,F,\bullet\\{G,H\\},\circ\\{I\\}\\}$

Graphically, the nested sequent can be represented as a tree (shown below
left) with two types of edges $\overset{\circ}{\rightarrow}$ and
$\overset{\bullet}{\rightarrow}$. Alternatively, the nested sequent can be
represented as the polytree shown below right with a single type of edge
$\overset{}{\rightarrow}$ and where the orientation of the edge encodes the
two types of structures $\circ{\\{}\\}$ and $\bullet{\\{}\\}$ of the nested
sequent (observe that the $\bullet$-edge from $E,F$ to $G,H$ in the left
diagram has been reversed in the right diagram).111A polytree is a directed
graph such that its underlying graph—the graph obtained by ignoring the
orientation of the edges—is a tree.

$\textstyle{A,B\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\circ}$$\scriptstyle{\circ}$$\textstyle{C,D}$$\textstyle{E,F\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\bullet}$$\scriptstyle{\circ}$$\textstyle{G,H}$$\textstyle{I}$ | $\textstyle{A,B\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{C,D}$$\textstyle{E,F\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{G,H\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{I}$
---|---

In the latter representation, the structure of the nested sequent can be
encoded using a single binary relation: we label each node of the tree
corresponding to the nested sequent (as shown above left) with unique labels
$x$, $y$, $z$, $\ldots$, encode each edge $x\overset{\circ}{\rightarrow}y$
from a label $x$ to a label $y$ with a relation $Rxy$, and encode each edge
$x\overset{\bullet}{\rightarrow}y$ with a relation $Ryx$ [3]. The above nested
sequent can then be equivalently represented as a labelled sequent where
$\mathcal{R}=\\{Ruv,Ruw,Rxw,Rwy\\}$ and $R$ is a relational symbol:

${\mathcal{R}}\vdash{u:A,u:B,v:C,v:D,w:E,w:F,x:G,x:H,y:I}$

Inference rules in a nested sequent calculus can be trivially encoded as rules
in a restricted labelled calculus seen as a ‘data structure’ rather than a
proper labelled sequent calculus.

We stress that our labelled notation to represent nested sequents is just a
matter of presentation: the labelled representation is notationally simpler
for presenting inference rules and composing nested sequents. For instance,
the operation of merging two nested sequents with isomorphic shapes is simply
the union of the multiset of labelled formulae.

##  3 Interpolation for Tense Logics

$\overline{A}\vee\square\blacklozenge
A\qquad\overline{A}\vee\blacksquare\lozenge
A\qquad\lozenge(A\wedge\overline{B})\vee\lozenge\overline{A}\vee\square
B\qquad\blacklozenge(A\wedge\overline{B})\vee\blacklozenge\overline{A}\vee\blacksquare
B\qquad\square AA\qquad\blacksquare AA$
Figure 1: The minimal tense logic $\mathsf{Kt}$ consists of all classical
propositional tautologies, modus ponens, and is additionally extended with the
above axioms and inference rules.

As usual, we interpret $\square A$ as saying that $A$ holds at every point in
the immediate future, and $\lozenge A$ as saying that $A$ holds at some point
in the immediate future. Conversely, the $\blacksquare$ and $\blacklozenge$
modalities make reference to the past: $\blacksquare A$ says that $A$ holds at
every point in the immediate past, and $\blacklozenge A$ says that $A$ holds
at some point in the immediate past. Last, we take $\overline{p}$ to be the
negation of $p$, and use the notation $[?]\in\\{\square,\blacksquare\\}$ and
$\langle?\rangle\in\\{\lozenge,\blacklozenge\\}$.

We consider tense formulae in negation normal form (nnf) as this simplifies
our calculi while retaining the expressivity of the original language. The
language for the tense logics we consider is given via the following BNF
grammar:

$A::=p\ |\ \overline{p}\ |\ (A\wedge A)\ |\ (A\vee A)\ |\ (\square A)\ |\
(\lozenge A)\ |\ (\blacksquare A)\ |\ (\blacklozenge A).$

Since our language excludes an explicit connective for negation, we define it
formally below (Def. 3.1). Using the definition, we may define an implication
$A\rightarrow B$ to be $\overline{A}\vee B$.

######  Definition 3.1.

For a formula $A$, we define the _negation_ $\overline{A}$ recursively on the
structure of $A$: if $A=p$ then $\overline{A}:=\overline{p}$ and if
$A=\overline{p}$ then $\overline{A}:=p$. The clauses concerning the
connectives are as follows: (1) $\overline{B\land
C}:=\overline{B}\vee\overline{C}$, (2)
$\overline{[?]B}:=\langle?\rangle\overline{B}$, (3) $\overline{B\lor
C}:=\overline{B}\wedge\overline{C}$, and (4) $\overline{\langle?\rangle
B}:=[?]\overline{B}$.

Path axioms are of the form
$[?]_{1}[?]_{2}\cdots[?]_{n}\;\bar{p}\;\vee\langle?\rangle p$ (or,
equivalently, $\langle?\rangle_{1}\cdots\langle?\rangle_{n}p\to\langle?\rangle
p$) with $n\in\mathbb{N}$. See [23] for an overview of path axioms.

The tense logics we consider are all extentions of the minimal tense logic
$\mathsf{Kt}$ (Fig. 1) with path axioms. Thus, $\mathsf{Kt\Pi}$ is the minimal
extension of $\mathsf{Kt}$ with all axioms from the finite set $\mathsf{\Pi}$
of path axioms.

The calculus for $\mathsf{Kt}$, extended with a set of path axioms
$\mathsf{\Pi}$, is given in Fig. 2. Labelled sequents are defined to be
syntactic objects of the form ${\mathcal{R}}\vdash{\Gamma}$, where
$\mathcal{R}$ is a multiset of relational atoms of the form $Rxy$ and $\Gamma$
is a multiset of labelled formulae of the form $x:A$, with $A$ a tense formula
and labels from a countable set $\\{x,y,z,\ldots\\}$.

Note that the side conditions $x\mathcal{R}^{\mathsf{\Pi}}y$ and
$y\mathcal{R}^{\mathsf{\Pi}}x$ of the $\lozenge$ and $\blacklozenge$ rules,
respectively, depend on the set $\mathsf{\Pi}$ of path axioms added to
$\mathsf{Kt}$. The definition of the relation $\mathcal{R}^{\mathsf{\Pi}}$ is
founded upon various auxiliary concepts that fall outside the main scope of
this paper. We therefore refer the interested reader to App. A.6 where the
$\mathcal{R}^{\mathsf{\Pi}}$ relation as well as the concepts needed for its
definition are explicitly provided. See also [9, 23] for details.

######  Lemma 3.2.

The contraction rules $ctr$, the weakening rules $wk$ and $cut_{1}$ are
admissible, and all inference rules are invertible in $\mathsf{Kt\Pi L}$.

######  Proof 3.3.

See Fig. 6 for rules222Note that since $\mathsf{Kt\Pi L}$ uses one sided
sequents, we only consider instances of the rules where labelled formulae
occur solely on the right of the sequent arrow. and [9, 23] for details.

${\mathcal{R}}\vdash{x:\bar{p},x:p,\Delta}\qquad{\mathcal{R}}\vdash{x:A\lor
B,\Delta}{\mathcal{R}}\vdash{x:A,x:B,\Delta}\qquad{\mathcal{R}}\vdash{x:A\land
B,\Delta}\lx@proof@logical@and{\mathcal{R}}\vdash{x:A,\Delta}{\mathcal{R}}\vdash{x:B,\Delta}$

${\mathcal{R}}\vdash{x:\lozenge A,\Delta}{\mathcal{R}}\vdash{x:\lozenge
A,y:A,\Delta}\qquad\qquad{\mathcal{R}}\vdash{x:\square
A,\Delta}{\mathcal{R},Rxy}\vdash{y:A,\Delta}$

${\mathcal{R}}\vdash{x:\blacklozenge
A,\Delta}{\mathcal{R}}\vdash{x:\blacklozenge
A,y:A,\Delta}\qquad\qquad{\mathcal{R}}\vdash{x:\blacksquare
A,\Delta}{\mathcal{R},Ryx}\vdash{y:A,\Delta}$

Figure 2: The calculus $\mathsf{Kt\Pi L}$ for $\mathsf{Kt}$ extended with a
set of path axioms $\mathsf{\Pi}$.

######  Example 3.4.

Consider the formula
$\square\lozenge\overline{q}\rightarrow\square(\lozenge\overline{p}\lor\lozenge\lozenge
p)$, which is a theorem in the logic $\mathsf{Kt\Pi}$ with
$\mathsf{\Pi}=\\{\square\square\overline{p}\vee\lozenge p\\}$. A proof of this
formula is provided in Fig. 3.

${}\vdash{x:\lozenge\square
q\lor\square(\lozenge\overline{p}\lor\lozenge\lozenge
p)}{}\vdash{x:\lozenge\square
q,x:\square(\lozenge\overline{p}\lor\lozenge\lozenge
p)}{Rxy}\vdash{x:\lozenge\square q,y:\lozenge\overline{p}\lor\lozenge\lozenge
p}{Rxy}\vdash{x:\lozenge\square q,y:\lozenge\overline{p},y:\lozenge\lozenge
p}{Rxy}\vdash{x:\lozenge\square q,y:\square
q,y:\lozenge\overline{p},y:\lozenge\lozenge
p}{Rxy,Ryz}\vdash{x:\lozenge\square
q,z:q,y:\lozenge\overline{p},y:\lozenge\lozenge
p}{Rxy,Ryz}\vdash{x:\lozenge\square q,z:\square
q,z:q,y:\lozenge\overline{p},y:\lozenge\lozenge
p}{Rxy,Ryz,Rzw}\vdash{x:\lozenge\square
q,w:q,z:q,y:\lozenge\overline{p},y:\lozenge\lozenge
p}{Rxy,Ryz,Rzw}\vdash{x:\lozenge\square
q,w:q,z:q,y:\lozenge\overline{p},w:\overline{p},y:\lozenge\lozenge
p}{Rxy,Ryz,Rzw}\vdash{x:\lozenge\square
q,w:q,z:q,y:\lozenge\overline{p},w:\overline{p},y:\lozenge\lozenge
p,z:\lozenge p}{Rxy,Ryz,Rzw}\vdash{x:\lozenge\square
q,w:q,z:q,y:\lozenge\overline{p},w:\overline{p},y:\lozenge\lozenge
p,z:\lozenge p,w:p}$
Figure 3: A proof in $\mathsf{Kt\Pi L}$ where
$\mathsf{\Pi}=\\{\square\square\overline{p}\vee\lozenge p\\}$.

As stated in Sec. 2, we extend the notion of an interpolant to a set of nested
sequents. In our definition of interpolants, we are interested only in duality
via cut. In particular, the relational atoms (encoding the tree shape of a
nested sequent) are not explicitly represented in the interpolants since they
can be recovered from the contexts of the sequents in which the interpolants
are used. We therefore define a flat sequent to be a sequent without
relational atoms. For classical tense logic, a flat sequent is thus a multiset
of labelled formulas.

######  Definition 3.5.

An interpolant, denoted $\mathcal{I}$, is a set of flat sequents.

For example, the set below is an interpolant in our context:

$\\{({}\vdash{x:A,y:B,z:W}),({}\vdash{x:C,y:D}),({}\vdash{u:E})\\}.$

Since our interpolant is no longer a formula, we need to define the dual of an
interpolant in order to generalise the statement of the interpolation result
to sequents. We have informally explained in Sec. 2 that duality in this case
is defined via cut. Intuitively, given an interpolant $\mathcal{I}_{1}$, its
_dual_ is any set of nested sequents $\mathcal{I}_{2}$ such that the empty
sequent can be derived from $\mathcal{I}_{1}$ and $\mathcal{I}_{2}$ using cut
(possibly with contraction). For example, given
$\mathcal{I}_{1}=\\{({}\vdash{x:A,y:B}),({}\vdash{u:C}),({}\vdash{v:D})\\}$,
there are several candidates for its dual:

$\begin{array}[]{rcl}\mathcal{I}_{2}&=&\\{({}\vdash{x:\overline{A}}),\leavevmode\nobreak\
({}\vdash{y:\overline{B},u:\overline{C},v:\overline{D}})\\}\\\
\mathcal{I}_{3}&=&\\{({}\vdash{x:\overline{A},u:\overline{C},v:\overline{D}}),\leavevmode\nobreak\
({}\vdash{y:\overline{B}})\\}\\\
\mathcal{I}_{4}&=&\\{({}\vdash{x:\overline{A},u:\overline{C}}),({}\vdash{x:\overline{A},v:\overline{D}}),({}\vdash{y:\overline{B},u:\overline{C}}),\\{y:\overline{B},v:\overline{D}\\}\\}\end{array}$

The empty sequent can be derived from $\mathcal{I}_{1}\cup{\mathcal{I}_{i}}$,
for $i=2,3,4$ using cut (and contraction, in the case of $\mathcal{I}_{4}$).
In principle, any of the dual candidates to $\mathcal{I}_{1}$ can be used, but
to make the construction of the interpolants deterministic, our definition
below will always choose $\mathcal{I}_{4}$, as it is relatively
straightforward to define as a function of $\mathcal{I}_{1}.$

######  Definition 3.6.

For an interpolant
$\mathcal{I}=\\{{}\vdash{\Lambda_{1}},\ldots,{}\vdash{\Lambda_{n}}\\}$, the
orthogonal $({\mathcal{I}})^{\bot}$ is defined as

$({\mathcal{I}})^{\bot}=\\{({}\vdash{x_{1}:\overline{A_{1}},\ldots,x_{n}:\overline{A_{n}}})\mid\forall
i\in\\{1,\dots,n\\},x_{i}:A_{i}\in\Lambda_{i}\\}.$

For example, the orthogonal of
$\mathcal{I}=\\{({}\vdash{x:A,y:B}),({}\vdash{x:C,z:D})\\}$ is

$({\mathcal{I}})^{\bot}=\\{({}\vdash{x:\overline{A},x:\overline{C}}),({}\vdash{x:\overline{A},z:\overline{D}}),({}\vdash{y:\overline{B},x:\overline{C}}),({}\vdash{y:\overline{B},z:\overline{D}})\\}.$

######  Definition 3.7.

Let $\mathcal{I}$ be the interpolant

$\\{({}\vdash{\Delta_{1},y:B_{1,1},\ldots,y:B_{1,k_{1}}}),\ldots,({}\vdash{\Delta_{n},y:B_{n,1},\ldots,y:B_{n,k_{n}}})\\}$

where $y$ does not occur in $\Delta_{1},\ldots,\Delta_{n}$ and define

$[?]\mathcal{I}^{y}_{x}:=\\{({}\vdash{\Delta_{1},x:[?]\bigvee_{j=1}^{k_{1}}B_{1,j}}),\ldots,({}\vdash{\Delta_{n},x:[?]\bigvee_{j=1}^{k_{n}}B_{n,j}})\\}$

where an empty disjunction is $\bot$.

######  Definition 3.8.

We define an _interpolation sequent_ to be a syntactic object of the form
${\mathcal{R},\Gamma_{1}\mid\Gamma_{2}}\vdash{\Delta_{1}\mid\Delta_{2}}\mathrel{\|}{\mathcal{I}}$,
where $\mathcal{R}$ is a set of relational atoms, $\Gamma_{i}$ and
$\Delta_{i}$ are multisets of labelled formulae (for $i\in\\{1,2\\}$), and
$\mathcal{I}$ is an interpolant. Note that in the interpolation calculus
$\mathsf{Kt\Pi LI}$, $\Gamma_{1}=\Gamma_{2}=\emptyset$ (see Fig. 4).

The vertical bar $\mid$ in an interpolation sequent marks where the sequent
will be partitioned, with the left partition serving as the antecedent and the
right partition serving as the consequent in the interpolation statement. For
example, the initial interpolation sequent shown below left splits into the
two sequents shown below right

$\mathcal{R}\vdash\Gamma\mid x:p,x:\overline{p},\Delta\mathrel{\|}\\{(\vdash
x:\top)\\}\qquad(\mathcal{R}\vdash\Gamma,x:\top)\qquad(\mathcal{R}\vdash
x:\bot,x:p,x:\overline{p},\Delta)$

where the first member $\Gamma$ of the split is placed in the left sequent and
the second member $x:p,x:\overline{p},\Delta$ is placed in the right sequent
(note that the relational atoms $\mathcal{R}$ are inherited by both sequents).
We think of the interpolant $x:\top$ as being _implied by_ the left sequent,
and so, we place it in the left sequent, and we think of the interpolant as
_implying_ the right sequent, so we place its negation (viz. $x:\bot$) in the
right sequent. Observe that an application of $cut_{1}$ between the two
sequents, yields $\mathcal{R}\vdash\Gamma,x:\overline{p},x:p,\Delta$ without
the interpolant. Performing a $cut_{1}$ in this way _syntactically
establishes_ (without evoking the semantics) that the interpolant is indeed an
interpolant (so long as the interpolant satisfies certain other properties;
cf. Lem. 3.12 below).

The interpolation calculus $\mathsf{Kt\Pi LI}$ (Fig. 4) uses interpolation
sequents. More importantly, the calculus succinctly represents our algorithm
for constructing interpolants. Most of the rules are straightforward
counterparts of the proof system in Fig. 2, except for the orthogonality rule
$orth.$ The orthogonality rule is arguably the most novel aspect of our
interpolation calculus, as it imposes a strong requirement on our generalised
notion of interpolants, that it must respect the underlying duality in the
logic. The key to the correctness of this rule is given in the Persistence
Lemma below, which shows that double-orthogonal transformation always retains
some sequents in the original interpolant.

######  Lemma 3.9 (Persistence).

If ${}\vdash{\Lambda}\in({({\mathcal{I}})^{\bot}})^{\bot}$, then there exists
a ${}\vdash{\Lambda^{\prime}}\in\mathcal{I}$ such that
$\Lambda^{\prime}\subseteq\Lambda.$

######  Proof 3.10.

Suppose otherwise, i.e., there exists
${}\vdash{\Lambda}\in({({\mathcal{I}})^{\bot}})^{\bot}$ such that for all
${}\vdash{\Lambda^{\prime}}\in\mathcal{I}$, we have
$\Lambda^{\prime}\not\subseteq\Lambda.$ Suppose
$\mathcal{I}=\\{{}\vdash{\Lambda_{1}},\ldots,{}\vdash{\Lambda_{n}}\\}.$ Then
for each $i$, there must be a labelled formula $x_{i}:A_{i}\in\Lambda_{i}$
such that $x_{i}:A_{i}\not\in\Lambda.$ Let
$\Theta=\\{x_{1}:A_{1},\ldots,x_{n}:A_{n}\\}.$ By construction, we must have
that $\Theta\cap\Lambda=\emptyset.$ However, by Def. 3.6, we have
$\overline{\Theta}\in({\mathcal{I}})^{\bot}$, and since
$\Lambda\in({({\mathcal{I}})^{\bot}})^{\bot}$, by Def. 3.6,
$\Theta\cap\Lambda\not=\emptyset$. Contradiction.

${\mathcal{R}}\vdash{\Gamma,x:\bar{p}\mid
x:{p},\Delta}\mathrel{\|}{\\{({}\vdash{x:p})\\}}\quad{\mathcal{R}}\vdash{\Gamma\mid
x:\bar{p},x:p,\Delta}\mathrel{\|}{\\{({}\vdash{x:\top})\\}}\quad{\mathcal{R}}\vdash{\Delta\mid\Gamma}\mathrel{\|}{({\mathcal{I}})^{\bot}}{\mathcal{R}}\vdash{\Gamma\mid\Delta}\mathrel{\|}{\mathcal{I}}$

${\mathcal{R}}\vdash{\Gamma\mid x:A\lor
B,\Delta}\mathrel{\|}{\mathcal{I}}{\mathcal{R}}\vdash{\Gamma\mid
x:A,x:B,\Delta}\mathrel{\|}{\mathcal{I}}\qquad{\mathcal{R}}\vdash{\Gamma\mid
x:A\land
B,\Delta}\mathrel{\|}{\mathcal{I}_{1}\cup\mathcal{I}_{2}}\lx@proof@logical@and{\mathcal{R}}\vdash{\Gamma\mid
x:A,\Delta}\mathrel{\|}{\mathcal{I}_{1}}{\mathcal{R}}\vdash{\Gamma\mid
x:B,\Delta}\mathrel{\|}{\mathcal{I}_{2}}$

${\mathcal{R}}\vdash{\Gamma\mid x:\lozenge
A,\Delta}\mathrel{\|}{\mathcal{I}}{\mathcal{R}}\vdash{\Gamma\mid x:\lozenge
A,y:A,\Delta}\mathrel{\|}{\mathcal{I}}\qquad{\mathcal{R}}\vdash{\Gamma\mid
x:\square
A,\Delta}\mathrel{\|}{\square\mathcal{I}^{y}_{x}}{\mathcal{R},Rxy}\vdash{\Gamma\mid
y:A,\Delta}\mathrel{\|}{\mathcal{I}}$

${\mathcal{R}}\vdash{\Gamma\mid x:\blacklozenge
A,\Delta}\mathrel{\|}{\mathcal{I}}{\mathcal{R}}\vdash{\Gamma\mid
x:\blacklozenge
A,y:A,\Delta}\mathrel{\|}{\mathcal{I}}\qquad{\mathcal{R}}\vdash{\Gamma\mid
x:\blacksquare
A,\Delta}\mathrel{\|}{\blacksquare\mathcal{I}^{y}_{x}}{\mathcal{R},Ryx}\vdash{\Gamma\mid
y:A,\Delta}\mathrel{\|}{\mathcal{I}}$

Figure 4: Calculus $\mathsf{Kt\Pi LI}$ for constructing interpolants for
$\mathsf{Kt}$ extended with path axioms $\mathsf{\Pi}$.

Given a formula $A$, we define the set of propositional variables $var(A)$ of
$A$ to be the set $\\{p\ |\ p\text{ or }\overline{p}\text{ in }A\\}$. This
notation extends straightforwardly to sets of formulae and interpolants.

We write ${\mathcal{R}}\Vdash{\Gamma,\Delta}$ to denote that the sequent
${\mathcal{R}}\vdash{\Gamma,\Delta}$ is provable in $\mathsf{Kt\Pi L}$.
Similarly, ${\mathcal{R}}\Vdash{\Gamma\mid\Delta}\mathrel{\|}{\mathcal{I}}$
denotes that the sequent
${\mathcal{R}}\vdash{\Gamma\mid\Delta}\mathrel{\|}{\mathcal{I}}$ is provable
in $\mathsf{Kt\Pi LI}.$

######  Definition 3.11.

A logic has the Craig interpolation property iff for every implication
$A\Rightarrow B$ in the logic, there is a formula $C$ such that (i)
$var(C)\subseteq var(A)\cap var(B)$ and (ii) $A\Rightarrow C$ and
$C\Rightarrow B$ are in the logic, where $\Rightarrow$ is taken to be the
implication connective of the logic.

We now establish that each tense logic $\mathsf{Kt\Pi}$ possess the Craig
interpolation property when the implication connective is taken to be
$\rightarrow$. To achieve this, we begin by showing that an interpolant
sequent can be constructed from any cut-free proof.

######  Lemma 3.12.

If ${\mathcal{R}}\Vdash{\Gamma,\Delta}$, then there exists an $\mathcal{I}$
such that ${\mathcal{R}}\Vdash{\Gamma\mid\Delta}\mathrel{\|}{\mathcal{I}}$,
$var(\mathcal{I})\subseteq var(\Gamma)\cap var(\Delta)$, and all labels
occuring in $\mathcal{I}$ also occur in $\mathcal{R},\Gamma$ or $\Delta$.

######  Proof 3.13.

Induction on the height of the proof of ${\mathcal{R}}\vdash{\Gamma,\Delta}$
and by using the rules of $\mathsf{Kt\Pi LI}$.

The next lemma establishes the correctness of the interpolants constructed
from our interpolation calculus in Fig. 4. Its proof can be found in App.
B.10.

######  Lemma 3.14.

For all $\mathcal{R},\Gamma,\Delta$ and $\mathcal{I}$, if
${\mathcal{R}}\Vdash{\Gamma\mid\Delta}\mathrel{\|}{\mathcal{I}}$, then

  1. 1.

For all $({}\vdash{\Lambda})\in\mathcal{I},$ we have
${\mathcal{R}}\Vdash{\Gamma,\Lambda}$ and

  2. 2.

For all $({}\vdash{\Theta})\in({\mathcal{I}})^{\bot}$, we have
${\mathcal{R}}\Vdash{\Theta,\Delta}.$

To prove Craig interpolation, we need to construct formula interpolants. Lem.
3.14 provides sequent interpolants, so the next step is to show how one can
derive a formula interpolant from a sequent interpolant. This is possible if
the formulas in an interpolant are all prefixed with the same label. In that
case, there is a straightforward interpretation of the interpolant as a
formula. More precisely, let
$\mathcal{I}=\\{({}\vdash{\Lambda_{1}}),\ldots,({}\vdash{\Lambda_{n}})\\}$,
where $\Lambda_{i}=\\{x:A_{i,1},\ldots,x:A_{i,k_{i}}\\}$ for all $1\leq i\leq
n$. Then, its formula interpretation is given by
$\bigwedge_{i=1}^{n}\bigvee_{j=1}^{k_{i}}A_{i,j}.$ Given such an interpolant
$\mathcal{I}$, we write $\bigwedge\bigvee\mathcal{I}$ to denote its formula
interpretation. The following lemma is a straightforward consequence of this
interpretation.

######  Lemma 3.15.

Let $\mathcal{I}=\\{{}\vdash{\Lambda_{1}},\ldots,{}\vdash{\Lambda_{n}}\\}$ be
an interpolant with $\Lambda_{i}=\\{x:A_{i,1},\ldots,x:A_{i,k_{i}}\\}$ for
each $1\leq i\leq n$. For any multiset of relational atoms $\mathcal{R}$ and
multiset of labelled formulae $\Gamma$, if
${\mathcal{R}}\Vdash{\Gamma,\Lambda}$ for all
${}\vdash{\Lambda}\in{\mathcal{I}}$, then
${\mathcal{R}}\Vdash{\Gamma,x:\bigwedge\bigvee\mathcal{I}}$.

However, the formula-interpolant derived in Lem. 3.15 gives only one-half of
the full picture, as one still needs to show that the orthogonal of a sequent
interpolant admits a dual interpretation as a formula. A key to this is the
following Duality Lemma that shows that orthogonality behaves like negation.

######  Lemma 3.16 (Duality).

Given an interpolant $\mathcal{I}$, the empty sequent is derivable from
$\mathcal{I}\cup({\mathcal{I}})^{\bot}$ using the $cut_{1}$ rule and the
contraction rule.

An interesting consequence of Duality Lemma is that it translates into duality
in the above formula interpretation as well, as made precise in the following
lemma.

######  Lemma 3.17.

Let $\mathcal{I}=\\{{}\vdash{\Lambda_{1}},\ldots,{}\vdash{\Lambda_{n}}\\}$ be
an interpolant with $\Lambda_{i}=\\{x:A_{i,1},\ldots,x:A_{i,k_{i}}\\}$ for
each $1\leq i\leq n$. For any multiset of relational atoms $\mathcal{R}$ and
multiset of labelled formulae $\Delta$, if
${\mathcal{R}}\Vdash{{\Theta},\Delta}$ for all
${}\vdash{\Theta}\in({\mathcal{I}})^{\bot}$, then
${\mathcal{R}}\Vdash{x:\overline{\bigwedge\bigvee\mathcal{I}},\Delta}$.

######  Proof 3.18.

Suppose
$({\mathcal{I}})^{\bot}=\\{({}\vdash{\Theta_{1}}),\ldots,({}\vdash{\Theta_{k}})\\}$
for some $k.$ By Lem. 3.16, we have a derivation $\Xi_{1}$ of the empty
sequent from assumptions $\mathcal{I}\cup({\mathcal{I}})^{\bot}$.

${}\vdash{}\vdots{}\vdash{\Lambda_{1}}\quad\cdots{}\vdash{\Lambda_{n}}\qquad{}\vdash{\Theta_{1}}\quad\cdots\quad{}\vdash{\Theta_{k}}$

Due to admissibility of weakening (Lem. 3.2), for each $\Lambda_{i}$, there is
a proof $\Psi_{i}$ of the sequent
${\mathcal{R}}\vdash{\Lambda_{i},x:\overline{\bigwedge\bigvee\mathcal{I}}}$.
Adding $x:\overline{\bigwedge\bigvee\mathcal{I}}$ to every leaf sequent in
$\Xi_{1}$ belonging to $\mathcal{I}$ gives us a derivation $\Xi_{2}$:

${\mathcal{R}}\vdash{x:\overline{\bigwedge\bigvee\mathcal{I}}}{\mathcal{R}}\vdash{(x:\overline{\bigwedge\bigvee\mathcal{I}})^{*}}\vdots[{\mathcal{R}}\vdash{x:F,\Lambda_{1}}]\quad\cdots\quad[{\mathcal{R}}\vdash{x:F,\Lambda_{n}}]\qquad{\mathcal{R}}\vdash{\Theta_{1}}\quad\cdots\quad{\mathcal{R}}\vdash{\Theta_{k}}$

where $F=\overline{\bigwedge\bigvee\mathcal{I}}$ and sequents in brackets are
provable, and where $*$ denotes multiple copies of sequents or rules. By the
assumption we know that each ${\mathcal{R}}\vdash{\Theta_{i},\Delta}$ is
provable, so by adding $\Delta$ to each premise sequent in $\Xi_{2}$, we get
the following proof:

${\mathcal{R}}\vdash{x:\overline{\bigwedge\bigvee\mathcal{I}},\Delta}{\mathcal{R}}\vdash{(x:\overline{\bigwedge\bigvee\mathcal{I}})^{*},\Delta^{*}}\vdots[{\mathcal{R}}\vdash{x:F,\Lambda_{1},\Delta}]\quad\cdots\quad[{\mathcal{R}}\vdash{x:F,\Lambda_{n},\Delta}]\qquad[{\mathcal{R}}\vdash{\Theta_{1},\Delta}]\quad\cdots\quad[{\mathcal{R}}\vdash{\Theta_{k},\Delta}]$

######  Theorem 3.19.

If ${}\Vdash{x:A\rightarrow B}$, then there exists a $C$ such that (i)
$var(C)\subseteq var(A)\cap var(B)$ and (ii) ${}\Vdash{x:A\rightarrow C}$ and
${}\Vdash{x:C\rightarrow B}$.

######  Corollary 3.20.

Every extension of the (minimal) tense logic $\mathsf{Kt}$ with a set
$\mathsf{\Pi}$ of path axioms has the Craig interpolation property.

######  Example 3.21.

Consider the formula given in example 3.4. By making use of its derivation in
Fig. 3, we can apply our interpolation algorithm as shown in Fig. 5 to
construct an interpolant for the formula.

${}\vdash{x:\lozenge\square q\mid
x:\square(\lozenge\overline{p}\lor\lozenge\lozenge
p)}\mathrel{\|}{\\{({}\vdash{x:\square\lozenge\lozenge\top})\\}}{Rxy}\vdash{x:\lozenge\square
q\mid y:\lozenge\overline{p}\lor\lozenge\lozenge
p}\mathrel{\|}{\\{({}\vdash{y:\lozenge\lozenge\top})\\}}{Rxy}\vdash{x:\lozenge\square
q\mid y:\lozenge\overline{p},y:\lozenge\lozenge
p}\mathrel{\|}{\\{({}\vdash{y:\lozenge\lozenge\top})\\}}{Rxy}\vdash{y:\lozenge\overline{p},y:\lozenge\lozenge
p\mid x:\lozenge\square
q}\mathrel{\|}{\\{({}\vdash{y:\square\square\bot})\\}}{Rxy}\vdash{y:\lozenge\overline{p},y:\lozenge\lozenge
p\mid x:\lozenge\square q,y:\square
q}\mathrel{\|}{\\{}({}\vdash{y:\square\square\bot})\\}{Rxy,Ryz}\vdash{y:\lozenge\overline{p},y:\lozenge\lozenge
p\mid x:\lozenge\square
q,z:q}\mathrel{\|}{\\{}({}\vdash{z:\square\bot})\\}{Rxy,Ryz}\vdash{y:\lozenge\overline{p},y:\lozenge\lozenge
p\mid x:\lozenge\square q,z:\square
q,z:q}\mathrel{\|}{\\{}({}\vdash{z:\square\bot)}\\}{Rxy,Ryz,Rzw}\vdash{y:\lozenge\overline{p},y:\lozenge\lozenge
p\mid x:\lozenge\square
q,w:q,z:q}\mathrel{\|}{\\{}({}\vdash{w:\bot})\\}{Rxy,Ryz,Rzw}\vdash{x:\lozenge\square
q,w:q,z:q\mid y:\lozenge\overline{p},y:\lozenge\lozenge
p}\mathrel{\|}{\\{}({}\vdash{w:\top})\\}{Rxy,Ryz,Rzw}\vdash{x:\lozenge\square
q,w:q,z:q\mid y:\lozenge\overline{p},w:\overline{p},y:\lozenge\lozenge
p}\mathrel{\|}{\\{}({}\vdash{w:\top})\\}{Rxy,Ryz,Rzw}\vdash{x:\lozenge\square
q,w:q,z:q\mid y:\lozenge\overline{p},w:\overline{p},y:\lozenge\lozenge
p,z:\lozenge
p}\mathrel{\|}{\\{}({}\vdash{w:\top})\\}{Rxy,Ryz,Rzw}\vdash{x:\lozenge\square
q,w:q,z:q\mid y:\lozenge\overline{p},w:\overline{p},y:\lozenge\lozenge
p,z:\lozenge p,w:p}\mathrel{\|}{\\{}({}\vdash{w:\top})\\}$ Figure 5: An
example of the construction of tense interpolants.

##  4 Interpolation for Bi-Intuitionistic Logic

The language for bi-intuitionistic logic $\mathsf{BiInt}$ is given via the
following BNF grammar:

$A::=p\ |\ \top\ |\ \bot\ |\ (A\wedge A)\ |\ (A\vee A)\ |\ (A\supset A)\ |\
(A-\\!\\!\\!<A)$

For an axiomatic definition of $\mathsf{BiInt}$ consult [21] and for a
semantic definition see [8, 19].

The calculus $\mathsf{BiIntL}$ for $\mathsf{BiInt}$ is given in Fig. 7. The
calculus makes use of sequents of the form
${\mathcal{R},\Gamma}\vdash{\Delta}$ with $\mathcal{R}$ a multiset of
relational atoms of the form $Rxy$, $\Gamma$ and $\Delta$ multisets of
labelled formulae of the form $x:A$ (where $A$ is a bi-intuitionistic
formula), and all labels are among a countable set $\\{x,y,z,\ldots\\}$. Note
that we need not restrict the consequent of sequents to at most one formula on
the right or left due to the eigenvariable condition imposed on the
$\supset_{R}$ and $-\\!\\!\\!<_{L}$ rules. Moreover, for a multiset
$\mathcal{R}$ of relational atoms or a multiset $\Gamma$ of labelled formulae,
we use the notation $\mathcal{R}[x/y]$ and $\Gamma[x/y]$ to represent the
multiset obtained by replacing each occurrence of the label $y$ for the label
$x$. The $monl$ and $monr$ rules are the natural way to capture monotonicity
when nested sequents are represented using labels.

${\mathcal{R},\Gamma,\Gamma^{\prime}}\vdash{\Delta}{\mathcal{R},\Gamma,\Gamma^{\prime},\Gamma^{\prime}}\vdash{\Delta}\quad{\mathcal{R},\Gamma}\vdash{\Delta,\Delta^{\prime}}{\mathcal{R},\Gamma}\vdash{\Delta,\Delta^{\prime},\Delta^{\prime}}\quad{\mathcal{R},\mathcal{R}^{\prime},\Gamma}\vdash{\Delta}{\mathcal{R},\mathcal{R}^{\prime},\mathcal{R}^{\prime},\Gamma}\vdash{\Delta}\quad{\mathcal{R},\Gamma}\vdash{\Delta,\Delta^{\prime}}{\mathcal{R},\Gamma}\vdash{\Delta}\quad{\mathcal{R},\Gamma,\Gamma^{\prime}}\vdash{\Delta}{\mathcal{R},\Gamma}\vdash{\Delta}$

${\mathcal{R},\mathcal{R}^{\prime},\Gamma}\vdash{\Delta}{\mathcal{R},\Gamma}\vdash{\Delta}\quad{\mathcal{R}}\vdash{\Gamma}\lx@proof@logical@and{\mathcal{R}}\vdash{\Gamma,x:A}{\mathcal{R}}\vdash{\Gamma,x:\overline{A}}\quad{\mathcal{R},\Gamma}\vdash{\Delta}\lx@proof@logical@and{\mathcal{R},\Gamma}\vdash{\Delta,x:A}{\mathcal{R},x:A,\Gamma}\vdash{\Delta}$

Figure 6: Admissible rules.

######  Lemma 4.1.

The calculus $\mathsf{BiIntL}$ enjoys the following: (1) admissibility of
$ctr$, $wk$ and $cut_{2}$ from Fig. 6; (2) invertibility of all inference
rules from Fig. 7; (3) if ${\mathcal{R},Rxy,\Gamma}\Vdash{\Delta}$, then
${\mathcal{R}[x/y],\Gamma[x/y]}\Vdash{\Delta[x/y]}$, and (4) If
${\Gamma}\Vdash{\Delta}$ where $\Gamma$ and $\Delta$ only contain formulae
solely labelled with $y$, then ${\Gamma[x/y]}\Vdash{\Delta[x/y]}$ for any
label $x$.

######  Proof 4.2.

For proofs of (1)-(4), see [19, Section 3]. Statement (4) follows from the
others.

${\mathcal{R},x:p,\Gamma}\vdash{\Delta,x:p}\qquad{\mathcal{R},\Gamma}\vdash{x:\top,\Delta}\qquad{\mathcal{R},\Gamma,x:\bot}\vdash{\Delta}$

${\mathcal{R},\Gamma,x:A\lor
B}\vdash{\Delta}\lx@proof@logical@and{\mathcal{R},\Gamma,x:A}\vdash{\Delta}{\mathcal{R},\Gamma,x:B}\vdash{\Delta}\qquad{\mathcal{R},\Gamma}\vdash{x:A\lor
B,\Delta}{\mathcal{R},\Gamma}\vdash{x:A,x:B,\Delta}\qquad{\mathcal{R},Rxy,x:A,\Gamma}\vdash{\Delta}{{\mathcal{R},Rxy,x:A,y:A,\Gamma}\vdash{\Delta}}$

${\mathcal{R},\Gamma}\vdash{x:A\land
B,\Delta}\lx@proof@logical@and{\mathcal{R},\Gamma}\vdash{x:A,\Delta}{\mathcal{R},\Gamma}\vdash{x:B,\Delta}\qquad{\mathcal{R},\Gamma,x:A\land
B}\vdash{\Delta}{\mathcal{R},\Gamma,x:A,x:B}\vdash{\Delta}\qquad{\mathcal{R},Rxy,\Gamma}\vdash{y:A,\Delta}{{\mathcal{R},Rxy,\Gamma}\vdash{x:A,y:A,\Delta}}$

${\mathcal{R},x:A-\\!\\!\\!<B,\Gamma}\vdash{\Delta}{\mathcal{R},Ryx,y:A,\Gamma}\vdash{y:B,\Delta}\quad{\mathcal{R},x:A\supset
B,\Gamma}\vdash{\Delta}\lx@proof@logical@and{\mathcal{R},x:A\supset
B,\Gamma}\vdash{x:A,\Delta}{\mathcal{R},x:B,\Gamma}\vdash{\Delta}$

${\mathcal{R},\Gamma}\vdash{x:A-\\!\\!\\!<B,\Delta}\lx@proof@logical@and{\mathcal{R},\Gamma}\vdash{x:A,\Delta}{\mathcal{R},x:B,\Gamma}\vdash{x:A-\\!\\!\\!<B,\Delta}\quad{\mathcal{R},\Gamma}\vdash{x:A\supset
B,\Delta}{\mathcal{R},Rxy,\Gamma,y:A}\vdash{y:B,\Delta}$

Figure 7: The calculus $\mathsf{BiIntL}$ for $\mathsf{BiInt}$ [19].

As in the case with tense logics, we define a generalised interpolant to be a
set of two-sided flat sequents. However, to ease the definition of orthogonal,
we shall use an encoding of two-sided sequents into single-sided sequents by
annotating the left-hand side occurrence of a formula with a $L$ and the
right-hand side occurrence with a $R$. In this way some results concerning
intuitionistic interpolants can be easily adapted from the classical
counterparts.

######  Definition 4.3.

A polarised formula is a formula annotated with $L$ (left-polarised) or $R$
(right-polarised). We write $A^{L}$ ($A^{R}$) for the left-polarised (right-
polarised) version of formula $A.$ A labelled polarised formula is a polarised
formula further annotated with a label. We write $x:A^{L}$ ($x:A^{R}$) to
denote a left-polarised (a right-polarised) formula labelled with $x.$ Given a
polarised formula $A^{L}$ (resp. $A^{R}$), its dual is defined as
$\overline{A^{L}}=A^{R}$ and $\overline{A^{R}}=A^{L}.$ That is, duality
changes polarities (the side where the formula occurs), but not the actual
formula.

######  Definition 4.4.

A polarised (flat) sequent is a single-sided (flat) sequent where all formulas
in the sequent are polarised. Given a two-sided sequent
$S={\mathcal{R},x_{1}:A_{1},\ldots,x_{m}:A_{m}}\vdash{y_{1}:B_{1},\ldots,y_{n}:B_{n}}$,
its corresponding polarised sequent is the following

${\mathcal{R}}\vdash{x_{1}:A_{1}^{L},\ldots,x_{m}:A_{m}^{L},y_{1}:B_{1}^{R},\ldots,y_{n}:B_{n}^{R}}.$

Given a two-sided sequent $S$, we denote with $\mathsf{P}(S)$ its encoding as
a polarised sequent. Conversely, given a polarised sequent $S$, we denote with
$\mathsf{T}(S)$ its two-sided counterpart. This notation extends to sets of
sequents by applying the encoding element-wise.

######  Definition 4.5.

An intuitionistic interpolant is a set of two-sided flat sequents. Given an
intuitionistic interpolant $\mathcal{I}$, its orthogonal
$({\mathcal{I}})^{\bot}$ is defined as
$\mathsf{T}(({\mathsf{P}(\mathcal{I})})^{\bot}).$

######  Example 4.6.

Let $\mathcal{I}=\\{({x:A}\vdash{y:B}),({}\vdash{u:C,v:D})\\}$. Then,
$({\mathcal{I}})^{\bot}$ is the set:

$\\{({x:A}\vdash{u:C}),({x:A}\vdash{v:D}),({}\vdash{u:C,y:B}),({}\vdash{v:D,y:B})\\}$

By defining orthogonality via the embedding into polarised sequents, the
Persistence Lemma for the intuitionistic case comes for free, by appealing to
Lem. 3.9. Note that for sequents ${\Gamma_{1}}\vdash{\Delta_{1}}$ and
${\Gamma_{2}}\vdash{\Delta_{2}}$, we write
${\Gamma_{1}}\vdash{\Delta_{1}}\subseteq{\Gamma_{2}}\vdash{\Delta_{2}}$ iff
$\Gamma_{1}\subseteq\Gamma_{2}$ and $\Delta_{1}\subseteq\Delta_{2}.$

######  Lemma 4.7 (Persistence).

If $\Lambda\in({({\mathcal{I}})^{\bot}})^{\bot}$, then there exists a
$\Lambda^{\prime}\in\mathcal{I}$ such that $\Lambda^{\prime}\subseteq\Lambda.$

######  Lemma 4.8 (Duality).

Given an intuitionistic interpolant $\mathcal{I}$, the empty sequent is
derivable from $\mathcal{I}\cup({\mathcal{I}})^{\bot}$ using the $cut_{2}$
rule and the contraction rule.

######  Proof 4.9.

Similar to Lem. 3.16.

######  Definition 4.10.

Let $\mathcal{I}$ be the interpolant below where $y$ does not occur in
$\Gamma_{1},\ldots,\Gamma_{n},\Delta_{1},\ldots,\Delta_{n}$:

$\begin{array}[]{ll}&\\{({\Gamma_{1},y:C_{1,1},\ldots,y:C_{1,k_{1}}}\vdash{\Delta_{1},y:D_{1,1},\ldots,y:D_{1,j_{1}}}),\ldots,\\\
&\hskip
5.0pt({\Gamma_{n},y:C_{n,1},\ldots,y:C_{n,k_{n}}}\vdash{\Delta_{n},y:D_{n,1},\ldots,y:D_{n,j_{n}}})\\}\\\
\end{array}$

The interpolants $-\\!\\!\\!<\mathcal{I}^{x}_{y}$ and
$\supset\mathcal{I}^{x}_{y}$ are shown below where empty conjunction denotes
$\top$ and empty disjunction denotes $\bot$:

$\displaystyle-\\!\\!\\!<\mathcal{I}^{x}_{y}$ $\displaystyle=$
$\displaystyle\\{({\Gamma_{1},x:\bigwedge^{k_{1}}_{i=1}C_{1,i}-\\!\\!\\!<\bigvee^{j_{1}}_{i=1}D_{1,i}}\vdash{\Delta_{1}}),\ldots,({\Gamma_{n},x:\bigwedge^{k_{n}}_{i=1}C_{n,i}-\\!\\!\\!<\bigvee^{j_{n}}_{i=1}D_{n,i}}\vdash{\Delta_{n}})\\}$
$\displaystyle\supset\mathcal{I}^{x}_{y}$ $\displaystyle=$
$\displaystyle\\{({\Gamma_{1}}\vdash{\Delta_{1},x:\bigwedge^{k_{1}}_{i=1}C_{1,i}\supset\bigvee^{j_{1}}_{i=1}D_{1,i}}),\ldots,({\Gamma_{n}}\vdash{\Delta_{n},x:\bigwedge^{k_{n}}_{i=1}C_{n,i}\supset\bigvee^{j_{n}}_{i=1}D_{n,i}})\\}$

The proof system $\mathsf{BiIntLI}$ for constructing intuitionistic
interpolants is given in Fig. 8.

${\mathcal{R},\Gamma_{1},x:p\mid\Gamma_{2}}\vdash{\Delta_{1}\mid
x:p,\Delta_{2}}\mathrel{\|}{\\{{}\vdash{x:p}\\}}\qquad{\mathcal{R},\Gamma_{1}\mid
x:p,\Gamma_{2}}\vdash{\Delta_{1}\mid
x:p,\Delta_{2}}\mathrel{\|}{\\{{}\vdash{x:\bot}\\}}$

${\mathcal{R},\Gamma_{1}\mid\Gamma_{2}}\vdash{\Delta_{1}\mid
x:\top,\Delta_{2}}\mathrel{\|}{\\{{}\vdash{x:\bot}\\}}\qquad{\mathcal{R},\Gamma_{1}\mid
x:\bot,\Gamma_{2}}\vdash{\Delta_{1}\mid\Delta_{2}}\mathrel{\|}{\\{{}\vdash{x:\bot}\\}}$

${\mathcal{R},\Gamma_{2}\mid\Gamma_{1}}\vdash{\Delta_{2}\mid\Delta_{1}}\mathrel{\|}{({\mathcal{I}})^{\bot}}{\mathcal{R},\Gamma_{1}\mid\Gamma_{2}}\vdash{\Delta_{1}\mid\Delta_{2}}\mathrel{\|}{\mathcal{I}}$

${\mathcal{R},Rxy,\Gamma_{1}\mid
x:A,\Gamma_{2}}\vdash{\Delta_{1}\mid\Delta_{2}}\mathrel{\|}{\mathcal{I}}{{\mathcal{R},Rxy,\Gamma_{1}\mid
x:A,y:A,\Gamma_{2}}\vdash{\Delta_{1}\mid\Delta_{2}}\mathrel{\|}{\mathcal{I}}}\qquad{{\mathcal{R},Rxy,\Gamma_{1}\mid\Gamma_{2}}\vdash{\Delta_{1}\mid
y:A,\Delta_{2}}\mathrel{\|}{\mathcal{I}}}{\mathcal{R},Rxy,\Gamma_{1}\mid\Gamma_{2}}\vdash{\Delta_{1}\mid
x:A,y:A,\Delta_{2}}\mathrel{\|}{\mathcal{I}}$

${\mathcal{R},\Gamma_{1}\mid x:A\lor
B,\Gamma_{2}}\vdash{\Delta_{1}\mid\Delta_{2}}\mathrel{\|}{\mathcal{I}_{1}\cup\mathcal{I}_{2}}\lx@proof@logical@and{\mathcal{R},\Gamma_{1}\mid
x:A,\Gamma_{2}}\vdash{\Delta_{1}\mid\Delta_{2}}\mathrel{\|}{\mathcal{I}_{1}}{\mathcal{R},\Gamma_{1}\mid
x:B,\Gamma_{2}}\vdash{\Delta_{1}\mid\Delta_{2}}\mathrel{\|}{\mathcal{I}_{2}}$

${\mathcal{R},\Gamma_{1}\mid\Gamma_{2}}\vdash{\Delta_{1}\mid x:A\land
B,\Delta_{2}}\mathrel{\|}{\mathcal{I}_{1}\cup\mathcal{I}_{2}}\lx@proof@logical@and{\mathcal{R},\Gamma_{1}\mid\Gamma_{2}}\vdash{\Delta_{1}\mid
x:A,\Delta_{2}}\mathrel{\|}{\mathcal{I}_{1}}{\mathcal{R},\Gamma_{1}\mid\Gamma_{2}}\vdash{\Delta_{1}\mid
x:B,\Delta_{2}}\mathrel{\|}{\mathcal{I}_{2}}$

${\mathcal{R},\Gamma_{1}\mid x:A\land
B,\Gamma_{2}}\vdash{\Delta_{1}\mid\Delta_{2}}\mathrel{\|}{\mathcal{I}}{\mathcal{R},\Gamma_{1}\mid
x:A,x:B,\Gamma_{2}}\vdash{\Delta_{1}\mid\Delta_{2}}\mathrel{\|}{\mathcal{I}}\qquad{\mathcal{R},\Gamma_{1}\mid\Gamma_{2}}\vdash{\Delta_{1}\mid
x:A\lor
B,\Delta_{2}}\mathrel{\|}{\mathcal{I}}{\mathcal{R},\Gamma_{1}\mid\Gamma_{2}}\vdash{\Delta_{1}\mid
x:A,x:B,\Delta_{2}}\mathrel{\|}{\mathcal{I}}$

${\mathcal{R},\Gamma_{1}\mid x:A\supset
B,\Gamma_{2}}\vdash{\Delta_{1}\mid\Delta_{2}}\mathrel{\|}{\mathcal{I}_{1}\cup\mathcal{I}_{2}}\lx@proof@logical@and{\mathcal{R},\Gamma_{1}\mid
x:A\supset B,\Gamma_{2}}\vdash{\Delta_{1}\mid
x:A,\Delta_{2}}\mathrel{\|}{\mathcal{I}_{2}}{\mathcal{R},\Gamma_{1}\mid
x:B,\Gamma_{1}}\vdash{\Delta_{1}\mid\Delta_{2}}\mathrel{\|}{\mathcal{I}_{1}}$

${\mathcal{R},\Gamma_{1}\mid\Gamma_{2}}\vdash{\Delta_{1}\mid
x:A-\\!\\!\\!<B,\Delta_{2}}\mathrel{\|}{\mathcal{I}_{1}\cup\mathcal{I}_{2}}\lx@proof@logical@and{\mathcal{R},\Gamma_{1}\mid\Gamma_{2}}\vdash{\Delta_{1}\mid
x:A,\Delta_{2}}\mathrel{\|}{\mathcal{I}_{1}}{\mathcal{R},\Gamma_{1}\mid
x:B,\Gamma_{2}}\vdash{\Delta_{1},x:A-\\!\\!\\!<B\mid\Delta_{2}}\mathrel{\|}{\mathcal{I}_{2}}$

${\mathcal{R},\Gamma_{1}\mid
x:A-\\!\\!\\!<B,\Gamma_{2}}\vdash{\Delta_{1}\mid\Delta_{2}}\mathrel{\|}{-\\!\\!\\!<\mathcal{I}^{y}_{x}}{\mathcal{R},Ryx,\Gamma_{1}\mid
y:A,\Gamma_{2}}\vdash{\Delta_{1}\mid
y:B,\Delta_{2}}\mathrel{\|}{\mathcal{I}}\qquad{\mathcal{R},\Gamma_{1}\mid\Gamma_{2}}\vdash{\Delta_{1}\mid
x:A\supset
B,\Delta_{2}}\mathrel{\|}{\supset\mathcal{I}^{y}_{x}}{\mathcal{R},Rxy,\Gamma_{1}\mid
y:A,\Gamma_{2}}\vdash{\Delta_{1}\mid y:B,\Delta_{2}}\mathrel{\|}{\mathcal{I}}$

Figure 8: The calculus $\mathsf{BiIntLI}$ used to compute interpolants for
$\mathsf{BiInt}$. In $\supset_{R}$ and $-\\!\\!\\!<_{L}$, $y$ is fresh.

######  Lemma 4.11.

If ${\mathcal{R},\Gamma_{1},\Gamma_{2}}\Vdash{\Delta_{1},\Delta_{2}}$, then
there exists an $\mathcal{I}$ such that
${\mathcal{R},\Gamma_{1}\mid\Gamma_{2}}\Vdash{\Delta_{1}\mid\Delta_{2}}\mathrel{\|}{\mathcal{I}}$,
$var(\mathcal{I})\subseteq var(\Gamma_{1},\Delta_{1})\cap
var(\Gamma_{2},\Delta_{2})$, and all labels in $\mathcal{I}$ also occur in
$\mathcal{R},\Gamma_{1},\Delta_{1}$ or $\Gamma_{2},\Delta_{2}$.

######  Proof 4.12.

Induction on the height of the proof of
${\mathcal{R},\Gamma_{1},\Gamma_{2}}\vdash{\Delta_{1},\Delta_{2}}$ using rules
of $\mathsf{BiIntLI}$.

The main technical lemma below asserts that the interpolants constructed via
the proof system in Fig. 8 obey duality properties which are essential for
proving the main theorem (Thm. 4.17). The proof of this lemma can be found in
App. B.10.

######  Lemma 4.13.

For all $\mathcal{R},\Gamma_{1},\Gamma_{2},\Delta_{1},\Delta_{2}$ and
$\mathcal{I}$, if
${\mathcal{R},\Gamma_{1}\mid\Gamma_{2}}\Vdash{\Delta_{1}\mid\Delta_{2}}\mathrel{\|}{\mathcal{I}}$,
then

  1. 1.

For all $({\Sigma}\vdash{\Theta})\in\mathcal{I}$, we have
${\mathcal{R},\Gamma_{1},\Sigma}\Vdash{\Theta,\Delta_{1}}$ and

  2. 2.

For all $({\Lambda}\vdash{\Omega})\in({\mathcal{I}})^{\bot}$, we have
${\mathcal{R},\Gamma_{2},\Lambda}\Vdash{\Omega,\Delta_{2}}.$

Given a sequent $\Lambda$, we denote with $\Lambda^{L}$ (resp., $\Lambda^{R}$)
the multiset of labelled formulas on the left (resp. right) hand side of
$\Lambda$. The following two lemmas are counterparts of Lem. 3.15 and Lem.
3.17. Lem. 4.14 essentially states that in a specific case, an interpolant can
be interpreted straightforwardly as a conjunction of implications. Its proof
is given in App. B.10. The proof of Lem. 4.15 follows the same pattern as in
the proof of Lem. 3.17.

######  Lemma 4.14.

Let
$\mathcal{I}=\\{({\Sigma_{1}}\vdash{\Theta_{1}}),\ldots,({\Sigma_{n}}\vdash{\Theta_{n}})\\}$
be an interpolant with

$({\Sigma_{i}}\vdash{\Theta_{i}})=({x:C_{i,1},\ldots,x:C_{i,k_{i}}}\vdash{x:D_{i,1},\ldots,x:D_{i,j_{i}}})\mbox{
for each }1\leq i\leq n.$

If ${\Sigma_{i},\Gamma}\Vdash{\Theta_{i}}$, for all
$({\Sigma_{i}}\vdash{\Theta_{i}})\in\mathcal{I}$, and every formula in
$\Gamma$ is labelled with $x$, then

${\Gamma}\Vdash{x:\bigwedge_{i=1}^{n}(\bigwedge_{m=1}^{k_{i}}C_{i,m}\supset\bigvee_{m=1}^{j_{i}}D_{i,m}}).$

######  Lemma 4.15.

Let
$\mathcal{I}=\\{({\Sigma_{1}}\vdash{\Theta_{1}}),\ldots,({\Sigma_{n}}\vdash{\Theta_{n}})\\}$
be an interpolant with

$({\Sigma_{i}}\vdash{\Theta_{i}})=({x:C_{i,1},\ldots,x:C_{i,k_{i}}}\vdash{x:D_{i,1},\ldots,x:D_{i,j_{i}}})\mbox{
for each }1\leq i\leq n.$

If ${\mathcal{R},\Sigma_{i},\Gamma}\Vdash{\Delta,\Theta_{i}}$ for all
$({\Sigma_{i}}\vdash{\Theta_{i}})\in({\mathcal{I}})^{\bot}$, then

${\mathcal{R},\Gamma,x:\bigwedge_{i=1}^{n}(\bigwedge_{m=1}^{k_{i}}C_{i,m}\supset\bigvee_{m=1}^{j_{i}}D_{i,m})}\Vdash{\Delta.}$

######  Proof 4.16.

Follows from Lem. 4.8 and is similar to Lem. 3.17.

######  Theorem 4.17.

If ${}\Vdash{x:A\supset B}$, then there exists a $C$ such that (i)
$var(C)\subseteq var(A)\cap var(B)$ and (ii) ${}\Vdash{x:A\supset C}$ and
${}\Vdash{x:C\supset B}$.

######  Corollary 4.18.

The logic $\mathsf{BiInt}$ has the Craig interpolation property.

##  5 Conclusion and Future work

We have presented a novel approach to proving the interpolation theorem for a
range of logics possessing a nested sequent calculus. The key insight in our
approach is the generalisation of the interpolation theorem to allow sets of
sequents as interpolants. There is a natural definition of duality between
interpolants via cut. We have shown that our method can be used to prove
interpolation for logics for which interpolation was known to be difficult to
prove.

We intend on applying our approach to prove interpolation for bi-
intuitionistic linear logic (BiILL) [4]. Unlike tense logics and bi-
intuitionistic logic, there is no obvious Kripke semantics for BiILL, so
Kuznets et. al.’s approach is not immediately applicable, and it seems a
proof-theoretic approach like ours would offer some advantage. We conjecture
that the key insight in our work, i.e., the generalisation of interpolants to
sets of sequents and the use of orthogonality to define duality between
interpolants, can be extended to the linear logic setting; for example, via a
similar notion of orthogonality as in multiplicative linear logic [5].

## References

  * [1] Kai Brünnler.  Deep sequent systems for modal logic.  Arch. Math. Log., 48(6):551–577, 2009.
  * [2] Agata Ciabattoni, Nikolaos Galatos, and Kazushige Terui.  From axioms to analytic rules in nonclassical logics.  In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA, pages 229–240, 2008.  URL: https://doi.org/10.1109/LICS.2008.39, doi:10.1109/LICS.2008.39.
  * [3] Agata Ciabattoni, Tim Lyon, and Revantha Ramanayake.  From display to labelled proofs for tense logics.  In Sergei Artemov and Anil Nerode, editors, Logical Foundations of Computer Science, pages 120–139, Cham, 2018. Springer International Publishing.
  * [4] Ranald Clouston, Jeremy E. Dawson, Rajeev Goré, and Alwen Tiu.  Annotation-free sequent calculi for full intuitionistic linear logic.  In Computer Science Logic 2013 (CSL 2013), CSL 2013, September 2-5, 2013, Torino, Italy, volume 23 of LIPIcs, pages 197–214. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013.  URL: https://doi.org/10.4230/LIPIcs.CSL.2013.197, doi:10.4230/LIPIcs.CSL.2013.197.
  * [5] Vincent Danos and Laurent Regnier.  The structure of multiplicatives.  Arch. Math. Log., 28(3):181–203, 1989.  URL: https://doi.org/10.1007/BF01622878, doi:10.1007/BF01622878.
  * [6] Melvin Fitting and Roman Kuznets.  Modal interpolation via nested sequents.  Ann. Pure Appl. Logic, 166(3):274–305, 2015.  URL: https://doi.org/10.1016/j.apal.2014.11.002, doi:10.1016/j.apal.2014.11.002.
  * [7] Rajeev Goré.  Substructural logics on display.  Logic Journal of the IGPL, 6(3):451–504, 1998.
  * [8] Rajeev Goré, Linda Postniece, and Alwen Tiu.  Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents.  In Advances in Modal Logic 7, papers from the seventh conference on "Advances in Modal Logic," held in Nancy, France, 9-12 September 2008, pages 43–66, 2008.  URL: http://www.aiml.net/volumes/volume7/Gore-Postniece-Tiu.pdf.
  * [9] Rajeev Goré, Linda Postniece, and Alwen Tiu.  On the correspondence between display postulates and deep inference in nested sequent calculi for tense logics.  Log. Methods Comput. Sci., 7(2):2:8, 38, 2011.
  * [10] Ryo Kashima.  Cut-free sequent calculi for some tense logics.  Studia Logica, 53(1):119–136, 1994.  URL: https://doi.org/10.1007/BF01053026, doi:10.1007/BF01053026.
  * [11] Hitoshi Kihara and Hiroakira Ono.  Interpolation properties, Beth definability properties and amalgamation properties for substructural logics.  Journal of Logic and Computation, 20(4), August 2010.
  * [12] Tomasz Kowalski and Hiroakira Ono.  Analytic cut and interpolation for bi-intuitionistic logic.  Rew. Symb. Logic, 10(2):259–283, 2017.  URL: https://doi.org/10.1017/S175502031600040X, doi:10.1017/S175502031600040X.
  * [13] Roman Kuznets.  Multicomponent proof-theoretic method for proving interpolation properties.  Ann. Pure Appl. Logic, 169(12):1369–1418, 2018.
  * [14] Roman Kuznets and Björn Lellmann.  Interpolation for intermediate logics via hyper- and linear nested sequents.  In Proc. AiML 2018. Kings College Publications, 2018.
  * [15] Carsten Lutz and Frank Wolter.  Foundations for uniform interpolation and forgetting in expressive description logics.  In IJCAI 2011, Proceedings of the 22nd International Joint Conference on Artificial Intelligence, Barcelona, Catalonia, Spain, July 16-22, 2011, pages 989–995, 2011.  URL: https://doi.org/10.5591/978-1-57735-516-8/IJCAI11-170, doi:10.5591/978-1-57735-516-8/IJCAI11-170.
  * [16] S. Maehara.  Craig no interpolation theorem (in japanese).  Suugaku, 12:235–237, 1960.
  * [17] Kenneth L. McMillan.  Interpolation and model checking.  In Handbook of Model Checking, pages 421–446. Springer, 2018.
  * [18] Sara Negri.  Proof analysis in modal logic.  J. Philosophical Logic, 34(5-6):507–544, 2005.
  * [19] Luís Pinto and Tarmo Uustalu.  A proof-theoretic study of bi-intuitionistic propositional sequent calculus.  J. Log. Comput., 28(1):165–202, 2018.  URL: https://doi.org/10.1093/logcom/exx044, doi:10.1093/logcom/exx044.
  * [20] Francesca Poggiolesi.  A cut-free simple sequent calculus for modal logic S5.  Rew. Symb. Logic, 1(1):3–15, 2008.  URL: https://doi.org/10.1017/S1755020308080040, doi:10.1017/S1755020308080040.
  * [21] Cecylia Rauszer.  An algebraic and Kripke-style approach to a certain extension of intuitionistic logic.  Instytut Matematyczny Polskiej Akademi Nauk, 1980.  URL: http://eudml.org/doc/268511.
  * [22] Balder ten Cate, Enrico Franconi, and Inanç Seylan.  Beth definability in expressive description logics.  J. Artif. Intell. Res., 48:347–414, 2013.
  * [23] Alwen Tiu, Egor Ianovski, and Rajeev Goré.  Grammar logics in nested sequent calculus: Proof theory and decision procedures.  In Advances in Modal Logic 9, papers from the ninth conference on "Advances in Modal Logic," held in Copenhagen, Denmark, 22-25 August 2012, pages 516–537, 2012.  URL: http://www.aiml.net/volumes/volume9/Tiu-Ianovski-Gore.pdf.
  * [24] Anne Troesltra and Helmut Schwichtenberg.  Basic Proof Theory.  CUP, 1996.

##  Appendix A Definition of $\mathcal{R}^{{\sf\Pi}}$

In this appendix we define the relation $\mathcal{R}^{{\sf\Pi}}$ that is used
as a side condition in the $\lozenge$ and $\blacklozenge$ rules in
$\mathsf{Kt\Pi L}$. Concepts needed for the definition are defined first
followed by the definition of the relation.

######  Definition A.1 (Path Axiom Inverse [9]).

Let $\langle?\rangle^{-1}=\lozenge$ if $\langle?\rangle=\blacklozenge$, and
$\langle?\rangle^{-1}=\blacklozenge$, if $\langle?\rangle=\lozenge$. If $F$ is
a path axiom of the form below left, then we define the _inverse of $F$_
(denoted $I(F)$) to be the axiom below right:

$\langle?\rangle_{F_{1}}\cdots\langle?\rangle_{F_{n}}p\rightarrow\langle?\rangle_{F}p\qquad
I(F)=\langle?\rangle^{-1}_{F_{n}}\cdots\langle?\rangle^{-1}_{F_{1}}p\rightarrow\langle?\rangle^{-1}_{F}p$

Given a set of path axioms ${\sf\Pi}$, we define the _set of inverses_ to be
the set $I({\sf\Pi})=\\{I(F)|F\in{\sf\Pi}\\}$.

######  Definition A.2 (Composition of Path Axioms [9]).

Given two path axioms

${F=\langle?\rangle_{F_{1}}\cdots\langle?\rangle_{F_{n}}p\rightarrow\langle?\rangle_{F}p\qquad
G=\langle?\rangle_{G_{1}}\cdots\langle?\rangle_{G_{m}}p\rightarrow\langle?\rangle_{G}p}$

we say _$F$ is composable with $G$ at $i$_ iff
$\langle?\rangle_{F}=\langle?\rangle_{G_{i}}$.

We define the _composition_

$F\triangleright^{i}G=\langle?\rangle_{G_{1}}\cdots\langle?\rangle_{G_{i-1}}\langle?\rangle_{F_{1}}\cdots\langle?\rangle_{F_{n}}\langle?\rangle_{G_{i+1}}\cdots\langle?\rangle_{G_{m}}p\rightarrow\langle?\rangle_{G}p$

when $F$ is composable with $G$ at $i$.

Using these individual compositions, we define the following _set of
compositions_ :

$F\triangleright G=\\{F\triangleright^{i}G\ |\ \text{F is composable with G at
$i$}\\}$

######  Definition A.3 (Completion [9]).

The _completion_ of a set ${\sf\Pi}$ of path axioms, written ${\sf\Pi}^{*}$,
is the smallest set of path axioms containing ${\sf\Pi}$ such that:

  * •

$\lozenge p\rightarrow\lozenge p,\blacklozenge p\rightarrow\blacklozenge
p\in{\sf\Pi}^{*}$;

  * •

If $F,G\in{\sf\Pi}^{*}$ and $F$ is composable with $G$ for some $i$, then
$F\triangleright G\subseteq{\sf\Pi}^{*}$.

######  Definition A.4 (Propagation Graph).

Let ${\mathcal{R}}\vdash{\Gamma}$ be a labelled sequent where $N$ is the set
of labels occurring in the sequent. We define the _propagation graph
$PG({\mathcal{R}}\vdash{\Gamma})=(N,E,L)$_ to be the directed graph with the
set of nodes $N$, and where the set of edges $E$ and function $L$ that labels
edges with either a $\lozenge$ or $\blacklozenge$ are defined as follows: For
every $Rxy\in\mathcal{R}$, we have an edge $(x,y)\in E$ with $L(x,y)=\lozenge$
and an edge $(y,x)\in E$ with $L(y,x)=\blacklozenge$.

######  Definition A.5 (Path [9]).

A _path_ is a sequence of nodes and diamonds (labelling edges) of the form:

$x_{1},\langle?\rangle_{1},x_{2},\langle?\rangle_{2},\cdots,\langle?\rangle_{n-1},x_{n}$

in the propagation graph $PG(\Gamma)$ of a sequent $\Gamma$ such that $x_{i}$
is connected to $x_{i+1}$ by an edge labelled with $\langle?\rangle_{i}$. For
a given path
$\pi=x_{1},\langle?\rangle_{1},x_{2},\langle?\rangle_{2},\cdots,\langle?\rangle_{n-1},x_{n}$,
we define the _string of $\pi$_ to be the string of diamonds
$s(\pi)=\langle?\rangle_{1}\langle?\rangle_{2}\cdots\langle?\rangle_{n-1}$.

######  Definition A.6 (The Relation $\mathcal{R}^{{\sf\Pi}}$).

Let ${\sf\Pi}$ be a set of path axioms. For any two labels $x$ and $y$
occurring in a labelled sequent ${\mathcal{R}}\vdash{\Gamma}$,
$x\mathcal{R}^{{\sf\Pi}}y$ holds if and only if there exists a path $\pi$ in
$PG({\mathcal{R}}\vdash{\Gamma})$ such that $s(\pi)p\rightarrow\langle?\rangle
p\in{\sf\Pi}^{*}$.

##  Appendix B Proofs

######  Lemma 3.16.

Given an interpolant $\mathcal{I}$, the empty sequent is derivable from
$\mathcal{I}\cup({\mathcal{I}})^{\bot}$ using the cut rule and the contraction
rule.

######  Proof B.1.

By induction on the size of $\mathcal{I}.$ Suppose

$\mathcal{I}=\\{({}\vdash{x_{1}:A_{1},\ldots,x_{n}:A_{n}})\\}\cup\mathcal{I}^{\prime}.$

Suppose

$({\mathcal{I}^{\prime}})^{\bot}=\\{{}\vdash{\Lambda_{1}},\ldots,{}\vdash{\Lambda_{k}}\\}.$

Then by the definition of orthogonal transformation:

$({\mathcal{I}})^{\bot}=\bigcup_{i=1}^{k}\bigcup_{j=1}^{n}\\{({}\vdash{\Lambda_{i},x_{j}:\overline{A_{j}}})\\}.$

So each $\Lambda_{i}\in({\mathcal{I}^{\prime}})^{\bot}$ corresponds to exactly
$n$ sequents in $({\mathcal{I}})^{\bot}$:

${}\vdash{x_{1}:\overline{A_{1}},\Lambda_{i}}\qquad\cdots\qquad{}\vdash{x_{n}:\overline{A_{n}},\Lambda_{i}}.$

From these, we can construct a derivaton $\Xi_{i}$ of ${}\vdash{\Lambda_{i}}$
using only cut and contraction:

${}\vdash{\Lambda_{i}}\vdots{}\vdash{x_{1}:A_{1},\ldots,x_{n}:A_{n}}\qquad{}\vdash{x_{1}:\overline{A_{1}},\Lambda_{i}}\quad\cdots\quad{}\vdash{x_{n}:\overline{A_{n}},\Lambda_{i}}$

By induction hypothesis, we have a derivation of ${}\vdash{}$ from
$\mathcal{I}^{\prime}\cup({\mathcal{I}^{\prime}})^{\bot}$:

${}\vdash{}\vdots\mathcal{I}^{\prime}\qquad{}\vdash{\Lambda_{1}}\cdots{}\vdash{\Lambda_{k}}$

By replacing every leaf ${}\vdash{\Lambda_{i}}$ with derivation $\Xi_{i}$, we
get a derivation of the empty sequent from assumptions $\mathcal{I}$ and
$({\mathcal{I}^{\prime}})^{\bot}$, using only cut and contraction as required.

######  Lemma 3.14.

For all $\mathcal{R},\Gamma,\Delta$ and $\mathcal{I}$, if
${\mathcal{R}}\Vdash{\Gamma\mid\Delta}\mathrel{\|}{\mathcal{I}}$, then

  1. 1.

For all $({}\vdash{\Lambda})\in\mathcal{I},$ we have
${\mathcal{R}}\Vdash{\Gamma,\Lambda}$ and

  2. 2.

For all $({}\vdash{\Theta})\in({\mathcal{I}})^{\bot}$, we have
${\mathcal{R}}\Vdash{\Theta,\Delta}.$

######  Proof B.2.

By induction on the height of the proof of
${\mathcal{R}}\vdash{\Gamma\mid\Delta}\mathrel{\|}{\mathcal{I}}$; we prove the
result for a representative set of cases since all others are simple or shown
similarly. The base cases are trivial, so we focus solely on the inductive
step.

###  $orth$-rule

Suppose the proof of
${\mathcal{R}}\vdash{\Gamma\mid\Delta}\mathrel{\|}{\mathcal{I}}$ ends with the
$orth$-rule:

${\mathcal{R}}\vdash{\Delta\mid\Gamma}\mathrel{\|}{({\mathcal{I}})^{\bot}}{\mathcal{R}}\vdash{\Gamma\mid\Delta}\mathrel{\|}{\mathcal{I}}$

  1. 1.

Let ${}\vdash{\Lambda}\in({\mathcal{I}})^{\bot}$: we need to establish that
${\mathcal{R}}\Vdash{\Lambda,\Delta}$. This follows immediately from the
induction hypothesis.

  2. 2.

Let ${}\vdash{\Lambda}\in({({\mathcal{I}})^{\bot}})^{\bot}$: We need to
establish that ${\mathcal{R}}\Vdash{\Gamma,\Lambda}.$ By Lem. 3.9, there
exists a $\Lambda^{\prime}\in\mathcal{I}$ such that
$\Lambda^{\prime}\subseteq\Lambda$. By the IH, we have
${\mathcal{R}}\Vdash{\Gamma,\Lambda^{\prime}}$, and applying admissibility of
weakening (Lem. 3.2), we get ${\mathcal{R}}\Vdash{\Gamma,\Lambda}$ as
required.

###  $\land$-rule

Suppose our proof ends with the inference:

${\mathcal{R}}\vdash{\Gamma\mid x:A\land
B,\Delta}\mathrel{\|}{\mathcal{I}_{1}\cup\mathcal{I}_{2}}\lx@proof@logical@and{\mathcal{R}}\vdash{\Gamma\mid
x:A,\Delta}\mathrel{\|}{\mathcal{I}_{1}}{\mathcal{R}}\vdash{\Gamma\mid
x:B,\Delta}\mathrel{\|}{\mathcal{I}_{2}}$

  1. 1.

Let ${}\vdash{\Lambda}\in\mathcal{I}_{1}\cup\mathcal{I}_{2}$. By the induction
hypothesis, for any ${}\vdash{\Lambda_{1}}\in\mathcal{I}_{1}$ and
${}\vdash{\Lambda_{2}}\in\mathcal{I}_{2}$, we have that
${\mathcal{R}}\Vdash{\Gamma,\Lambda_{1}}$, and
${\mathcal{R}}\Vdash{\Gamma,\Lambda_{2}}$. Regardless of if
${}\vdash{\Lambda}\in\mathcal{I}_{1}$ or
${}\vdash{\Lambda}\in\mathcal{I}_{2}$, we achieve the desired conclusion.

  2. 2.

Let ${}\vdash{\Lambda}\in({\mathcal{I}_{1}\cup\mathcal{I}_{2}})^{\bot}$. By
the induction hypothesis, for any
${}\vdash{\Lambda_{1}}\in({\mathcal{I}_{1}})^{\bot}$ and
${}\vdash{\Lambda_{2}}\in({\mathcal{I}_{2}})^{\bot}$,
${\mathcal{R}}\Vdash{x:A,\Delta,\Lambda_{1}}$ and
${\mathcal{R}}\Vdash{x:B,\Delta,\Lambda_{2}}$. Observe that by the definition
of orthogonal, there is a ${}\vdash{\Lambda_{1}}\in({\mathcal{I}_{1}})^{\bot}$
and ${}\vdash{\Lambda_{2}}\in({\mathcal{I}_{2}})^{\bot}$ such that
$({}\vdash{\Lambda})=({}\vdash{\Lambda_{1},\Lambda_{2}})$. Hence, by
admissibility of weakening (Lem. 3.2) we can derive
${{\mathcal{R}}\vdash{x:A,\Delta,\Lambda_{1},\Lambda_{2}}}$ and
${{\mathcal{R}}\vdash{x:B,\Delta,\Lambda_{1},\Lambda_{2}}}$, from which, an
application of the conjunction rule gives the desired conclusion.

###  $\square$-rule

Suppose the proof of
${\mathcal{R}}\vdash{\Gamma\mid\Delta}\mathrel{\|}{\mathcal{I}}$ ends with a
$\square$ rule, i.e., $\Delta=\Delta^{\prime}\cup\\{x:\square A\\}$,
$\mathcal{I}=\square\mathcal{I}^{\prime y}_{x}$, and the proof has the form:

${\mathcal{R}}\vdash{\Gamma\mid x:\square
A,\Delta^{\prime}}\mathrel{\|}{\square\mathcal{I}^{\prime
y}_{x}}{\mathcal{R},Rxy}\vdash{\Gamma\mid
y:A,\Delta^{\prime}}\mathrel{\|}{\mathcal{I}^{\prime}}$

  1. 1.

Let ${}\vdash{\Lambda}\in\square\mathcal{I}^{\prime y}_{x}$: we need to show
that ${\mathcal{R}}\Vdash{\Gamma,\Lambda}$. From the definition of
$\square\mathcal{I}^{\prime y}_{x}$, $\Lambda$ must be of the form
$\\{\Lambda^{\prime},x:\square(B_{1}\lor\cdots\lor B_{k})\\}$ where
$({}\vdash{\Lambda^{\prime},y:B_{1},\ldots,y:B_{k}})\in\mathcal{I}^{\prime}.$
The proof of ${\mathcal{R}}\vdash{\Gamma,\Lambda}$ is constructed as follows:

${\mathcal{R}}\vdash{\Gamma,\Lambda^{\prime},x:\square(B_{1}\lor\cdots\lor
B_{k})}{\mathcal{R},Rxy}\vdash{\Gamma,\Lambda^{\prime},y:B_{1}\lor\cdots\lor
B_{k}}{\mathcal{R},Rxy}\vdash{\Gamma,\Lambda^{\prime},y:B_{1},\ldots,y:B_{k}}$

with the premise derivable by the induction hypothesis.

  2. 2.

Let ${}\vdash{\Lambda}\in({\square\mathcal{I}^{\prime y}_{x}})^{\bot}$: we
need to show that ${\mathcal{R}}\Vdash{\Lambda,x:\square A,\Delta^{\prime}}$.
In this case, $\Lambda$ could contain zero or more formulae of the form
$x:\overline{\square(B_{1}\lor\cdots\lor B_{k})}$ such that there exists
${}\vdash{\Lambda^{\prime}}\in\mathcal{I}^{\prime}$ with
$\\{y:B_{1},\ldots,y:B_{k}\\}\subseteq\Lambda^{\prime}.$ Let us refer to these
formulae as a boxed-interpolant formulae. We suppose for the sake of
simplicity that exactly one boxed-interpolant formula exists in $\Lambda$ and
that $k=2$; the general case is obtained similarly. We may therefore write
$\Lambda$ as $\\{{x:\overline{\Box(B_{1}\lor B_{2})}}\\}\cup\Theta$.

It follows from our assumptions then that there exists
$\Lambda^{\prime}\in\mathcal{I}^{\prime}$ with
$\\{y:B_{1},y:B_{2}\\}\subseteq\Lambda^{\prime}$. Hence, there must exist a
$\Lambda_{1}\in({\mathcal{I}^{\prime}})^{\bot}$ of the form
$\\{y:\overline{B_{1}}\\}\cup\Theta$ and a
$\Lambda_{2}\in({\mathcal{I}^{\prime}})^{\bot}$ of the form
$\\{y:\overline{B_{2}}\\}\cup\Theta$. By the induction hypothesis,
${\mathcal{R},Rxy}\Vdash{y:\overline{B}_{1},{\Theta},y:A,\Delta^{\prime}}$ and
${\mathcal{R},Rxy}\Vdash{y:\overline{B}_{2},{\Theta},y:A,\Delta^{\prime}}$.
Evoking weakening admissibility from Lem. 3.2, we have that

$\displaystyle{\mathcal{R},Rxy}\Vdash{y:\overline{B}_{1},{\Theta},x:\lozenge(\overline{B}_{1}\land\overline{B}_{2}),y:A,\Delta^{\prime}}$
$\displaystyle{\mathcal{R},Rxy}\Vdash{y:\overline{B}_{2},{\Theta},x:\lozenge(\overline{B}_{1}\land\overline{B}_{2}),y:A,\Delta^{\prime}}$

By using the $\land$ rule with $y:B_{1}$ and $y:B_{2}$ principal, we can
derive

${\mathcal{R},Rxy}\vdash{y:\overline{B}_{1}\land\overline{B}_{2},{\Theta},x:\lozenge(\overline{B}_{1}\land\overline{B}_{2}),y:A,\Delta^{\prime}}.$

The desired result is obtained as follows:

${\mathcal{R}}\vdash{{\Theta},x:\lozenge(\overline{B}_{1}\land\overline{B}_{2}),y:\square
A,\Delta^{\prime}}{\mathcal{R},Rxy}\vdash{{\Theta},x:\lozenge(\overline{B}_{1}\land\overline{B}_{2}),y:A,\Delta^{\prime}}{\mathcal{R},Rxy}\vdash{y:\overline{B}_{1}\land\overline{B}_{2},{\Theta},x:\lozenge(\overline{B}_{1}\land\overline{B}_{2}),y:A,\Delta^{\prime}}$

######  Theorem 3.19.

If ${}\Vdash{x:A\rightarrow B}$, then there exists a $C$ such that (i)
$var(C)\subseteq var(A)\cap var(B)$ and (ii) ${}\Vdash{x:A\rightarrow C}$ and
${}\Vdash{x:C\rightarrow B}$.

######  Proof B.3.

Assume that ${}\Vdash{x:A\rightarrow B}$, i.e. ${}\Vdash{x:\overline{A}\vee
B}$. By Lem. 3.2, we know that ${}\Vdash{x:\overline{A},x:B}$. Therefore, by
Lem. 3.12, we know that there exists an interpolant
$\mathcal{I}=\\{{}\vdash{\Lambda_{1}},\ldots,{}\vdash{\Lambda_{n}}\\}$ with
$\Lambda_{i}=\\{x:A_{i,1},\ldots,x:A_{i,k_{i}}\\}$ for each $1\leq i\leq n$
such that ${}\Vdash{x:\overline{A}\mid x:B}\mathrel{\|}{\mathcal{I}}$,
$var(\mathcal{I})\subseteq var(x:A)\cap var(x:B)$, and all formulae in
$\mathcal{I}$ are labelled with $x$. By Lem. 3.14, the following two
statements hold: (a) for all $(\vdash\Lambda)\in\mathcal{I}$,
${}\Vdash{x:\overline{A},\Lambda}$, (b) for all
$(\vdash\Theta)\in({\mathcal{I}})^{\bot}$, ${}\Vdash{\Theta,x:B}$. We now use
the interpolant $\mathcal{I}$ to construct a $C$ satisfying the conclusion of
the theorem.

The fact that all labelled formulae in $\mathcal{I}$ have the same label $x$,
along with statement (a) and Lem. 3.15, imply that
${}\Vdash{x:\overline{A},x:\bigwedge\bigvee\mathcal{I}}$. Moreover, statement
(b) and Lem. 3.17 imply that
${}\Vdash{x:\overline{\bigwedge\bigvee\mathcal{I}},x:B}$. Applying the $\lor$
rule in both cases implies that
${}\Vdash{x:\overline{A}\vee\bigwedge\bigvee\mathcal{I}}$ and
${}\Vdash{x:\overline{\bigwedge\bigvee\mathcal{I}}\vee B}$, thus giving the
desired result with $\bigwedge\bigvee\mathcal{I}$ the interpolant. Last, note
that since $\bigwedge\bigvee\mathcal{I}$ is our interpolant, and
$var(\mathcal{I})\subseteq var(x:A)\cap var(x:B)$ holds,
$var(\bigwedge\bigvee\mathcal{I})\subseteq var(A)\cap var(B)$ will be
satisfied as well.

######  Lemma B.4.

The following two rules are derivable in $\mathsf{BiIntL}$:

${\mathcal{R},Rxy,\Gamma,x:A\supset
B}\vdash{\Delta}\lx@proof@logical@and{\mathcal{R},Rxy,\Gamma,x:A\supset
B}\vdash{\Delta,y:A}{\mathcal{R},Rxy,\Gamma,y:B}\vdash{\Delta}$
${\mathcal{R},Ryx,\Gamma}\vdash{x:A-\\!\\!\\!<B,\Delta}\lx@proof@logical@and{\mathcal{R},Ryx,\Gamma}\vdash{\Delta,y:A}{\mathcal{R},Rxy,\Gamma,y:B}\vdash{x:A-\\!\\!\\!<B,\Delta}$

######  Proof B.5.

We prove the claim for the $\supset^{*}_{L}$ rule; the proof for
$-\\!\\!\\!<^{*}_{R}$ is similar. Assume that
${\mathcal{R},Rxy,\Gamma,x:A\supset B}\Vdash{\Delta,y:A}$ and
${\mathcal{R},Rxy,\Gamma,y:B}\Vdash{\Delta}$. By evoking admissibility of
weakening (Lem. 4.1), we obtain proofs of the following sequents:

$\displaystyle{\mathcal{R},Rxy,\Gamma,x:A\supset B,y:A\supset
B}\vdash{\Delta,y:A}\qquad$ $\displaystyle{\mathcal{R},Rxy,\Gamma,x:A\supset
B,y:B}\vdash{\Delta}$

By applying $\supset_{L}$ with the above sequents, we obtain the premise
below; the desired conclusion is derived with one application of $monl$:

${\mathcal{R},Rxy,\Gamma,x:A\supset
B}\vdash{\Delta}{\mathcal{R},Rxy,\Gamma,x:A\supset B,y:A\supset
B}\vdash{\Delta}$

######  Lemma B.6.

The rule

$\mathcal{R},\Gamma\vdash\Delta\mathcal{R},Rxx,\Gamma\vdash\Delta$

is admissible in $\mathsf{BiIntL}$.

######  Proof B.7.

We prove the result by induction on the height of the derivation of
$\mathcal{R},Rxx,\Gamma\vdash\Delta$. The base case is simple since if
$\mathcal{R},Rxx,\Gamma\vdash\Delta$ is an initial sequent, then so is
$\mathcal{R},\Gamma\vdash\Delta$. For all rules, with the exception of the
$monl$ and $monr$ rule, the inductive step is proven by applying the inductive
hypothesis followed by an application of the rule. We therefore focus on the
above two cases:

###  $monl$-, $monr$-rules

If $Rxx$ is not principal in a $monl$ or $monr$ inference, then the case is
resolved by applying the inductive hypothesis followed by an application of
the rule. However, if $Rxx$ is principal, then the inferences are of the
following forms:

$\mathcal{R},Rxx,x:A,x:A,\Gamma\vdash\Delta$ $\mathcal{R},Rxx,x:A,\Gamma\vdash\Delta$ |  $\mathcal{R},Rxx,\Gamma\vdash x:A,x:A,\Delta$ $\mathcal{R},Rxx,\Gamma\vdash x:A,\Delta$
---|---

Applying the inductive hypothesis to the premises, followed by an application
of $ctr$ admissibility (Lem. 4.1), gives the desired conclusion.

######  Lemma 4.13.

For all $\mathcal{R},\Gamma_{1},\Gamma_{2},\Delta_{1},\Delta_{2}$ and
$\mathcal{I}$, if
${\mathcal{R},\Gamma_{1}\mid\Gamma_{2}}\Vdash{\Delta_{1}\mid\Delta_{2}}\mathrel{\|}{\mathcal{I}}$,
then

  1. 1.

For all $({\Sigma}\vdash{\Theta})\in\mathcal{I}$, we have
${\mathcal{R},\Gamma_{1},\Sigma}\Vdash{\Theta,\Delta_{1}}$ and

  2. 2.

For all $({\Lambda}\vdash{\Omega})\in({\mathcal{I}})^{\bot}$, we have
${\mathcal{R},\Gamma_{2},\Lambda}\Vdash{\Omega,\Delta_{2}}.$

######  Proof B.8.

By induction on the height of proofs; we prove the result for a representative
set of cases since all others are simple or shown similarly. Moreover, the
base cases are trivial, so we focus solely on the inductive step, where we
show the cases for $\lor_{L}$ and $\supset_{R}$ since all other cases are
similar or simple.

###  $\lor_{L}$-rule

Suppose that our derivation ends with the upmost $\lor_{L}$ in Fig. 8.

  1. 1.

Let $({\Sigma}\vdash{\Theta})\in\mathcal{I}_{1}\cup\mathcal{I}_{2}$. By the
inductive hypothesis, we have that for all
$({\Sigma}\vdash{\Theta})\in\mathcal{I}_{1}$,
${\mathcal{R},\Gamma_{1},\Sigma}\Vdash{\Delta_{1},\Theta}$ and for all
$({\Sigma}\vdash{\Theta})\in\mathcal{I}_{2}$,
${\mathcal{R},\Gamma_{1},\Sigma}\Vdash{\Delta_{1},\Theta}$. Therefore,
regardless of if $({\Sigma}\vdash{\Theta})$ is in $\mathcal{I}_{1}$ or
$\mathcal{I}_{2}$, we have that
${\mathcal{R},\Gamma_{1},\Sigma}\Vdash{\Delta_{1},\Theta}$.

  2. 2.

Let
$({\Sigma}\vdash{\Theta})\in({\mathcal{I}_{1}\cup\mathcal{I}_{2}})^{\bot}$. By
the inductive hypothesis, we have that for all
$({\Sigma}\vdash{\Theta})\in({\mathcal{I}_{1}})^{\bot}$,
${\mathcal{R},x:A,\Gamma_{2},\Sigma}\Vdash{\Delta_{2},\Theta}$ and for all
$({\Sigma}\vdash{\Theta})\in({\mathcal{I}_{2}})^{\bot}$,
${\mathcal{R},x:B,\Gamma_{2},\Sigma}\Vdash{\Delta_{2},\Theta}$. Observe that
by the definition of orthogonal, there will be a
$({\Sigma_{1}}\vdash{\Theta_{1}})$ and $({\Sigma_{2}}\vdash{\Theta_{2}})$ such
that
$({\Sigma_{1},\Sigma_{2}}\vdash{\Theta_{1},\Theta_{2}})\in({\mathcal{I}_{1}\cup\mathcal{I}_{2}})^{\bot}$.
Hence, by the inductive hypothesis and the admissibility of weakening (Lem.
4.1) we may derive

${\mathcal{R},x:A,\Gamma_{2},\Sigma_{1},\Sigma_{2}}\vdash{\Delta_{2},\Theta_{1},\Theta_{2}}\quad\mbox{and}\quad{\mathcal{R},x:B,\Gamma_{2},\Sigma_{1},\Sigma_{2}}\Vdash{\Delta_{2},\Theta_{1},\Theta_{2}}.$

One application of the $\lor_{L}$ rule gives the desired conclusion.

###  $\supset_{R}$-rule

Assume that our derivation of
${\mathcal{R},\Gamma_{1}\mid\Gamma_{2}}\vdash{\Delta_{1}\mid\Delta_{2}}\mathrel{\|}{\mathcal{I}}$
ends with a $\supset_{R}$ rule, where $\mathcal{I}\ =\
\supset{\mathcal{I}^{\prime}}^{y}_{x}$ and the last inference has the form:

${\mathcal{R},\Gamma_{1}\mid\Gamma_{2}}\vdash{\Delta_{1}\mid x:A\supset
B,\Delta_{2}}\mathrel{\|}{\supset\mathcal{I}^{\prime
y}_{x}}{\mathcal{R},Rxy,\Gamma_{1}\mid y:A,\Gamma_{2}}\vdash{\Delta_{1}\mid
y:B,\Delta_{2}}\mathrel{\|}{\mathcal{I}^{\prime}}$

  1. 1.

Let $({\Sigma}\vdash{\Theta})\in\mathcal{I}$. We want to show that
${\mathcal{R},\Gamma_{1},\Sigma}\Vdash{\Delta_{1},\Theta}$. Note that
${\Sigma}\vdash{\Theta}$ is of the form:

${\Sigma}\vdash{x:C_{1}\wedge...\wedge C_{k}\supset D_{1}\vee...\vee
D_{n},\Theta^{\prime}},$

where $\Theta=x:C_{1}\wedge...\wedge C_{k}\supset D_{1}\vee...\vee
D_{n},\Theta^{\prime}$. This implies that there exists a
$({\Lambda}\vdash{\Omega})\in\mathcal{I}^{\prime}$ of the form

${\Sigma,y:C_{1},...,y:C_{k}}\vdash{y:D_{1},...,y:D_{n},\Theta^{\prime}}$

Therefore, the inductive hypothesis implies that the premise below is
derivable:

${\mathcal{R},\Gamma_{1},\Sigma}\vdash{x:C_{1}\wedge...\wedge C_{k}\supset
D_{1}\vee...\vee
D_{n},\Theta^{\prime},\Delta_{1}}{\mathcal{R},Rxy,\Gamma_{1},\Sigma,y:C_{1}\wedge...\wedge
C_{k}}\vdash{y:D_{1}\vee...\vee
D_{n},\Theta^{\prime},\Delta_{1}}{\mathcal{R},Rxy,\Gamma_{1},\Sigma,y:C_{1},...,C_{k}}\vdash{y:D_{1},...,y:D_{n},\Theta^{\prime},\Delta_{1}}$

The last $\supset_{R}$ inference may be applied because, by our assumption,
$y$ does not occur in
$\mathcal{R},\Gamma_{1},\Sigma,\Theta^{\prime},\Delta_{1}$.

  2. 2.

Let $({\Sigma}\vdash{\Theta})\in({\mathcal{I}})^{\bot}$. Observe that $\Sigma$
will contain zero or more formulae of the form $x:C_{1}\land...\land
C_{k}\supset D_{1}\lor...\lor D_{n}$, which we refer to as an implication-
interpolant formula, such that there exists a sequent in
$\mathcal{I}^{\prime}$ of the form:

${\Sigma^{\prime},y:C_{1},...,y:C_{k}}\vdash{y:D_{1},...,y:D_{n},\Theta}.$

where $\Sigma^{\prime}$ is equal to $\Sigma$ minus all implication-interpolant
formulae. We assume for the sake of simplicity that $\Sigma$ contains one
implication-interpolant formula, that $k=2$, and $n=2$; the general case is
tedious, but shown similarly. ${\Sigma}\vdash{\Theta}$ is therefore of the
form:

${x:C_{1}\land...\land C_{k}\supset D_{1}\lor...\lor
D_{n},\Sigma^{\prime}}\vdash{\Theta}.$

It follows from our assumptions that there exists a
$({\Lambda}\vdash{\Omega})\in\mathcal{I}^{\prime}$ of the form

${\Sigma^{\prime},y:C_{1},y:C_{2}}\vdash{y:D_{1},y:D_{2},\Theta}.$

Hence, by the definition of the orthogonal, the following four sequents are
members of $({\mathcal{I}^{\prime}})^{\bot}$:

${\Sigma^{\prime}}\vdash{\Theta,y:C_{1}}\qquad{\Sigma^{\prime}}\vdash{\Theta,y:C_{2}}\qquad{y:D_{1},\Sigma^{\prime}}\vdash{\Theta}\qquad{y:D_{2},\Sigma^{\prime}}\vdash{\Theta}$

By the inductive hypothesis the following four claims hold:

$\displaystyle{\mathcal{R},Rxy,y:A,\Gamma_{2},\Sigma^{\prime}}\Vdash{\Theta,\Delta_{2},y:B,y:C_{1}}$
$\displaystyle{\mathcal{R},Rxy,y:A,\Gamma_{2},\Sigma^{\prime}}\Vdash{\Theta,\Delta_{2},y:B,y:C_{2}}$
$\displaystyle{\mathcal{R},Rxy,y:A,y:D_{1},\Gamma_{2},\Sigma^{\prime}}\Vdash{\Theta,\Delta_{2},y:B}$
$\displaystyle{\mathcal{R},Rxy,y:A,y:D_{2},\Gamma_{2},\Sigma^{\prime}}\Vdash{\Theta,\Delta_{2},y:B}$

Applying the $\land_{R}$ rule to the first two sequents with $y:C_{1}$ and
$y:C_{2}$ active, and the $\lor_{L}$ rule to the latter two sequents with
$y:D_{1}$ and $y:D_{2}$ active, gives derivations of the following two
sequents:

$\displaystyle{\mathcal{R},Rxy,y:A,\Gamma_{2},\Sigma^{\prime}}\vdash{\Theta,\Delta_{2},y:B,y:C_{1}\land
C_{2}}$ $\displaystyle{\mathcal{R},Rxy,y:A,y:D_{1}\lor
D_{2},\Gamma_{2},\Sigma^{\prime}}\vdash{\Theta,\Delta_{2},y:B}$

By admissibility of weakening (Lem. 4.1), we may weaken in $x:C_{1}\land
C_{2}\supset D_{1}\lor D_{2}$ on the left side of both sequents and apply the
$\supset^{*}_{L}$ rule (Lem. B.4) to obtain a derivation of:

${\mathcal{R},Rxy,y:A,x:C_{1}\land C_{2}\supset D_{1}\lor
D_{2},\Gamma_{2},\Sigma^{\prime}}\vdash{\Theta,\Delta_{2},y:B}$

An application of $\supset_{R}$ with $Rxy$, $y:A$, and $y:B$ principal gives
the desired result.

######  Lemma 4.14.

Let
$\mathcal{I}=\\{({\Sigma_{1}}\vdash{\Theta_{1}}),\ldots,({\Sigma_{n}}\vdash{\Theta_{n}})\\}$
be an interpolant with

$({\Sigma_{i}}\vdash{\Theta_{i}})=({x:C_{i,1},\ldots,x:C_{i,k_{i}}}\vdash{x:D_{i,1},\ldots,x:D_{i,j_{i}}})\mbox{
for each }1\leq i\leq n.$

If ${\Sigma_{i},\Gamma}\Vdash{\Theta_{i}}$, for all
$({\Sigma_{i}}\vdash{\Theta_{i}})\in\mathcal{I}$, and every formula in
$\Gamma$ is labelled with $x$, then

${\Gamma}\Vdash{x:\bigwedge_{i=1}^{n}(\bigwedge_{m=1}^{k_{i}}C_{i,m}\supset\bigvee_{m=1}^{j_{i}}D_{i,m}}).$

######  Proof B.9.

By assumption,
${x:C_{i,1},\ldots,x:C_{i,k_{i}},\Gamma}\Vdash{x:D_{i,1},\ldots,x:D_{i,j_{i}}}$
for all $1\leq i\leq n$. By repeated application of $\land_{L}$ and
$\lor_{R}$, we obtain a derivation of the following sequent for each $1\leq
i\leq n$:

${x:\bigwedge_{m=1}^{k_{i}}C_{i,m},\Gamma}\vdash{x:\bigvee_{m=1}^{j_{i}}D_{i,m}}$

Let $y$ be a fresh variable and let $\Gamma^{\prime}=\Gamma[y/x]$, i.e., the
multiset of labelled formulae $\Gamma$ but with every formula labelled with
$y$ instead of $x$. By the admissibility of weakening (Lem. 4.1) and the
derivability of the above sequents, we may derive the following:

${Ryx,x:\bigwedge_{m=1}^{k_{i}}C_{i,m},\Gamma,\Gamma^{\prime}}\vdash{x:\bigvee_{m=1}^{j_{i}}D_{i,m}}$

for all $1\leq i\leq n$. We construct derivations from the derivations of the
above sequents by adding the following inferences to the bottom of each:

${\Gamma^{\prime}}\vdash{y:\bigwedge_{m=1}^{k_{i}}C_{i,m}\supset\bigvee_{m=1}^{j_{i}}D_{i,m}}{Ryx,x:\bigwedge_{m=1}^{k_{i}}C_{i,m},\Gamma^{\prime}}\vdash{x:\bigvee_{m=1}^{j_{i}}D_{i,m}}{Ryx,x:\bigwedge_{m=1}^{k_{i}}C_{i,m},\Gamma,\Gamma^{\prime}}\vdash{x:\bigvee_{m=1}^{j_{i}}D_{i,m}}$

for all $1\leq i\leq n$. By successively applying $\land_{R}$ we may derive
the following:

${\Gamma^{\prime}}\vdash{y:\bigwedge_{i=1}^{n}(\bigwedge_{m=1}^{k_{i}}C_{i,m}\supset\bigvee_{m=1}^{j_{i}}D_{i,m}})$

By the fact that the above sequent is derivable and by statement (4) of Lem.
4.1, we obtain the desired conclusion:

${\Gamma}\Vdash{x:\bigwedge_{i=1}^{n}(\bigwedge_{m=1}^{k_{i}}C_{i,m}\supset\bigvee_{m=1}^{j_{i}}D_{i,m})}$

######  Theorem 4.17.

If ${}\Vdash{x:A\supset B}$, then there exists a $C$ such that (i)
$var(C)\subseteq var(A)\cap var(B)$ and (ii) ${}\Vdash{x:A\supset C}$ and
${}\Vdash{x:C\supset B}$.

######  Proof B.10.

Suppose that ${}\Vdash{x:A\supset B}$. By Lem. 4.1 (2), (4) and Lem. B.6, this
implies that ${x:A}\Vdash{x:B}$. By Lem. 4.11, we know there exists an
$\mathcal{I}=\\{({\Sigma_{1}}\vdash{\Theta_{1}}),\ldots,({\Sigma_{n}}\vdash{\Theta_{n}})\\}$
with

$({\Sigma_{i}}\vdash{\Theta_{i}})=({x:C_{i,1},\ldots,x:C_{i,k_{i}}}\vdash{x:D_{i,1},\ldots,x:D_{i,j_{i}}})$

for each $1\leq i\leq n$ such that ${x:A\mid\cdot}\Vdash{\cdot\mid
x:B}\mathrel{\|}{\mathcal{I}}$, $var(\mathcal{I})\subseteq var(x:A)\cap
var(x:B)$, and $x$ is the only label occurring in $\mathcal{I}$. By Lem. 4.13,
the following two statements hold: (a) for all
$({\Sigma}\vdash{\Theta})\in\mathcal{I}$, we have
${x:A,\Sigma}\Vdash{\Theta}$, and (b) for all
$({\Sigma}\vdash{\Theta})\in({\mathcal{I}})^{\bot}$, we have
${\Sigma}\Vdash{\Theta,x:B}$.

We now use the interpolant $\mathcal{I}$ to construct a formula $C$ satisfying
the conditions specified in the claim of the theorem.

By the assumption that $\mathcal{I}$ only contains formulae with the label $x$
along with statement (a) and Lem. 4.14, we obtain the following:

${x:A}\Vdash{x:\bigwedge_{i=1}^{n}(\bigwedge_{m=1}^{k_{i}}C_{i,m}\supset\bigvee_{m=1}^{j_{i}}D_{i,m})}$

Additionally, statement (b) and Lem. 4.15 imply the following:

${x:\bigwedge_{i=1}^{n}(\bigwedge_{m=1}^{k_{i}}C_{i,m}\supset\bigvee_{m=1}^{j_{i}}D_{i,m})}\Vdash{x:B}$

By weakening admissibility (Lem. 4.1), we may weaken both sequents with $Ryx$
and apply $\supset_{R}$ to obtain the following:

${}\Vdash{y:A\supset\bigwedge_{i=1}^{n}(\bigwedge_{m=1}^{k_{i}}C_{i,m}\supset\bigvee_{m=1}^{j_{i}}D_{i,m})}$
${}\Vdash{y:\bigwedge_{i=1}^{n}(\bigwedge_{m=1}^{k_{i}}C_{i,m}\supset\bigvee_{m=1}^{j_{i}}D_{i,m})\supset
B}$

Evoking statement (4) of Lem. 4.1 allows us to replace the label $y$ with $x$.
Last, since $var(\mathcal{I})\subseteq var(x:A)\cap var(x:B)$, it is easy to
see that
$\bigwedge_{i=1}^{n}(\bigwedge_{m=1}^{k_{i}}C_{i,m}\supset\bigvee_{m=1}^{j_{i}}D_{i,m})$
is our formula interpolant for $A$ and $B$.