数理解析研究所講究録
1021 巻 1997 年 178-186

178

Interpolation Theo-rem for$L_{\mathrm{D}\mathrm{B}\mathrm{C}\mathrm{C}}$,

Bayu Surarso

and$L_{\mathrm{D}\mathrm{B}\mathrm{C}\mathrm{K}}$$(/\backslash ^{\backslash i}\mathrm{y}_{-}\mathrm{x}_{\text{フノ}^{}\sim_{1\mathrm{V}^{\backslash }}})$

Graduate School of Information Engineering,
Hiroshima University, Higashi Hiroshima, 739, Japanand
Department of Mathematics,
Faculty of Mathematics and Natural Sciences,
Diponegoro University, Semarang, Indonesia.

1

Introduction

It is known that the interpolation theorem holds for the logics LR and LRW, which are
obtained from the relevant logic and RW respectively by omitting the distributive
axiom $A\wedge(B\vee C)arrow$ ( A ) (A A ) (see [7] and [2]). On the other hand, Urquhart
proved in [13] that the interpolation theorem fails for , RW and some other relevant$\mathrm{R}$

$A$

$B$

${ }$

$C$

$\mathrm{R}$logics. He also claims that the interpolation theorem fails for the positive versions of
all the logics discussed, provided that either the language contains the constant or theis provable. This fact shows that the distributive axiom
formulaI( $(A\supset B)$ A )seems to play a critical role in the interpolation problems for substructural logics. In
the present study we will show that the interpolation theorem holds for the logics, respectively, by addingand, which are obtained fromandthe distributive law A $(B\vee C)arrow$ ( A ) (A A ) as an initial sequent. Ono and.
andKomori proved in [11] that the interpolation theorem holds for
Slaney in [12] introduced sequent systems without cut rule which are equivalent to. We will take Slaney’s systems, but in a slightly modified form, andanduse essentially Maehara’s method introduced in [6] to prove the interpolation theorem
$t$

$A$

$L_{\mathrm{D}\mathrm{B}\mathrm{C}\mathrm{C}}$$\supset B$$L_{\mathrm{B}\mathrm{C}\mathrm{K}}$$L_{\mathrm{B}\mathrm{C}\mathrm{C}}$$L_{\mathrm{D}\mathrm{B}\mathrm{C}\mathrm{K}}$

$A$

$A$

$B$

${ }$

$C$

$L_{\mathrm{B}\mathrm{C}\mathrm{C}}$$L_{\mathrm{D}\mathrm{B}\mathrm{C}\mathrm{C}}$$L_{\mathrm{B}\mathrm{C}\mathrm{K}}$$L_{\mathrm{D}\mathrm{B}\mathrm{C}\mathrm{K}}$for these logics.
A note about the names of the logics discussed. To avoid any confusion with those

