
\documentclass{article}

\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{url}
\usepackage{exptrees}

\newcommand\comment[1]{} 

\newcommand\wbox\square
\newcommand\wdia\lozenge
\newcommand\bbox\blacksquare
\newcommand\bdia\blacklozenge

\begin{document}

\title{Isabelle work on Interpolation for the Display Calculus for Tense Logic}

\author{Jeremy E.\ Dawson}

\maketitle

\section{Introduction} \label{s-intro}
This document describes my attempts to prove interpolation for tense logic,
using techniques similar to those used for classical logic,
as described in the papers

James Brotherston \& Rajeev Gor\'e, Craig Interpolation in Displayable Logics
(TABLEAUX 2011)

and the draft paper by Jeremy Dawson, James Brotherston \& Rajeev Gor\'e,
currently called

``Machine-checked Interpolation Theorems for Substructural Logics using
Display Calculi''.

Alternatively, this note could be read in conjunction with my note
``{Isabelle work on Interpolation for Display Calculi}''

\section{Comparison with Tableau Proofs} \label{s-tableaux}

Recall that the general method of proof of the result for classical logic was
to consider the property \texttt{ldi} below, which approximates to $LADI$ in 
Brotherston \& Gor\'e, which is the property, of a given sequent $S$, that
all sequents which are display-equivalent to $S$ have interpolants.

This property was proved by induction over a derivation, which requires
that each derivation rule preserves that property.

We can compare a proof by such a method to a proof using methods similar to
those of Nguyen, Studia Logica 69 (2001), 41-57, whose proofs were for tableau
systems.
His method expressed in terms of a sequent system,
could be described thus. 
Given a partition of the propositional variables into two sets, which we
could call red and green, and a given sequent 
$\Gamma_R, \Gamma_G \vdash \Delta_R, \Delta_G$,
an interpolant $K$ is a formula such that 
$\Gamma_R \vdash \Delta_R, K$ and $K, \Gamma_G \vdash \Delta_G$ 
where the variables in $K$ appear both in 
$\Gamma_R, \Delta_R$ and in $\Gamma_G, \Delta_G$.

Then, for a display rule such as $X \vdash A, Y \equiv X, *A \vdash Y$,
supposing that $A$ is a single variable, and so is either red or green
(say it is red),
then the requirements for an interpolant $K$ of $X \vdash A, Y$ would be 
$X_R \vdash A, Y_R, K$ and $K, X_G \vdash Y_G$ 
whereas an interpolant $K$ of $X, *A \vdash Y$ would satisfy 
$X_R, *A \vdash Y_R, K$ and $K, X_G \vdash Y_G$.
That is, this rule preserves interpolants.

This approach presupposes that the structure $A$ is either red or green, 
and that $X$ and $Y$ are comma-separated lists of substuctures which are either
red or green.  Briefly, this mapping of Nguyen's approach into display logic
works because of the rules giving associativity and commutativity of the comma,
and because a structure $*(U, V)$ is display-equivalent to $*U, *V$.

When we consider the rule 
$$ \frac {X \vdash A, B} {X \vdash A \lor B} \qquad
 \frac {X \vdash A \quad X \vdash B} {X \vdash A \land B}$$
 we must also note that the partition of variables into red and green is 
 determined by the end-sequent which is simply 
$X_R \vdash Y_G$ --- thus $A$ and $B$ in the rules above are the same colour.

Thus the proof method of Brotherston \& Gor\'e amounts to proving, inductively,
that each derivable sequent, for each red-green colouring, has an interpolant
in the red-green sense described above, by a proof method analogous to that of
Nguyen.

We now discuss our attempts to extend the proof method of 
Brotherston \& Gor\'e to handle the display calculus for tense logic, 
and the problems that arose.
It is interesting to reflect that attempting to extend Nguyen's approach to
tense logic would look rather different, and we will comment also on the
difficulties in doing this.

