# Tensor term logic for categorial grammars: simple unification of commutative
and noncommutative structure

Sergey Slavnov
<EMAIL_ADDRESS>
###### Abstract

A prototypical example of categorial grammars are those based on Lambek
calculus, i.e. noncommutative intuitionistic linear logic. However, it has
been noted that purely noncommutative operations are often not sufficient for
modeling even very simple natural language phenomena. Therefore a number of
alternative formalisms are considered in the literature: those using purely
“commutative” linear logic as well as combining (to some level) commutative
and non-commutative operations. The logic of tensor terms that we propose is a
variant of such a combination. This logical calculus was designed specially
for defining categorial grammars. It contains Lambek calculus and
multiplicative linear logic as conservative fragments, yet the syntax is very
simple, not departing much from that of multiplicative linear logic. The
system is cut-free and decidable, it has both intuitionistic and classical
versions, besides it is equipped with a simple intuitive semantics, which is
sound and complete.

##  1 Introduction

###  1.1 Lambek calculus and its variations

A prototypical example of categorial grammars are those based on Lambek
calculus (LC) [6], [7], i.e. noncommutative intuitionistic linear logic.
However, it has been noted that purely noncommutative operations are often not
sufficient for modeling even very simple natural language phenomena (such as,
for example, medial extraction).

An alternative, or rather, complementary approach is to use ordinary,
“commutative” multiplicative linear logic (MLL or MILL for the intuitionistic
version). The best known example of a “commutative” formalism are abstract
categorial grammars (ACG) [2] (see also [14], [8]). But on the other hand,
there are some linguistic situations (such as non-constituent coordination)
where, on the contrary, the noncommutative structure of LC is wanted and such
systems as ACG behave very poorly, see [10] for a discussion.

For those reasons, it might be interesting to have formalisms that combine (to
some level) commutative and noncommutative structures. One of the options
considered in the literature is to allow connectives of LC and MLL coexist.
Among examples of this sort one could mention non-commutative logic [1],
partially commutative logic [3], as well as more recent hybrid type logical
categorial grammars (HTLCG) [5]. However, the price for this coexistence of
two sorts of connectives is the rather complicated syntax and sequent calculus
structure in these systems. A somewhat different approach is taken in
displacement calculus (DC) [13], which is the logic of ordered string tuples
(in the same sense as LC is the logic of strings), however it suffers from the
similar drawback. In the case of DC even a sequent calculus in the usual sense
is absent, and for a cut-free formulation one has to use specific, extremely
complicated structure of hyper-sequents.

###  1.2 First order linear logic and categorial grammars

A remarkable observation [12] is that first order (commutative) multiplicative
linear logic (MLL1 or MILL1 for the intuitionistic version) can be used as a
kind of grammatical formalism. In particular, both LC and ACG, as well as
HTLCG, can be encoded as conservative fragments of MILL1 [9], [11], [10]. (A
similar encoding for DC is also available, but in this case the embedding is
not conservative, see [11].) This suggests another approach to combining
commutative and noncommutative structure, which avoids syntactic
complications, staying in the limits of familiar commutative linear logic and
usual sequent calculus.

The encodings are based on interpreting first order variables as denoting
string positions. Noncommutative constructions, such as string concatenation,
are represented by means of quantifiers binding variables. Typically, an LC
formula $F$ has the MILL1 translation $||F||^{x,y}$ parameterized by the free
variables $x,y$ defined by induction as

$\begin{array}[]{rl}||p||^{x,y}=p(x,y),&|||A\bullet B||^{x,y}=\exists
t(||A||^{x,t}\otimes||B||^{t,y}),\\\ ||A\backslash B||^{x,y}=\forall
t(||A||^{t,x}\multimap||B||^{t,y}),&||B/A||^{x,y}=\forall
t(||A||^{x,t}\multimap||B||^{y,t}),\end{array}$ (1)

where $p$ is a literal.

However, one might argue that the full system of MILL1 is quite redundant for
the above linguistic interpretations. Actually, only a tiny fragment of the
system is used in these constructions, and the “linguistic” meaning of general
MILL1 formulas and sequents seems, at least, obscure. Moreover, the fragment
of interest is not closed either under subformulas or proof-search. Typically,
when deriving in MILL1 the translation of an LC sequent, in general, we have
to use at intermediate steps sequents that have no clear linguistic meaning,
if any.

In [17] (elaborating on [15], [16]) we proposed to isolate the relevant
fragment of MILL1, calling it the linguistic fragment, and then gave an
alternative formulation for the latter. In a greater detail, we proposed so
called extended tensor type calculus (ETTC), which is a certain calculus of
typed terms, called tensor terms, and is equipped with an intrinsic deductive
system and a transparent linguistic interpretation. Then we established strict
equivalence of the proposed calculus and the linguistic fragment.

In the current work, which can be seen as an upgrade of the above, we propose
the logic of tensor terms. Tensor term logic (TTL), is very similar to the
previously defined ETTC, but has much simpler syntax and sequent calculus, not
too different from ordinary propositional MLL. Besides, TTL is equipped with a
sound and complete semantics, similar to phase semantics of linear logic.

(On the other hand, the direct translation to the linguistic fragment of MILL1
in the case of TTL is lost. Connections of TTL to first order linear logic
remain to be understood; we make several side remarks on this subject
throughout the text.)

###  1.3 Tensor term logic

Tensor terms [16], [17] are, basically, tuples of words (written
multiplicatively, as formal products) with labeled endpoints. We write words
in square brackets and represent the endpoints as lower and upper indices,
lower indices standing for right endpoints and upper indices for left ones.
Thus, tensor terms can have the form

$[\mbox{a}]_{i}^{j},\quad[\mbox{a}]_{i}^{j}\cdot[\mbox{b}]_{k}^{l}\cdot[\mbox{c}]_{r}^{s},\quad[\epsilon]_{i}^{j}$

(where $\epsilon$ stands for the empty word) and so on.

An index in a term can be repeated at most twice, once as an upper, and once
as a lower one. A repeated index is called bound; it means that the
corresponding words are concatenated along matching endpoints. For example, we
have the term equality

$[\mbox{a}]_{j}^{i}\cdot[\mbox{b}]_{l}^{k}\cdot[\mbox{c}]_{k}^{j}=[\mbox{acb}]_{l}^{i}$

(the product is commutative). Naturally, indices that are not bound are called
free.

In the logic of tensor terms (TTL), formulas or types denote sets of terms,
and sequents denote relations between those (just as in LC formulas denote
sets of strings and sequents denote relations between strings). The syntax of
TTL is just that of MLL with the addition that formulas are decorated with
indices and the sequent calculus is supplemented with a couple of rules for
index manipulation. Typically, an atomic TTL formula $p^{i_{1}\ldots
i_{m}}_{j_{1}\ldots j_{n}}$ denotes a set of tensor terms all whose elements
have as their set of upper, respectively lower free indices the collection
$i_{1},\ldots,i_{m}$, respectively ${j_{1},\ldots,j_{n}}$ . Tensor product of
types corresponds to product of terms (just as product in LC corresponds to
concatenation of strings), and implication is the adjoint operation.

TTL formulas can also have bound indices; these may occur in compound
formulas. For example, the formula $a^{i}_{j}\otimes b^{j}_{k}$ denotes the
product of term sets corresponding to $a^{i}_{j}$ and $b^{j}_{k}$. The latter
sets have elements of the form $[u]^{i}_{j}$ and $[v]^{j}_{k}$ respectively;
these are just strings with marked endpoints. Since the endpoints match, the
product becomes concatenation, and the denotation of $a^{i}_{j}\otimes
b^{j}_{k}$ consists of elements of the form $[uv]^{i}_{k}$, with only two free
indices. We say that the index $j$ in $a^{i}_{j}\otimes b^{j}_{k}$ is bound.

The above sketchy analysis suggests how to encode LC to TTL. In fact, the
encoding is almost the same as the translation to MILL1 in (1), with the only
difference that we do not need cumbersome quantifiers. The translation of an
LC formula $F$ is parameterized by two free indices according to the rules

$\begin{array}[]{rl}||p||^{i}_{j}=p^{i}_{j},&|||A\bullet
B||^{i}_{j}=||A||^{i}_{k}\otimes||B||^{k}_{j},\\\ ||A\backslash
B||^{i}_{j}=||A||^{k}_{i}\multimap||B||^{k}_{j},&||B/A||^{i}_{j}=||A||^{j}_{k}\multimap||B||^{i}_{k}).\end{array}$

On the other hand, when the indices in subformulas are disjoint, we obtain
discontinuous operations typical for “commutative” grammars such as ACG.
Tensor corresponds to “disjoint union” and implication produces a “hole”in a
string. In this way we get both “commutative” and “noncommutative” operations
available, without departing much from the simple syntax of propositional MLL.
Cut elimination, decidability and a simple, intuitive semantics are also at
hand.

##  2 Tensor terms

######  Definition 2.1.

Given an alphabet $T$ of terminal symbols and an infinite set $\mathit{Ind}$
of indices, we consider the free commutative monoid (written multiplicatively
with the unit denoted as 1) of tensor pseudo-terms (over $T$ and
$\mathit{Ind}$) generated by the sets

$\\{[w]_{i}^{j}|~{}i,j\in\mathit{Ind},w\in T^{*}\\}\mbox{ and }\\{[w]|~{}w\in
T^{*}\\}.$ (2)

A pseudo-term $t$ is well-formed if any index in $t$ has at most one lower and
one upper occurrence. The set of tensor terms (over $T$ and $\mathit{Ind}$) is
the set of well-formed pseudo-terms quotiented by the congruence generated by
the relations

$\begin{array}[]{c}[u]_{j}^{i}\cdot[v]_{k}^{j}\equiv[uv]_{k}^{i},\quad[w]^{i}_{i}\equiv[w],\\\
{[}a_{1}\ldots a_{n}]\equiv[a_{n}a_{1}\ldots a_{n-1}]\mbox{ for
}a_{1},\ldots,a_{n}\in T.\end{array}$ (3)

Generating set (2) elements of the form $[w]_{i}^{j}$ are elementary regular
tensor terms and those of the form $[w]$ are elementary singular tensor terms.

An index occurring in a well-formed pseudo-term $t$ is free in $t$ if it
occurs in $t$ exactly once. An index occurring in $t$ twice (once as an upper
one and once as a lower one) is bound in $t$. Sets of free indices are
invariant under congruence (3), so that free indices of a tensor term are
well-defined as well.

######  Definition 2.2.

For a tensor term or a well-formed tensor pseudo-term $t$ we denote the set of
its free upper, respectively lower indices as $FI^{\bullet}(t)$, respectively
$FI_{\bullet}(t)$. We call the pair $FI(t)=(FI^{\bullet}(t),FI_{\bullet}(t))$
the boundary of $t$.

The meaning of relations (3) is as follows. Terms stand for string tuples,
indices denote string endpoints. Repeated, i.e. bound, indices correspond to
matching endpoints and strings are glued along them. The unit $1$ corresponds
to the empty tuple. As for singular terms, such as $[w]^{i}_{i}$, they
correspond to cyclic words (this explains the last relation in (3)). These
arise when strings are glued cyclically. Singular terms are pathological, but
we need them for consistency of definitions.

One can take a more geometric view and represent elementary regular terms as
directed string-labeled edges with indices denoting vertices and elementary
singular terms as closed loops labeled with cyclic words. Edges are glued
along matching vertices. General terms become graphs constructed from
elementary ones by taking disjoint unions and gluing edges along matching
vertices. The title “boundary” is inspired precisely by such a view.

######  Definition 2.3.

For a well-formed pseudo-term $t$ with $i\in FI^{\bullet}(t)$ and $j$ not
occurring in $t$, the reparameterization $t^{[\nicefrac{{j}}{{i}}]}$ of $t$ is
the pseudo-term obtained from $t$ by replacing the index $i$ with $j$.
Similarly, for $t$ with $i\in FI_{\bullet}(t)$ and $j$ not occurring in $t$,
the reparameterization $t_{[\nicefrac{{j}}{{i}}]}$ is $t$ where $i$ is
replaced with $j$. The same convention applies when $t$ is a tensor term.

It is easy to see that reparameterization takes well-formed pseudo-terms to
well-formed pseudo-terms and preserves congruence classes, hence it is indeed
well-defined for terms as well.

We have the following zoology of tensor terms.

######  Definition 2.4.

A tensor term $t$ is regular if it can be written as
$t=[w_{1}]^{i_{1}}_{j_{1}}\cdots[w_{n}]^{i_{n}}_{j_{n}}$, where the indices
$i_{1},j_{1},\ldots,i_{n},j_{n}$ are pairwise distinct. The term $t$ is
singular if it has the form $[u_{1}]\cdots[u_{k}]t^{\prime}$, where $k>0$ and
$t^{\prime}$ is regular.

The term $t$ is lexical if it has the form
$t=[u_{1}]\cdots[u_{k}]\cdots[w_{1}]^{i_{1}}_{j_{1}}\cdots[w_{n}]^{i_{n}}_{j_{n}}$,
where the indices $i_{1},j_{1},\ldots,i_{n},j_{n}$ are pairwise distinct and
all words $u_{1},\ldots,u_{k},w_{1},\ldots,w_{n}$ are nonempty.

The elementary term $[\epsilon]^{j}_{i}$ where $i\not=j$ and $\epsilon$
denotes the empty word, is called Kronecker delta and is denoted as
$\delta^{j}_{i}$.

######  Proposition 2.5.

If $t$ is a term with $i\in FI^{\bullet}(t)$, $j\in FI_{\bullet}(t)$ and
$i^{\prime},j^{\prime}$ are fresh then $\delta_{i}^{i^{\prime}}\cdot
t=t^{[\nicefrac{{i^{\prime}}}{{i}}]}$ and $\delta_{j^{\prime}}^{j}\cdot
t=t_{[\nicefrac{{j^{\prime}}}{{j}}]}$. $\Box$

######  Remark 2.6.

In extended tensor type calculus (ETTC) of [17] we had the additional term
congruence

$[\epsilon]\equiv 1.$ (4)

This was needed for the main result of that paper, namely, for conservative
translation of ETTC to first order linear logic MLL1. In the current work we
drop this congruence, because it leads to unnecessary complications.

It should be emphasized that multiplication of terms is only partially
defined: the product $ts$ exists as a well-defined term only if
$FI^{\bullet}(t)\cap FI^{\bullet}(s)=FI_{\bullet}(t)\cap
FI_{\bullet}(s)=\emptyset$. It is associative in the following sense: if both
$(ts)k$ and $t(sk)$ are well-defined then they are equal. However, it may be
the case that one side is undefined, while the other one is a well-defined
term.

We will assume the following convention.

######  Definition 2.7.

The expression $t_{(1)}\ldots t_{(n)}$ denotes the iterated product of terms
satisfying the condition $FI^{\bullet}(t_{(i)})\cap
FI^{\bullet}(t_{(j)})=FI_{\bullet}(t_{(i)})\cap
FI_{\bullet}(t_{(j)})=\emptyset$ for all $i\not=j$.

(In the definition above we put sequence numbers in brackets in order to avoid
confusion with indices.)

In the sequel, when writing products of terms we will implicitly assume that
the operations are well-defined and, in the case of iterated products, the
convention from the above definition applies. This makes expressions with
iterated products unambiguous.

##  3 Intuitionistic tensor term logic

###  3.1 Intuitionistic tensor types

######  Definition 3.1.

Given a set $\mathit{Lit}$ of literals, where every element $p\in\mathit{Lit}$
is assigned a valency $v(p)\in\mathbb{N}^{2}$ and an infinite set
$\mathit{Ind}$ of indices, the set $\widetilde{\mathit{Fm}}$ of intuitionistic
tensor pseudoformulas over the alphabet $\mathit{Lit}$ is built according to
the grammar in Figure LABEL:ITTP_lang, where $\mathit{Prop}$ is the set of
propositional symbols. The set $\widetilde{\mathit{At}}$ is the set of atomic
pseudoformulas.

The connectives $\otimes$ and $\multimap$ are called, respectively, tensor
(also times) and linear implication. The propositional constant ${\bf 1}$ is
called one (also the unit).

######  Definition 3.2.

For every pseudoformula $A$ (over the given alphabet $\mathit{Lit}$) the set
of index occurrences in $A$ is partitioned into the pair
$(I^{\bullet}(A),I_{\bullet}(A))$ of sets, the set of upper and lower polarity
indices respectively. The partition is defined by induction on $A$ in Figure
LABEL:ITTP_polarities.

An atomic pseudoformula $p^{i_{1}\ldots i_{m}}_{j_{1}\ldots j_{n}}$ is well-
formed if all indices $i_{1},\ldots,i_{m}$, $j_{1},\ldots,j_{m}$ are pairwise
distinct. A general intuitionistic pseudoformula $A$ is well-formed if it is
built of well-formed atomic ones and any index has at most one upper and one
lower polarity occurrence in $A$. A well-formed intuitionistic tensor
pseudoformula $F$ is an intuitionistic tensor formula or an intuitionistic
tensor type (over $\mathit{Lit}$). A well-formed atomic intuitionistic tensor
pseudoformula is an atomic intuitionistic tensor formula. The set of atomic
formulas is denoted as $At$. The set of intuitionistic tensor formulas over
the given $\mathit{Lit}$ is the intuitionistic tensor language generated by
$\mathit{Lit}$ or, simply the intuitionistic tensor language over
$\mathit{Lit}$.

We emphasize that there is a certain notational inconsistency in our language.
The polarity of an index occurrence does not necessarily coincide with its
actual graphical location in the formula. Typically, upper indices written in
the antecedent of an implication will have lower polarity and so on. Such an
inconsistency does not arise when tensor formulas are written in the format of
classical, rather than intuitionistic, linear logic.

######  Definition 3.3.

An index in a tensor formula is free if it occurs exactly once, otherwise it
is bound. The set of free upper, respectively lower indices of a tensor
formula $A$ is denoted as $FI^{\bullet}(A)$, respectively $FI_{\bullet}(A)$.
The pair $FI(A)=(FI^{\bullet}(A),FI_{\bullet}(A))$ is the boundary  of $A$.
Tensor formulas $F,G$ are $\alpha$-equivalent ($F\equiv_{\alpha}G$) if they
can be obtained from each other by successively renaming bound indices.

$\begin{array}[]{c}\mathit{Prop}=\mathit{Lit}\cup\\{{\bf 1}\\},\quad v({\bf
1})=(1,1),\\\\[2.84544pt] \widetilde{\mathit{At}}=\\{p_{j_{1}\ldots
j_{n}}^{i_{1}\ldots i_{m}}|~{}p\in\mathit{Prop},i_{1}\ldots i_{m},j_{1}\ldots
j_{n}\subset\mathit{Ind},v(p)=(m,n)\\},\\\\[2.84544pt]
\widetilde{\mathit{Fm}}::=\widetilde{\mathit{At}}|(\widetilde{\mathit{Fm}}\otimes\widetilde{\mathit{Fm}})|(\widetilde{\mathit{Fm}}\multimap\widetilde{\mathit{Fm}}).\end{array}$

(a)

$\begin{array}[]{rl}I^{\bullet}({p^{i_{1},\ldots,i_{n}}_{j_{1},\ldots,j_{m}}})=\\{i_{1},\ldots,i_{n}\\},&I_{\bullet}({p^{i_{1},\ldots,i_{n}}_{j_{1},\ldots,j_{m}}})=\\{j_{1},\ldots,j_{m}\\}\mbox{
for }p\in\mathit{Prop},\\\ I^{\bullet}(A\otimes B)=I^{\bullet}(A)\cup
I^{\bullet}(B),&I_{\bullet}(A\otimes B)=I_{\bullet}(A)\cup I_{\bullet}(B),\\\
I^{\bullet}(A\multimap B)=I^{\bullet}(B)\cup
I_{\bullet}(A),&I_{\bullet}(A\multimap B)=I_{\bullet}(B)\cup
I^{\bullet}(A).\end{array}$

(b)

Figure 1: ITTL language