179
.
and
[11] and [12], here we also use the names of logics
However it must be noticed that the letters and which appear in them have no
and K. Better names for them can be found inconnection with the combinators[9] or [10]. In those papers Ono introduced the basic logical system FL (full Lambek
since they can beandforlogic) and then gave the names
andobtained from FL by adding the weakening rule and the exchange and weakening rules,$L_{\mathrm{B}\mathrm{C}\mathrm{C}},$$L_{\mathrm{B}\mathrm{C}\mathrm{K}},$$L_{\mathrm{D}\mathrm{B}\mathrm{C}\mathrm{C}}$$L_{\mathrm{D}\mathrm{B}\mathrm{C}\mathrm{I}(}$$\mathrm{K}$$\mathrm{C}$$\mathrm{C}$$\mathrm{F}\mathrm{L}_{w}$$L_{\mathrm{B}\mathrm{C}\mathrm{K}}$$L_{\mathrm{B}\mathrm{C}\mathrm{C}}$$\mathrm{F}\mathrm{L}_{\mathrm{e}w}$respectively. By the reason mentioned above we will denote our systems, which are, respectively.
, byandequivalent toand$L_{\mathrm{o}}L_{\mathrm{D}\mathrm{B}\mathrm{c}}\kappa$$L_{O}L_{\mathrm{D}\mathrm{B}}\mathrm{c}\mathrm{C}$$L_{\mathrm{D}\mathrm{B}\mathrm{C}\mathrm{K}}$$L_{\mathrm{D}\mathrm{B}\mathrm{C}\mathrm{C}}$The full version of the present paper will appear as [1]. The authour would like toexpress his sincere gratitude to Professor Hiroakira Ono and Dr. Toshiyasu Arai for
their suggestions and comments.

2

Gentzen sequent systems$L_{\theta}L_{\mathrm{D}\mathrm{B}}\mathrm{c}\mathrm{C}$and$L_{\mathrm{o}}L_{\mathrm{D}\mathrm{B}\mathrm{C}\mathrm{K}}$, in theandSlaney in [12] introduced sequent systems without cut rulesame way as relevant systems discussed in [3] and [5]. These systems are equivalent to. They contain two types of structural connectives, the extensional
andstructural connective “,” which corresponds to the extensional conjunction and theintensional structural connective “;” which corresponds to the intensional conjunction
or fusion. Having these two types of structural connective, two types of structural
rules (extensional and intensional) will be formulated in these systems. By using these$LL_{\mathrm{D}\mathrm{B}\mathrm{C}\mathrm{K}}$$LL_{\mathrm{D}\mathrm{B}\mathrm{C}\mathrm{C}}$$L_{\mathrm{D}\mathrm{B}\mathrm{C}\mathrm{K}}$$L_{\mathrm{D}\mathrm{B}\mathrm{C}\mathrm{C}}$rules, the distributive law can be derived.

In the following, we will give a definition of these systems, but in a slightly modified form. As in [12] our language will contain the false constant , implication ,disjunction V and two kinds of conjunction, i.e. the extensional conjunction A and the$\perp$$\supset$.
intensional, structures (see [5]), which are called bunches
First, for our sequent systemof premises in [12], are defined recursively as follows;
1) any formula is a structure,2) for $n\geq 2$ , if eachis a structure for $i=1,$ , , then both sequences$\mathrm{c}\mathrm{o}\mathrm{n}\mathrm{i}\mathrm{u}\mathrm{n}\mathrm{C}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}*$$L_{o}L_{\mathrm{D}\mathrm{B}\mathrm{c}}\mathrm{c}$$z\mathrm{Y}_{i}$$\ldots$

and$(_{Z}\mathrm{Y}_{1}$;$\ldots$;$z\mathrm{Y}_{n})$$(X_{1}, \ldots , X_{n})$$n$are structures.

are said to be
and of the form
Structures of the form
is called an immediate
extensional and intensional, respectively. Each structure;;
is of the form
. Here, if
andconstituent of$(X_{1}; \ldots;X_{n})$$(X_{1}, \ldots, X_{n})$$X_{1}$$(X_{1}, \ldots , \mathrm{X}_{n})$$(X_{1}$$\ldots$$z\mathrm{Y}_{n})$$X_{k}$$(\mathrm{Y}_{1}, \ldots, l_{m_{1}}’)$

180, , then the above. $(X_{1}, \ldots,X_{n})$ should be un$j=1,$
for some structures
is of the form
. Similarly, if
derstood as;;should, , then the above$j=1,$;;
for some structures. Thus, we will assume thatbe understood as
no extensional (intensional) structures have an extensional (intensional) structure as
their immediate constituent.
$Z,$
and $W$ with or without subscripts will denoteIn the sequel, the letters
structures. We will omit parentheses when no confusions will occur.
$\mathrm{Y}_{j},$$\ldots$$m_{1}$$(X1, \ldots,xk-1,\mathrm{Y}1, \ldots,\mathrm{Y}m’ X_{k+}1, \ldots , X_{n})$$\mathrm{Y}_{m_{2}})$$(\mathrm{Y}_{1}$$\mathrm{Y}_{j},$$\ldots$$\ldots$$X_{l}$$(X_{1}$$m_{\mathit{2}}$$\ldots$$X_{n})$$(X_{1}; \ldots ; X_{l-1;}\mathrm{Y}1;\cdots ; \mathrm{Y}_{m_{2}} ; X_{l+}1;\cdots ; X_{n})$$U$$X,\mathrm{Y},$

Substructures of a given structure $X$ in
1) if a structure$X_{1},$$\ldots$,$X_{n}$$L_{\mathrm{o}}L_{\mathrm{D}\mathrm{B}\mathrm{c}}\mathrm{c}$occurs in $X$ thenis a substructure of $X$ for $i=1,$1.2) any subsequence of the sequence1.1) each$x_{:}$$X_{1},$$X_{1}$$\ldots$, ,$n$$\ldots$$\ldots,X_{n}$; ;occurs in $X$ then
2.1) eachis a substructure of $X$ for $i=1,$;;2.2) any subsequence of the sequence2) if a structure