\section{Extending Brotherston \& Gor\'e to tense logic}

Recall that the general method of proof is that, given a rule
${\mathcal S'} \Longrightarrow {\mathcal S}$ we want to prove that it preserves
the extended display interpolation property (EDI), that is, it
satisfies the local display interpolation property (LDI).
Thus, where $\mathcal S \equiv \mathcal T$,
we want to find $\mathcal T'$ such that $\mathcal S' \equiv \mathcal T'$
and it is easy to see that,
if $\mathcal T'$ has an interpolant, then so does $\mathcal T$.
Then, if $\mathcal S'$ satisfies EDI, then $\mathcal T'$ has an interpolant,
so $\mathcal T$ has an interpolant: that is, $\mathcal S$ satisfies EDI.

Furthermore, we generally define an appropriate relation between sequents
$\mathcal T'$ and $\mathcal T$ to facilitate the proof.  For example, 
where ${\mathcal S'} \Longrightarrow {\mathcal S}$ is an instance of the
weakening rule, we consider the relation where $\mathcal T'$ consists of 
$\mathcal T$ with a similar weakening, possibly ``deep'' 
(ie, weakening applied to some substructure).
Or where ${\mathcal S'} \Longrightarrow {\mathcal S}$
is the $(\vdash\wbox)$ rule,
$X \vdash \bullet A \Longrightarrow X \vdash \wbox A$,
then the required relation is that $\mathcal T'$ has $\bullet A$ in some
antecedent position where $\mathcal T$ has $\wbox A$ instead.

The display rule which generally is involved in the difficulties
is the $(\bullet)$ rule, ${X \vdash \bullet Y} \equiv {\bullet X \vdash Y}$.

\subsection{The Contraction Rule}
We note first that in the display calculus for tense logic, 
contraction and weakening are sensibly considered as integral, rather than as
optional extras.  This is because they are required to prove even
$\wbox A \land \wbox B \vdash \wbox (A \land B)$,
via the derived rule 
$\bullet X, \bullet Y \vdash Z \Longrightarrow \bullet (X, Y) \vdash Z$.

Consider where ${\mathcal S'} \Longrightarrow {\mathcal S}$ is an instance of
the contraction rule, say
${\bullet X, \bullet X \vdash Y} \Longrightarrow {\bullet X \vdash Y}$,
and let $\mathcal T$ be ${X \vdash \bullet Y}$.
Then the natural choice for the relation 
between $\mathcal T'$ and $\mathcal T$ is that 
$\mathcal T$ is obtained from $\mathcal T'$ by contraction 
(possibly by multiple or deep contractions).
The natural choice for the $\mathcal T'$ 
might seem to be ${X, X \vdash \bullet Y}$
but this is not display-equivalent to ${\bullet X, \bullet X \vdash Y}$.

By way of a further example, suppose that $X = (X', X'')$, and let 
$\mathcal T$ be ${X' \vdash *X'', \bullet Y}$.
Then it is perhaps even clearer that the natural choice for $\mathcal T'$
is either ${X',X' \vdash *X'',*X'' \bullet Y}$ or
${X',X' \vdash *(X'',X'') \bullet Y}$,
but these are not display-equivalent to ${\bullet X, \bullet X \vdash Y}$.

To solve this problem we changed the definition of the
local display interpolation property, 
and the related extended display interpolation property (EDI): 
we say $\mathcal S$ satisfies the EDI property if 
all sequents ${\mathcal T}$ such that
${\mathcal S} \Longrightarrow_D {\mathcal T}$ have interpolants,
where $\Longrightarrow_D$ refers to derivability using some set of rules,
and need not be an equivalence.

We did a ``proof-of-concept'' of this sort of change for classical logic, 
allowing weakening to be included in the definition of $\Longrightarrow_D$:
in fact the proofs go through nicely, more easily, in fact, than in the
original proof.

So for tense logic we tried this approach where we included the
$\bullet$-distribution rules 
$$\frac {\bullet X, \bullet Y \vdash Z} {\bullet (X, Y) \vdash Z} 
\qquad
\frac {Z \vdash \bullet X, \bullet Y} {Z \vdash \bullet (X, Y)}$$
Note that we could not use the variant of these rules which require $X = Y$ 
because some other lemmas rely on all the symbols in the premise of a
rule in $\Longrightarrow_D$ to be distinct.

Doing this dealt with the contraction rule easily.

\subsection{The $\wbox\vdash$ rule, and equivalents}

Here is the $\wbox\vdash$ rule as often presented, and the version we used
(these are, by the $(\bullet)$ rule, equivalent).
$$
\frac {X \vdash A} {\bullet X \vdash \wbox A} \qquad 
\frac {X \vdash A} {X \vdash \bullet \wbox A} $$

Now if ${X \vdash \bullet \wbox A}$ is display-equivalent to ${\mathcal T}$
(\emph{not} using the $(\bullet)$ rule), then there exists ${\mathcal T'}$
which is display-equivalent to ${X \vdash A}$, and in fact ${\mathcal T}$
has the same interpolant as ${\mathcal T'}$.
Here the relevant relation between ${\mathcal T}$ and ${\mathcal T'}$
is that ${\mathcal T'}$ has $A$ in some succedent position where ${\mathcal T}$
has $\bullet \wbox A$.

But where we allow the $(\bullet)$ rule, further sequents which are 
display-equivalent to ${X \vdash \bullet \wbox A}$ can be got using
the $(\bullet)$ rule, to give, first, ${\bullet X \vdash \wbox A}$.
Consider which display rules can then be applied:
apart from a reverse application of the $(\bullet)$ rule, the only
possibilities are the rules which add two stars. 

Pursuing this line of analysis, we define the relation between sequents
${\mathcal T}$ and ${\mathcal T'}$, called \texttt{lseqrep\_Blob}:
$(T, [T']) \in \texttt{lseqrep\_Blob} \ldots$ iff there exist
$\mathcal T_l, \mathcal T_b$ such that  
\begin{itemize}
\item $\mathcal T_b$ is equivalent to $\mathcal T$ by the rules which delete
two stars
\item $\mathcal T_l = \mathcal T_b$ or these are related by a single
application of the $(\bullet)$ rule 
\item $\mathcal T_l$ is related to $\mathcal T'$ by changing 
$\bullet \wbox A$ to $A$
\end{itemize}

To prove that 
\begin{itemize}
\item 
with this relation, given $\mathcal T$ display-equivalent to 
${X \vdash \bullet \wbox A}$, there exists a related
$\mathcal T'$ display-equivalent to ${X \vdash A}$, and
\item 
if $\mathcal T'$ has an interpolant, then so does $\mathcal T$
\end{itemize}
was more difficult than for the logical introduction rules in the usual form,
but nonetheless feasible.

However if you also add the $(\bullet)$-distribution rules to the definition
of EDI and LDI, then it becomes much more complicated.
For example:
$$
\frac {\mathcal S'} {\mathcal S} =
\frac {A, \bullet G \vdash D} {\bullet \wbox A, \bullet G \vdash D} \ 
\begin{array}{c} \\ \Longrightarrow_D \end{array}\ 
\frac {A, \bullet G \vdash D} {\bullet (\wbox A, G) \vdash D} \  
\begin{array}{c} \\ \equiv \end{array}\ 
\frac {?? A \vdash *\bullet G, D ??} {\wbox A \vdash *G, \bullet D} 
$$

Here $\mathcal S$ is ${A, \bullet G \vdash D}$ and
$\mathcal S'$ is ${\bullet \wbox A, \bullet G \vdash D}$ (diagram, left).
If we let $\mathcal T$ be $\bullet (\wbox A, G) \vdash D$ (diagram, centre)
then we can use $\mathcal T' = \mathcal S'$,
but if we let $\mathcal T$ be $\wbox A \vdash *G, \bullet D$ (diagram, right)
then what should we use for $\mathcal T'$?
If we let $\mathcal T'$ be the sequent shown, $A \vdash *\bullet G, D$,
this is certainly display-equivalent to $\mathcal S$, and if it has
interpolant $K$ then $\mathcal T$ has interpolant $\wbox K$, 
but how can we describe the appropriate relation between  
$\mathcal T'$ and $\mathcal T$, if it exists?

Furthermore, let us make this example slightly more complicated by
letting $G = (B, *C)$.
Then we could have 
$$
\frac {\mathcal S'} {\mathcal S} =
\frac {A, \bullet (B, *C) \vdash D} {\bullet \wbox A, \bullet (B, *C) \vdash D} \ 
\begin{array}{c} \\ \Longrightarrow_D \end{array}\ 
\frac {A, \bullet (B, *C) \vdash D} {\bullet (\wbox A, (B, *C)) \vdash D} \  
\begin{array}{c} \\ \equiv \end{array}\ 
\frac {??} {\wbox A, B \vdash C, \bullet D} 
 = \frac {\mathcal T'} {\mathcal T} 
$$
In this diagram, what $\mathcal T'$ can we put in place of ?? such that
$\mathcal S' \Longrightarrow_D \mathcal T'$, and such that we can get an 
interpolant for $\mathcal T = \wbox A, B \vdash C, \bullet D$
from an interpolant for $\mathcal T'$?

\subsection{Some examples} \label{s-ex}
We looked at examples based on the situation above, and their interpolants.
Most simply, we let $B = \wbox (A \to H)$ and $C = \wdia (H \land \lnot D)$.
Then \mbox{$\lnot C \Leftrightarrow \wbox (H \to D)$}, so 
\mbox{$B \land \lnot C \Rightarrow \wbox (A \to D)$}.
(This result will hold in all our subsequent examples, though we will
have different $B$ and $C$).
Thus $(B, *C) \vdash \bullet (*A, D)$ will be derivable, as will
$\bullet (B, *C) \vdash (*A, D)$.
From these we can derive any of the following:
$$
\wbox A, B \vdash C, \wbox D \quad
\wdia A, B \vdash C, \wdia D \quad
A, \bbox B \vdash \bbox C, D \quad
A, \bdia B \vdash \bdia C, D
$$
with interpolants, respectively, $\wbox H$, $\wdia H$,
$\bdia \top \to H$ and $\bdia \top \land H$.

An easy way to see derivation of these is as follows:

\bpf
\A "$(B \to C) \lor \wbox (A \to D)$"
\U "$\bbox (B \to C) \lor (A \to D)$"
\U "$(\bdia B \to \bdia C) \lor (A \to D)$"
\U "$A \land \bdia B \to \bdia C \lor D$"
\U "$A , \bdia B \vdash \bdia C , D$"
\epf



We now look at more complex formulae for $B$ and $C$.
Let $$B_M = M \to N \land \wbox (A \to H) \qquad
C_M = M \to N \land \wdia (H \land \lnot D)$$
As above, $B_M \land \lnot C_M \Rightarrow \wbox (A \to D)$ is derivable,
and similarly for $B_N, C_N$.
Alternatively, note that $B \to C \Rightarrow B_M \to C_M$.
Thus, these are derivable:
$$
\wbox A, B_M \vdash C_M, \wbox D \quad
\wdia A, B_M \vdash C_M, \wdia D \quad
A, \bbox B_M \vdash \bbox C_M, D \quad
A, \bdia B_M \vdash \bdia C_M, D
$$
The first two of these have interpolants 
$M \to N \land \wbox H$ and $M \to N \land \wdia H$.
For the latter two it is more difficult.
\\ For $A, \bdia B_M \vdash \bdia C_M, D$
an interpolant is $\bbox M \to \bdia N \land H$.
\\ For $A, \bbox B_M \vdash \bbox C_M, D$
an interpolant is $\bbox (M \to N) \land (\bdia M \to H)$,
or, equivalently, $\bdia M \to \bbox (M \to N) \land H$.

Alternatively, let 
$$B_N = N \land (M \to \wbox (A \to H)) \qquad
C_N = N \land (M \to \wdia (H \land \lnot D))$$
Again, $B_N \land \lnot C_N \Rightarrow \wbox (A \to D)$ is derivable,
as are  
$$
\wbox A, B_N \vdash C_N, \wbox D \quad
\wdia A, B_N \vdash C_N, \wdia D \quad
A, \bbox B_N \vdash \bbox C_N, D \quad
A, \bdia B_N \vdash \bdia C_N, D
$$
The first two of these have interpolants 
$N \land (M \to \wbox H)$ and $N \land (M \to \wdia H)$.
\\ For $A, \bbox B_N \vdash \bbox C_N, D$
an interpolant is $\bbox N \land (\bdia M \to H)$.
\\ For $A, \bdia B_N \vdash \bdia C_N, D$
an interpolant is $\bbox (N \to M) \to \bdia N \land H$,
or, equivalently, $\bdia N \land (\bbox (N \to M) \to H)$.

Look for a constructive way of deriving these interpolants.
A particular difficulty is that any display logic proof of the sequents
involves sequents such as $\bullet (B, *C) \vdash (*A, D)$,
where either $B$ and $C$ appear together, or $A$ and $D$ appear together.
So interpolants of such sequents don't help in finding an interpolant of
(eg) $A, \bbox B \vdash \bbox C, D$.

One way for the above examples is thus (interpolants in the middle): 

\bpf
\A "$A, \bdia B \vdash H \vdash \bbox C, D$"
\U "$A, \bdia N \land \bdia B \vdash \bdia N \land H 
  \vdash \bdia N \land \bbox C, D$"
\U "$A, \bdia (N \land B) \vdash \bdia N \land H \vdash \bdia (N \land C), D$"
\U "$A, \bbox M \to \bdia (N \land B) \vdash \bbox M \to \bdia N \land H 
  \vdash \bbox M \to \bdia (N \land C), D$"
\U "$A, \bdia (M \to N \land B) \vdash \bbox M \to \bdia N \land H 
  \vdash \bdia (M \to N \land C), D$"
\U "$A, \bdia B_M \vdash \bbox M \to \bdia N \land H \vdash \bdia C_M, D$"
\epf

\bpf
\A "$A, \bdia B \vdash H \vdash \bbox C, D$"
\U "$A, \bdia M \to \bdia B \vdash \bdia M \to H \vdash \bdia M \to \bbox C, D$"
\U "$A, \bbox (M \to B) \vdash \bdia M \to H \vdash \bbox (M \to C), D$"
\U "$A, \bbox N \land \bbox (M \to B) \vdash \bbox N \land (\bdia M \to H)
  \vdash \bbox N \land \bbox (M \to C), D$"
\U "$A, \bbox (N \land (M \to B)) \vdash \bbox N \land (\bdia M \to H)
  \vdash \bbox (N \land (M \to C)), D$"
\U "$A, \bbox B_N \vdash \bbox N \land (\bdia M \to H) \vdash \bbox C_N, D$"
\epf

~

For $A, \bbox B_M \vdash \bbox C_M, D$,
do as for $A, \bbox B_N \vdash \bbox C_N, D$,
but replacing $N$ by $M \to N$.
Note that $B_M \equiv (M \to N) \land (M \to B)$, and 
similarly for $C$.
Thus $A, \bbox B_M \vdash \bbox C_M, D$ has interpolant
$\bbox (M \to N) \land (\bdia M \to H)$.

~

For $A, \bdia B_N \vdash \bdia C_N, D$,
do as for $A, \bdia B_M \vdash \bdia C_M, D$,
but replacing $M$ by $N \to M$.
Note that $B_N \equiv (N \to M) \land (N \land B)$, and 
similarly for $C$.
Thus $A, \bdia B_N \vdash \bdia C_N, D$ has interpolant
$\bbox (N \to M) \to \bdia N \land H$.

\subsection{Towards an alternative proof system which gives interpolants}
\label{s-alt}
We tried to find a proof system which doesn't move variables from one side to
another.  We could also think of this as a system where variables are coloured
red or green, and retain those colours throughout, and interpolants are
defined as in \S\ref{s-tableaux}.
Here the sequent $\bullet (B, *C) \vdash (*A, D)$, where 
$A$ and $B$ are red, and $C$ and $D$ are green, becomes
$$ B \vdash C \qquad A \vdash D $$
that is, a list of sequents.
What it means, semantically, is that for any worlds $u,v$, where
$uRv$, $B(u) \land A(v) \Longrightarrow C(u) \lor D(v)$.
Equivalently, either $(B \Longrightarrow C)(u)$ or $(A \Longrightarrow D)(v)$.

This approach resembles the hypersequents of Restall, 
“Proofnets for S5: sequents and circuits for modal logic,” pages 151-172 in
Logic Colloquium 2005, C. Dimitracopoulos, L. Newelski, and D. Normann (eds.),
number 28 in Lecture Notes in Logic. Cambridge University Press, 2007.
There a hypsersequent $X_1 \vdash Y_1 | \ldots | X_n \vdash Y_n$ means that 
given any worlds $w_1, \ldots, w_n$, 
there is some $i \in \{1,\ldots,n\}$ such that $X_i \vdash Y_i$ holds at $w_i$.

Here are derivations in this system of some of the sequents derived above.

\bpf
\A "$A, A \to H \vdash H \land \lnot D, D$"
\U "$A, \bullet \wbox (A \to H) \vdash * \bullet * \wdia (H \land \lnot D), D$" 
  "deep $(\wbox \vdash), (\vdash \wdia)$"
\U "$ \wbox (A \to H) \vdash \qquad
  A \vdash * \bullet * \wdia (H \land \lnot D), D$" "(a)" 
\U "$ \wbox (A \to H) \vdash \wdia (H \land \lnot D) \qquad
  A \vdash D$" "(b)"
\U "$ B \vdash C \qquad A \vdash D$" 
\epf

Steps (a) and (b) allow moving a formula preceded by $\bullet$ or $*\bullet*$
to an adjacent sequent (creating it if necessary).
Here the conclusion of (b) means
$\forall u, v$ such that $uRv$,
either $\wbox (A \to H) \vdash \wdia (H \land \lnot D)$ at $u$ or 
$A \vdash D$ at $v$.

The last sequent above is just an abbreviation of the previous one.
Using purely classical logic steps we can get either of 
the following derivations
$$\frac{B \vdash C \qquad A \vdash D}{B_M \vdash C_M \qquad A \vdash D}
\qquad \qquad
\frac{B \vdash C \qquad A \vdash D}{B_N \vdash C_N \qquad A \vdash D}$$
with $ B_M, C_M, B_N, C_N$ defined as shown, 
since, clearly, it is valid to perform any derivation 
on a single member of a list of sequents.
\begin{align*}
B_M & = M \to N \land \wbox (A \to H) &
C_M & = M \to N \land \wdia (H \land \lnot D) \\
B_N & = N \land (M \to \wbox (A \to H)) &
C_N & = N \land (M \to \wdia (H \land \lnot D))
\end{align*}

From $B \vdash C \qquad A \vdash D$ (or, similarly, $B_M, C_M$ or $B_N, C_N$)
we can perform the following derivation

\bpf
\A "$ B \vdash C \qquad A \vdash D$" 
\U "$ \vdash C \qquad A, \bbox B \vdash D$" "(c)"
\U "$ \qquad A, \bbox B \vdash \bbox C, D$" "(d)"
\epf
\qquad \qquad
\bpf
\A "$\forall u,v \mbox{ st } uRv.\ (B \Longrightarrow C)(u) \mbox{ or } 
  (A \Longrightarrow D)(v)$" 
\U "$\forall u,v \mbox{ st } uRv.\ C(u) \mbox{ or } 
  (A \land \bbox B \Longrightarrow D)(v)$" 
\U "$(A \land \bbox B \Longrightarrow \bbox C \lor D)(v)$" 
\epf

\bpf
\A "$ B \vdash C \qquad A \vdash D$" 
\U "$ B \vdash \qquad A \vdash \bdia C, D$" "(e)"
\U "$ \qquad A, \bdia B \vdash \bdia C, D$" "(f)"
\epf
\qquad
\bpf
\A "$\forall u,v \mbox{ st } uRv.\ (B \Longrightarrow C)(u) \mbox{ or } 
  (A \Longrightarrow D)(v)$" 
\U "$\forall u,v \mbox{ st } uRv.\ 
  \mbox{ if } B(u)$ \mbox{ then } $(A \Longrightarrow \bdia C \lor D)(v)$" 
\U "$(A \land \bdia B \Longrightarrow \bdia C \lor D)(v)$" 
\epf

~

Each derivation is shown using rules for lists of sequents,
with, on the right, the meanings of each of these sequents.
Here the rules for steps (c) and (e) are instances of a general rule which
permits moving a formula to a sequent to the right, with a $\bbox$ (antecedent)
or $\bdia$ (succedent).
The rules for steps (d) and (f) permit introduction of $\bbox$ (succedent) or
$\bdia$ (antecedent) into the sequent on the right,
which is only possible when the sequent on the left is being eliminated.

We also include all rules for a single sequent, applied to any sequent in a
list, which do not shift a formula from left to right or vice versa.
To compensate for the lack of a display property, we also allow ``deep''
application of inference rules.
The rules involving $\bullet$ and multiple sequents in the list
generalise to lists of sequents longer than just two, and
we think that this approach gives a complete set of rules.

Now, hopefully the steps shown on the right have interpolants, which can be
derived constructively, since
the rules do not shift formulae from left to right, or vice versa.

Here we list the derivations on the right of the above (rewritten), without the
$\forall u, v$, where 
$$B = \wbox (A \to H) \qquad C = \wdia (H \land \lnot D)$$

\vspace{-2ex}
\bpf
\A "$A(v), B(u) \vdash H(v) \vdash C(u), D(v)$" 
\U "$A(v), (\bbox B)(v) \vdash \top(u) to H(v) \vdash C(u), D(v)$" 
\U "$A(v), (\bbox B)(v) \vdash (\bdia\top \to H)(v) \vdash (\bbox C)(v), D(v)$" 
\epf
\vspace{2ex}

Note that the third line doesn't follow from the second as written:
the omitted ``$\forall u$'' in the second line justifies this inference.
The following example is similar.

\vspace{-2ex}
\bpf
\A "$A(v), B(u) \vdash H(v) \vdash C(u), D(v)$" 
\U "$A(v), B(u) \vdash \top(u) \land H(v) \vdash (\bdia C)(v), D(v)$" 
\U "$A(v), (\bdia B)(v) \vdash (\bdia\top \land H)(v)
  \vdash (\bdia C)(v), D(v)$" 
\epf
\vspace{2ex}

That is, the interpolant for 
$ A, \bbox B \vdash \bbox C, D$ is $\bdia\top \to H$
and for $ A, \bdia B \vdash \bdia C, D$ is $\bdia\top \land H$.

\subsubsection{Some more complex examples, using $B_M, C_M$ or $B_N, C_N$}
\label{s-mc}
Now let us try more complex examples, replacing $B, C$ with
$B_M, C_M$ or $B_N, C_N$, where
\begin{align*}
B_M & = M \to N \land \wbox (A \to H) &
C_M & = M \to N \land \wdia (H \land \lnot D) \\
B_N & = N \land (M \to \wbox (A \to H)) &
C_N & = N \land (M \to \wdia (H \land \lnot D))
\end{align*}

\paragraph{Examples, using $B_M, C_M$}
Then $A(v), B_M(u) \vdash C_M(u), D(v)$ 
has interpolant $M(u) \to N(u) \land H(v)$,
as do $A(v), (\bbox B_M)(v) \vdash C_M(u), D(v)$ 
and $A(v), B_M(u) \vdash (\bdia C_M)(v), D(v)$.

That is, for all $u$ such that $uRv$ (and where we write $\forall u$ or
$\exists u$, this implies $u$ such that $uRv$), the following hold:
\begin{align*}
A(v), (\bbox B_M)(v) & \vdash M(u) \to N(u) \land H(v) \\ 
A(v), (\bbox B_M)(v) & \vdash (\forall u.\ M(u) \to N(u) \land H(v)) \\ 
A(v), (\bbox B_M)(v) & \vdash (\forall u.\ M(u) \to N(u)) \land
 ((\exists u.\ M(u)) \to H(v)) \\
A(v), (\bbox B_M)(v) & \vdash (\bbox (M \to N))(v) \land
 ((\bdia M)(v) \to H(v)) \\
A, \bbox B_M & \vdash \bbox (M \to N) \land (\bdia M \to H)
\end{align*}

Likewise, for all $u$ such that $uRv$, we have:
\begin{align*}
M(u) \to N(u) \land H(v) & \vdash C_M(u), D(v) \\
(\forall u.\ M(u) \to N(u) \land H(v)) & \vdash (\forall u.\ C_M(u)), D(v) \\
\bbox (M \to N) \land (\bdia M \to H) & \vdash \bbox C_M, D
\end{align*}

so $(\bbox (M \to N)) \land (\bdia M \to H)$ is an interpolant for 
$A, \bbox B_M \vdash \bbox C_M, D$

By similar argument we have, for all $u$ such that $uRv$,
\begin{align*}
A(v), B_M(u) & \vdash M(u) \to N(u) \land H(v) \\
A(v), (\exists u.\ B_M(u)) & \vdash (\exists u.\ M(u) \to N(u) \land H(v)) \\
A(v), (\bdia B_M)(v) & \vdash
  (\forall u.\ M(u)) \to (\exists u.\ N(u)) \land H(v)) \\
A, \bdia B_M & \vdash \bbox M \to \bdia N \land H
\end{align*}

Likewise, for all $u$ such that $uRv$,
\begin{align*}
M(u) \to N(u) \land H(v) & \vdash (\bdia C_M)(v), D(v) \\
(\exists u.\ M(u) \to N(u) \land H(v)) & \vdash (\bdia C_M)(v), D(v) \\
\bbox M \to \bdia N \land H & \vdash \bdia C_M, D
\end{align*}

so $\bbox M \to \bdia N \land H$ is an interpolant for 
$A, \bdia B_M \vdash \bdia C_M, D$.

A simpler approach to these particular examples follows:
we have
$$\forall v.\ \forall u.\ 
A(v), B_M(u) \vdash M(u) \to N(u) \land H(v) \vdash C_M(u), D(v)$$

Therefore the following hold, for all $v$:
\begin{align*}
\forall u.\ A(v), B_M(u) \vdash \forall u.\ M(u) \to N(u) \land H(v) \vdash
\forall u.\ C_M(u), D(v) \\
\exists u.\ A(v), B_M(u) \vdash \exists u.\ M(u) \to N(u) \land H(v) \vdash
\exists u.\ C_M(u), D(v) 
\end{align*}

Now, except if there are no $u$ such that $uRv$, we have

\begin{align*}
\forall u.\ A(v), B_M(u) & \equiv A(v), (\bbox B_M)(v) \\
\forall u.\ C_M(u), D(v) & \equiv (\bbox C_M)(v), D(v) \\
\exists u.\ A(v), B_M(u) & \equiv A(v), (\bdia B_M)(v) \\
\exists u.\ C_M(u), D(v) & \equiv (\bdia C_M)(v), D(v) 
\end{align*}

Finally, we have that 
\begin{align*}
\forall u.\ M(u) \to N(u) \land H(v) & \equiv
(\forall u.\ M(u) \to N(u)) \land (\forall u.\ M(u) \to H(v)) \\
 & \equiv (\bbox (M \to N))(v) \land (\bdia M \to H)(v) 
\\
\exists u.\ M(u) \to N(u) \land H(v) & \equiv
(\forall u.\ M(u)) \to (\exists u.\ N(u)) \land H(v) \\
 & \equiv
(\bbox M \to \bdia N \land H)(v)
\end{align*}

\paragraph{Examples, using $B_N, C_N$}
Similarly $A(v), B_N(u) \vdash C_N(u), D(v)$ 
has interpolant $N(u) \land (M(u) \to H(v))$,
as do $A(v), (\bbox B_N)(v) \vdash C_N(u), D(v)$ 
and $A(v), B_N(u) \vdash (\bdia C_N)(v), D(v)$.

Then similar arguments to the above give 
$A, \bbox B_N \vdash \bbox N \land (\bdia M \to H)$ and
$\bbox N \land (\bdia M \to H) \vdash \bbox C_N, D$,
so $\bbox N \land (\bdia M \to H)$ is an interpolant for 
$A, \bbox B_N \vdash \bbox C_N, D$.

Likewise, using the fact that 
$N(u) \land (M(u) \to H(v)) = (N(u) \to M(u)) \to (N(u) \land H(v))$,
similar arguments give 
$A, \bdia B_N \vdash \bbox (N \to M) \to \bdia N \land H$ and
$\bbox (N \to M) \to \bdia N \land H \vdash \bdia C_N, D$,
so $\bbox (N \to M) \to \bdia N \land H$ is an interpolant for 
$A, \bdia B_N \vdash \bdia C_N, D$.

In more detail, the interpolant $N(u) \land (M(u) \to H(v))$
gives interpolants in the modal logic as follows:
\begin{align*}
\forall u.\ N(u) \land (M(u) \to H(v)) & \equiv
(\forall u.\ N(u)) \land (\forall u.\ M(u) \to H(v)) \\
 & \equiv (\bbox N)(v) \land (\bdia M \to H)(v) 
\\
\exists u.\ N(u) \land (M(u) \to H(v)) & \equiv
\exists u.\ (N(u) \to M(u)) \to (N(u) \land H(v)) \\
& \equiv (\forall u.\ N(u) \to M(u)) \to (\exists u.\ N(u) \land H(v)) \\
& \equiv (\bbox (N \to M)) (v) \to (\bdia N \land H)(v) 
\end{align*}


We now need to look at to what extent these construction of interpolants can be
generalised.  
Recall that at the end of \S\ref{s-ex} we found these interpolants but said 
``I couldn't see any constructive way of deriving these interpolants.''
In \S\ref{s-alt} we have found these same interpolants in a more constructive
way, but the question remains as to how much this can be generalised.

It should be possible to mimic derivations using lists of sequents by
derivations involving expressions such as 
$\forall u,v \mbox{ st } uRv.\ A(v), B_M(u) \vdash C_M(u), D(v)$ 
and since these derivations do not move formula from left to right or vice
versa, it should be generally possible to construct an interpolant 
(such as $M(u) \to N(u) \land H(v)$ in this example).

From there we had the problem that we had to be able to express
$\forall u.\ M(u) \to N(u) \land H(v)$ or
$\exists u.\ M(u) \to N(u) \land H(v)$
as $F(v)$ for some formula $F$.
This should be generally possible, as in an example like the ones given 
(where we aim to get a sequent in terms of $v$ by eliminating $u$), we could
\begin{itemize}
\item 
express the formula in conjunctive or disjunctive (respectively) normal form,
\item 
in each conjunct (disjunct) collect the disjuncts (conjuncts)
involving $u$ together, and those involving $v$
\item apply the quantifier just to the disjuncts (conjuncts) involving $u$ 
\item turn these into formulae using $\bbox$ or $\bdia$
\end{itemize}

\section{Using only rules which don't move formulae from side to side}
We tried to devise a proof system which has the property that formulae are not
moved from side to side of a sequent.
Then there should be no difficulty in showing that rules preserve the existence
of an interpolant.  
For example, the standard sequent rule for modal logic,
preserves interpolants because if $K$ is an interpolant for the numerator, 
then $\wbox K$ is an interpolant for the denominator. 

$$
\frac{\Gamma \vdash A}{\wbox \Gamma \vdash \wbox A}(\wbox) \qquad
\frac{X, Y \vdash Z}{X \vdash *Y, Z}(ca1) \qquad
\frac{X \vdash Y}{*Y \vdash *X}(*) \qquad
\frac{*(X, Y) \vdash Z}{*X, *Y \vdash Z}(*\mbox{-}dist\vdash)
$$ 

The obvious first requirement for this is that we do not use the comma rules
such as $(ca1)$ above
(although it is alright to use the (*) rule, since
an interpolant $K$ for the numerator gives the interpolant $\lnot K$ for the
denominator).
Also we can allow certain derived rules such as $(*\mbox{-}dist\vdash)$, shown.

This means that we must allow deep application of rules,
such as 
$$
\frac{X[A] \vdash Y}{X[\bullet \wbox A] \vdash Y}(\wbox\vdash) 
$$
where $A$ is a succedent part of $X[A]$, etc.

Now if we avoid using the rules like $(ca1)$, this creates a problem for proofs
like

\vspace{-2ex}
\bpf
\A "$\bullet B, C \vdash * \bullet * X$" 
\U "$\bullet B, \bullet * X \vdash * C$" 
\U "$\bullet (B, *X) \vdash * C$" "$(\bullet\mbox{-}dist\vdash)$"
\U "$B, *X \vdash \bullet * C$"
\U "$B, * \bullet * C \vdash X$"
\epf
\vspace{2ex}

We can simply include this (and others like it) as a derived rule.
Our hope is that no proof really needs to bring (here) $B$ and $X$
together under a $\bullet$ since they eventually get separated
(assuming the sequent to be proved eventually has $B$ and $X$ on the opposite
sides.

There remains a problem with contraction.  If we disallow rules such as 
$(ca1)$, we need to allow the following rule:
$$
\frac{A \vdash *A, X}{A \vdash X}(ctr) 
$$
which does not (obviously) preserve the property of having an interpolant.

\subsection{Is contraction admissible?}
So, can we do without contraction?

We need the rule $(\bullet\mbox{-}dist\vdash)$
$$
\frac{\bullet (X, Y) \vdash Z}{\bullet X, \bullet Y \vdash Z}
  (\bullet\mbox{-}dist\vdash)
$$
which is proved using contraction --- so let us include it as a derived
rule (which does not cause a problem for interpolation).
Having included this rule we can limit the need for contraction to formulae,
by virtue of the rules $(\bullet\mbox{-}dist\vdash), (*\mbox{-}dist\vdash)$,
commutativity and associativity.
This was proved in Isabelle, theorem \texttt{fml\_ctr}.
This may make the proof of admissibility of contraction simpler.

Having included the $(\bullet\mbox{-}dist\vdash)$ rule, and shown that we then
need contraction for (at most) formulae only, can we do without contraction
completely?
This would require modifying all the logical introduction rules to include a
copy of the principal formula in the premises, for example changing 
the rule on the left below to the one on the right.
$$
\frac{X \vdash A, B}{X \vdash A \lor B} \qquad
\frac{X \vdash A, B, A \lor B}{X \vdash A \lor B} 
$$

\subsubsection{Proof of some contraction admissibility result}
The natural way of proving that contraction is admissible is to 
consider a sequent $A, A \vdash X$, and prove it by induction on the derivation
of that sequent.
Thus, for example, when the previous step in the derivation of $A, A \vdash X$
is say $A, A \vdash X'$, we assume as the inductive hypothesis that 
if $A, A \vdash X'$ is derivable then $A \vdash X'$ is derivable.
Since $A, A \vdash X'$ is derivable, we have that $A \vdash X'$ is derivable
and now the last step is that therefore $A \vdash X$ is derivable.

But if the last step is one of the display postulates, for example
$$
\frac{A \vdash X, *A}{A, A \vdash X} \qquad
\frac{\bullet (A, A) \vdash X}{A, A \vdash \bullet X} \qquad
\frac{*X \vdash * (A, A)}{A, A \vdash X} 
$$
this proof method doesn't seem to work unless we set the property of a
sequent $S$, to be proved by induction on the derivation of $S$ is as follows:
that any sequent $S'$, got by applying any sequence of rules from the set
$\mathcal R$ to $S$,
is derivable without using contraction.
And considering the rules above, it appears that $\mathcal R$ needs to consist
of at least the display postulates and formula contractions. 

Note that the last step may be another contraction,
from ${A, A, A \vdash \bullet X}$.
Thus we need to allow the sequence of steps from $S$ to $S'$ to contain
\emph{multiple} contraction steps.

Considering now the $\bullet$-distribution rule,
we may have the derivation step 
$$
\frac {\bullet A, \bullet A \vdash X} {\bullet (A, A) \vdash X} 
\begin{array}{c}  ~ \\ (~= S) \end{array}
$$
Here, since display postulates (rules in $\mathcal R$)
and contraction give ${\bullet A \vdash X}$
from $S$, we want to prove that ${\bullet A \vdash X}$
is derivable without using contraction.
For this we need to add $\bullet$-distribution to $R$;
then, since rules in $\mathcal R$ 
and contraction give ${\bullet A \vdash X}$
from ${\bullet A, \bullet A \vdash X}$
the inductive hypothesis gives that ${\bullet A \vdash X}$ is derivable without
using contraction.

Now, to make contraction admissible the natural approach is to add the
principal formula of logical introduction rules to the premises.
Thus for example the rule on the left becomes the rule on the right.
$$
\frac{A' \vdash X}{A \vdash X} \qquad
\frac{A', A \vdash X}{A \vdash X}
$$
Then, any sequence of display postulates from $A \vdash X$ 
(to get, say, $Z[A] \vdash X$) can be reproduced 
as a sequence of display postulates from $A', A \vdash X$ 
to get $Z[A', A] \vdash X$.
Then, when $Z[A] \vdash X$ admits contraction on A
(say $Z[A]$ is $Y [A, A]$),
$Z[A', A]$ is $Y [(A', A), A]$, from which associativity and contraction
gives $Y [A', A]$.
By the inductive hypothesis, the sequent 
$Y[A', A] \vdash X$ is derivable without using contraction.
Then the modified form of the introduction rule gives $Y[A] \vdash X$,
which is the result of contracting $Z[A] \vdash X$.
This is the usual way of proving contraction admissibility.

However, now that we have enlarged $\mathcal R$ to include the
$\bullet$-distribution rules, this does not seem to work.
Consider the proof step (on the right) using the rule on the left.
$$
\frac{\bullet \wbox A, A \vdash X}{\bullet \wbox A \vdash X} \qquad 
\frac{\bullet \wbox A, A, \bullet G \vdash X}
  {\bullet \wbox A, \bullet G \vdash X} 
\begin{array}{c}  ~ \\ (~= S) \end{array}
$$
Now, from $S$ a sequence of rules in $\mathcal R$, 
where $G' \equiv G$ and from $G'$ you can obtain $\wbox A, G''$, gives

\vspace{-2ex}
\bpf
\A "$\bullet \wbox A, \bullet G \vdash D$"
\U "$\bullet \wbox A, \bullet (\wbox A, G'') \vdash D$"
\U "$\bullet (\wbox A, \wbox A, G'') \vdash D$" "$(\bullet\mbox{-}dist)$"
\U "$\bullet (\wbox A, G'') \vdash D$" "$(ctr)$"
\epf
\vspace{2ex}

So what can we get from the numerator that corresponds to this?
We want to do a contraction on $\wbox A$, see below.

\vspace{-2ex}
\bpf
\A "$\bullet \wbox A, A, \bullet G \vdash D$"
\U "$\bullet \wbox A, A, \bullet (\wbox A, G'') \vdash D$"
\U "$\bullet (\wbox A, \wbox A, G''), A \vdash D$" "$(\bullet\mbox{-}dist)$"
\U "$\bullet (\wbox A, G''), A \vdash D$" "$(ctr)$"
\epf
\vspace{2ex}

Then we have the inductive result that $\bullet (\wbox A, G''), A \vdash D$
is derivable without the use of contraction.
We then want to use the logical introduction rule to remove the $A$,
but we can't.

What to do?  

Here the good news is that it is logically valid to go from 
$\bullet (\wbox A, G''), A \vdash D$ to $\bullet (\wbox A, G'') \vdash D$.
How to do this in a way which is simplest and most general?

\subsubsection{The system DKt}
In \cite{gore-postniece-tiu-deep-tense}, a system \textbf{DKt} of rules is
given for tense logic.  \textbf{DKt} does not include contraction, and contains
logical introduction rules for $\wbox$, $\bbox$, $\land$ and $\lor$ which have
the principal formula copied into the premises.
\textbf{DKt} is a deep inference system, working on multisets of formula (like
the right-hand side of a sequent).

The rules called $\wdia_1$ and $\wdia_2$ are shown, translated into sequents,
and with our connectives, without showing the deep inference.
$$
\frac{X \vdash \bullet (\Delta, A), \wdia A} {X \vdash \bullet \Delta, \wdia A} 
(\wdia_1) \qquad
\frac{X \vdash * \bullet * (\Delta, \wdia A), A}
  {X \vdash * \bullet * (\Delta, \wdia A)} 
(\wdia_2)  \qquad
\frac{\bullet (\wbox A, G''), A \vdash D} {\bullet (\wbox A, G'') \vdash D}
$$
Here we note that the rule $(\wdia_2)$ is equivalent to the rule on the right
which is exactly what we need in the example discussed above.

We now have a complete contraction-free system.
How does it go for proving interpolation?
We need to consider interpolation in the sense where formula in the conclusion
are coloured red or green.
The rule $(\wdia_1)$ does not look good for this because it may be that 
$\Delta$ is red and $A$ is green, or vice versa,
and they get put together in the premises.

However this rule could also be seen as (1) below
$$
\frac {\wbox B \vdash \wbox (B \to D)} {\wbox B \vdash \wbox D}(1) \qquad
\frac{\wbox B \vdash \wbox (B' \to D)}{\wbox B \vdash \wbox B' \to \wbox D}(2) 
$$
This can be proved using the interpolation-friendly rule (2)
(by setting $B' = B$), but then to prove $\wbox B \vdash \wbox B \to \wbox D$
requires propositional logic including contraction.

Can we replace $(\wdia_1)$ with some interpolation-friendly rule without
requiring contraction?

Alternatively, note that the rule is like a combination of the rule (3)
(equivalent to (3')) with contraction, and,
given that weakening is admissible, $(\wdia_1)$ makes (3) admissible.
$$
\frac{X \vdash \bullet (\Delta, A)} {X \vdash \bullet \Delta, \wdia A}(3)
\qquad
\frac{X \vdash \wbox (\Delta, A)} {X \vdash \wbox \Delta, \wdia A}(3')
$$

\section{Conclusion and Discussion}
We have recounted the difficulties we found in adapting the proof of 
Brotherston \& Gor\'e of interpolation for the display calculus for classical
propositional logic to tense logic.
Considering the proof of Nguyen for tableau systems for modal logic we 
could relate his proof method to the proof for the display calculus for
classical logic.
However, when applied to tense logic, these two proof methods no longer show a
simple correspondence.
We described the difficulties encountered in attempting to use the display
calculus proof method (involving the local display interpolation property)
for tense logic.

Having devised some rather difficult examples, we examined how an interpolant
for these might be constructed, and devised an alternative calculus for proofs
in tense logic, involving lists of sequents, where each sequent in the list
applies to different worlds.  
We gave examples of how to find interpolants for our difficult examples
based on proofs using this calculus, suggesting that this
calculus might enable a constructive proof of the interpolation property
for tense logic.

\begin{thebibliography}{10}
\bibitem{brotherston-gore-interpolation}
\newblock James Brotherston \& Rajeev Gor\'e.
\newblock Craig Interpolation in Displayable Logics
\newblock In Proc.\ Tableaux, 2011. DETAILS

\bibitem{gore-postniece-tiu-deep-tense}
R Gor\'e, L Postniece and A Tiu.
On the Correspondence between Display Postulates and Deep Inference in Nested
Sequent Calculi for Tense Logics.
Logical Methods in Computer Science 7 (2:8) 2011. 

\end{thebibliography}
\end{document}