The notation $A^{[\nicefrac{{i}}{{j}}]}$ stands for $A$ with $i$ substituted
instead of a free upper occurrence of $j$ (if there is any), where it is
implicitly assumed that the result of the substitution is a well-formed tensor
formula and the index $i$ does not become bound after substitution, i.e. if
$j\in FI^{\bullet}(A)$ then $i$ does not occur in $A$. Similarly,
$A_{[\nicefrac{{i}}{{j}}]}$ stands for $A$ with $i$ substituted instead of a
free lower occurrence of $j$, with the implicit assumption that if $j\in
FI_{\bullet}(A)$ then $i$ does not occur in $A$. When two formulas differ by
such a substitution of free indices we say that they are reparameterizations
of each other. Two formulas that can be obtained from each other by a chain of
reparameterizations and $\alpha$-equivalences are said to have the same type
symbol. The valency of a type symbol $a$ is the pair
$(\\#FI^{\bullet}(A),\\#FI_{\bullet}(A))$, where $A$ is any formula with
symbol $a$. A type symbol is balanced if its valency is of the form $(n,n)$.
An intuitionistic tensor language is balanced if all its literals are
balanced.

The intended semantics is that tensor types are sets of tensor terms. In a
greater detail, each type $A$ should be assigned a set $||A||$ of terms with
boundary $FI(A)$, and this assignment should be consistent with
reparameterization: for $i\in FI^{\bullet}(A)$ we have $t\in||A||$ iff
$t^{[\nicefrac{{i}}{{j}}]}\in||A^{[\nicefrac{{i}}{{j}}]}||$, similarly with
lower indices.

A “naive” semantics of connectives is as follows. The tensor product $A\otimes
B$ stands for the set $\\{ts|~{}t\in||A||,s\in||B||\\}$, and for the
implicational type $A\multimap B$ we have $t\in||A\multimap B||$ iff for all
$s\in||A||$ it holds that $ts\in||B||$. As for the unit we may put $||{\bf
1}^{i}_{j}||=\\{\delta^{i}_{j}\\}$. Note that consistency with
reparameterization implies that if $j\in FI^{\bullet}(A)$ and $i$ does not
occur in $A$ then

$||A^{[\nicefrac{{i}}{{j}}]}||=||A\otimes{\bf 1}^{i}_{j}||=||{\bf
1}^{j}_{i}\multimap A||,$ (5)

similarly for lower indices. Such an interpretation is sound for the system of
intuitionistic tensor type logic (ITTL) that we are about to introduce,
although its completeness is under question. In any case, it does not make
much sense when the language is not balanced, because for a “non-balanced”
formula $A=a^{i_{1}\ldots i_{m}}_{j_{1}\ldots j_{n}}$, where $m\not=n$ we
cannot have any terms with boundary $FI(A)$. A complete semantics for ITTL in
a balanced language, which is only a slight refinement of the above, will be
discussed later.

###  3.2 Sequent calculus

$\begin{array}[]{c}\begin{array}[]{rl}\quad\cfrac{A\in At}{A\vdash
A}{\rm{(Id)}}&\cfrac{\Gamma\vdash A\quad A,\Delta\vdash B}{\Gamma,\Delta\vdash
B}({\rm{Cut}})\\\ \cfrac{\Gamma\vdash A\quad B,\Delta\vdash
C}{\Gamma,A\multimap B,\Delta\vdash
C}({\rm{L}}\multimap)&\cfrac{\Gamma,A\vdash B}{\Gamma\vdash A\multimap
B}({\rm{R}}\multimap)\\\ \cfrac{\Gamma,A,B\vdash C}{\Gamma,A\otimes B\vdash
C}({\rm{L}}\otimes)&\cfrac{\Gamma\vdash A\quad\Delta\vdash
B}{\Gamma,\Delta\vdash A\otimes B}({\rm{R}}\otimes)\\\ \cfrac{\Gamma,A\vdash
B~{}j\in FI_{\bullet}(A)}{\Gamma,A_{[\nicefrac{{i}}{{j}}]},{\bf
1}_{j}^{i}\vdash B}({\rm{L}}{\bf 1}_{\to})&\cfrac{\Gamma\vdash A~{}j\in
FI^{\bullet}(A)}{\Gamma,{\bf 1}^{i}_{j}\vdash
A^{[\nicefrac{{i}}{{j}}]}}({\rm{R}}{\bf 1}^{\to})\\\ \cfrac{\Gamma,A,{\bf
1}^{i}_{j}\vdash B~{}j\in
FI^{\bullet}(A)}{\Gamma,A^{[\nicefrac{{i}}{{j}}]}\vdash B}({\rm{L}}{\bf
1}^{\leftarrow})&\cfrac{\Gamma,{\bf 1}^{i}_{j}\vdash A~{}j\in
FI_{\bullet}(A)}{\Gamma\vdash A_{[\nicefrac{{i}}{{j}}]}}({\rm{R}}{\bf
1}_{\leftarrow})\end{array}\\\\[17.07182pt] \mbox{In }({\rm{L}}{\bf
1}_{\to}),({\rm{R}}{\bf 1}^{\to}),({\rm{L}}{\bf 1}^{\leftarrow}),({\rm{R}}{\bf
1}_{\leftarrow})~{}i\not\in FI^{\bullet}(A)\cup FI_{\bullet}(A)\end{array}$

(a)

$\begin{array}[]{c}\begin{array}[]{rl}\cfrac{\Gamma,A\vdash B~{}j\in
FI^{\bullet}(A)}{\Gamma,A^{[\nicefrac{{i}}{{j}}]},{\bf 1}^{j}_{i}\vdash
B}({\rm{L}}{\bf 1}^{\to})&\cfrac{\Gamma\vdash A~{}j\in
FI_{\bullet}(A)}{\Gamma,{\bf 1}_{i}^{j}\vdash
A_{[\nicefrac{{i}}{{j}}]}}({\rm{R}}{\bf 1}_{\to})\\\ \cfrac{\Gamma,A,{\bf
1}_{i}^{j}\vdash B~{}j\in
FI_{\bullet}(A)}{\Gamma,A_{[\nicefrac{{i}}{{j}}]}\vdash B}({\rm{L}}{\bf
1}_{\leftarrow})&\cfrac{\Gamma,{\bf 1}_{i}^{j}\vdash A~{}j\in
FI^{\bullet}(A)}{\Gamma\vdash A^{[\nicefrac{{i}}{{j}}]}}({\rm{R}}{\bf
1}^{\leftarrow})\end{array}\\\\[17.07182pt] \mbox{In all rules above }i\not\in
FI^{\bullet}(A)\cup FI_{\bullet}(A)\end{array}$

(b)

Figure 2: ITTL sequent rules

######  Definition 3.4.

An intuitionistic tensor context is a finite set $\Gamma$ of intuitionistic
tensor formulas such that for any $A,B\in\Gamma$ it holds that

$FI_{\bullet}(A)\cap FI_{\bullet}(B)=FI^{\bullet}(A)\cap
FI^{\bullet}(B)=\emptyset.$ (6)

We denote $FI^{\bullet}(\Gamma)=\bigcup\limits_{A\in\Gamma}FI^{\bullet}(A)$,
$FI_{\bullet}(\Gamma)=\bigcup\limits_{A\in\Gamma}FI_{\bullet}(A)$.

An intuitionistic tensor sequent is an expression of the form $\Gamma\vdash
A$, where $\Gamma$ is an intuitionistic tensor context, $A$ an intuitionistic
tensor formula and it holds that

$FI^{\bullet}(\Gamma)\cap FI_{\bullet}(A)=FI_{\bullet}(\Gamma)\cap
FI^{\bullet}(A)=\emptyset,\quad FI^{\bullet}(\Gamma)\cup
FI_{\bullet}(A)=FI_{\bullet}(\Gamma)\cup FI^{\bullet}(A).$

The polarity of a free index occurrence $i$ in the sequent $\Gamma\vdash A$ is
the same as the polarity of $i$ in $A$ if $i$ is located in $A$ and is the
opposite of its polarity in $\Gamma$ if it is located in $\Gamma$.

The definition says that every index occurring in a sequent has exactly one
upper and one lower polarity free occurrence (keeping in mind that polarities
to the left of the turnstile are read upside down.)

The intended semantics of the sequent $A_{(1)},\ldots,A_{(n)}\vdash B$
(sequence numbers in brackets in order to avoid confusion with indices) is the
following: if we have terms $t_{(1)},\ldots,t_{(n)}$ of types
$A_{(1)},\ldots,A_{(n)}$ respectively, then the product $t_{(1)}\cdots
t_{(n)}$ is of type $B$. (When $n=0$, i.e. the sequent has the form $\vdash
B$, this should be understood that the term $1$ is of type $B$.)

######  Definition 3.5.

The system of intuitionistic tensor term logic (ITTL) is given by the rules in
Figure LABEL:ITTL_rules, where it is assumed that all expressions are well-
formed sequents, i.e. each free index has exactly one upper and one lower
polarity occurrence .

We encourage the reader to check that the “naive” semantics of types discussed
in the preceding subsection is sound for the above system. The last four rules
(i.e. the part that is not the usual intuitionistic linear logic) express the
requirement that the interpretation of types should be consistent with
reparameterization as in (5). In this group, the rules marked with the arrow
directed from the unit are expansion rules, and those with the arrow directed
towards the unit are reduction rules. There are other, admissible, expansion
and reduction rules of a similar form and with the same meaning shown in
Figure LABEL:ITTL_admissible_rules. Their admissibility will be proven in the
next subsection. Finally, note also that there is another rule introducing the
unit, namely the special instance ${\bf 1}^{i}_{j}\vdash{\bf 1}^{i}_{j}$ of
the $({\rm{Id}})$ axiom.

######  Remark 3.6.

It might be interesting to study what will be the logic of tensor terms when
we add to the definition of terms the additional congruence from (4) (see
Remark 2.6). For example the “naive” semantics will validate the principle
$\vdash(A^{i}_{j}\multimap A^{i}_{k})\otimes(A^{l}_{k}\multimap A^{l}_{j})$.
(Indeed, we have $\delta^{j}_{k}\in||A^{i}_{j}\multimap A^{i}_{k}||$,
$\delta_{j}^{k}\in||A^{l}_{k}\multimap A^{l}_{j}||$, and
$\delta^{j}_{k}\delta^{k}_{j}$ becomes $1$ under (4).) But the latter sequent
is easily seen to be underivable in the given formulation of ITTL without the
Cut rule. (The sequent has no free indices, therefore the last rule in its
derivation cannot be $({\rm{R}}{\bf 1}_{\leftarrow})$. So it could only be the
$(\otimes)$ rule, and this does not work.) That the proposed formulation of
ITTL is cut-free will be shown shortly.

###  3.3 Simplest properties

######  Definition 3.7.

Let $\Gamma\vdash A$ be a sequent with a free index $i$. A similarity
transformation of $\Gamma\vdash A$ consists in replacing both free occurrences
of $i$ with a fresh index. Two sequents are similar (notation $\sim$) if they
can be obtained from each other by a chain of similarity transformations.
$\alpha$-Equivalence of tensor sequents (notation $\equiv_{\alpha}$) is the
smallest equivalence relation such that similar sequents and sequents
differing by renaming bound indices in formulas are $\alpha$-equivalent.

######  Proposition 3.8.

In ITTL

  1. (i)

Similar sequents are cut-free derivable from each other;

  2. (ii)

rules in Figure LABEL:ITTL_admissible_rules are admissible and can be emulated
without use of the Cut rule;

  3. (iii)

$\alpha$-equivalent formulas are provably equivalent, i.e. if
$F\equiv_{\alpha}F^{\prime}$ then the sequents $F\vdash F^{\prime}$,
$F^{\prime}\vdash F$ are derivable;

  4. (iv)

$\alpha$-equivalent sequents are derivable from each other;

  5. (v)

if $j\in FI^{\bullet}(A)$, and $i$ is an index not occurring in $A$ then there
are provable equivalences $A\otimes{\bf 1}^{i}_{j}\cong{\bf
1}_{i}^{j}\multimap A\cong A^{[\nicefrac{{i}}{{j}}]}$.

Similarly if $j\in FI_{\bullet}(A)$, and $i$ is an index not occurring in $A$
then there are provable equivalences $A\otimes{\bf 1}^{j}_{i}\cong{\bf
1}^{i}_{j}\multimap A\cong A_{[\nicefrac{{i}}{{j}}]}$.

Proof

  1. (i)

Assume that the sequent $\Gamma^{\prime}\vdash A^{\prime}$ is obtained from
$\Gamma\vdash A$ by a similarity transformation replacing index $j$ with $i$.
Applying to $\Gamma\vdash A$ an expansion rule we replace the upper polarity
occurrence of $j$ with $i$ and introduce into the sequent the formula ${\bf
1}^{i}_{j}$. Then we use a reduction rule and replace the lower polarity
occurrence of $j$ and get the primed sequent.

  2. (ii)

As an example consider the $({\rm{L}}{\bf 1}_{\leftarrow})$ rule. Assume that
we have a sequent of the form $\Gamma,A,{\bf 1}_{i}^{j}\vdash B$, where $j\in
FI_{\bullet}(A)$, $i\not\in FI^{\bullet}(A)$. By definition of intuitionistic
tensor sequents there must be also an upper polarity free occurrence of $i$
located in some formula $F$, which is necessarily distinct from $A$. Assume
for definiteness that $F$ is in $\Gamma$, so that $\Gamma=\Gamma^{\prime},F$.
Note that $j\not\in FI_{\bullet}(F)$ because we already have the lower
polarity occurrence of $j$ in $A$. The derivation is shown in Figure
LABEL:L1<-_rule. Another case is $F=B$, which is treated similarly.

  3. (iii)

Induction on $F,F^{\prime}$, the base cases being $F=A\otimes B$,
$F^{\prime}=A^{[\nicefrac{{i}}{{j}}]}\otimes B_{[\nicefrac{{i}}{{j}}]}$ or
$F^{\prime}=A_{[\nicefrac{{i}}{{j}}]}\otimes B^{[\nicefrac{{i}}{{j}}]}$ and
analogously when the main connective is implication. The derivation for the
first case is shown in Figure LABEL:alpha-equiv_tensor. Other cases are
treated analogously.

  4. (iv)

Follows from the two preceding clauses.

  5. (v)

As an example we derive the equivalence $A\otimes{\bf 1}^{i}_{j}\cong
A^{[\nicefrac{{i}}{{j}}]}$ for $j\in FI^{\bullet}(A)$, $i$ fresh in Figure
LABEL:reparameterization_derivation. $\Box$

The crucial property of cut-elimination will be proven separately in Section
5, after the introduction of classical tensor term logic.

$\Gamma^{\prime},F,A,{\bf 1}_{i}^{j}\ \vdash\ B~{}j\in FI_{\bullet}(A),i\in
FI^{\bullet}(F)$ (${\rm{L}}{\bf 1}^{\leftarrow}$)
$\mathord{\Gamma^{\prime},F^{[\nicefrac{{j}}{{i}}]},A}\ \vdash\ \mathord{}$$B$
(${\rm{L}}{\bf 1}_{\to}$)
$\mathord{\Gamma^{\prime},F^{[\nicefrac{{j}}{{i}}]},A_{[\nicefrac{{i}}{{j}}]},{\bf
1}^{i}_{j}}\ \vdash\ \mathord{}$$B$ (${\rm{L}}{\bf 1}^{\leftarrow}$)
$\mathord{\Gamma^{\prime},F,A_{[\nicefrac{{i}}{{j}}]}}\ \vdash\ \mathord{}$$B$

(a)

$A\ \vdash\ A$ $B\ \vdash\ B$ (${\rm{R}}\otimes$) $\mathord{A,B}\ \vdash\
\mathord{}$$A\otimes B$ (${\rm{L}}{\bf 1}_{\to}$)
$\mathord{A,B_{[\nicefrac{{i}}{{j}}]},{\bf 1}^{i}_{j}}\ \vdash\
\mathord{}$$A\otimes B$ (${\rm{L}}{\bf 1}^{\leftarrow}$)
$\mathord{A^{[\nicefrac{{i}}{{j}}]},B_{[\nicefrac{{i}}{{j}}]}}\ \vdash\
\mathord{}$$A\otimes B$ (${\rm{L}}\otimes$)
$\mathord{A^{[\nicefrac{{i}}{{j}}]}\otimes B_{[\nicefrac{{i}}{{j}}]}}\ \vdash\
\mathord{}$$A\otimes B$

(b)

$A\ \vdash\ A~{}j\in FI^{\bullet}(A)$ ${\bf 1}^{i}_{j}\ \vdash\ {\bf
1}^{i}_{j}$ (${\rm{R}}\otimes$) $\mathord{A,{\bf 1}^{i}_{j}}\ \vdash\
\mathord{}$$A\otimes{\bf 1}^{i}_{j}$ (${\rm{L}}{\bf 1}^{\leftarrow}$)
$\mathord{A^{[\nicefrac{{i}}{{j}}]}}\ \vdash\ \mathord{}$$A\otimes{\bf
1}^{i}_{j}$ $A\ \vdash\ A~{}j\in FI^{\bullet}(A)$ (${\rm{R}}{\bf 1}^{\to}$)
$\mathord{A,{\bf 1}^{i}_{j}}\ \vdash\ \mathord{}$$A^{[\nicefrac{{i}}{{j}}]}$
(${\rm{L}}\otimes$) $\mathord{A\otimes{\bf 1}^{i}_{j}}\ \vdash\
\mathord{}$$A^{[\nicefrac{{i}}{{j}}]}$

(c)

##  4 Classical format

######  Definition 4.1.

Given a set $\mathit{Lit}_{+}$ of positive literals, where every element
$p\in\mathit{Lit}_{+}$ is assigned a valency $v(p)\in\mathbb{N}^{2}$, and an
infinite set $\mathit{Ind}$ of indices, the set $\widetilde{\mathit{Fm}}$ of
classical tensor pseudoformulas over $\mathit{Lit}_{+}$ is built according to
the grammar in Figure LABEL:TTL_lang, where $\mathit{Lit}_{-}$ and
$\mathit{Lit}$ are, respectively, the set of negative literals and of all
literals. The convention for negative literals is that $v(\overline{p})=(m,n)$
if $v(p)=(n,m)$. The set $\widetilde{\mathit{At}}$ is the set of classical
atomic pseudoformulas.

The connective $\parr$ is called cotensor (also par). The constant $\bot$ is
the counit. Duality $\overline{(.)}$ is not a connective or operator, but is
definable. Unlike the intuitionistic case we do not have to define upper/lower
index polarities different from actual index locations.

######  Definition 4.2.

An atomic tensor pseudoformula $p^{i_{1}\ldots i_{m}}_{j_{1}\ldots j_{n}}$
(over the given alphabet $\mathit{Lit}_{+}$) is well-formed if all indices
$i_{1},\ldots,i_{m}$, $j_{1},\ldots,j_{m}$ are pairwise distinct. A general
classical tensor pseudoformula $A$ is well-formed if it is built from well-
formed atomic ones and any index has at most one upper and one lower
occurrence in $A$. A well-formed classical tensor pseudoformula $F$ is a
classical tensor formula or a classical tensor type (over $\mathit{Lit}_{+}$).
A well-formed classical atomic tensor pseudoformula is a classical atomic
tensor formula. The set of classical atomic tensor formulas is denoted as
$At$. The set of classical tensor formulas over the given alphabet
$\mathit{Lit}_{+}$ is the classical tensor language generated by
$\mathit{Lit}_{+}$ or, simply the classical tensor language over
$\mathit{Lit}_{+}$. Free and bound indices, boundaries, $\alpha$-equivalence,
reparameterizations, type symbols, valencies and balanced type symbols are
defined exactly as in the intuitionistic case.

The set of intuitionistic tensor formulas is identified with a subset of
classical ones by means of the familiar translation $A\multimap
B=\overline{A}\parr B$.

######  Definition 4.3.

A classical tensor context is a finite set $\Gamma$ of tensor formulas
satisfying the same requirement (6) as in the intuitionistic case. As in the
intuitionistic case we denote
$FI^{\bullet}(\Gamma)=\bigcup\limits_{A\in\Gamma}FI^{\bullet}(A)$,
$FI_{\bullet}(\Gamma)=\bigcup\limits_{A\in\Gamma}FI_{\bullet}(A)$. A classical
tensor sequent $\Sigma$ is an expression of the form $\vdash\Gamma$, where
$\Gamma$ is a tensor context satisfying
$FI^{\bullet}(\Gamma)=FI_{\bullet}(\Gamma)$.

Just as in the intuitionistic case, the above definition means that every
index occurring in a classical tensor sequent has exactly one upper and one
lower occurrence. Intuitionistic tensor sequents are identified with classical
ones by translating $\Gamma\vdash B$ to $\vdash\overline{\Gamma},B$, where the
negated context $\overline{\Gamma}$ is defined by
$\overline{A_{(1)},\ldots,A_{(n)}}=\overline{A_{(1)}},\ldots,\overline{A_{(n)}}$.
Arguably, the classical format allows more symmetric notation and compact
definitions. The sequent calculus is also more compact.

######  Definition 4.4.

The system of classical tensor tern logic (TTL) is given by the rules in
Figure LABEL:TTL_rules, where it is assumed that all expressions are well-
formed.

Observe that there is the special instance $\vdash\bot^{j}_{i},{\bf
1}^{i}_{j}$ of the $({\rm{Id}})$ axiom, which is the rule introducing the unit
$\bf 1$.

$\begin{array}[]{c}\quad\quad\quad\quad\quad\quad\mathit{Lit}_{-}=\\{\overline{p}|~{}p\in\mathit{Lit}_{+}\\},\quad\overline{\overline{p}}=p\mbox{
for
}p\in\mathit{Lit}_{+},\quad\mathit{Lit}=\mathit{Lit}_{+}\cup\mathit{Lit}_{-}.\\\\[2.84544pt]
\quad\quad\quad\quad\quad\quad\mathit{Prop}=\mathit{Lit}\cup\\{{\bf
1},\bot\\},\quad v({\bf 1})=v(\bot)=(1,1),\quad\overline{{\bf
1}}=\bot,~{}\overline{\bot}={\bf 1}.\\\\[2.84544pt]
\quad\quad\quad\quad\quad\widetilde{\mathit{At}}=\\{p_{j_{1}\ldots
j_{n}}^{i_{1}\ldots
i_{m}}|~{}p\in\mathit{Prop},i_{1},\ldots,i_{m},j_{1},\ldots,j_{n}\subset\mathit{Ind},v(p)=(m,n)\\}.\\\\[2.84544pt]
\widetilde{\mathit{Fm}}::=\widetilde{\mathit{At}}|(\widetilde{\mathit{Fm}}\otimes\widetilde{\mathit{Fm}})|(\widetilde{\mathit{Fm}}\parr\widetilde{\mathit{Fm}}).\\\\[2.84544pt]
\quad\quad\quad\quad\quad\quad\overline{p^{i_{1},\ldots,i_{n}}_{j_{1},\ldots,j_{m}}}=\overline{p}_{{i_{n}},\ldots,{i_{1}}}^{{j_{m}},\ldots,{j_{1}}}\mbox{
for }p\in\mathit{Prop},~{}\overline{A\otimes
B}=\overline{B}\wp\overline{A},~{}\overline{A\wp
B}=\overline{B}\otimes\overline{A}.\end{array}$

(a)

$\begin{array}[]{c}\begin{array}[]{rl}\cfrac{A\in
At}{\vdash\overline{A},A}{\rm{(Id)}}&\cfrac{\vdash\Gamma,A\quad\vdash\overline{A},\Delta}{\vdash\Gamma,\Delta}({\rm{Cut}})\\\
\cfrac{\vdash\Gamma,A\quad\vdash B,\Delta}{\vdash\Gamma,A\otimes
B,\Delta}(\otimes)&\cfrac{\vdash\Gamma,A,B}{\vdash\Gamma,A\parr B}(\parr)\\\
\cfrac{\vdash\Gamma,A~{}j\in
FI^{\bullet}(A)}{\vdash\Gamma,\bot^{j}_{i},A^{[\nicefrac{{i}}{{j}}]}}({\bot}^{\to})&\cfrac{\vdash\Gamma,A,\bot_{i}^{j}~{}j\in
FI_{\bullet}(A)}{\vdash\Gamma,A_{[\nicefrac{{i}}{{j}}]}}({\bot}_{\leftarrow})\end{array}\\\\[17.07182pt]
\mbox{In }({\bot}^{\to}),({\bot}_{\leftarrow})~{}i\not\in FI^{\bullet}(A)\cup
FI_{\bullet}(A)\end{array}$

(b)

$\begin{array}[]{c}\begin{array}[]{rl}\cfrac{\vdash\Gamma,A~{}j\in
FI_{\bullet}(A)}{\vdash\Gamma,{\bot}^{i}_{j},A_{[\nicefrac{{i}}{{j}}]}}({\bot}_{\to})&\cfrac{\vdash\Gamma,A,{\bot}^{i}_{j}~{}j\in
FI^{\bullet}(A)}{\vdash\Gamma,A^{[\nicefrac{{i}}{{j}}]}}({\bot}^{\leftarrow})\end{array}\\\\[17.07182pt]
\mbox{In both rules above }i\not\in FI^{\bullet}(A)\cup
FI_{\bullet}(A)\end{array}$

(c)

Figure 4: Classical TTL

In general, the classical system is much more convenient for proof-theoretic
analysis (cut-elimination, proof-search etc), and we will use it whenever such
an analysis is important. The embedding of the intuitionistic system is
conservative (as we will show shortly), so the results obtained for the
classical version apply to the intuitionistic fragment as well. We will
sometimes use the two-sided format for TTL as well and write
$\Gamma\vdash\Delta$ for $\vdash\overline{\Gamma},\Delta$.

As in the intuitionistic case we define similarity transformation of sequents
as simultaneous replacement of all free occurrences of an index with a fresh
one, and similar sequents as those related by similarity transformations.
$\alpha$-Equivalence of sequents is also defined the same as in the
intuitionistic case. Then we list simplest properties of TTL, parallel to
those of ITTL. Proofs are analogous to Proposition 3.8.

######  Proposition 4.5.

In TTL

  1. (i)

Similar sequents are cut-free derivable from each other;

  2. (ii)

rules in Figure LABEL:TTL_admissible_rules are admissible and can be emulated
without use of the Cut rule;

  3. (iii)

$\alpha$-equivalent formulas are provably equivalent, i.e. if
$F\equiv_{\alpha}F^{\prime}$ then the sequents
$\vdash\overline{F},F^{\prime}$, $\vdash\overline{F^{\prime}},F$ are
derivable;

  4. (iv)

$\alpha$-equivalent sequents are derivable from each other;

  5. (v)

if $j\in FI^{\bullet}(A)$, and $i$ is an index not occurring in $A$ then there
are provable equivalences $A\otimes{\bf 1}^{i}_{j}\cong{\bot}^{i}_{j}\parr
A\cong A^{[\nicefrac{{i}}{{j}}]}$.

Similarly if $j\in FI_{\bullet}(A)$, and $i$ is an index not occurring in $A$
then there are provable equivalences $A\otimes{\bf
1}^{j}_{i}\cong{\bot}^{j}_{i}\parr A\cong A_{[\nicefrac{{i}}{{j}}]}$. $\Box$

##  5 Cut-elimination

In this section we prove cut-elimination for the classical TTL and then, as a
consequence, for the intuitionistic version.

We use the following notation for iterated substitutions. Capital Latin
letters ($I,J,\ldots$) stand for sequences of pairwise distinct indices and
the expression $A^{[\nicefrac{{I}}{{J}}]}$, where
$I=\\{i_{1},\ldots,i_{n}\\}$, $J=\\{j_{1},\ldots,j_{n}\\}$, stands for
$A^{[\nicefrac{{i_{1}}}{{j_{1}}}],\ldots[\nicefrac{{i_{n}}}{{j_{n}}}]}$,
similarly with lower indices.

###  5.1 Alternative formulation

$\begin{array}[]{c}\cfrac{\vdash\Gamma,A,B}{\vdash\Gamma,A^{[\nicefrac{{K}}{{I}}]}_{[\nicefrac{{L}}{{J}}]}\parr
B_{[\nicefrac{{K}}{{I}}]}^{[\nicefrac{{L}}{{J}}]}}(\parr_{\equiv\alpha})~{}~{}\cfrac{\vdash\Gamma,A~{}\vdash
B,\Theta}{\vdash\Gamma,A^{[\nicefrac{{K}}{{I}}]}_{[\nicefrac{{L}}{{J}}]}\otimes
B_{[\nicefrac{{K}}{{I}}]}^{[\nicefrac{{L}}{{J}}]},\Theta}(\otimes_{\equiv\alpha})\\\\[14.22636pt]
\mbox{where }I\subseteq FI^{\bullet}(A)\cap FI_{\bullet}(B),J\subseteq
FI_{\bullet}(A)\cap FI^{\bullet}(B),\\\ K\cap(FI^{\bullet}(A,B)\cup
FI_{\bullet}(A,B))=L\cap(FI^{\bullet}(A,B)\cup
FI_{\bullet}(A,B))=\emptyset.\end{array}$

(a)

$\begin{array}[]{c}k\in FI^{\bullet}(\Gamma)\cap FI_{\bullet}(\Gamma),l\in
FI_{\bullet}(\Delta)\cap FI^{\bullet}(\Delta),k^{\prime},l^{\prime}\mbox{
fresh},\\\ i\in FI_{\bullet}(\Gamma)\cap FI^{\bullet}(A)\cap
FI_{\bullet}(B)\cap FI^{\bullet}(\Delta),\\\ j\in FI^{\bullet}(\Gamma)\cap
FI_{\bullet}(A)\cap FI^{\bullet}(B)\cap FI_{\bullet}(\Delta):\\\\[5.69046pt]
\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
126.74998pt\hbox{\vbox{\vbox{\vbox{\hbox{\vbox{\vbox{\hbox{\hskip
0.1pt\hbox{$\mathord{}\ \vdash\ \mathord{}$}\hbox{$\Gamma,A$}\hskip
0.1pt}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to48.46873pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
0.5pt($\sim$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\hbox{\hskip
0.1pt\hbox{$\mathord{}\ \vdash\
\mathord{}$}\hbox{$\Gamma_{[\nicefrac{{k^{\prime}}}{{k}}]}^{[\nicefrac{{k^{\prime}}}{{k}}]},A$}\hskip
0.1pt}}}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to69.6415pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
0.5pt($\sim$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\hbox{\hskip
0.1pt\hbox{$\mathord{}\ \vdash\
\mathord{}$}\hbox{$(\Gamma_{[\nicefrac{{k^{\prime}}}{{k}}]}^{[\nicefrac{{k^{\prime}}}{{k}}]})_{[\nicefrac{{k}}{{i}}]}^{[\nicefrac{{l}}{{j}}]},A^{[\nicefrac{{k}}{{i}}]}_{[\nicefrac{{l}}{{j}}]}$}\hskip
0.1pt}}}\hbox{\hskip 14.45377pt}\vbox{\vbox{\hbox{\hskip
0.1pt\hbox{$\mathord{}\ \vdash\ \mathord{}$}\hbox{$B,\Delta$}\hskip
0.1pt}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to49.26668pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
0.5pt($\sim$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\hbox{\hskip
0.1pt\hbox{$\mathord{}\ \vdash\
\mathord{}$}\hbox{$B,\Delta^{[\nicefrac{{l^{\prime}}}{{l}}]}_{[\nicefrac{{l^{\prime}}}{{l}}]}$}\hskip
0.1pt}}}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to70.43944pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
0.5pt($\sim$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\hbox{\hskip
0.1pt\hbox{$\mathord{}\ \vdash\
\mathord{}$}\hbox{$B_{[\nicefrac{{k}}{{i}}]}^{[\nicefrac{{l}}{{j}}]},(\Delta^{[\nicefrac{{l^{\prime}}}{{l}}]}_{[\nicefrac{{l^{\prime}}}{{l}}]})^{[\nicefrac{{k}}{{i}}]}_{[\nicefrac{{l}}{{j}}]}$}\hskip
0.1pt}}}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox to170.5903pt{\xleaders\hrule\hfill}\lower
2.3pt\hbox{\hskip 0.5pt($\otimes$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
21.18797pt\hbox{\hskip 0.1pt\hbox{$\mathord{}\ \vdash\
\mathord{}$}\hbox{$(\Gamma_{[\nicefrac{{k^{\prime}}}{{k}}]}^{[\nicefrac{{k^{\prime}}}{{k}}]})_{[\nicefrac{{k}}{{i}}]}^{[\nicefrac{{l}}{{j}}]},A^{[\nicefrac{{k}}{{i}}]}_{[\nicefrac{{l}}{{j}}]}\otimes
B_{[\nicefrac{{k}}{{i}}]}^{[\nicefrac{{l}}{{j}}]},(\Delta^{[\nicefrac{{l^{\prime}}}{{l}}]}_{[\nicefrac{{l^{\prime}}}{{l}}]})^{[\nicefrac{{k}}{{i}}]}_{[\nicefrac{{l}}{{j}}]}$}\hskip
0.1pt}}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
21.18797pt\lower-0.2pt\hbox{}\hbox to128.21436pt{\xleaders\hrule\hfill}\lower
2.3pt\hbox{\hskip 0.5pt($\sim$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
21.18797pt\hbox{\hskip 0.1pt\hbox{$\mathord{}\ \vdash\
\mathord{}$}\hbox{$\Gamma^{[\nicefrac{{k^{\prime}}}{{k}}]}_{[\nicefrac{{k^{\prime}}}{{k}}]},A^{[\nicefrac{{k}}{{i}}]}_{[\nicefrac{{l}}{{j}}]}\otimes
B_{[\nicefrac{{k}}{{i}}]}^{[\nicefrac{{l}}{{j}}]},\Delta^{[\nicefrac{{l^{\prime}}}{{l}}]}_{[\nicefrac{{l^{\prime}}}{{l}}]}$}\hskip
0.1pt}}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
21.18797pt\lower-0.2pt\hbox{}\hbox to99.2638pt{\xleaders\hrule\hfill}\lower
2.3pt\hbox{\hskip 0.5pt($\sim$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
21.18797pt\hbox{\hskip 0.1pt\hbox{$\mathord{}\ \vdash\
\mathord{}$}\hbox{$\Gamma,A^{[\nicefrac{{k}}{{i}}]}_{[\nicefrac{{l}}{{j}}]}\otimes
B_{[\nicefrac{{k}}{{i}}]}^{[\nicefrac{{l}}{{j}}]},\Delta$}\hskip
0.1pt}}}}\ignorespaces\end{array}$

(b)

Figure 5: Alternative formulation of TTL

For proving cut-elimination it is convenient to give an alternative
formulation for (classical) TTL, where the $(\otimes)$ and the $(\parr)$ rules
are replaced with their closures under $\alpha$-equivalence of sequents.

######  Definition 5.1.

The system ${\bf TTL}^{\prime}$ is obtained from TTL by replacing the
$(\otimes)$ and the $(\parr)$ rules with their closures
$(\otimes_{\equiv_{\alpha}})$, $(\parr_{\equiv_{\alpha}})$ under
$\alpha$-equivalence shown in Figure LABEL:primed_system.

######  Proposition 5.2.

A sequent is derivable, respectively cut-free derivable, in ${\bf
TTL}^{\prime}$ iff it is derivable, respectively cut-free derivable, in ${\bf
TTL}$.

Proof TTL rules are special instances of ${\bf TTL}^{\prime}$ rules, so the
direction from ${\bf TTL}$ to ${\bf TTL}^{\prime}$ is trivial. For the other
direction it can be observed that the $(\otimes)^{\prime}$, $(\parr)^{\prime}$
rules can be cut-free emulated in TTL using Proposition 4.5, clause (i). In
Figure LABEL:primed_system_emulation_figure we show a generic example for the
$(\otimes_{\equiv\alpha})$ rule, where, for notational simplicity, we assume
that all sequences $K,L,I,J$ are singletons $k,l,i,j$. Note, however, that we
should take into account that the indices $k$ and $l$ may occur in $\Gamma$
$\Delta$ respectively. The indices $k^{\prime}$ and $l^{\prime}$ in Figure
LABEL:primed_system_emulation_figure are fresh; they are needed in order to
avoid index collisions. $\Box$

######  Proposition 5.3.

If $\vdash\Gamma$, $\vdash\Gamma^{\prime}$ are $\alpha$-equivalent tensor
sequents and $\pi$ is a ${\bf TTL}^{\prime}$ derivation of $\Gamma$ then there
exists an ${\bf TTL}^{\prime}$ derivation $\pi^{\prime}$ of
$\vdash\Gamma^{\prime}$, which is obtained from $\pi$ by renaming some
indices.

Proof Easy induction on $\pi$. $\Box$

###  5.2 Cut-elimination in ${\bf TTL}^{\prime}$

We define the size of a derivation in ${\bf TTL}^{\prime}$ as follows. If the
derivation $\pi$ is an axiom then the size $\mathit{size}(\pi)$ of $\pi$ is
$1$. If $\pi$ is obtained from a derivation $\pi^{\prime}$ by a single-premise
rule then $\mathit{size}(\pi)=\mathit{size}(\pi^{\prime})+1$. If $\pi$ is
obtained from derivations $\pi_{1}$, $\pi_{2}$ by a two-premise rule then
$\mathit{size}(\pi)=\mathit{size}(\pi_{1})+\mathit{size}(\pi_{2})+1$.

Given a ${\bf TTL}^{\prime}$ derivation with two subderivations $\pi_{1}$,
$\pi_{2}$ of the sequents $\vdash\Gamma,A$ and $\vdash\overline{A},\Delta$
respectively followed by the Cut rule, we say that this application of the Cut
rule is a principal cut if $A=F\otimes G$ and $\pi_{1}$, respectively
$\pi_{2}$, ends with the $(\otimes_{\equiv\alpha})$, respectively the
$(\parr_{\equiv\alpha})$ rule introducing formula $A$, respectively
$\overline{A}$. An application of the Cut rule that is not principal is a side
cut.

######  Lemma 5.4.

There is an algorithm transforming a ${\bf TTL}^{\prime}$ derivation $\pi$ of
a sequent $\vdash\Gamma$ to a derivation $\pi^{\prime}$ of some sequent
$\vdash\Gamma^{\prime}$ such that $\vdash\Gamma$ and $\vdash\Gamma^{\prime}$
are $\alpha$-equivalent, $\mathit{size}(\pi^{\prime})=\mathit{size}(\pi)$ and
all cuts in $\pi^{\prime}$ principal.

Let $\pi_{1},\ldots,\pi_{n}$ be all subderivations of $\pi$ ending with side
cuts and $N=\sum\mathit{size}(\pi_{i})$. We will use $N$ as the induction
parameter for proving termination of the algorithm.

The algorithm consists in permuting a side cut with the preceding rule, which
may be accompanied with tours of index renaming. There are two types of side
cuts. First type is when the last rule in each of the two subderivations does
not involve the cut-formula at all. The second type is when the last rule in
one of the two subderivations is the $(\bot^{\to})$ or the
$(\bot_{\leftarrow})$ rule modifying the cut-formula.

A generic example for the first type is shown in Figure LABEL:side_cut_figure,
where we have an application of the $(\parr_{\equiv\alpha})$ rule to the
sequent $\vdash\Gamma,F,G,A$ followed by a side cut with the sequent
$\vdash\overline{A},\Delta$, and the side contexts $F,G$ and $\Delta$ have
common free indices. We cannot cut the premise $\vdash\Gamma,F,G,A$ of the
$(\parr_{\equiv_{\alpha}})$ rule with the right premise
$\vdash\overline{A},\Delta$ of the side cut, because this would introduce
forbidden repetitions of indices. Therefore we use Proposition 5.3 and replace
the derivation of $\vdash\overline{A},\Delta$ with a derivation of the same
size and an $\alpha$-equivalent conclusion
$\vdash\overline{A},\Delta^{\prime}$ involving fresh indices. In the new
derivation we safely push the cut upwards, and get the conclusion
$\alpha$-equivalent to that of the original one.

The induction parameter $N$ for the new derivation is smaller at least by 1.

A generic example for the second type is shown in Figure
LABEL:side_cut_figure2, where we have an application of the
$(\bot_{\leftarrow})$ rule to the sequent
$\vdash\overline{A},\bot^{j}_{i},\Delta$ on the right, which is followed by a
side cut with the sequent $\vdash\Gamma,A^{[\nicefrac{{i}}{{j}}]}$. Here we
need two tours of index renaming in the left sequent using Proposition 5.3. In
order to push the cut upwards we need to replace the formula
${A^{[\nicefrac{{i}}{{j}}]}}$ with $A$, which means replacing the index $i$
with $j$. But we also need to take into account that the index $j$ may be
already present in the left sequent. Therefore we need first to replace it
with a fresh $j^{\prime}$.

Again, after the transformation we obtain a derivation whose conclusion is
$\alpha$-equivalent to that of the original one and the induction parameter
$N$ is smaller at least by 1. $\Box$

$\begin{array}[]{c}i\in FI^{\bullet}(F)\cap FI_{\bullet}(G)\cap
FI^{\bullet}(\Delta)\cap FI_{\bullet}(\Delta),\\\ j\in FI_{\bullet}(F)\cap
FI^{\bullet}(G)\cap FI^{\bullet}(\Delta)\cap FI_{\bullet}(\Delta),\\\
F^{\prime}=F^{[\nicefrac{{k}}{{i}}]}_{[\nicefrac{{l}}{{j}}]},~{}G^{\prime}=G_{[\nicefrac{{k}}{{i}}]}^{[\nicefrac{{l}}{{j}}]},~{}i^{\prime},j^{\prime}\mbox{
fresh},\Delta^{\prime}=\Delta_{[\nicefrac{{i^{\prime}}}{{i}}][\nicefrac{{j^{\prime}}}{{j}}]}^{[\nicefrac{{i^{\prime}}}{{i}}][\nicefrac{{j^{\prime}}}{{j}}]}:\\\\[8.5359pt]
\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
50.80553pt\hbox{\vbox{\hbox{\vbox{\hbox{\hskip 0.1pt\hbox{$\mathord{}\ \vdash\
\mathord{}$}\hbox{$\Gamma,F,G,A$}\hskip
0.1pt}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to71.22565pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
3.0pt($\parr_{\equiv\alpha}$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
0.0pt\hbox{\hskip 0.1pt\hbox{$\mathord{}\ \vdash\
\mathord{}$}\hbox{$\Gamma,F^{\prime}\parr G^{\prime},A$}\hskip
0.1pt}}}\hbox{\hskip 1.0pt}\hbox{\hskip 0.1pt\hbox{$\mathord{}\ \vdash\
\mathord{}$}\hbox{$\overline{A},\Delta$}\hskip
0.1pt}}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to139.6551pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
3.0pt(${\rm{Cut}}$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
33.79805pt\hbox{\hskip 0.1pt\hbox{$\mathord{}\ \vdash\
\mathord{}$}\hbox{$\Gamma,F^{\prime}\parr G^{\prime},\Delta$}\hskip
0.1pt}}}}\ignorespaces\Longrightarrow\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
49.83331pt\hbox{\vbox{\vbox{\hbox{\hbox{\hskip 0.1pt\hbox{$\mathord{}\ \vdash\
\mathord{}$}\hbox{$\Gamma,F,G,A$}\hskip 0.1pt}\hbox{\hskip 5.0pt}\hbox{\hskip
0.1pt\hbox{$\mathord{}\ \vdash\
\mathord{}$}\hbox{$\overline{A},\Delta^{\prime}$}\hskip
0.1pt}}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to108.59386pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
3.0pt(${\rm{Cut}}$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
21.90549pt\hbox{\hskip 0.1pt\hbox{$\mathord{}\ \vdash\
\mathord{}$}\hbox{$\Gamma,F,G,\Delta^{\prime}$}\hskip
0.1pt}}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
15.79437pt\lower-0.2pt\hbox{}\hbox to79.7101pt{\xleaders\hrule\hfill}\lower
2.3pt\hbox{\hskip
3.0pt($\parr_{\equiv\alpha}$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
15.79437pt\hbox{\hskip 0.1pt\hbox{$\mathord{\vdash}\ \vdash\
\mathord{}$}\hbox{$\Gamma,F^{\prime}\parr G^{\prime},\Delta^{\prime}$}\hskip
0.1pt}}}}\ignorespaces\end{array}$

(a)

$\begin{array}[]{c}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
49.3611pt\hbox{\vbox{\hbox{\hbox{\hskip 0.1pt\hbox{$\mathord{}\ \vdash\
\mathord{}$}\hbox{$\Gamma,A^{[\nicefrac{{i}}{{j}}]}$}\hskip 0.1pt}\hbox{\hskip
1.0pt}\vbox{\hbox{\hskip 0.1pt\hbox{$\mathord{}\ \vdash\
\mathord{}$}\hbox{$\overline{A},\bot^{j}_{i},\Delta$}\hskip
0.1pt}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to52.8266pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
3.0pt($\bot_{\leftarrow}$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
0.0pt\hbox{\hskip 0.1pt\hbox{$\mathord{}\ \vdash\
\mathord{}$}\hbox{$\overline{A_{[\nicefrac{{i}}{{j}}]}},\Delta$}\hskip
0.1pt}}}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox to85.95955pt{\xleaders\hrule\hfill}\lower
2.3pt\hbox{\hskip
3.0pt(${\rm{Cut}}$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
23.08817pt\hbox{\hskip 0.1pt\hbox{$\mathord{}\ \vdash\
\mathord{}$}\hbox{$\Gamma,\Delta$}\hskip
0.1pt}}}}\ignorespaces\Longrightarrow\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
52.64998pt\hbox{\vbox{\vbox{\hbox{\hbox{\hskip 0.1pt\hbox{$\mathord{}\ \vdash\
\mathord{}$}\hbox{$(\Gamma^{[\nicefrac{{j^{\prime}}}{{j}}]}_{[\nicefrac{{j^{\prime}}}{{j}}]})_{[\nicefrac{{j}}{{i}}]},A,$}\hskip
0.1pt}\hbox{\hskip 5.0pt}\hbox{\hskip 0.1pt\hbox{$\mathord{}\ \vdash\
\mathord{}$}\hbox{$\overline{A},\bot^{j}_{i},\Delta$}\hskip
0.1pt}}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to122.55199pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
3.0pt(${\rm{Cut}}$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
23.29439pt\hbox{\hskip 0.1pt\hbox{$\mathord{}\ \vdash\
\mathord{}$}\hbox{$(\Gamma^{[\nicefrac{{j^{\prime}}}{{j}}]}_{[\nicefrac{{j^{\prime}}}{{j}}]})_{[\nicefrac{{j}}{{i}}]},\bot^{j}_{i},\Delta$}\hskip
0.1pt}}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
23.29439pt\lower-0.2pt\hbox{}\hbox to75.96321pt{\xleaders\hrule\hfill}\lower
2.3pt\hbox{\hskip
3.0pt($\bot_{\leftarrow}$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
23.29439pt\hbox{\hskip 0.1pt\hbox{$\mathord{}\ \vdash\
\mathord{}$}\hbox{$\Gamma^{[\nicefrac{{j^{\prime}}}{{j}}]}_{[\nicefrac{{j^{\prime}}}{{j}}]},\Delta$}\hskip
0.1pt}}}}\ignorespaces\end{array}$

(b)

Figure 6: Transforming a side cut in ${\bf TTL}^{\prime}$

######  Lemma 5.5.

There is an algorithm transforming a ${\bf TTL}^{\prime}$ derivation $\pi$ of
a sequent $\vdash\Gamma$ with cuts into a ${\bf TTL}^{\prime}$ derivation
$\pi^{\prime}$ of some sequent $\vdash\Gamma^{\prime}$ such that
$\vdash\Gamma$ and $\vdash\Gamma^{\prime}$ are $\alpha$-equivalent and
$\mathit{size}(\pi^{\prime})<\mathit{size}(\pi)$, provided that all cuts in
$\pi$ are principal.

Proof The algorithm consists in pushing principal cuts upwards to axioms,
sometimes replacing sequents with $\alpha$-equivalent ones, similar to the
preceding lemma. $\Box$

######  Corollary 5.6.

The system ${\bf TTL}^{\prime}$ is cut-free.

Proof Follows from the two preceding lemmas and Proposition 5.3. $\Box$

######  Corollary 5.7.

The system TTL is cut-free.

Proof Follows from the preceding corollary and Proposition 5.2. $\Box$

######  Corollary 5.8.

The system ITTL is a conservative fragment of TTL. In particular, ITTL is cut-
free. $\Box$

In the sequel we will be also interested in derivations from non-logical
axioms. For this case we have the following version of cut-elimination that is
proven identically.

######  Lemma 5.9.

Let $\Xi$ be a set of tensor sequents closed under $\alpha$-equivalence. If a
sequent $\vdash\Gamma$ is TTL derivable from $\Xi$ then there exists a TTL
derivation $\pi$ of $\vdash\Gamma$ from $\Xi$ such that for any application of
the Cut rule in $\pi$ at least one of the two premises is an element of $\Xi$
and if the cut-formula is atomic non-unit (i.e. not of the form ${\bf
1}^{i}_{j}$ or $\bot^{i}_{j}$) then both premises are elements of $\Xi$.
$\Box$

##  6 Decidability

Although TTL is cut-free, it does not satisfy the subformula property in the
direct sense, unless we agree that the counit $\bot^{j}_{i}$ is a subformula
of everything, which seems rather exotic. The reason is in the reduction rule
$(\bot_{\leftarrow})$. This rule also makes decidability of the system rather
non-obvious. Our current goal is to show that applications of this rule can be
heavily restricted, which makes proof-search finite and the system decidable.

######  Definition 6.1.

An application

$\cfrac{\vdash\Gamma,A,\bot^{j}_{i}\quad j\in
FI_{\bullet}(A)}{\vdash\Gamma,A_{[\nicefrac{{i}}{{j}}]}}$

of the $(\bot_{\leftarrow})$ rule in a TTL proof is essential if there is a
bound occurrence of the index $j$ in $\Gamma$. Otherwise it is inessential.

Our first goal is to show that inessential applications of the rule can be
eliminated from the derivation.

######  Proposition 6.2.

Assume that $\vdash\Gamma$ is a sequent derivable in ${\bf TTL}$ with a cut-
free derivation $\pi$ and the index $j$ occurs in $\Gamma$ freely and has no
bound occurrences. Let $i$ be a fresh index. The sequent
$\vdash\Gamma^{[\nicefrac{{i}}{{j}}]}_{[\nicefrac{{i}}{{j}}]}$ is derivable in
TTL with a derivation $\pi^{\prime}$, which is obtained from $\pi$ by
replacing the index $j$ with $i$.

Proof Induction on $\pi$. The essential step is the $(\otimes)$ rule.

Assume that $\pi$ is obtained from derivations $\pi_{1}$, $\pi_{2}$ with
conclusions $\vdash\Gamma_{1}$, $\vdash\Gamma_{2}$ respectively by the
$(\otimes)$ rule. Every occurrence of $j$ in $\vdash\Gamma$ comes from one of
the premises $\vdash\Gamma_{1}$, $\vdash\Gamma_{2}$. Assume for definiteness
that the upper free occurrence of $j$ in $\vdash\Gamma$ comes from
$\vdash\Gamma_{1}$. There is also a lower free occurrence of $j$ in
$\vdash\Gamma_{1}$, and since there are no bound occurrences of $j$ in
$\vdash\Gamma$ the latter occurrence remains free in $\vdash\Gamma$. It
follows that both occurrences of $j$ in $\vdash\Gamma$ come from
$\vdash\Gamma_{1}$. Also, there is no bound occurrence of $j$ in
$\vdash\Gamma_{1}$, because otherwise it would be inherited by $\Gamma$. Thus
the induction hypothesis can be applied to $\Gamma_{1}$ and $\pi_{1}$, and we
have a derivation $\pi_{1}^{\prime}$ of
$\vdash(\Gamma_{1})^{[\nicefrac{{i}}{{j}}]}_{[\nicefrac{{i}}{{j}}]}$ obtained
from $\pi_{1}$ by replacing $j$ with $i$. The desired derivation
$\pi^{\prime}$ of
$\vdash\Gamma^{[\nicefrac{{i}}{{j}}]}_{[\nicefrac{{i}}{{j}}]}$ is obtained
from $\pi_{1}^{\prime}$ and $\pi_{2}$ by the $(\otimes)$ rule. $\Box$

######  Proposition 6.3.

Let a sequent $\vdash\Gamma,A,\bot^{j}_{i}$, where $j\in FI_{\bullet}(A)$,
$i\not\in FI^{\bullet}(A)\cup FI_{\bullet}(A)$ and there is no bound
occurrence of $j$ in $\Gamma$, be derivable in TTL with a cut-free derivation
$\pi$. The sequent $\vdash\Gamma,A_{[\nicefrac{{i}}{{j}}]}$ is derivable in
${\bf TTL}$ with a cut-free derivation of the size smaller than that of $\pi$.

Proof Induction on the size of $\pi$.

Assume that $\pi$ is obtained from a derivation $\pi^{\prime}$ by the
$(\bot^{\to})$ introducing the formula $\bot^{j}_{i}$. This means
$\Gamma=\Gamma^{\prime},B^{[\nicefrac{{i}}{{j}}]}$, and $\pi^{\prime}$ has the
conclusion $\vdash\Gamma^{\prime},B,A$, where $j\in FI^{\bullet}(B)$,
$i\not\in FI^{\bullet}(B)\cup FI_{\bullet}(B)$. Also, $i$ does not occur in
$\Gamma^{\prime}$, otherwise the sequent $\vdash\Gamma,A,\bot^{j}_{i}$ is not
well-formed. By the preceding proposition we have a derivation
$\pi^{\prime\prime}$ of
$\vdash\Gamma^{\prime},B^{[\nicefrac{{i}}{{j}}]},A_{[\nicefrac{{i}}{{j}}]}$
obtained from $\pi^{\prime}$ by replacing $j$ with $i$. But the conclusion of
$\pi^{\prime\prime}$ is precisely the desired sequent
$\vdash\Gamma,A_{[\nicefrac{{i}}{{j}}]}$ and the size of $\pi^{\prime\prime}$
equals the size of $\pi^{\prime}$, which is strictly smaller than the size of
$\pi$.

Assume that the last rule in $\pi$ is $(\bot_{\leftarrow})$ modifying one of
the formulas $\bot^{j}_{i}$ or $A$. Assume for definiteness that the
$(\bot_{\leftarrow})$ rule modifies the formula $A$ (the other case being very
similar). Then the premise of the $(\bot_{\leftarrow})$ rule is a sequent
$\vdash\Gamma^{\prime\prime}$ of the form
$\vdash\Gamma^{\prime},A_{[\nicefrac{{k}}{{j}}]},\bot^{k}_{j}$, where
$\Gamma^{\prime}=\Gamma,\bot^{j}_{i}$, and the derivation $\pi^{\prime}$ of
$\vdash\Gamma^{\prime\prime}$ has the size
$\mathit{size}(\pi^{\prime})=\mathit{size}(\pi)-1$. Then, by the induction
hypothesis the sequent $\vdash\Gamma^{\prime},A$, is derivable with a cut-free
derivation $\pi^{\prime\prime}$ with the size
$\mathit{size}(\pi^{\prime\prime})<\mathit{size}(\pi^{\prime})<\mathit{size}(\pi)$,
and, applying the induction hypothesis once again, the desired sequent
$\vdash\Gamma,A_{[\nicefrac{{i}}{{j}}]}$ is derivable with a cut-free
derivation $\rho$ with
$\mathit{size}(\rho)<\mathit{size}(\pi^{\prime\prime})<\mathit{size}(\pi)$.

The case of the $(\otimes)$ rule is very similar to that of the $(\otimes)$
rule in the proof of the preceding proposition. Other cases are very easy.
$\Box$

######  Corollary 6.4.

Any TTL derivable sequent is derivable with a cut-free derivation where all
applications of the $(\bot_{\leftarrow})$ rule are essential. $\Box$

Thus, when searching for a TTL derivation of a tensor sequent we may restrict
to cut-free derivations where all applications of the $(\bot_{\leftarrow})$
rule are essential. In such a derivation premises of any rule are built from
subformulas of the conclusion and, possibly, counits $\bot^{j}_{i}$, where the
indices $i,j$ occur in the conclusion. In particular there are only finitely
many possible rule applications with a given conclusion. In order to guarantee
that the proof-search stops we introduce a specific complexity measure of the
sequent.

Let the complexity $c(A)$ of a formula $A$ be defined by

$c(A)=1\mbox{ for }A\mbox{ atomic},~{}c(A_{1}\otimes A_{2})=c(A_{1}\parr
A_{2})=c(A_{1})+c(A_{2})+1.$

Let us say that an index $j$ is suspicious for the sequent $\vdash\Gamma$ if
there is a bound occurrence of $j$ in $\Gamma$, but the formula $\bot^{j}_{i}$
does not occur in $\Gamma$ for any $i$. Let $d(\Gamma)$ be the number of
indices suspicious for $\vdash\Gamma$. Finally, let the complexity $c(\Gamma)$
of $\vdash\Gamma$ be defined as
$c(\Gamma)=\sum\limits_{A\in\Gamma}c(A)+2d(\Gamma)$. Then if $\vdash\Gamma$ is
a conclusion of any TTL rule that is not a cut or an inessential application
of the $(\bot_{\leftarrow})$ rule, the premises of the rule have complexity
strictly less than $\vdash\Gamma$. This provides us with a decision procedure
for TTL and, by conservativity, for ITTL as well.

######  Corollary 6.5.

The systems TTL and ITTL are decidable. $\Box$

##  7 Semantics

We have already sketched the “naive” semantics for ITTL, which is sound, but
whose completeness is under question. In this section we slightly refine the
above and define semantics for both TTL and ITTL, which is definitely complete
when the language is balanced. (Completeness will be proven in the end of the
paper.)

###  7.1 Semantic types

######  Definition 7.1.

Given a terminal alphabet $T$, a semantic pretype $A$ over $T$ is a set $A$ of
tensor terms (over $T$) having common boundary, which is called the boundary
of $A$. We denote the boundary of $A$ as $FI(A)$ and its two components as
$FI^{\bullet}(A)$ and $FI_{\bullet}(A)$.

In order to define a system of semantic types that will interpret tensor
formulas we need to choose a special pretype $\bot\\!\\!\\!\\!\\!\\!\bot$ with
empty boundary.

######  Definition 7.2.

A semantic type system consists of a terminal alphabet $T$ and a pretype
$\bot\\!\\!\\!\\!\\!\\!\bot$ over $T$, called the dualizing type, satisfying
$FI^{\bullet}(\bot\\!\\!\\!\\!\\!\\!\bot)=FI_{\bullet}(\bot\\!\\!\\!\\!\\!\\!\bot)=\emptyset$.

Given a semantic type system $(T,\bot\\!\\!\\!\\!\\!\\!\bot)$ and a pretype
$A$ over $T$, the dual $\overline{A}$ of $A$ is the set of terms (over $T$)
defined by $\overline{A}=\\{s|~{}\forall t\in
A~{}ts\in\bot\\!\\!\\!\\!\\!\\!\bot\\}$.

The pretype $A$ is a semantic type if $A=\overline{\overline{A}}$.

In the following we assume that a semantic type system is given. We will omit
the prefix “semantic”, unless it leads to a confusion.

######  Proposition 7.3.

  1. (i)

For any pretype $A$ we have
$FI(\overline{A})=(FI_{\bullet}(A),FI^{\bullet}(A))$.

  2. (ii)

If $A,B$ are pretypes and $A\subseteq B$ then
$\overline{B}\subseteq\overline{A}$.

  3. (iii)

A pretype $A$ is a type iff $A=\overline{B}$ for some pretype $B$.

  4. (iv)

The dualizing type $\bot\\!\\!\\!\\!\\!\\!\bot=\overline{\\{1\\}}$ is indeed a
type. $\Box$

####  7.1.1 Multiplicative operations

######  Definition 7.4.

Let $A$, $B$ be types such that $FI^{\bullet}(A)\cap
FI_{\bullet}(B)=FI_{\bullet}(A)\cap FI^{\bullet}(B)=\emptyset$. The internal
hom type $A\multimap B$ is the set

$A\multimap B=\\{t|~{}\forall s\in A~{}ts\in B\\}.$

######  Definition 7.5.

Let $A$, $B$ be types such that $FI^{\bullet}(A)\cap
FI^{\bullet}(B)=FI_{\bullet}(A)\cap FI_{\bullet}(B)=\emptyset$. The product
pretype $A\cdot B$, the tensor product type $A\otimes B$ and the cotensor
product type are given by

$\begin{array}[]{c}A\cdot B=\\{ts|~{}t\in A,s\in B\\},~{}A\parr
B=\overline{\overline{A}\cdot\overline{B}},~{}A\otimes
B=\overline{\overline{A\cdot B}},\end{array}$

Proposition 7.3, clause (iii) guarantees that tensor and cotensor products of
types return types (and not just pretypes). That the the internal hom is also
a type, follows from the simple proposition below.

######  Proposition 7.6.

Let $A,B$ be types with $FI^{\bullet}(A)\cap
FI^{\bullet}(B)=FI_{\bullet}(A)\cap FI_{\bullet}(B)=\emptyset$. We have

  1. (i)

$FI(A\otimes B)=FI(A\parr B)=((FI^{\bullet}(A)\cup FI^{\bullet}(B))\setminus
X,(FI_{\bullet}(A)\cup FI_{\bullet}(B))\setminus X)$, where
$X=(FI^{\bullet}(A)\cap FI_{\bullet}(B))\cup(FI_{\bullet}(A)\cap
FI^{\bullet}(B))$;

  2. (ii)

$A\otimes B=\overline{\overline{B}\parr\overline{A}}$, $A\parr
B=\overline{\overline{B}\otimes\overline{A}}$;

  3. (iii)

$A\multimap B=\overline{A\cdot\overline{B}}=\overline{A}\parr B$. $\Box$

Note that tensor and cotensor products of types are partial operations. In
addition, they are, generally speaking, non-associative. If we have types
$A,B,C$ with $FI^{\bullet}(A)\cap FI_{\bullet}(B)\cap FI^{\bullet}(C)$
nonempty, then, as is seen from the preceding proposition, clause (i), the
types $(A\otimes B)\otimes C$ and $A\otimes(B\otimes C)$ (assuming that they
are well-defined) even have different boundaries. We will assume the
convention similar to the one assumed for iterated product of terms (in
Definition 2.7).

######  Definition 7.7.

The expression $X_{1}\otimes\ldots\otimes X_{n}$ denotes the iterated tensor
product of types satisfying the condition $FI^{\bullet}(X_{i})\cap
FI^{\bullet}(X_{j})=FI_{\bullet}(X_{i})\cap FI_{\bullet}(X_{j})=\emptyset$ for
all $i\not=j$. Similarly for cotensor product.

In the sequel, when writing tensor and cotensor products of types we will
implicitly assume that the operations are well-defined and, in the case of
iterated products, the convention from Definition 7.7 applies. This makes
expressions with iterated products unambiguous.

######  Proposition 7.8.

  1. ($i$)

If $A,B,C$ are types and the tensor/cotensor products below are defined then

$\begin{array}[]{c}A\parr(B\parr
C)=\overline{\overline{A}\cdot\overline{B}\cdot\overline{C}},\quad
A\otimes(B\otimes C)=\overline{\overline{A\cdot B\cdot C}}.\end{array}$

  2. ($ii$)

Tensor and cotensor product of types are associative whenever defined and the
convention from Definition 7.7 applies.

  3. ($iii$)

A term $t$ is in $A_{1}\parr\ldots\parr A_{n}$ iff for all

$s_{(1)}\in\overline{A_{1}},\ldots
s_{(i-1)}\in\overline{A_{i-1}},k_{(1)}\in\overline{A_{i+1}},\ldots
k_{(n-i)}\in\overline{A_{n}}$

it holds that

$ts_{(1)}\ldots s_{(i-1)}k_{(1)}\ldots k_{(n-i)}\in A_{i}.\quad\Box$

####  7.1.2 Units and reparameterization

######  Definition 7.9.

Given two indices $x,y$, $x\not=y$, the counit type $\bot^{x}_{y}$ and the
unit type ${\bf 1}^{x}_{y}$ are defined by

$\bot^{x}_{y}=\overline{\\{\delta^{y}_{x}\\}},~{}{\bf
1}^{x}_{y}=\overline{\overline{\\{\delta^{x}_{y}\\}}}.$

Given a type $A$ and indices $x\in FI^{\bullet}(A)$, $y\not\in
FI^{\bullet}(A)\cup FI_{\bullet}(A)$, we define the reparameterization
$A^{[\nicefrac{{y}}{{x}}]}$ as
$A^{[\nicefrac{{y}}{{x}}]}=\\{t^{[\nicefrac{{y}}{{x}}]}|~{}t\in A\\}$.

Similarly, if $x\in FI_{\bullet}(A)$, $y\not\in FI^{\bullet}(A)\cup
FI_{\bullet}(A)$, we define
$A_{[\nicefrac{{y}}{{x}}]}=\\{t_{[\nicefrac{{y}}{{x}}]}|~{}t\in A\\}$.

######  Proposition 7.10.

Given a type $A$ and indices $x\in FI^{\bullet}(A)$, $y\not\in
FI^{\bullet}(A)\cup FI_{\bullet}(A)$, we have

  1. (i)

$A^{[\nicefrac{{y}}{{x}}]}=\overline{\overline{A}_{[\nicefrac{{y}}{{x}}]}}$,
in particular, $A^{[\nicefrac{{y}}{{x}}]}$ is a type;

  2. (ii)

$A^{[\nicefrac{{y}}{{x}}]}=A\otimes{\bf 1}^{y}_{x}=\bot^{y}_{x}\parr A$.

Similarly, if $x\in FI_{\bullet}(A)$, $y\not\in FI^{\bullet}(A)\cup
FI_{\bullet}(A)$, we have
$A_{[\nicefrac{{y}}{{x}}]}=\overline{\overline{A}^{[\nicefrac{{y}}{{x}}]}}$
and $A_{[\nicefrac{{y}}{{x}}]}=A\otimes{\bf 1}_{y}^{x}=\bot_{y}^{x}\parr A$.

Proof

  1. (i)

Let $t\in\overline{\overline{A}_{[\nicefrac{{y}}{{x}}]}}$. Pick
$k\in\overline{A}$ and let $k^{\prime}=k_{[\nicefrac{{y}}{{x}}]}$. Then
$k^{\prime}\in\overline{A}_{[\nicefrac{{y}}{{x}}]}$ and
$tk^{\prime}\in\bot\\!\\!\\!\\!\\!\\!\bot$. Let
$t^{\prime}=t^{[\nicefrac{{x}}{{y}}]}$. From term congruence relations (3) we
have that
$t^{\prime}k=t^{\prime}k^{\prime}_{[\nicefrac{{x}}{{y}}]}=t^{[\nicefrac{{x}}{{y}}]}k^{\prime}_{[\nicefrac{{x}}{{y}}]}=tk^{\prime}$,
hence $t^{\prime}k\in\bot\\!\\!\\!\\!\\!\\!\bot$. Since $k\in\overline{A}$ was
arbitrary, we get that $t^{\prime}\in\overline{\overline{A}}=A$. But
$t=(t^{\prime})^{[\nicefrac{{y}}{{x}}]}$, so $t\in A^{[\nicefrac{{y}}{{x}}]}$.
Since $t\in\overline{\overline{A}_{[\nicefrac{{y}}{{x}}]}}$ was arbitrary we
get $\overline{\overline{A}_{[\nicefrac{{y}}{{x}}]}}\subseteq
A^{[\nicefrac{{y}}{{x}}]}$. The opposite inclusion is proven analogously.

  2. (ii)

If $x\in FI^{\bullet}(t)$ and $y$ does not occur in $t$ then
$t^{[\nicefrac{{y}}{{x}}]}=t\delta^{y}_{x}$. Hence
$A^{[\nicefrac{{y}}{{x}}]}\subseteq A\cdot{\bf 1}^{y}_{x}\subseteq
A\otimes{\bf 1}^{y}_{x}$.

If $t\in\bot^{y}_{x}\parr A$ then by Proposition 7.6, clause (iii) we have
that $\delta_{y}^{x}t\in A$. But $\delta_{y}^{x}t=t^{[\nicefrac{{x}}{{y}}]}$,
hence $t^{[\nicefrac{{x}}{{y}}]}\in A$. It follows that $t\in
A^{[\nicefrac{{y}}{{x}}]}$. Thus $\bot^{y}_{x}\parr A\subseteq
A^{[\nicefrac{{y}}{{x}}]}\subseteq A\otimes{\bf 1}^{y}_{x}$.

By the identical reasoning we get
$\overline{A}\parr\bot^{x}_{y}\subseteq\overline{A}_{[\nicefrac{{y}}{{x}}]}\subseteq{\bf
1}^{x}_{y}\otimes\overline{A}$, which yields by duality (i.e. by Proposition
7.3, clause (ii)) that $A\otimes{\bf 1}^{y}_{x}\subseteq
A^{[\nicefrac{{y}}{{x}}]}\subseteq\bot^{y}_{x}\parr A$. $\Box$

###  7.2 Interpretation

######  Definition 7.11.

Given the alphabet $\mathit{Lit}_{+}$ of (positive) literals, a tensor term
model of the tensor language (intuitionistic or classical) generated by
$\mathit{Lit}_{+}$ consists of a semantic type system
$(T,\bot\\!\\!\\!\\!\\!\\!\bot)$ and a valuation $||.||$ mapping every non-
unit atomic formula $A$ (i.e. a formula of the form $p^{i_{1}\ldots
i_{k}}_{j_{1}\ldots j_{k}}$, where $p\in\mathit{Lit}_{+}$) to a semantic type
$||A||$ with the boundary $FI(||A||)=(\\{i_{1}\ldots i_{k}\\},\\{j_{1}\ldots
j_{k}\\})$ satisfying the conditions

$\begin{array}[]{c}||A^{[\nicefrac{{i}}{{j}}]}||=||A||^{[\nicefrac{{i}}{{j}}]}\mbox{
for }j\in FI^{\bullet}(A),i\mbox{ fresh},\\\
||A_{[\nicefrac{{i}}{{j}}]}||=||A||_{[\nicefrac{{i}}{{j}}]}\mbox{ for }j\in
FI_{\bullet}(A),i\mbox{ fresh}.\end{array}$

The valuation extends to all tensor formulas (intuitionistic or classical) by

$\begin{array}[]{c}||{\bf 1}^{i}_{j}||={\bf 1}^{i}_{j},||A\otimes
B||=||A||\otimes||B||,~{}||A\multimap B||=||A||\multimap||B||,\\\
||\bot^{i}_{j}||=\bot^{i}_{j},~{}||\overline{A}||=\overline{||A||},~{}||A\parr
B||=||A||\parr||B||.\end{array}$

It is clear from the discussion in the preceding subsections (in particular,
Proposition 7.6) that the above extension of the valuation is unambiguous.

######  Definition 7.12.

A tensor sequent $A_{(1)},\ldots,A_{(n)}\vdash A$ (i,e,
$\vdash\overline{A_{(1)}},\ldots,\overline{A_{(n)}},A$ in the classical
format) is valid in the given model if one of the two equivalent condition
holds:

  1. (i)

whenever $t_{(1)}\in{||A_{(1)}||},\ldots,t_{(n)}\in{||A_{(n-1)}||}$ we get
$t_{(1)}\cdots t_{(n)}\in||A||$;

  2. (ii)

$1\in\overline{||A_{(1)}||}\parr\ldots\parr\overline{||A_{(n)}||}\parr||A||$.

The equivalence of the two above conditions follows from Proposition 7.8,
clause (iii).

######  Theorem 7.13.

A sequent derivable in TTL, respectively, ITTL is valid in any tensor term
model.

Proof For the classical case, use induction on derivation using Propositions
7.8 and 7.10. For the intuitionistic case use that the intuitionistic system
is a conservative fragment of a classical one. $\Box$

##  8 Embedded fragments

###  8.1 Propositional systems of multiplicative linear logic

######  Definition 8.1.

Given a set $\mathit{Lit}_{+}$ of positive literals the set ${Fm}$ of
classical multiplicative formulas over $\mathit{Lit}_{+}$ is built according
to the grammar $Fm::=\mathit{Lit}|(Fm\otimes Fm)|(Fm\parr Fm)$, where the set
of all literals $\mathit{Lit}=\mathit{Lit}_{+}\cup\mathit{Lit}_{-}$ is defined
same as for TTL. Duality of multiplicative formulas is defined same as for
TTL.

There are two natural systems in the multiplicative language, corresponding to
(cyclically) ordered and unordered sequents.

######  Definition 8.2.

A cyclically ordered sequence consists of a finite multiset $s$ equipped with
a binary relation $\prec$ on $s$ such that there is an enumeration
$x_{1},\ldots,x_{n}$ of elements of $s$ satisfying $x_{i}\prec x_{j}$ iff
$j=i+1(\mod n)$. We say that such an enumeration induces the cyclic ordering
of $s$.

######  Definition 8.3.

A classical multiplicative, respectively cyclic multiplicative, context is a
finite multiset, respectively cyclically ordered sequence $\Gamma$ of
classical multiplicative formulas. A classical multiplicative, respectively
cyclic multiplicative sequent is an expression of the form $\vdash\Gamma$,
where $\Gamma$ is a classical multiplicative, respectively cyclic
multiplicative, context.

The system of classical multiplicative [4], respectively cyclic multiplicative
linear logic [18] (MLL, respectively CMLL), is the set of classical
multiplicative, respectively cyclic multiplicative sequents derivable by the
rules $({\rm{Id}})$, $({\rm{Cut}})$, $(\parr)$ and $(\otimes)$ of TTL.

Lambek calculus (more precisely, Lambek calculus allowing empty antecedents
[7]) is just the intuitionistic fragment of CMLL.

######  Definition 8.4.

Given a set $\mathit{Lit}$ of literals the set ${Tp}$ of Lambek types over
$\mathit{Lit}$ is built according to the grammar $Tp::=\mathit{Lit}|(Tp\bullet
Tp)|(Tp\backslash TP)|(Tp/Tp)$. Lambek context is a finite sequence of Lambek
types, Lambek sequent is an expression of the form $\Gamma\vdash A$, where
$\Gamma$ is a Lambek context and $A$ is a Lambek type.

The translation of Lambek types to CMLL is given by

$A\bullet B=A\otimes B,~{}A\backslash B=\overline{A}\parr
B,~{}B/A=B\parr\overline{A}.$

The Lambek sequent $A_{1},\ldots,A_{n}\vdash B$ translates to CMLL as
$\vdash\overline{A_{1}},\ldots,\overline{A_{n}},B$. Lambek calculus (LC) is
the set of Lambek sequents derivable in CMLL under the above translation.

The rules of Lambek calculus (LC) that can be found, for example, in [7].

###  8.2 TTL and noncommutative logic

####  8.2.1 Embedding cyclic logic in TTL

Let the set $\mathit{Lit}_{+}$ of positive literals be given. We equip each
element $p\in\mathit{Lit}_{+}$ with valency $(1,1)$ and define a translation
from the classical multiplicative language over $\mathit{Lit}_{+}$ to the
classical tensor language over $\mathit{Lit}_{+}$, which will induce
conservative embedding of CMLL and LC.

######  Definition 8.5.

In the setting as above, the cyclic translation $||F||^{i}_{j}$ parameterized
by $i,j\in\mathit{Ind}$, where $i\not=j$, from a classical multiplicative
formula $F$ to the tensor language is defined up to renaming bound indices by
induction as

$||p||^{i}_{j}=p^{i}_{j}\mbox{ for }p\in\mathit{Lit},~{}||A\otimes
B||^{i}_{j}=||A||^{i}_{k}\otimes||B||^{k}_{j},~{}||A\parr
B||^{i}_{j}=||A||^{i}_{k}\parr||B||^{k}_{j},$ (7)

where the representatives of $||A||^{i}_{k}$ and $||B||^{k}_{j}$ are chosen so
that they have no common indices except $k$.

######  Proposition 8.6.

If a classical multiplicative sequent $\vdash A_{1},\ldots,A_{n}$, where
$n>1$, is CMLL derivable and $i_{1},\ldots,i_{n}$ are indices such that
$\Gamma=||A_{1}||^{i_{0}}_{i_{1}},||A_{2}||^{i_{1}}_{i_{2}},\ldots,||A_{n}||^{i_{n-1}}_{i_{0}}$
is a well-formed tensor context then the sequent $\vdash\Gamma$ is derivable
in TTL. If $\vdash A$ is CMLL derivable then the sequent
$\vdash\bot^{i}_{j},||A||^{j}_{i}$ is derivable in TTL.

Proof Induction on a cut-free derivation in CMLL. All steps are shown in
Figure 7. $\Box$

$\begin{array}[]{c}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
25.5pt\hbox{\vbox{\hbox{\hbox{\hskip 0.1pt\hbox{$\vdash
A_{1},\ldots,A_{m}$~{}$m>1$}\hskip 0.1pt}\hbox{\hskip 1.0pt}\hbox{\hskip
0.1pt\hbox{$\vdash B_{1},\ldots,B_{n}$~{}$n>1$}\hskip
0.1pt}}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to151.78271pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
3.0pt($\otimes$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
10.66925pt\hbox{\hbox{\hskip 0.1pt\hbox{$\vdash
A_{1},\ldots,A_{m-1},A_{m}\otimes B_{1},B_{2},\ldots,B_{n}$}\hskip
0.1pt}}}}}\ignorespaces\Longrightarrow\\\\[8.5359pt]
\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
27.85777pt\hbox{\vbox{\hbox{\hskip 34.56851pt\hbox{\hbox{\hskip
0.1pt\hbox{$\vdash||A_{1}||^{i_{0}}_{i_{1}},\ldots,||A_{m}||^{i_{m-1}}_{i_{0}}$}\hskip
0.1pt}\hbox{\hskip 1.0pt}\hbox{\hskip
0.1pt\hbox{$\vdash||B_{1}||^{i_{0}}_{i_{n}},\ldots,||B_{n}||^{i_{n+m-1}}_{i_{0}}$}\hskip
0.1pt}}}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to233.53482pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
3.0pt($\otimes$)}}\vskip-2.8pt\nointerlineskip\hbox{\hbox{\hskip
0.1pt\hbox{$\vdash||A_{1}||^{i_{0}}_{i_{1}},\ldots,||A_{m-1}||^{i_{m-2}}_{i_{m-1}},||A_{m}||^{i_{m-1}}_{i_{0}}\otimes||B_{1}||^{i_{0}}_{i_{n}},||B_{2}||^{i_{n}}_{i_{n+1}}\ldots,||B_{n}||^{i_{n+m-1}}_{i_{0}}$}\hskip
0.1pt}}}}\ignorespaces\\\\[19.91684pt]
\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
25.5pt\hbox{\vbox{\hbox{\hbox{\hskip 0.1pt\hbox{$\vdash A$}\hskip
0.1pt}\hbox{\hskip 5.0pt}\hbox{\hskip 0.1pt\hbox{$\vdash
B_{1},\ldots,B_{n}$~{}$n>1$}\hskip
0.1pt}}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to95.40033pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
3.0pt($\otimes$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
5.0733pt\hbox{\hbox{\hskip 0.1pt\hbox{$\vdash A\otimes
B_{1},\ldots,A_{n-1},A_{n}$}\hskip
0.1pt}}}}}\ignorespaces\Longrightarrow\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
52.42331pt\hbox{\vbox{\vbox{\hbox{\hskip 13.49692pt\hbox{\hbox{\hskip
0.1pt\hbox{$\vdash||A||^{i_{0}}_{j},\bot^{j}_{i_{0}}$}\hskip
0.1pt}\hbox{\hskip 5.0pt}\hbox{\hskip
0.1pt\hbox{$\vdash||B_{1}||^{j}_{i_{1}},\ldots,||B_{n}||^{i_{n-1}}_{j}$}\hskip
0.1pt}}}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to155.58363pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
3.0pt($\otimes$)}}\vskip-2.8pt\nointerlineskip\hbox{\hbox{\hskip
0.1pt\hbox{$\vdash||A||^{i_{0}}_{j}\otimes||B_{1}||^{j}_{i_{1}},||B_{2}||^{i_{1}}_{i_{2}},\ldots,||B_{n}||^{i_{n-1}}_{j},\bot^{j}_{i_{0}}$}\hskip
0.1pt}}}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to155.58363pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
3.0pt($\bot\leftarrow$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
6.59113pt\hbox{\hbox{\hskip
0.1pt\hbox{$\vdash||A||^{i_{0}}_{j}\otimes||B_{1}||^{j}_{i_{1}},||B_{2}||^{i_{1}}_{i_{2}},\ldots,||B_{n}||^{i_{n-1}}_{i_{0}}$}\hskip
0.1pt}}}}}\ignorespaces\\\\[19.91684pt]
\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
24.88889pt\hbox{\vbox{\hbox{\hbox{\hskip 0.1pt\hbox{$\vdash A$}\hskip
0.1pt}\hbox{\hskip 14.45377pt}\hbox{\hskip 0.1pt\hbox{$\vdash B$}\hskip
0.1pt}}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to48.21826pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
3.0pt($\otimes$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
5.66023pt\hbox{\hbox{\hskip 0.1pt\hbox{$\vdash A\otimes B$}\hskip
0.1pt}}}}}\ignorespaces\Longrightarrow\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
52.56998pt\hbox{\vbox{\vbox{\hbox{\hbox{\hskip
0.1pt\hbox{$\vdash||A||^{j}_{k},\bot^{k}_{j}$}\hskip 0.1pt}\hbox{\hskip
14.45377pt}\hbox{\hskip 0.1pt\hbox{$\vdash||B||^{k}_{i},\bot^{i}_{k}$}\hskip
0.1pt}}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to105.62425pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
3.0pt($\otimes$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
6.49355pt\hbox{\hbox{\hskip
0.1pt\hbox{$\vdash||A||^{j}_{k}\otimes||B||^{k}_{i},\bot^{k}_{j},\bot^{i}_{k}$}\hskip
0.1pt}}}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
6.49355pt\lower-0.2pt\hbox{}\hbox to92.63716pt{\xleaders\hrule\hfill}\lower
2.3pt\hbox{\hskip
3.0pt($\bot\leftarrow$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
12.96846pt\hbox{\hbox{\hskip
0.1pt\hbox{$\vdash||A||^{j}_{k}\otimes||B||^{k}_{i},\bot_{j}^{i}$}\hskip
0.1pt}}}}}\ignorespaces\end{array}$

(a)

$\begin{array}[]{c}\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
25.5pt\hbox{\vbox{\hbox{\hskip 8.45216pt\hbox{\hskip 0.1pt\hbox{$\vdash
A_{1},\ldots,A_{n}$~{}$n>2$}\hskip
0.1pt}}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to89.54222pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
3.0pt($\parr$)}}\vskip-2.8pt\nointerlineskip\hbox{\hbox{\hskip
0.1pt\hbox{$\vdash A_{1},\ldots,A_{n-2},A_{n-1}\parr A_{n}$}\hskip
0.1pt}}}}\ignorespaces\Longrightarrow\\\\[8.5359pt]
\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
27.72444pt\hbox{\vbox{\hbox{\hskip 22.22371pt\hbox{\hskip
0.1pt\hbox{$\vdash||A_{1}||^{i_{0}}_{i_{1}},\ldots,||A_{n-1}||^{i_{n-2}}_{i_{n-1}},||A_{n}||^{i_{n-1}}_{i_{0}}$}\hskip
0.1pt}}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to159.84386pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
3.0pt($\parr$)}}\vskip-2.8pt\nointerlineskip\hbox{\hbox{\hskip
0.1pt\hbox{$\vdash||A_{1}||^{i_{0}}_{i_{1}},\ldots,||A_{n-2}||^{i_{n-3}}_{i_{n-2}},||A_{n-1}||^{i_{n-2}}_{i_{n-1}}\parr||A_{n}||^{i_{n-1}}_{i_{0}}$}\hskip
0.1pt}}}}\ignorespaces\\\\[19.91684pt]
\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
24.47221pt\hbox{\vbox{\hbox{\hskip 2.31252pt\hbox{\hskip 0.1pt\hbox{$\vdash
A,B$}\hskip 0.1pt}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox to33.74509pt{\xleaders\hrule\hfill}\lower
2.3pt\hbox{\hskip
3.0pt($\parr$)}}\vskip-2.8pt\nointerlineskip\hbox{\hbox{\hskip
0.1pt\hbox{$\vdash A\parr B$}\hskip
0.1pt}}}}\ignorespaces\Longrightarrow\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
51.87999pt\hbox{\vbox{\hbox{\hskip 3.14581pt\vbox{\hbox{\hskip
6.59114pt\hbox{\hskip 0.1pt\hbox{$\vdash||A||^{i}_{k},||B||^{k}_{i}$}\hskip
0.1pt}}\vskip-3.52245pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox to73.9899pt{\xleaders\hrule\hfill}\lower
3.02245pt\hbox{\hskip
3.0pt($\bot^{\to}$)}}\vskip-3.52245pt\nointerlineskip\hbox{\hbox{\hskip
0.1pt\hbox{$\vdash\bot^{i}_{j},||A||^{j}_{k},||B||^{k}_{i}$}\hskip
0.1pt}}}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox to80.28154pt{\xleaders\hrule\hfill}\lower
2.3pt\hbox{\hskip
3.0pt($\parr$)}}\vskip-2.8pt\nointerlineskip\hbox{\hbox{\hskip
0.1pt\hbox{$\vdash\bot^{i}_{j},||A||^{j}_{k}\parr||B||^{k}_{i}$}\hskip
0.1pt}}}}\ignorespaces\end{array}$

(b)

Figure 7: Translating CMLL derivations

######  Definition 8.7.

A tensor formula is cyclic if it is in the image of translation (7). The
cyclic fragment of TTL consists of sequents all whose formulas are cyclic. The
extended cyclic fragment of TTL consists of sequents all whose formulas are
cyclic or counits $\bot^{i}_{j}$.

######  Definition 8.8.

For a tensor sequent $\vdash\Gamma$ in the extended cyclic fragment we define
the neighboring relation $\prec$ between formulas of $\Gamma$ by $A\prec B$
iff $FI_{\bullet}(A)=FI^{\bullet}(B)$.

######  Lemma 8.9.

For any TTL derivable sequent in the extended cyclic fragment the neighboring
relation is a cyclic ordering.

Proof Induction on a cut-free derivation. As an illustration consider the
induction step corresponding to the $(\otimes)$ rule.

Let the sequent $\vdash\Theta$ of the form $\vdash\Gamma,A\otimes B,\Delta$ in
the extended cyclic fragment be obtained from TTL derivable sequents
$\vdash\Theta_{1}$, $\vdash\Theta_{2}$ of the form $\vdash\Gamma,A$, $\vdash
B,\Delta$ respectively by the $(\otimes)$ rule.

By the induction hypothesis we have enumerations of $\Theta_{1}$ and
$\Theta_{2}$, respectively $A_{(1)},\ldots,A_{(n)},A$ and
$B,B_{(1)},\ldots,B_{(m)}$, that induce the respective neighboring relations.
In particular, we have $FI_{\bullet}(A_{(i)})=FI^{\bullet}(A_{(i+1)})$ for
$i<n$, $FI_{\bullet}(A_{(n)})=FI^{\bullet}(A)$,
$FI_{\bullet}(A)=FI^{\bullet}(A_{(1)})$ and similarly
$FI_{\bullet}(B_{(i)})=FI^{\bullet}(B_{(i+1)})$ for $i<m$,
$FI_{\bullet}(B_{(m)})=FI^{\bullet}(B)$,
$FI_{\bullet}(B)=FI^{\bullet}(B_{(1)})$.

Now $A\otimes B$ must be a cyclic formula, which means
$FI_{\bullet}(A)=FI^{\bullet}(B)$. Then we compute $FI_{\bullet}(A\otimes
B)=FI_{\bullet}(B)=FI^{\bullet}(B_{(1)})$ and $FI^{\bullet}(A\otimes
B)=FI^{\bullet}(A)=FI_{\bullet}(A_{(n)})$. Finally
$FI_{\bullet}(B_{m})=FI^{\bullet}(B)=FI_{\bullet}(A)=FI^{\bullet}(A_{(1)})$.

It follows that the neighboring relation on $\Gamma,A\otimes B,\Delta$
coincides with the cyclic ordering induced by the enumeration
$A_{(1)},\ldots,A_{(n)},A\otimes B,B_{(1)},\ldots,B_{(m)}$. $\Box$

######  Proposition 8.10.

Let $\vdash\Gamma$ be a TTL derivable sequent in the extended cyclic fragment,
and let $A_{(1)},\ldots A_{(n)}$ be an enumeration of formulas in $\Gamma$
inducing the neighboring relation. Let the cyclic sequent
$\vdash\Gamma^{\prime}$ be obtained from the expression $\vdash A_{(1)},\ldots
A_{(n)}$ by erasing all indices and all counits. Then $\vdash\Gamma^{\prime}$
is derivable in CMLL.

Proof Induction on a cut-free derivation of $\vdash\Gamma$. $\Box$

######  Corollary 8.11.

The cyclic translation is conservative. The CMLL sequent $\vdash
A_{1},\ldots,A_{n}$, where $n>1$, is derivable (in CMLL) iff for some (hence
any) array of indices $i_{1},\ldots,i_{n}$ such that
$\Gamma=||A_{1}||^{i_{1}}_{i_{2}},||A_{2}||^{i_{2}}_{i_{3}},\ldots,||A_{n}||^{i_{n}}_{i_{1}}$
is a well-formed tensor context the sequent $\vdash\Gamma$ is derivable in
TTL. The CMLL sequent $\vdash A$ is derivable in CMLL of the sequent
$\vdash\bot^{i}_{j},||A||^{j}_{i}$ is derivable in TTL. $\Box$

####  8.2.2 Embedding Lambek calculus

Given that LC is a conservative fragment of CMLL and ITTL is a conservative
fragment of TTL, the embedding of CMLL into TTL induces the embedding of LC
into ITTL. As in the case of CMLL, we equip each literal $p\in\mathit{Lit}$
with valency $(1,1)$ and define a translation from the language of LC over
$\mathit{Lit}$ to the intuitionistic tensor language over $\mathit{Lit}$.

######  Definition 8.12.

In the setting as above, the translation $||F||^{i}_{j}$ parameterized by
$i,j\in\mathit{Ind}$, where $i\not=j$, from a Lambek type $F$ to the
intuitionistic tensor language is defined up to renaming bound indices by
induction as

$\begin{array}[]{rl}||p||^{i}_{j}=p^{i}_{j},&||A\bullet
B||^{i}_{j}=||A||^{i}_{k}\otimes||B||^{k}_{j},\\\ ||A\backslash
B||^{i}_{j}=||A||^{k}_{i}\multimap||B||^{k}_{j},&||B/A||^{i}_{j}=||A||_{k}^{j}\multimap||B||_{k}^{i},\end{array}$

where the representatives in every pair $(||A||^{i}_{k},||B||^{k}_{j})$,
$(||A||^{k}_{i},||B||^{k}_{j},)$, $(||A||_{k}^{j},||B||_{k}^{i})$ are chosen
so that they have no common indices except $k$.

Conservativity of LC in CMLL and ITTL in TTL (together with the provable
equivalence
$\overline{||A||_{k}^{j}}\parr||B||_{k}^{i}\cong||B||_{k}^{i}\parr\overline{||A||_{k}^{j}})$
immediately yield the following corollary from Corollary 8.11

######  Corollary 8.13.

The LC sequent $A_{1},\ldots,A_{n}\vdash A$, where $n>0$, is derivable (in LC)
iff for some (hence any) array of indices $i_{1},\ldots,i_{n}$ such that
$\Gamma=||A_{1}||^{i_{0}}_{i_{1}},\ldots,||A_{n}||^{i_{n-1}}_{i_{n}}$ is a
well-formed intuitionistic tensor context the sequent
$\Gamma\vdash||A||^{i_{0}}_{i_{n}}$ is derivable in ITTL. The sequent $\vdash
A$ is derivable in LC iff ${\bf 1}^{i}_{j}\vdash||A||^{i}_{j}$ is derivable in
ITTL. $\Box$

######  Remark 8.14.

Comparing the above translation from LC to ITTL with formulas (1) giving the
translation from LC to MILL1 suggests that ITTL could itself be translated to
MILL1, with indices becoming first order variables and bound indices
corresponding to variables bound by a quantifier, according to the informal
scheme

$A^{i}\otimes B_{i}\mapsto\exists i(A(i)\otimes B(i)),~{}A^{i}\multimap
B^{i}\mapsto\forall i(A(i)\multimap B(i)).$

As for the propositional constant ${\bf 1}$, the ITTL formula ${\bf
1}^{i}_{j}$ behaves much like the equality $(i=j)$, so one might attempt a
translation into the first order language with equality.

We note however that such a translation could not be conservative. Indeed, the
sequent $\vdash(A^{i}_{j}\multimap A^{i}_{k})\otimes(A^{l}_{k}\multimap
A^{l}_{j})$, which is underivable in ITTL (see Remark 3.6), should translate
as $\vdash\exists k\exists j(\forall i(A(i,j)\multimap A(i,k))\otimes\forall
l(A(l,k)\multimap A(l,j)))$, and the latter is MILL1 derivable. It seems that
in order to have a direct relation with MILL1 we need to consider tensor terms
with congruence (4) added to the definition (see Remarks 2.6, 3.6).

###  8.3 TTL and MLL

####  8.3.1 MLL-like fragment

######  Definition 8.15.

A tensor formula is MLL-like if it does not involve units ${\bf 1}^{i}_{j}$ or
counits $\bot^{i}_{j}$ and has no bound indices. The MLL-like fragment of TTL
consists of sequents all whose formulas are MLL-like.

######  Proposition 8.16.

If an MLL-like sequent $\vdash\Gamma$ is derivable in TTL then it is derivable
not using the $(\bot_{\leftarrow})$ and the $(\bot^{\to})$ rules.

Proof By Corollary 6.4, if $\vdash\Gamma$ has a derivation in TTL then it has
a cut-free derivation where all applications of the $(\bot_{\leftarrow})$ rule
are essential. But a cut-free derivation of $\vdash\Gamma$ involves only
subformulas of $\Gamma$ and, possibly, counits, and these have no bound
indices. Without bound indices we cannot have essential applications of the
$(\bot_{\leftarrow})$ rule, hence there are no $(\bot_{\leftarrow})$ rules at
all. Now, $\vdash\Gamma$ does not contain counits, and since the derivation is
cut-free and does not use the $(\bot_{\leftarrow})$ rule, it does not use the
$(\bot^{\to})$ rule, which introduces counits, either. $\Box$

We see that the MLL-like fragment uses only rules of MLL, which suggests that
the above fragment and the system of MLL should be translatable to each other.
And indeed there exists a translation from MLL to the MLL-like fragment,
however the input of the translation is not a provable MLL sequent, but a
pair: an MLL sequent together with its derivation. “Morally” the situation is
as follows. Given an MLL sequent $\vdash\Gamma$, we try to decorate it with
indices to obtain a TTL derivable sequent from the MLL-like fragment.
Different successful decorations of $\vdash\Gamma$ correspond to its different
derivations in MLL (more precisely, to different proof-nets).

####  8.3.2 Embedding MLL derivations

In this section we will follow notational conventions of Section 5, where we
used capital Latin letters for sequences of indices. Also, we will write
$\bot^{I}_{J}$ for the context
$\bot^{i_{1}}_{j_{1}},\ldots,\bot^{i_{n}}_{j_{n}}$, where
$I=i_{1},\ldots,i_{n}$, $J=j_{1},\ldots,j_{n}$.

We assume that we are given the alphabet $\mathit{Lit}_{+}$ of positive
literals generating a classical multiplicative language, and that elements of
$\mathit{Lit}_{+}$ are, furthermore, assigned valencies so that they generate
a classical tensor language as well.

######  Definition 8.17.

For an MLL sequent $\Pi$ of the form $\vdash A_{1}\ldots A_{n}$ together with
a derivation $\pi$ of $\Pi$ the TTL representation of the pair $(\Pi,\pi)$ is
a TTL derivable tensor sequent $||(\Pi,\pi)||$ of the form
$\vdash||A_{1}||^{\pi},\ldots,||A_{n}||^{\pi}$, where each tensor formula
$||A_{i}||^{\pi}$ is $A_{i}$ decorated with some indices, defined up to
similarity of tensor sequents by induction on $\pi$ as follows.

  1. (i)

If $\pi$ is an axiom and $\Pi$ has the form $\vdash\overline{p},p$, where
$v(p)=(m,n)$, choose two sequences of pairwise distinct indices
$I=i_{1},\ldots,i_{m}$, $J=j_{1},\ldots,j_{m}$, $I\cap J=\emptyset$ and put
$||p||^{\pi}=p^{I}_{J}$, $||\overline{p}||^{\pi}=\overline{||p||^{\pi}}$. The
obtained sequent is an instance of the $({\rm{Id}})$ axiom of TTL.

  2. (ii)

If $\Pi$ has the form $\vdash\Gamma,A\parr B$ and $\pi$ is obtained from a
derivation $\pi^{\prime}$ of the sequent $\Pi^{\prime}$ having the form
$\vdash\Gamma,A,B$ by the $(\parr)$ rule, put
$||F||^{\pi}=||F||^{\pi^{\prime}}$ for $F\in\Gamma$ and $||A\parr
B||^{\pi}=||A||^{\pi^{\prime}}\parr||B||^{\pi^{\prime}}$. The sequent
$||(\Pi,\pi)||$ is derivable from $||(\Pi^{\prime},\pi^{\prime})||$ by the
$(\parr)$ rule.

  3. (iii)

If $\Pi$ has the form $\vdash\Gamma,A\otimes B,\Delta$ and $\pi$ is obtained
from derivations $\pi_{1}$, $\pi_{2}$ with the conclusions $\Pi_{1}$,
$\Pi_{2}$ of the form $\vdash\Gamma,A$, $\vdash B,\Delta$ respectively by the
$(\otimes)$ rule, choose representatives of $||(\Pi_{1}\pi_{1})||$ and
$||(\Pi_{2},\pi_{2})||$ that have no indices in common and put
$||F||^{\pi}=||F||^{\pi_{1}}$ for $F\in\Gamma$, $||F||^{\pi}=||F||^{\pi_{2}}$
for $F\in\Delta$ and $||A\otimes
B||^{\pi}=||A||^{\pi_{1}}\otimes||B||^{\pi_{2}}$. The sequent $||(\Pi,\pi)||$
is derivable from $||(\Pi_{1},\pi_{1})||$ and $||(\pi_{2},\pi_{2})||$ by the
$(\otimes)$ rule.

  4. (iv)

If $\Pi$ has the form $\vdash\Gamma,\Delta$ and $\pi$ is obtained from
derivations $\pi_{1}$, $\pi_{2}$ with the conclusions $\Pi_{1}$, $\Pi_{2}$ of
the form $\vdash\Gamma,A$, $\vdash\overline{A},\Delta$ respectively by the Cut
rule, choose representatives of $||(\Pi_{1},\pi_{1})||$ and
$||(\Pi_{2},\pi_{2})||$ that have no indices in common. Let
$FI(||A||^{\pi_{1}})=(I,J)$ and $FI(||\overline{A}||^{\pi_{2}})=(K,L)$. Put
$||F||^{\pi}=(||F||^{\pi_{1}})_{[\nicefrac{{L}}{{I}}]}$ for $F\in\Gamma$,
$||F||^{\pi}=(||F||^{\pi_{2}})_{[\nicefrac{{J}}{{K}}]}$ for $F\in\Delta$. The
sequent $||\pi||$ is derivable from $||\pi_{1}||$ and $||\pi_{2}||$ by a
combination of the rules $(\bot^{\to})$, Cut and $(\bot_{\leftarrow})$ as
shown in Figure 8.

$\begin{array}[]{c}FI(||A||^{\pi_{1}})=(I,J),~{}FI(||\overline{A}||^{\pi_{2}})=(K,L)\\\
\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
146.38167pt\hbox{\vbox{\vbox{\vbox{\hbox{\vbox{\hbox{\hskip
15.40334pt\vbox{\hbox{\hskip
0.1pt\hbox{$\vdash||\Gamma||^{\pi_{1}},||A||^{\pi_{1}}$}\hskip 0.1pt}\vskip
2.47755pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to63.5342pt{\xleaders\hrule\hfill}\lower 3.02245pt\hbox{\hskip
3.0pt($\bot^{\to}$)}}\vskip 2.47755pt\nointerlineskip\hbox{\hskip
27.91708pt\hbox{\hbox{\hskip 0.1pt\hbox{$\cdots$}\hskip
0.1pt}}}}}\vskip-2.52245pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox to94.34085pt{\xleaders\hrule\hfill}\lower
3.02245pt\hbox{\hskip
3.0pt($\bot^{\to}$)}}\vskip-2.52245pt\nointerlineskip\hbox{\hbox{\hskip
0.1pt\hbox{$\vdash||\Gamma||^{\pi_{1}},\bot^{I}_{L},(||A||^{\pi_{1}})^{[\nicefrac{{L}}{{I}}]}$}\hskip
0.1pt}}}\hbox{\hskip 14.45377pt}\vbox{\hbox{\hskip 0.55554pt\vbox{\hbox{\hskip
17.27695pt\vbox{\hbox{\hskip
0.1pt\hbox{$\vdash||\overline{A}||^{\pi_{2}},||\Delta||^{\pi_{2}}$}\hskip
0.1pt}\vskip-3.52245pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox to58.6732pt{\xleaders\hrule\hfill}\lower
3.02245pt\hbox{\hskip
3.0pt($\bot^{\to}$)}}\vskip-3.52245pt\nointerlineskip\hbox{\hskip
25.48659pt\hbox{\hbox{\hskip 0.1pt\hbox{$\cdots$}\hskip
0.1pt}}}}}\vskip-3.52245pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox to93.22708pt{\xleaders\hrule\hfill}\lower
3.02245pt\hbox{\hskip
3.0pt($\bot^{\to}$)}}\vskip-3.52245pt\nointerlineskip\hbox{\hbox{\hskip
0.1pt\hbox{$\vdash\bot^{K}_{J},(||\overline{A}||^{\pi_{2}})^{[\nicefrac{{J}}{{K}}]},||\Delta||^{\pi_{2}}$}\hskip
0.1pt}}}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox to94.33817pt{\xleaders\hrule\hfill}\lower
2.3pt\hbox{\hskip
3.0pt(${\rm{Ex}}$)}}\vskip-2.8pt\nointerlineskip\hbox{\hbox{\hskip
0.1pt\hbox{$\vdash(||\overline{A}||^{\pi_{2}})^{[\nicefrac{{J}}{{K}}]},\bot^{K}_{J},||\Delta||^{\pi_{2}}$}\hskip
0.1pt}}}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox to224.48839pt{\xleaders\hrule\hfill}\lower
2.3pt\hbox{\hskip
3.0pt(${\rm{Cut}}$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
65.47595pt\hbox{\hbox{\hskip
0.1pt\hbox{$\vdash||\Gamma||^{\pi_{1}},\bot^{I}_{L},\bot^{K}_{J},||\Delta||^{\pi_{2}}$}\hskip
0.1pt}}}}\vskip-0.8pt\nointerlineskip\hbox{\hskip
65.47595pt\lower-0.2pt\hbox{}\hbox to93.53647pt{\xleaders\hrule\hfill}\lower
2.3pt\hbox{\hskip
3.0pt($\bot_{\leftarrow}$)}}\vskip-0.8pt\nointerlineskip\hbox{\hskip
108.39418pt\hbox{\hbox{\hskip 0.1pt\hbox{$\cdots$}\hskip
0.1pt}}}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
61.40907pt\lower-0.2pt\hbox{}\hbox to101.67023pt{\xleaders\hrule\hfill}\lower
2.3pt\hbox{\hskip
3.0pt($\bot_{\leftarrow}$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
61.40907pt\hbox{\hbox{\hskip
0.1pt\hbox{$\vdash(||\Gamma||^{\pi_{1}})_{[\nicefrac{{L}}{{I}}]},(||\Delta||^{\pi_{2}})_{[\nicefrac{{J}}{{K}}]}$}\hskip
0.1pt}}}}}\ignorespaces\end{array}$

Figure 8: Translating MLL cut to TTL

######  Proposition 8.18.

TTL translation of MLL is an invariant of cut-elimination. If an MLL
derivation $\pi^{\prime}$ of a sequent $\Pi$ is obtained from the derivation
$\pi$ by cut-elimination then $||(\Pi,\pi)||$ and $||(\Pi,\pi^{\prime})||$
coincide.

Proof Induction on the cut-elimination algorithm for MLL. $\Box$

######  Theorem 8.19.

Every TTL derivable sequent $\vdash\Gamma$ from the MLL-like fragment is the
translation of an MLL sequent with a chosen derivation.

Proof Induction on a cut-free derivation of $\vdash\Gamma$ not using the
$(\bot_{\leftarrow})$ and $(\bot^{\to})$ rules. $\Box$

It is quite obvious that we can restrict the above construction to the
intuitionistic fragment of MLL and obtain a translation to ITTL. Now we note
that, in the intuitionistic setting, the inputs of our translation, i.e.
sequents equipped with chosen derivations, canonically correspond via the
Curry-Howard isomorphism to $\lambda$-calculus typing judgements, and it is
precisely $\lambda$-calculus typing judgements that play the main role in the
“commutative” categorial grammars, i.e. ACG. On one hand, this suggests that,
as far as categorial grammars are concerned, the input of the translation is
chosen correctly. On the other hand this leads to the question of representing
ACG in ITTL. We leave this question to future research.

##  9 Grammars

###  9.1 Typing judgements and grammars

######  Definition 9.1.

A classical, respectively intuitionistic typing judgement is an expression of
the form $t\rhd A$, where $t$ is a term and $A$ is a classical, respectively
intuitionistic formula with the same boundary: $FI(t)=FI(A)$. The typing
judgement is regular, respectively lexical, if the term $t$ is regular,
respectively lexical. A typing judgement of the form $\delta^{i}_{j}\rhd{\bf
1}^{i}_{j}$ is a typing axiom. The set of all typing axioms is denoted as
$\mathit{TpAx}$.

The intended semantics of the typing judgement $t\rhd A$ is that $t\in||A||$.
With such a semantics, typing axioms are always valid, and this explains the
title “axiom”.

######  Definition 9.2.

A classical, respectively intuitionistic, tensor grammar $G$ is a pair
$G=(\mathit{Lex},S)$, where $\mathit{Lex}$, the lexicon of $G$, is a set of
classical, respectively intuitionistic, regular lexical typing judgements,
called axioms of $G$ or axioms of $\mathit{Lex}$, and $S$, the sentence type
symbol, is a positive literal of valency $(1,1)$.

A typing judgement $t\rhd A$ is derivable in $G$, notation $t\rhd_{G}A$, if
there exist axioms $t_{(1)}\rhd A_{(1)},\ldots,t_{(n)}\rhd A_{(n)}$ of
$\mathit{Lex}\cup\mathit{TpAx}$ such that $t=t_{(1)}\cdots t_{(n)}$ and the
sequent $A_{(1)},\ldots A_{(n)}\vdash A$ (i.e., in the classical case,
$\vdash\overline{A_{(1)}},\ldots\overline{A_{(n)}},A$) is derivable in TTL,
respectively ITTL. (The number $n$ may equal zero, which means that $t=1$ and
the sequent $\vdash A$ is derivable in TTL, respectively ITTL. )

The language $L(G)$ generated by $G$ or, simply, the language $L(G)$ of $G$ is
the set $L(G)=\\{w\in T^{*}|~{}[w]^{i}_{j}\rhd_{G}S^{i}_{j}\\}$.

Typing judgements can be understood as a special kind of sequents and grammars
as systems of nonlogical axioms (this will be discussed shortly below). In
particular, we can define $\alpha$-equivalence of typing judgements.

######  Definition 9.3.

$\alpha$-Equivalence of typing judgements is generated by the following
relations:

$\begin{array}[]{c}A\equiv_{\alpha}B\Rightarrow(t\rhd A)\equiv_{\alpha}(t\rhd
B),\\\ j\in FI^{\bullet}(t),i\mbox{
fresh}\Rightarrow(t^{[\nicefrac{{i}}{{j}}]}\rhd
A^{[\nicefrac{{i}}{{j}}]})\equiv_{\alpha}(t\rhd A)\\\ j\in
FI_{\bullet}(t),i\mbox{ fresh}\Rightarrow(t_{[\nicefrac{{i}}{{j}}]}\rhd
A_{[\nicefrac{{i}}{{j}}]})\equiv_{\alpha}(t\rhd A).\end{array}$

######  Proposition 9.4.

The set of typing judgements derivable in a given tensor grammar $G$
(intuitionistic or classical) is closed under $\alpha$-equivalence.

Proof We will discuss the classical case.

The proof is by induction on the definition of $\alpha$-equivalence. We will
discuss one step. Let $\mathit{Lex}$ be the lexicon of $G$ and assume, for
example, that $t\rhd_{G}A$, $j\in FI^{\bullet}(A)$, $i$ is fresh and
$t^{\prime}=t^{[\nicefrac{{i}}{{j}}]}$,
$A^{\prime}=A^{[\nicefrac{{i}}{{j}}]}$. We need to show that
$t^{\prime}\rhd_{G}A^{\prime}$.

By definition, we have axioms $t_{(1)}\rhd A_{(1)},\ldots,t_{(n)}\rhd A_{(n)}$
in $\mathit{Lex}\cup\mathit{TpAx}$ such that $t=t_{(1)}\ldots t_{(n)}$ and the
sequent $\vdash\overline{A_{(1)}},\ldots,\overline{A_{(n)}},A$ is derivable in
TTL.

By the $(\bot^{\to})$ rule we get that the sequent
$\vdash\overline{A_{(1)}},\ldots,\overline{A_{(n)}},\bot_{i}^{j},A^{\prime}$
is derivable in TTL as well. Also we have
$t^{\prime}=t\delta^{i}_{j}=t_{(1)}\ldots t_{(n)}\delta^{i}_{j}$. Put
$t_{(n+1)}=\delta^{i}_{j}$, $A_{(n+1)}={\bf 1}^{i}_{j}$. Then $t_{(n+1)}\rhd
A_{(n+1)}$ is a typing axiom and we get the list $t_{(1)}\rhd
A_{(1)},\ldots,t_{(n+1)}\rhd A_{(n+1)}$ in $\mathit{Lex}\cup\mathit{TpAx}$
such that $t^{\prime}=t_{(1)}\ldots t_{(n+1)}$ and the sequent
$\vdash\overline{A_{(1)}},\ldots,\overline{A_{(n+1)}},A^{\prime}$ is derivable
in TTL. Which means exactly that $t^{\prime}\rhd_{G}A^{\prime}$. $\Box$

######  Proposition 9.5.

Let $G$ be a tensor grammar and assume that $t\rhd_{G}A$. Let $G^{\prime}$ be
the grammar obtained from $G$ by adding the typing judgement $t\rhd A$ to the
lexicon. Then $G^{\prime}$ has the same set of derivable typing judgements as
$G$. $\Box$

The two preceding propositions imply that we may always assume that the
lexicon of a tensor grammar is closed under $\alpha$-equivalence, and this
will be our convention in the following. Prior to giving an example of a
tensor grammar we will discuss a convenient representation of those as systems
of sequents, non-logical axioms, in the extended tensor formula language where
terminal symbols are treated as additional literals.

###  9.2 Typing judgements as sequents

######  Definition 9.6.

Given a set $\mathit{Lit}_{+}$ of positive literals with assigned valencies
and a terminal alphabet $T$, the extended tensor language is the tensor
language (respectively intuitionistic or classical) generated by
$\mathit{Lit}_{+}\cup T$, where every element of $T$ is assigned valency
$(1,1)$. The subset of the extended language not using terminal symbols (i.e.
generated by $\mathit{Lit}_{+}$) is the base language.

When writing formulas and sequents in the extended language, it will be
convenient to distinguish notationally terminal symbols and formulas of the
base language. When using an element $a\in T$ as a literal in the extended
language we will write it in boldface as ${\bf a}$.

The extended language allows representing terms over $T$ as formulas and
typing judgements as sequents. Typically, “atomic” terms of the form
$[a]^{i}_{j}$ can be seen as atomic formulas of the form ${\bf a}^{i}_{j}$,
the Kronecker delta $\delta^{i}_{j}$ correspond to the unit ${\bf 1}^{i}_{j}$
and the product of terms corresponds to the tensor product of formulas. For
the proof-theoretic analysis, however, it is more convenient to represent
terms not as formulas, but as tensor contexts in the extended language.

######  Definition 9.7.

The map $\mathit{ct}$ from well-formed pseudo-terms to classical tensor
contexts in the extended language is partially defined by the following
induction:

$\mathit{ct}(1)=\emptyset,\mathit{ct}([a]^{i}_{j})={\bf\overline{a}}_{i}^{j}\mbox{
for }a\in T,~{}\mathit{ct}(\delta^{i}_{j})=\bot^{j}_{i},~{}\mathit{ct}(t\cdot
s)=\mathit{ct}(t),\mathit{ct}(s).$

######  Proposition 9.8.

For every term $t$ over $T$ there exists a well-formed pseudo-term $\tau$
representing $t$ such that $\mathit{ct}(\tau)$ is defined.

Proof This follows from the fact that every term can be represented as the
product of elementary regular terms of the form $[a]^{i}_{j}$ or
$\delta^{i}_{j}$, $i\not=j$.

For the elementary regular term $t=[a_{1}\ldots a_{n}]^{i}_{j}$, where
$a_{1},\ldots,a_{n}\in T$ $n>0$, we have
$t=[a_{1}]^{i}_{i_{1}}\cdots[a_{n}]^{i_{n-1}}_{j}$, where
$i,i_{1},\ldots,i_{n-1},j$ are pairwise distinct.

For the elementary singular term $t=[\epsilon]$ we have
$t={\delta}^{i}_{j}{\delta}^{j}_{i}$, where $i\not=j$, and for $t=[a]$, where
$a\in T$, we have $t=\delta^{j}_{i}[a]^{i}_{j}$. For the elementary singular
term $t=[a_{1}\ldots a_{n}]$, where $a_{1},\ldots,a_{n}\in T$ and $n>1$, we
have $t=[a_{1}]^{i}_{i_{1}},\cdots,[a_{n}]^{i_{n-1}}_{i}$, where
$i,i_{1},\ldots,i_{n-1},$ are pairwise distinct.

For non-elementary terms the statement follows from the above. $\Box$

######  Proposition 9.9.

If $t,t^{\prime}$ are well-formed pseudo-terms and $t\equiv t^{\prime}$ then
the contexts $\mathit{ct}(t)$ and $\mathit{ct}(t^{\prime})$ are equivalent in
the sense that for any context $\Gamma$ the sequents
$\vdash\mathit{ct}(t),\Gamma$ and $\vdash\mathit{ct}(t^{\prime}),\Gamma$ are
TTL derivable from each other.

Proof Induction on the definition of term equality (i.e. well-formed pseudo-
term congruence) using that the context
${\bf\overline{a}}^{i}_{j},{\bf\overline{b}}^{j}_{k}$ is equivalent to
${\bf\overline{a}}^{i}_{j^{\prime}},{\bf\overline{b}}^{j^{\prime}}_{k}$ and
${\bf\overline{a}}^{i}_{j}$ is equivalent to
${\bf\overline{a}}^{i}_{k},\bot^{k}_{j}$ and to
$\bot^{i}_{k},{\bf\overline{a}}^{k}_{j}$. $\Box$

The two preceding propositions imply that the map $\mathit{ct}$ induces a
well-defined map from terms to equivalence classes of contexts.

######  Definition 9.10.

For a tensor term $t$ the notation $\overline{\bf t}$ stands for the context
$\mathit{ct}(\tau)$, where $\tau$ is any well-formed pseudo-term representing
$t$. Similarly, the notation ${\bf t}$ stands for the context
$\overline{\mathit{ct}(\tau)}$. For the classical, respectively intuitionistic
typing judgement $t\rhd A$, its classical, respectively intuitionistic sequent
encoding is the sequent $\vdash\overline{\bf t},A$, respectively ${\bf
t}\vdash A$.

The above definition is, strictly speaking, ambiguous, because the sequent
$\vdash\overline{\bf t},A$, respectively ${\bf t}\vdash A$, depends on the
pseudo-term representing $t$. But by Proposition 9.9, different
representations of $t$ give rise to equivalent sequents.

###  9.3 Derivations of typing judgements

######  Definition 9.11.

A lexical sequent is a sequent in the (classical) extended language of the
form $\vdash\overline{\bf t},A$, where $A$ is a formula in the base language,
$t$ is a lexical term and the representative of $\overline{\bf t}$ is a
context consisting of formulas of the form $\overline{\bf a}^{i}_{j}$, where
$a\in T$ (i.e. it does not contain counits $\bot^{i}_{j}$). A sequent lexicon
is a set of lexical sequents closed under $\alpha$-equivalence.

Obviously, lexical sequents represent lexical typing judgements and the
lexicon of a tensor grammar gives rise to a sequent lexicon. (Remember our
convention that lexicons of tensor grammars are closed under
$\alpha$-equivalence.)

######  Proposition 9.12.

Let $\Xi$ be a sequent lexicon and assume that the sequent $\vdash\Gamma$ is
TTL derivable from elements of $\Xi$. Then there exists a derivation $\pi$ of
$\vdash\Gamma$ from elements of $\Xi$ such that for any application of the Cut
rule in $\pi$ one of the two premises is an element $\vdash\overline{\bf t},A$
of $\Xi$ and the cut-formula is $A$.

Proof This follows directly from Lemma 5.9. $\Box$

######  Lemma 9.13.

Let $\Xi$ be a sequent lexicon. A sequent of the form $\vdash\overline{\bf
t},\Gamma$, where $t$ is a tensor term and $\Gamma$ is a context in the base
language, is derivable from elements of $\Xi$ iff there exists elements
$\vdash\overline{\bf t_{(1)}},A_{(1)},\ldots,\vdash\overline{\bf
t_{(n)}},A_{(n)}$ of $\Xi$ and indices $i_{1},j_{1},\ldots,i_{k},j_{k}$ such
that $t=t_{(1)}\cdots
t_{(n)}\delta^{i_{1}}_{j_{1}}\cdots\delta^{i_{k}}_{j_{k}}$ and the sequent

$\vdash\overline{A_{(1)}},\ldots,\overline{A_{(n)}},\bot_{i_{1}}^{j_{1}},\ldots,\bot_{i_{k}}^{j_{k}},\Gamma$
(8)

is derivable in TTL.

Proof For the “if” direction use the Cut rule, for the “only if” direction use
induction on a derivation of $\vdash\overline{\bf t},\Gamma$ from Proposition
9.12.

The most important part is the base of induction. Let the sequent $\vdash\Pi$,
where $\Pi=\overline{\bf t},\Gamma$ be an element of $\Xi$. This means that
$\Pi$ has a representation $\Pi=\overline{{\bf t}_{(1)}},A_{(1)}$, where the
context $\overline{{\bf t}_{(1)}}$ represents a lexical term $t_{(1)}$ and
does not contain counits, while $A_{(1)}$ is a formula in the base language.
There are two possibilities. The first one is that $\overline{\bf
t}=\overline{{\bf t}_{(1)}}$, $\Gamma={A_{(1)}}$ and then the statement is
obvious. The second one is that $A_{(1)}=\bot^{i}_{j}$, $\overline{\bf
t}=\overline{{\bf t}_{(1)}},\bot^{i}_{j}$, and $\Gamma=\emptyset$. In this
latter case we have that $t=t_{(1)}\delta^{j}_{i}$ and the sequent
$\vdash\overline{A_{(1)}},\bot^{i}_{j},\Gamma$, i.e $\vdash{\bf
1}^{j}_{i},\bot^{i}_{j}$ is derivable in TTL. The statement holds.

Induction steps are straightforward. $\Box$

######  Corollary 9.14.

Given a classical, respectively intuitionistic, tensor grammar
$G=(\mathit{Lex},S)$, a lexical typing judgement $t\rhd A$ is derivable in $G$
iff the sequent $\vdash\overline{\bf t},F$, respectively ${\bf t}\vdash F$, is
TTL, respectively ITTL, derivable from the set of nonlogical axioms

${\bf Lex}=\\{\vdash\overline{\bf t},A|~{}(t\rhd A)\in\mathit{Lex}\\},$

respectively

${\bf Lex}=\\{{\bf t}\vdash A|~{}(t\rhd A)\in\mathit{Lex}\\}.\quad\Box$

Proof We consider the classical case.

If $t\rhd_{G}A$ then the statement follows from the definition of derivability
in a grammar (keeping in mind that the typing axiom $\delta^{i}_{j}\rhd{\bf
1}^{i}_{j}$ corresponds to the TTL derivable sequent $\vdash\bot^{j}_{i},{\bf
1}^{i}_{j}$). Assume that $\vdash\overline{\bf t},A$ is derivable from
elements of Lex.

Since derivability in TTL or in a tensor grammar is closed under
$\alpha$-equivalence, we may assume that ${\bf Lex}$ and $\mathit{Lex}$ are
closed under $\alpha$-equivalence of sequents, respectively typing judgements.
By Lemma 9.13, we have a list $\vdash\overline{\bf
t_{(1)}},A_{(1)},\ldots,\vdash\overline{\bf t_{(n)}},A_{(n)}$ of elements of
${\bf Lex}$ and indices $i_{1},j_{1},\ldots,i_{k},j_{k}$ such that
$t=\delta^{i_{1}}_{j_{1}}\cdots\delta^{i_{k}}_{j_{k}}t_{(1)}\cdots t_{(n)}$
and sequent (8) is derivable in TTL. Put
$t_{(n+\alpha)}=\delta^{i_{\alpha}}_{j_{\alpha}}$, $A_{(n+\alpha)}={\bf
1}^{i_{\alpha}}_{j_{\alpha}}$, $\alpha=1,\ldots,k$. Then for every $\alpha\leq
k$ the typing judgement $t_{(n+\alpha)}\rhd A_{(n+\alpha)}$ is a typing axiom.
We have the list ${t_{(1)}}\rhd A_{(1)},\ldots,{t_{(n+k)}}\rhd A_{(n+k)}$ of
elements of $\mathit{Lex\cup TpAx}$ such that $t=t_{(1)}\ldots t_{n+k}$ and
the sequent $\vdash\overline{A_{(1)}},\ldots,\overline{A_{(n+k)}},A$ is
derivable in TTL. Which means exactly that $t\rhd_{G}A$.

The intuitionistic version of the statement follows from conservativity of the
intuitionistic fragment of TTL. $\Box$

Thus we obtain a convenient representation of tensor grammars as systems of
non-logical axioms in the extended language. When using such a representation
it is natural to add to the system the following lexical substitution rule :

$\cfrac{\vdash A,\Gamma\quad(t\rhd A)\in\mathit{Lex}}{\vdash\overline{\bf
t},A}~{}({\rm{Lex}})$

in the classical format or

$\cfrac{A,\Gamma\vdash B\quad(t\rhd A)\in\mathit{Lex}}{{\bf t},A\vdash
B}~{}({\rm{Lex}})$

in the intuitionistic format. The rule is just a special instance of the Cut
rule where one of the premises is an axiom from Lex.

###  9.4 Example

$\begin{array}[]{c}[{\rm{Mary}}]^{i}_{j}\rhd
np^{i}_{j},\quad[{\rm{John}}]^{i}_{j}\rhd
np^{i}_{j},\quad[{\rm{loves}}]^{i}_{j}\rhd np_{y}^{j}\multimap
np_{i}^{x}\multimap s^{x}_{y},\\\
\mbox{[{\rm{madly}}]}^{y}_{k}\rhd(np^{x}_{i}\multimap s^{x}_{y})\multimap
np_{i}^{z}\multimap s^{z}_{k},\quad\mbox{[{\rm{who}}]}^{t}_{z}\rhd{\bf
1}^{j}_{y}\otimes(np^{j}_{y}\multimap s^{z}_{k})\multimap np_{t}^{u}\multimap
np^{u}_{k}\end{array}$

(a)

$np^{j}_{y}\vdash np^{j}_{y}$ $np^{x}_{i}\vdash np^{x}_{i}$ $s^{x}_{y}\vdash
s^{x}_{y}$ $(\multimap{\rm{L}})$ $np^{x}_{i},np^{x}_{i}\multimap
s^{x}_{y}\vdash s^{x}_{y}$ $(\multimap{\rm{L}})$
$np^{x}_{i},np^{j}_{y},np^{j}_{y}\multimap np^{x}_{i}\multimap s^{x}_{y}\vdash
s^{x}_{y}$ $({\rm{Lex}})$ $np^{x}_{i},np^{j}_{y},{\bf loves}^{i}_{j}\vdash
s^{x}_{y}$ $(\multimap{\rm{R}})$ $np^{j}_{y},{\bf loves}^{i}_{j}\vdash
np^{x}_{i}\multimap s^{x}_{y}$ ${\bf John}^{z}_{i}\vdash np^{z}_{i}$
$s^{z}_{k}\vdash s^{z}_{k}$ $(\multimap{\rm{L}})$ ${\bf
John}^{z}_{i},np^{z}_{i}\multimap s^{z}_{k}\vdash s^{z}_{k}$
$(\multimap{\rm{L}})$ ${\bf John}^{z}_{i},np^{j}_{y},{\bf
loves}^{i}_{j},(np^{x}_{i}\multimap s^{x}_{y})\multimap np^{z}_{i}\multimap
s^{z}_{k}\vdash s^{z}_{k}$ $({\rm{Lex}})$ ${\bf John}^{z}_{i},np^{j}_{y},{\bf
loves}^{i}_{j},{\bf madly}^{y}_{k}\vdash s^{z}_{k}$ $(\multimap{\rm{R}})$
${\bf John}^{z}_{i},{\bf loves}^{i}_{j},{\bf madly}^{y}_{k}\vdash
np^{j}_{y}\multimap s^{z}_{k}$
---
${\bf 1}_{y}^{j}\vdash{\bf 1}_{y}^{j}$ ${\bf John}^{z}_{i},{\bf
loves}^{i}_{j},{\bf madly}^{y}_{k}\vdash np^{j}_{y}\multimap s^{z}_{k}$
$(\otimes{\rm{R}})$ ${\bf John}^{z}_{i},{\bf loves}^{i}_{j},{\bf
madly}^{y}_{k},{\bf 1}_{y}^{j}\vdash{\bf 1}_{y}^{j}\otimes(np^{j}_{y}\multimap
s^{z}_{k})$ $({\rm{L{\bf 1}^{\leftarrow}}})$ ${\bf John}^{z}_{i},{\bf
loves}^{i}_{j},{\bf madly}^{j}_{k}\vdash{\bf
1}_{y}^{j}\otimes(np^{j}_{y}\multimap s^{z}_{k})$
${\bf John}^{z}_{i},{\bf loves}^{i}_{j},{\bf madly}^{j}_{k}\vdash{\bf
1}_{y}^{j}\otimes(np^{j}_{y}\multimap s^{z}_{k})$ ${\bf Mary}^{u}_{t}\vdash
np^{u}_{t}$ $np^{u}_{k}\vdash np^{u}_{k}$ $(\multimap{\rm{L}})$ ${\bf
Mary}^{u}_{t},np^{u}_{t}\multimap np^{u}_{k}\vdash np^{u}_{k}$
$(\multimap{\rm{L}})$ ${\bf Mary}^{u}_{t},{\bf John}^{z}_{i},{\bf
loves}^{i}_{j},{\bf madly}^{j}_{k},{\bf 1}_{y}^{j}\otimes(np^{j}_{y}\multimap
s^{z}_{k})\multimap np^{u}_{t}\multimap np^{u}_{k}\vdash np^{u}_{k}$
$({\rm{Lex}})$ ${\bf Mary}^{u}_{t},{\bf John}^{z}_{i},{\bf loves}^{i}_{j},{\bf
madly}^{j}_{k},{\bf who}^{t}_{z}\vdash np^{u}_{k}$ $(=)$ ${\bf
Mary}^{u}_{t},{\bf who}^{t}_{z},{\bf John}^{z}_{i},{\bf loves}^{i}_{j},{\bf
madly}^{j}_{k}\vdash np^{u}_{k}$
(b)

Figure 9: Tensor grammar example

A linguistically motivated example of tensor grammar is given in Figure 9.
Figure LABEL:Axioms shows the lexicon (assumed closed under
$\alpha$-equivalence), and in Figure LABEL:ND_grammar_derivation we derive the
noun phrase “Mary who John loves madly”, using the representation in the
extended language. (For readability, the derivation is broken into three
parts.)

##  10 Completeness of tensor term semantics

In this section we establish completeness of TTL and, consequently, of ITTL in
a balanced language for the tensor term semantics. We will discuss the
classical system, the intuitionistic case will follow by conservativity. We
assume that we are given a classical tensor language generated by a finite set
of balanced positive literals. We also assume that we have an infinite
alphabet $T$ of terminal symbols. We will extensively use the extended
language as discussed in Sections 9.2, 9.3.

###  10.1 Canonical lexicon

######  Definition 10.1.

A set $\mathbf{Lex}$ of lexical sequents in the (classical) extended language
is a canonical lexicon if the following hold:

  1. (i)

for any formula $A$ of the base language there are infinitely many elements of
the form $\vdash\overline{\bf t},A$ in $\mathbf{Lex}$,

  2. (ii)

if $\vdash\overline{\bf t},A$, $\vdash\overline{\bf s},A^{\prime}$ are
elements of $\mathbf{Lex}$ that are not $\alpha$-equivalent, then for any two
terminal symbols $a,b\in T$ such that $\overline{\bf
a}^{i}_{j}\in\overline{\bf t}$, $\overline{\bf b}^{k}_{l}\in\overline{\bf s}$
it holds that $a\not=b$;

  3. (iii)

the set $\mathbf{Lex}$ is closed under $\alpha$-equivalence of sequents.

The elements of $\mathbf{Lex}$ will serve as “axioms” describing the model.

######  Proposition 10.2.

Canonical lexicons exist.

Proof A canonical lexicon can be constructed in countably many steps as
follows. Choose an enumeration of the set
$\mathit{Fm}(\mathit{Lit}_{+})\times\mathbb{N}$. Let
$\mathbf{Lex}_{0}=\emptyset$. On the $i$th step consider the $i$th element
$(A,n)$. Let $FI(A)=(\\{i_{1},\ldots,i_{k}\\},\\{j_{1},\ldots,j_{k}\\})$. If
$k>0$ , choose pairwise distinct terminal symbols
$a_{1},\ldots,a_{k},b_{1},\ldots,b_{k}\in T$ not occurring in
$\mathbf{Lex}_{i-1}$ and define $\mathbf{Lex}_{i}$ as $\mathbf{Lex}_{i-1}$
plus the sequent $\vdash\overline{\bf
a_{1}}^{i_{1}}_{j_{1}},\ldots,\overline{\bf a_{k}}^{i_{k}}_{j_{k}},A$. If
$k=0$, choose $a,b\in T$ not occurring in $\mathbf{Lex}_{i-1}$ and define
$\mathbf{Lex}_{i}$ as $\mathbf{Lex}_{i-1}$ plus the sequent
$\vdash\overline{\bf a}^{i}_{j},\overline{\bf b}^{j}_{i},A$. Finally, define
$\mathbf{Lex}$ as the closure of $\bigcup\limits_{i}\mathbf{Lex}_{i}$ under
$\alpha$-equivalence of sequents. $\Box$

######  Proposition 10.3.

If $\vdash\Gamma$ is a sequent in the base language TTL derivable from
elements of a canonical lexicon $\mathbf{Lex}$ then $\vdash\Gamma$ is
derivable in TTL.

Proof The statement is a trivial case of Lemma 9.13. $\Box$

######  Proposition 10.4.

Let $\vdash\Gamma$ be a sequent in the extended language TTL derivable from
elements of a canonical lexicon $\mathbf{Lex}$. The formula $\overline{\bf
a}^{i}_{j}$, where $a\in T$, occurs in $\Gamma$ iff there is an element
$\vdash{\overline{\bf t}},A$ of $\mathbf{Lex}$ such that $a$ occurs in $t$ and
the context $\overline{\bf t}$ is contained in $\Gamma$.

Proof Induction on the derivation from Proposition 9.12, using clauses (ii),
(iii) of Definition 10.1. $\Box$

######  Proposition 10.5.

If $\vdash\overline{\bf t},A$ is an element of a canonical lexicon
$\mathbf{Lex}$, where $A$ is a formula in the base language, $\Gamma$ is a
context in the extended language having no common literal with $\overline{\bf
t}$, and the sequent $\vdash\overline{\bf t},\Gamma$ is TTL derivable from
elements of ${\mathbf{Lex}}$ then the sequent $\vdash\overline{A},\Gamma$ is
also derivable from elements of $\mathbf{Lex}$.

Proof Induction on derivation from Proposition 9.12 using Proposition 10.4.
$\Box$

###  10.2 Canonical model

######  Definition 10.6.

Given a canonical lexicon $\mathbf{Lex}$, the canonical type system is defined
by the dualizing type

$\bot\\!\\!\\!\\!\\!\\!\bot=\\{t|~{}\vdash\overline{\bf t}\mbox{ is derivable
from }\mathbf{Lex}\\}$ (9)

The canonical model of TTL is defined by the valuation

$||A||=\\{t|~{}\vdash\overline{\bf t},A\mbox{ is derivable from
}\mathbf{Lex}\\},$ (10)

where $A=p^{i_{1}\ldots i_{k}}_{j_{1}\ldots j_{k}}$, $p\in\mathit{Lit}_{+}$,
$v(p)=(k,k)$.

It is easy to check that valuation (10) satisfies the conditions for a model
of TTL (Definition 7.11).

######  Lemma 10.7.

In the setting of the canonical model, formula (10) holds for any formula $A$
of the base language.

Proof Induction on $A$, where we use that any formula of the base language can
be constructed from atomic ones of the form $A=p^{i_{1}\ldots
i_{k}}_{j_{1}\ldots j_{k}}$, where $p\in\mathit{Lit}_{+}$, and
$A=\bot^{i}_{j}$ by means of the operations $\overline{(.)}$ and $\parr$.

Base: we only need to consider the case $A=\bot^{i}_{j}$. If the sequent
$\vdash\overline{\bf t},\bot^{i}_{j}$ is derivable from $\mathbf{Lex}$ then,
by definition (9), we have that
$t\delta^{j}_{i}\in\bot\\!\\!\\!\\!\\!\\!\bot$, hence
$t\in\overline{\\{\delta^{j}_{i}\\}}=\bot^{i}_{j}=||\bot^{i}_{j}||$. If, on
the other hand, $t\in||\bot^{i}_{j}||=\bot^{i}_{j}$ then
$t\delta^{j}_{i}\in\bot\\!\\!\\!\\!\\!\\!\bot$, which, again by definition
(9), means precisely that the sequent $\vdash\overline{\bf t},\bot^{i}_{j}$ is
derivable from $\mathbf{Lex}$. The base of induction is proven.

Let $A=\overline{B}$, and assume that the statement holds for $B$. Assume that
the sequent $\vdash\overline{\bf t},A$ is derivable from $\mathbf{Lex}$. Pick
any $s\in||B||$. By the induction hypothesis, we have that the sequent
$\vdash\overline{\bf s},B$ is derivable from $\mathbf{Lex}$. Using the Cut
rule we get that the sequent $\vdash\overline{\bf t},\overline{\bf s}$, i.e.
$\vdash\overline{\bf t\cdot s}$, is derivable from $\mathbf{Lex}$ as well,
hence $ts\in\bot\\!\\!\\!\\!\\!\\!\bot$. Since $s\in||B||$ was arbitrary we
conclude that $t\in\overline{\overline{||B||}}=||A||$. Now assume that
$t\in||A||$. It follows from Definition 10.1 that there exists an element
$\vdash\overline{\bf s},B$ in $\mathbf{Lex}$ such that $t$ and $s$ have no
common literals. By the induction hypothesis $\overline{\bf s}\in||B||$ and it
follows that $ts\in\bot\\!\\!\\!\\!\\!\\!\bot$. This means that the sequent
$\vdash\overline{\bf t\cdot s}$, i.e. $\vdash\overline{\bf t},\overline{\bf
s}$, is derivable from $\mathbf{Lex}$. Then by Proposition 10.5 the sequent
$\vdash\overline{\bf t},\overline{B}$, i.e. $\vdash\overline{\bf t},A$ is
derivable from $\mathbf{Lex}$ as well.

The step $A=B\parr C$ is very similar to the preceding one. $\Box$

######  Corollary 10.8.

The sequent $\vdash\Gamma$ in the base language is valid in a canonical model
if it is derivable in TTL.

Proof Let $\Gamma=A_{(1)},\ldots,A_{(n)}$. The sequent $\vdash\Gamma$ is valid
in the canonical model iff $1\in||A_{(1)}\parr\ldots\parr A_{(n)}||$. By the
preceding lemma, the latter condition implies that $\vdash
A_{(1)}\parr\ldots\parr A_{(n)}$ is TTL derivable from the canonical lexicon.
The latter sequent is equivalent to $\vdash\Gamma$, hence $\vdash\Gamma$ is
derivable from the canonical lexicon. Then, by Proposition 10.3 the sequent
$\vdash\Gamma$ is derivable in TTL. $\Box$

######  Corollary 10.9 (Completeness Theorem).

A sequent in a balanced classical, respectively intuitionistic tensor language
is derivable in TTL, respectively ITTL iff it is valid in any tensor term
model. $\Box$

##  11 Conclusion and future work

We proposed a simple logical system, TTL, which combines commutative and non-
commutative operations of linear logic, and is designed specially for defining
categorial grammars. TTL contains cyclic logic and Lambek calculus (allowing
empty antecedents) as conservative fragments. It also allows encoding
derivations of ordinary (commutative) multiplicative linear logic. The logic
is cut-free and decidable, it has intuitionistic and classical versions and is
equipped with a simple intuitive semantics, which is sound and complete. We
also defined categorial grammars based on TTL.

A number of topics are left for future research. Among them are complexity of
the calculus, algorithms for proof-search and grammar parsing, proof-nets. We
plan to study representation of known grammatical formalism, such as ACG and
HTLCG, in TTL. Also, connections with first order linear logic remain to be
understood. We also think that there are some interesting extensions and
modifications of the calculus. Can we add additive connectives? Can we add
some structure that will allow representing ordered tuples of strings and
obtain a conservative representation of displacement calculus? We think that
other research questions might arise as well, because the setting seems to us
rather rich.

## References

  * [1] V. Michele Abrusci and Paul Ruet.  Non-commutative logic i: The multiplicative fragment.  Annals of Pure and Applied Logic, 101(1):29–64, 1999.