are defined as follows;

is a substructure of $X$ ,$X_{n}$$x_{:}$$X_{1}$$\ldots$, ,$n$$\ldots$$X_{n}$

is a substructure of $X$ .

Here, subsequences are defined as usual. Thus, suppose $X=\mathrm{Y},$ $(Z;U),$ $W$ . Then$(Z;U),$ $W$ and $X$ itself are examples of subsequences of $X$ . On the other hand, $Z$ and$\mathrm{Y},$are examples of sequences which are not subsequences of .
is used for denoting the structure with an
Following [12], an expression like
$X$

$Z,$ $W$$\Gamma(X)$denotes the structure obtained
indicated substructure-occurrence $X$ in it. Thenby replacing the indicated substructure-occurence $X$ in it by a structure
from
Y. A sequent is an expression of the form $Xarrow A$ , where $X$ is a structure (possibly
will be given as follows:
empty) and is a formula. Then$\Gamma(\mathrm{Y})$$\Gamma(X)$$A$$L_{\mathrm{o}}L_{\mathrm{D}\mathrm{B}}\mathrm{c}\mathrm{C}$It consists of the initial sequentsand$Aarrow A$$\perparrow A$,

the following structural rules$\frac{\Gamma(\mathrm{Y},X)arrow C}{\Gamma(X,\mathrm{Y})arrow c}$$\frac{\Gamma(X,x)arrow c}{\Gamma(X)arrow C}$

and the following$\mathrm{r}\mathrm{u}$( $E$ –exchange)$\frac{\Gamma(X)arrow C}{\Gamma(X,\mathrm{Y})arrow c}$( $E$ –contraction).

(E–weakening)$\frac{\Gamma(X)arrow C}{\Gamma(X,\mathrm{Y})arrow c}$(I–weakening).les for logical connectives$. \frac{X,Aarrow B}{Xarrow A\supset B}(arrow\supset)$$\frac{Xarrow A\mathrm{r}(B)arrow c}{\Gamma(A\supset B\cdot X)arrow c},(\supsetarrow)$

181$\frac{\sim \mathrm{Y}arrow A}{\lambda’arrow A\mathrm{v}B}(arrow\vee 1)$$\frac{z\mathrm{Y}arrow B}{X’arrow A\mathrm{v}B}(arrow\vee 2)$$\frac{\Gamma(A)arrow C\mathrm{r}(B)arrow c}{\Gamma(A\vee B)arrow c}(\veearrow)$$\frac{Xarrow A\mathrm{Y}arrow B}{X,\mathrm{Y}arrow A\wedge B}(arrow\wedge)$$\frac{\Gamma(A,B)arrow C}{\Gamma(A\wedge B)arrow c}(\wedgearrow)$$, \frac{Xarrow A\mathrm{Y}arrow B}{X\cdot \mathrm{Y}arrow A*B}(arrow*)$$\frac{\Gamma(A,B)arrow c}{\Gamma(A*B)arrow C}.(*arrow)$.

For instance, applying ( $E$ –contraction) to a sequent of the form $(l’,\mathrm{x}, X, z)arrow C$ ,we can get the sequent $(l’, X, Z)arrow C$ . Thus, $X,X$ in $\Gamma(X, X)$ will be understood not
as a substructure but as a subexpression. We will use these sloppy definition\’{s}, simply
to avoid unnecessary complications. (See the footnotes 28 and 29 in Dunn [4]. )For our sequent system, if we define intensional structures as sequences,some difficulties will occur in the proof of the interpolation theorem given in the next
section. So, instead of taking sequences, we will take multisets, since the exchange law
holds in it. Thus for
we will modify the definition of structures as follows;
1) any formula is a structure,2) for $n\geq 2$ , if eachis a structure for $i=1,$ , , then both the sequence$L_{\mathrm{o}}L_{\mathrm{D}\mathrm{B}\mathrm{c}}\kappa$$L_{\mathrm{o}}L_{\mathrm{D}\mathrm{B}\mathrm{C}\mathrm{K}}$$z\mathrm{Y}_{i}$$\ldots$$n$are structures.
Substructures are defined similarly to that in the case for. Since we define
intensional structures as multisets, we can dispense with the intensional exchange rule.
Thus,
will have the same initial sequents, structural rules and rules for logical$(X_{1}, \ldots , X_{n})$and the multiset$\{X_{1}$;$\ldots$;$z\mathrm{Y}_{n}\}$$L_{\mathrm{o}}L_{\mathrm{D}\mathrm{B}}\mathrm{c}\mathrm{C}$$L_{\theta}L_{\mathrm{D}\mathrm{B}}\mathrm{C}\kappa$

connectives as the above$L_{\mathrm{o}}L_{\mathrm{D}\mathrm{B}\mathrm{C}}\mathrm{c}$.

For the equivalence of
see the proof of the equivalence of$L_{\mathrm{O}}L_{\mathrm{D}\mathrm{B}}\mathrm{c}\mathrm{C}(L_{O}L_{\mathrm{D}\mathrm{B}}\mathrm{C}\kappa)$3

and Hilbert system
and$LL_{\mathrm{D}\mathrm{B}\mathrm{C}\mathrm{C}}(LL_{\mathrm{D}\mathrm{B}\mathrm{C}\mathrm{K}})$Interpolation theorem for$H_{\mathrm{D}\mathrm{B}\mathrm{C}\mathrm{C}}(H_{\mathrm{D}\mathrm{B}\mathrm{C}\mathrm{K}})$$H_{\mathrm{D}\mathrm{B}\mathrm{C}\mathrm{C}}(H_{\mathrm{D}\mathrm{B}\mathrm{C}\mathrm{K}})$$L_{\mathrm{D}\mathrm{B}\mathrm{C}\mathrm{C}}$and,in [12].

$L_{\mathrm{D}\mathrm{B}\mathrm{C}\mathrm{K}}$We will show that the interpolation theorem holds forandby using thesystems, respectively. In the following the expressions $V(X)$anddenotes the set of propositional variables which occur in $X$ .
Ono and Komori proved in [11] that the interpolation theorem holds forandby showing that interpolation theorem of the following form holds for them:$L_{\mathrm{D}\mathrm{B}\mathrm{C}\mathrm{C}}$$L_{O}L_{\mathrm{D}\mathrm{B}}\mathrm{c}\mathrm{C}$$L_{\mathrm{D}\mathrm{B}\mathrm{C}\mathrm{K}}$$L_{\mathrm{o}}L_{\mathrm{D}\mathrm{B}\mathrm{C}\mathrm{K}}$$L_{\mathrm{B}\mathrm{C}\mathrm{C}}$$L_{\mathrm{B}\mathrm{C}\mathrm{K}}$182

If a sequent$X;\mathrm{Y};Zarrow D$

is provable, then there is a formula$C$such thatis provable,
2) $X;C;^{z}arrow D$ is provable,
1)$\mathrm{Y}arrow C$

3) $V(C,)\subset V(\mathrm{Y})\cap[V(x;Z)\cup V(D)]$ .

Here, all of

and$X,\mathrm{Y}$Thus forof the following:$L_{\mathrm{o}}L_{\mathrm{D}\mathrm{B}\mathrm{c}}\mathrm{c}$

$Z$

and

are sequences of formulas of the form

$L_{\mathrm{o}}L_{\mathrm{D}\mathrm{B}\mathrm{c}\kappa}$$A_{1}$;;$\ldots$$A_{n}$.

, a desirable form of interpolation theorem might be

Let $Xarrow D$ be a provable sequent. Suppose that
Then there is a formula such that
1) $Zarrow C$ is provable,
2) $X_{\{C/\}}zarrow D$ is provable,$Z$

is a substructure-occurrence in $X$ .

$C$3) $V(C)\subset V(Z)\cap[V(_{\mathrm{Y}},\{-/Z\})\cup V(D)1\cdot$
denotes the structure obtained from $X$ by replacing
Heredenotes the structure obtained from $X$ by deleting .

$Z$$X_{\mathrm{t}^{c}/\}}\mathrm{z}$

by

$C$

and

$X_{\{-}/Z$}$Z$

In fact, even the folowing stronger form of interpolation theorem holds for them.
, .
be a substructure-occurrence in a structure for $i=1,$
do not intersect each another when $j\neq k$ and 2) there is
andand $Z”$
such that $Z’$ contains
inno structure-occurrences of the form $Z’$ ;contains
for some and . Then, if the sequent $Zarrow D$ is provable, there exist

Theorem 1 Let
Suppose that 1).

$Z$$Z_{*}$$Z$$Z^{\prime r}$1) each2)Here$\ldots,$$n$such thatis provable for $j=1,$ , ,} $:arrow D$ is provable,, $V(C_{j})\subset V(Z_{j})\cap[V(Z\mathrm{t}-/zi\}.\cdot)\cup V(D)1$ ,$p_{om}z$ by replacing Z. byfor every} denotes the stntcture obtained
, and
for
}: denotes the structure obtained $p_{om}z$ by deleting$Z_{j}arrow C_{j}$$z_{\mathrm{t}C:/Z}i$3) forfor $i=1,$$Z_{j}$$k$$j$$Z_{k}$$C_{i}$$j^{\mathrm{J}}=1,$$\ldots$$\ldots$

$n$

$n,$

$\cdot$$Z_{\{C:/}Z_{i}$$i=1,$$n$$Z_{k}$$Z_{j}$

formulas$\ldots$$c_{:}$$.\cdot$$\ldots,$$n$$z_{:}$$Z_{\{-/Z}:$$even/i=1,$ $\ldots,n$ .

To understand the conditions of in the above theorem, let us consider the case
. Here the above conditions are not satisfied if
where
are substructures of $Z’=X_{1}$andwe take $n=2,$ $Z_{1}=X_{1}$ and $Z_{2}=X_{3}$ , for, respectively. On the other hand, if we take $n=2,$ $Z_{1}=X_{1}$ andand $Z^{rr}=$.
$Z_{2}=X_{5}$ , then the above conditions are satisfied. In this case the above theorem says
such that
andthat if $Xarrow D$ is provable, then there exist formulas$z_{:}$$X=(_{p}\mathrm{Y}_{1}; x2;d\mathrm{Y}_{3}),z\mathrm{Y}_{4},$$(\mathrm{x}_{5;d}\mathrm{Y}_{6})$$X_{1}$$X_{3}$$z\mathrm{Y}_{2;_{J}\mathrm{Y}_{3}}$$C_{1}$$C_{2}$

1831) both$X_{1}arrow C_{1}$and$\mathit{1}\mathrm{Y}_{5}arrow C_{2}$are provable,
is provable,2)$(C_{1}; z\mathrm{Y}_{2;_{Z}}\mathrm{x}r_{3}),$3)$V(C_{1},)\subset V(_{-}\mathrm{Y}_{1})\cap[V((,\mathrm{Y}\mathit{2};d\mathrm{Y}_{3}), Z\mathrm{Y}_{4}, X_{6})\cup V(D)]$$x_{4},$ $(C_{2;}I\mathrm{Y}6)arrow D$

and.

$V(C_{2})\subset V(X_{5})\cap[V((X_{2;}z\mathrm{v}_{3}),J\mathrm{Y}4, d\mathrm{Y}6)\cup V(D)]$Next, let us consider the proof of Theorem 1 for$L_{o}L_{\mathrm{D}\mathrm{B}\mathrm{C}}\mathrm{c}$. As usual, the theorem

is proved by induction on the number of inferences in the proof figure of the sequent$Zarrow D$ . Here we will show the proof for the following case.
$l$

Case 1. $l>0$ and the last inference is. Here $Zarrow D$ will be of the form$\Gamma(AB)arrow D$ and the last inference will be of thellowing form;$(\veearrow)$$\mathrm{f}\dot{\mathrm{o}}$$\frac{\Gamma(A)arrow D\Gamma(B)arrow D}{\Gamma(A\vee B)arrow D}(\veearrow)$.

is substructure-occurence in $\Gamma(AB)$ for $i=1,$ , , such that theconditions in the theorem are satisfied. Here we will consider the following subcase;
Suppose that

$Z_{i}$$\ldots$

Subcase 1.1 The ’displayed’ $A\vee B$ in $\Gamma(AB)$ occcurs in$Z_{k}$$n$for some .
$k$Let . $=Z_{k\{A/}AB$ } and $U_{i}=Z_{i}$ when $i\neq k$ . Then by the hypothesis of induction
there exist formulas
for $i=1,$
such thatla) each,is provable for $j=1,$
is provable,$V(C_{j})\subset V.(U_{j})\cap[V(\Gamma(A)\{-/U:\}:)\cup V(D)]$ .
for $j=1,$$U_{k}$$C_{1}$$n$$\ldots,$$U_{j}arrow C_{j}$$\ldots,$$n$$2\mathrm{a})\mathrm{r}(A)_{\mathrm{t}}C:/U:\}iarrow D$$3\mathrm{a})$$\ldots n,$

Let
and $W_{1}=Z_{i}$ when $i\neq k$ . Then by the hypothesis of induction
there exist formulas C.’. for $i=1,$
such thateach
is provable for $j=1$ , . . . , ,is provable,$V(C’)j\subset V(W_{j})\cap[V(\Gamma(B)_{\mathrm{t}-/}W:\}:)\cup V(D)]$ .
for $j=1,$$W_{k}=z_{\iota_{\mathrm{t}}B/\}}.AB$$n$$\ldots,$$1\mathrm{b})$$W_{j}arrow C_{j}’$$n$$2\mathrm{b})\Gamma(B)\{c’.\cdot/W:\}_{i}arrow D$$3\mathrm{b})$$\ldots,$$n,$Now, for $i\neq k$ by. Note that whento this sequent we can get

. ..

to

$\mathrm{a}_{}\mathrm{P}\mathrm{p}\mathrm{l}\mathrm{y}\mathrm{i}\mathrm{n}\mathrm{g}(arrow\wedge)$$U$$arrow C$$i\neq k,$ $U_{i}=W_{i}=Z_{1}$$C_{i}\wedge C_{i}’$$Z_{i}arrow c_{:}$

A$C_{:}’$.

$W$, we can get
andThen, by applying (E–contraction)$W_{1}arrow C_{1}’.$$U_{:},$$arrow$;.

$U_{1}$$arrow C_{i}W_{i}arrow c,\underline{i\prime}(\wedgearrow)$$\frac{U.,W:arrow C_{i}\wedge c_{i}}{z_{:}arrow C.\wedge c_{i}}.$’By applying$(arrow\vee 1)$to$U_{k}arrow C_{k}$and(E–contraction)$(arrow\vee 2)$to.

$W_{k}$$arrow C_{k}’$we can get$U_{k}arrow c_{k}.\mathrm{v}c_{k}’$

and

184

$W_{k}arrow c_{k}\mathrm{v}c_{k}’$, respectively. Then by applying$(\veearrow)$

to them we can get$Z_{k}arrow C_{k}\vee C_{k}’$,;$\frac{\frac{z_{k\{A/A}\mathrm{v}B\}arrow C_{k}}{z_{k\{A/B\}^{arrow c_{k^{}}C_{k}}}AZ_{k\{A\vee}\prime}(arrow\vee 1)\frac{z_{k\{B/A\vee}B\}arrow c’k}{\prime k^{\vee C_{k}}Z_{k\{B/AB\}k}\mathrm{v}arrow c\mathrm{v}C_{k}^{1}}}{B/A\mathrm{v}B\}^{arrow C}\prime}(\veearrow)(arrow\vee 2)$

So by la) and$1\mathrm{b}$), $Z_{k}arrow C_{k}C_{k}’$ and$Z_{i}arrow c_{:}$

A

C.’. are provable when$i\neq k$.

, $n-1$ times,, whe.re. $E_{k}=C_{k}$ and $E_{i}=C_{i}$ A
we can get
when $i\neq k$ . Also,, by applying ( –weakening), ( –exchange) and,from, where $E_{k}’=C_{k}’$ and$n-1$ times, we can get
when$i\neq k$ . Note again that when $i\neq k,$$=W_{i}=Z..$ Then by applyingto, whereand $\Gamma(B)\{E_{i}/W:’\}:arrow D$ we can get. So by ) and ), we can get. and . $=E_{i}’=E_{i}=C_{i}$ A when.
the proof of $\Gamma(AB)_{\{E_{:}’’/Z\}}i:arrow D$ as follows;
Next, from$\Gamma(A)_{\{}c.\cdot/U:\}:arrow D$, by applying ( $E$ –weakening) and$(\wedgearrow)$$C_{i}’$$\Gamma(A)_{\{:}E/\sigma:\}.\cdotarrow D$$E$$\Gamma(B)_{\{}C’.\cdot/W_{i}\}:arrow D$$E$$(\wedgearrow)$.

$E_{i}’=C_{i}\wedge C^{i}.\cdot$$\Gamma(B)_{\{E}’.\cdot/W:\}_{i}arrow D$$U$$(\veearrow)$$\Gamma(A)_{\{/\cdot\}:}E:U.arrow D$$E_{k}’’$$=C_{k}\vee C_{k}’$$\Gamma(AB)_{\{\dot{.}/}E’’z_{*}.\}:arrow D$$E_{*}’’$$C_{i}’$$i,$$\neq k$$2\mathrm{a}$$2\mathrm{b}$.
Lastly, by ) and ) we can easily show thata) for $h=1,$, $k-1,$ $k+1,$, $V(C_{h},\wedge C_{h}’)\subset V(Z_{h})\cap[V(\Gamma(AB)_{\{-/z\}:}i)\cup V(D)]$ ,b) $V(C_{k}$. $\vee C_{k}’.)\subset V(Z_{k})\cap[V(\Gamma(A\vee B)_{\{-/\cdot\}:}Z.)\cup D]$ .
$3\mathrm{b}$$3\mathrm{a}$$\ldots$Thus$C_{h}\wedge C_{h}’$$\ldots$

for $h=1,$$\ldots,$$n,$$k-1,$ $k+1,$$\ldots,$$n$, and $C_{k}C_{k}’$. become the interpolants.

The proof of Theorem 1 forgoes similarly to the above proof of Theorem
1 for. In fact as we define intensional structures by multisets, we can omit
some subcases in the proof.
$L_{\mathrm{o}}L_{\mathrm{D}\mathrm{B}\mathrm{C}\mathrm{K}}$$L_{\mathrm{o}}L_{\mathrm{D}\mathrm{B}\mathrm{c}}\mathrm{c}$Corollary 2 The interpolation theorem holds fororif the formula $A\supset B$ is provable (in$L_{\mathrm{D}\mathrm{B}\mathrm{C}}\mathrm{c}$that both$A\supset C$

and$C\supset B$

are provable and. More precisely,and), then there is a formula such.

$L_{\mathrm{D}\mathrm{B}\mathrm{C}\mathrm{C}}$$L_{\mathrm{D}\mathrm{B}\mathrm{C}\mathrm{K}}$$L_{\mathrm{D}\mathrm{B}\mathrm{C}\mathrm{K}}$$\mathfrak{s}\nearrow(c)\subset[V(A)\cap V(B)]$

$C$
,

185
As an important application of Theorem 1, we can get the following theorem,
which says tluat tlle Maksimova’s principle of variable separation holds forand. The detail ofthe proof will be announced in [8]. In fact, our interpolation
theorem in a stronger form is necessary for proving this.
$L_{\mathrm{o}}L_{\mathrm{D}\mathrm{B}\mathrm{c}}\mathrm{c}$$L_{\mathrm{o}}L_{\mathrm{D}\mathrm{B}}\mathrm{C}\kappa$

Theorem 3 Suppose thathave no propositional variables incommon. Then the following holds forand.
1) if the sequentA
is provable, then eitheroris$A_{1}\supset A_{2}$and$B_{1}\supset B_{2}$$L_{\mathrm{o}}L_{\mathrm{D}\mathrm{B}\mathrm{c}}\mathrm{c}$$L_{\mathrm{o}}L_{\mathrm{D}\mathrm{B}\mathrm{C}\mathrm{K}}$$B_{1}arrow A_{2}B_{\mathit{2}}$$A_{1}$$A_{1}arrow A_{\mathit{2}}$$B_{1}arrow B_{\mathit{2}}$provable,2) if the sequent$A_{1}$

A $B_{1}arrow A_{2}$ is provable, then either $A_{1}arrow A_{2}$ or $B_{1}arrow is$ provable,

3) if the sequent $A_{1}arrow A_{2}B_{2}$ is provable, then either$A_{1}arrow A_{\mathit{2}}orarrow B_{2}$is provable.

References[1] Bayu Surarso, Interpolation theorem for some $dist\gamma ibutive$ substructural logics, tobe submitted.
[2] R.T. Brady, Gentzenizations of relevant logics without distnibution II, The Journalof Symbolic Logic 61 (1996), pp. 379-401.
[3] J.M. Dunn, Consecution formulation of positive R with $co$ -tenability and t, in

Entailment: The Logic of Relevance and Necessity Vol. 1, edited by A.R. Anderson
and N.D. Belnap, Princeton University Press, 1975, pp. 381-391.
[4] J.M. Dunn, Relevance logic and entailments, in Handbook of Philosophical Logic
vol. III, edited by D. Gabbay and F. Guenthner, Reidel Publishing Company,
1986, pp.117-224.
[5] S. Giambrone, $TW_{+}$ and $RW_{+}$ are decidable, Journal of Philosophical Logic 14(1985), pp. 235-254.

[6] S. Maehara, Craig no interpolation theorem, Suugaku 12, (1960/61), pp. 235-237.
(in Japanese.)[7] M.A. McRobbie, Interpolation tfieorems for some first-order distribution-free relevant logics (Abstract), Journal of Symbolic Logic (1983), pp. 522-523.
[8] H. Naruse, Bayu Surarso and H. Ono, A syntactic approach to Maksimova’s principle of variable separation for some substructural logics, to be submitted.

186[9] H. Ono, Structural rules and a logical hierarchy, in Mathematical Logic, edited byp.p. Petkov, Plenum Press, 1990, pp. 95-104.

[10] H. Ono, Semantics for substructural logics, in Substructural Logics, edited by K.
Do\v{s}en and P. Schroeder-Heister, Oxford Univ. Press, 1993, pp. 259-291.
, Logics without the contraction rule, Journal of Symbolic[11] H. Ono and Y.
Logic 50 (1985), pp. 169-201.
$\mathrm{I}<_{\mathrm{o}\mathrm{m}}\mathrm{o}\mathrm{r}\mathrm{i}$[12] J. Slaney, Solution to a problem of Ono and Komori, Journal of Philosophical
Logic 18 (1989), pp. 103-111.
[13] A. Urquhart, Failure of interpolation in relevant logics, Journal of Philosophical
Logic 22 (1993), pp. 449-479.