19411 LABEL:LastPageJun. 22, 2022Nov. 17, 2023

# Making first order linear logic
a generating grammar

Sergey Slavnov0000-0001-8825-7318<EMAIL_ADDRESS>
###### Abstract.

It is known that different categorial grammars have surface representation in
a fragment of first order multiplicative linear logic (MLL1). We show that the
fragment of interest is equivalent to the recently introduced extended tensor
type calculus (ETTC). ETTC is a calculus of specific typed terms, which
represent tuples of strings, more precisely bipartite graphs decorated with
strings. Types are derived from linear logic formulas, and rules correspond to
concrete operations on these string-labeled graphs, so that they can be
conveniently visualized. This provides the above mentioned fragment of MLL1
that is relevant for language modeling not only with some alternative syntax
and intuitive geometric representation, but also with an intrinsic deductive
system, which has been absent.

In this work we consider a non-trivial notationally enriched variation of the
previously introduced ETTC, which allows more concise and transparent
computations. We present both a cut-free sequent calculus and a natural
deduction formalism.

###### Key words and phrases:

categorial grammars, linear logic, Lambek calculus, diagrammatic reasoning

##  1\. Introduction

The best known examples of categorial grammars are Lambek grammars, which are
based on Lambek calculus (LC) [Lam58], i.e. noncommutative intuitionistic
linear logic (for background on linear logic see [Gir87],[Gir95], for
categorial grammars [MR12]). These, however, have somewhat limited expressive
power, and a lot of extensions/variations have been proposed, using
discontinuous tuples of strings and $\lambda$-terms, commutative and non-
commutative logical operations, modalities etc. Let us mention displacement
grammars [MVF11], abstract categorial grammars (ACG, also called
$\lambda$-grammars and linear grammars) [dG01], [Mus07], [MP12] and hybrid
type logical categorial grammars [KL12].

It has been known for a while that different grammatical formalisms, such as
those just mentioned, have surface representation in the familiar first order
multiplicative intuitionistic linear logic (MILL1), which provides them in
this way with some common ground. In the seminal work [MP01] it was shown that
LC translates into MILL1 as a conservative fragment; later similar
representations were obtained for other systems [Moo14a], [Moo14b] (however,
in the case of displacement calculus, the representation is not conservative,
see [Moo15]). This applies equally well to the classical setting of first
order multiplicative linear logic (MLL1), which is a conservative extension of
MILL1 anyway.

The translations are based on interpreting first order variables as denoting
string positions. Basically, this induces (at least on the intuitive level) an
interpretation of certain well-formed formulas and sequents as expressing
relations between strings, in particular, those encoded in formal grammars.
Unfortunately, this intuitive interpretation (to the author’s knowledge) has
never been formulated explicitly and rigorously, i.e. as a specific semantics
for (a fragment of) MILL1. Therefore the underlying structures for
constructions of the above cited works, arguably, remain somewhat unclear.

It should be emphasised that only a small fragment of MILL1, let us call it
linguistically well-formed, is actually used in the above translations. It is
this fragment that obtains in this way the above discussed “linguistic”
interpretation in terms of relations between strings. As for the whole MILL1,
the “linguistic” meaning of general formulas and sequents seems, at least,
obscure. On the other hand, standard deductive systems of linear logic are not
intrinsic to this fragment. Typically, when deriving, say, the MILL1
translation of an LC sequent, in general, we have to use at intermediate steps
sequents that have no clear linguistic meaning, if any. It can be said that
representation of formal grammars makes first order linear logic an auxiliary
tool, but hardly something like a generating grammar. Derivations do not
translate step-by-step to operations generating language elements.

(We should note, however, that the first order logic formalism has, in
general, wider usage in linguistic applications. Apart from encoding string
positions, first order constructions allow representing grammatical features,
locality domains, tree depth levels etc. We do not discuss the latter
applications in our paper.)

The system of extended tensor type calculus (ETTC) based on (classical)
propositional MLL, recently proposed in [Sla21b] (elaborating on [Sla21a]),
was directly designed for linguistic interpretation, namely for concrete
geometric representation of ACG extended with constructions emulating
noncommutative operations of LC. ETTC is a calculus of specific typed terms,
which represent tuples of strings, more precisely bipartite graphs decorated
with strings. Types are derived from MLL formulas, and rules correspond to
concrete operations on these string-labeled graphs, so that they can be
conveniently visualized. Typed terms become language elements, from which
words are gradually assembled using these geometric operations.

It was shown in [Sla21b] that tensor grammars based on ETTC include both
Lambek grammars and ACG as conservative fragments. Moreover, the
representation of LC types in ETTC is very similar to that in MILL1. This led
to the question (raised explicitly in that paper) about relations between the
two systems. In this work we show that ETTC is equivalent precisely to the
above discussed linguistically well-formed fragment of MLL1. (Actually, we
consider a non-trivial notationally enriched variation of ETTC rather than the
one proposed in [Sla21b]. The enriched system allows more concise and
transparent computations.) Thus, it turns out that ETTC provides the
linguistic fragment with an alternative syntax, together with an intrinsic
deductive system and intuitive pictorial representation. It can be said that,
in some sense, ETTC does “make the linguistic fragment a generating grammar”,
as announced in the title. Speaking less ambitiously, it allows a different
perspective on the MILL1 representations, which might be clarifying and
useful.

In this paper we will work on the basis of classical linear logic, mostly
because it suggests some nice symmetric notation, but all constructions
automatically restrict to the intuitionistic setting.

##  2\. Background: systems of linear logic

$\begin{array}[]{c}\mathit{Pred}_{-}=\\{\overline{p}|~{}p\in\mathit{Pred}_{+}\\},\quad
p\mbox{ is }n\mbox{-ary}\Rightarrow{\overline{p}}\mbox{ is
}n\mbox{-ary},\quad\mathit{Pred}=\mathit{Pred}_{+}\cup\mathit{Pred}_{-},\\\\[1.42271pt]
\mathit{At}=\\{p(e_{1},\ldots,e_{n})|~{}e_{1},\ldots,e_{n}\in\mathit{Var},~{}p\in\mathit{Pred},~{}p\mbox{
is }n\mbox{-ary}\\},\\\\[1.42271pt]
\mathit{Fm}::=\mathit{At}|(\mathit{Fm}\otimes\mathit{Fm})|(\mathit{Fm}\parr\mathit{Fm})|\forall
x\mathit{Fm}|\exists x\mathit{Fm},~{}x\in\mathit{Var}\\\\[4.26773pt]
\overline{p(e_{1},\ldots,e_{n})}=\overline{p}(e_{n},\ldots,e_{1}),\quad\overline{\overline{p(e_{1},\ldots,e_{n})}}=p(e_{n},\ldots,e_{1})\mbox{
for }P\in Pred_{+},\\\\[2.84544pt] \overline{A\otimes
B}=\overline{B}\parr\overline{A},\quad\overline{A\parr
B}=\overline{B}\otimes\overline{A},\quad\overline{\forall xA}=\exists
x(\overline{A}),\quad\overline{\exists xA}=\forall
x(\overline{A}).\end{array}$

(a)

$\begin{array}[]{c}\cfrac{A\in
At}{\vdash\overline{A},A}~{}(\mbox{Id})\quad\cfrac{\vdash\Gamma,A\quad\vdash\overline{A},\Theta}{\vdash\Gamma,\Theta}~{}(\mbox{Cut})\\\\[7.11317pt]
\cfrac{\vdash\Gamma,A,B}{\vdash\Gamma,A\parr
B}~{}(\parr)~{}\cfrac{\vdash\Gamma,A~{}\vdash B,\Theta}{\vdash\Gamma,A\otimes
B,\Theta}~{}{}(\otimes)~{}\cfrac{\vdash\Gamma,A[\nicefrac{{v}}{{x}}],~{}v\not\in
FV(\Gamma)}{\vdash\Gamma,\forall
xA}~{}(\forall)~{}\cfrac{\vdash\Gamma,A[\nicefrac{{v}}{{x}}]}{\vdash\Gamma,\exists
xA}~{}(\exists)\end{array}$

(b)

$\mathit{Fm}::=\mathit{Prop}|(\mathit{Fm}\backslash\mathit{Fm})|(\mathit{Fm}/\mathit{Fm})|(\mathit{Fm}\bullet\mathit{Fm})$

(c)

$\begin{array}[]{c}\begin{array}[]{lcr}||p||^{(l,r)}=p(l,r)\mbox{ for
}p\in\mathit{Prop},&&||B/A||^{(l,r)}=\forall
x||A||^{(r,x)}\multimap||B||^{(l,x)},\\\\[1.42271pt] ||A\bullet
B||^{(l,r)}=\exists x||A||^{(l,x)}\otimes||B||^{(x,r)},&&||A\backslash
B||^{(l,r)}=\forall
x||A||^{(x,l)}\multimap||B||^{(x,r)}.\end{array}\\\\[2.84544pt]
\begin{array}[]{rcl}A_{1},\ldots,A_{n}\vdash_{\bf
LC}B&\Longleftrightarrow&||A_{1}||^{(c_{0},c_{1})},\ldots,||A_{n}||^{(c_{n-1},c_{n})}\vdash_{\bf
MILL1}||B||^{(c_{0},c_{n})}.\end{array}\end{array}$

(d)

Figure 1. Systems of linear logic

Language and sequent calculus of first order multiplicative linear logic
(MLL1) are shown in Figures LABEL:MLL1_formulas, LABEL:MLL1. We are given a
set $\mathit{Pred}_{+}$ of positive predicate symbols with assigned arities
and a set $\mathit{Var}$ of variables. The sets $\mathit{Pred}_{-}$ and
$\mathit{Pred}$ of negative and of all predicate symbols respectively are
defined. The sets of first order atomic, respectively, linear multiplicative
formulas are denoted as $\mathit{At}$, respectively, $\mathit{Fm}$.
Connectives $\otimes$ and $\parr$ are called respectively tensor (also times)
and cotensor (also par). Linear negation $\overline{(.)}$ is not a connective,
but is definable by induction on formula construction, as in Figure
LABEL:MLL1_formulas. Note that, somewhat non-traditionally, we follow the
convention that negation flips tensor/cotensor factors, typical for
noncommutative systems. This does not change the logic (the formulas $A\otimes
B$ and $B\otimes A$ are provably equivalent), but is more consistent with our
intended geometric interpretation.

A context ${\Gamma}$ is a finite multiset of formulas, and a sequent is an
expression of the form $\vdash\Gamma$, where $\Gamma$ is a context. The set of
free variables of $\Gamma$ is denoted as $FV(\Gamma)$. In this work we will
consider several systems of sequent calculus, and, in order to avoid
confusion, we will sometimes use abbreviations like $\vdash_{\bf MLL1}\Gamma$
to say that the sequent $\vdash\Gamma$ is derivable in ${\bf MLL1}$, similarly
for other systems. We also emphasize that a commutative system like MLL1 can
be given an alternative ordered formulation, where contexts are defined as
finite sequences (rather than multisets) of formulas and rules are
supplemented with the explicit Exchange rule
$\cfrac{\vdash\Gamma,A,B,\Theta}{\vdash\Gamma,B,A,\Theta}~{}({\rm{Ex}})$.

First order multiplicative intuitionistic logic (MILL1) is the fragment of
MLL1 restricted to sequents of the form $\vdash
B,\overline{A_{1}},\ldots,\overline{A_{n}}$, written in MILL1 in a two-sided
form as ${A_{1}},\ldots,{A_{n}}\vdash B$, where ${A_{1}},\ldots,{A_{n}},B$ are
multiplicative intuitionistic formulas, which means constructed using only
positive predicate symbols, quantifiers, tensor and linear implication defined
by $A\multimap B=\overline{A}\parr B$. (Note that we can define linear
implication differently as $A\multimap B=B\parr\overline{A}$ and get an
equivalent system.)

The language of Lambek calculus (LC), i.e. noncommutative multiplicative
intuitionistic linear logic, is summarised in Figure LABEL:LC_rules.
Noncommutative tensor is denoted as $\bullet$, and the two directed
implications caused by noncommutativity are denoted as slashes. Formulas of LC
are often called types. A context in LC is, by definition, a sequence of
types, and a sequent is an expression of the form $\Gamma\vdash F$, where
$\Gamma$ is a context and $F$ is a type. In LC there is no analogue of the
Exchange rule or “unordered” formulation, i.e. the system is genuinely
noncommutative. We will not reproduce the rules which can be found, for
example, in [Lam58].

Given a finite alphabet $T$ of terminal symbols, a Lambek grammar $G$ (over
$T$) is a pair $G=(\mathit{Lex},S)$, where $\mathit{Lex}$, the lexicon is a
finite set of lexical entries, which are expressions $t:A$, where $t\in T$ and
$A$ is a type, and $S$ is a selected atomic type. The language $L(G)$ of $G$
is the set of words

$L(G)=\bigg{\\{}t_{1}\ldots
t_{n}\bigg{|}\begin{array}[]{l}~{}t_{1}:A_{1},\ldots,t_{n}:A_{n}\in Lex,\\\
A_{1},\ldots,A_{n}\vdash_{\bf LC}S\end{array}\bigg{.}\bigg{\\}},$ (1)

where $t_{1}\ldots t_{n}$ stands for the concatenation of strings
$t_{1},\ldots,t_{n}$. More details on categorial grammars can be found in
[MR12].

Given two variables $l,r$, the first order translation $||F||^{(l,r)}$ of an
LC formula $F$ parameterized by $l,r$ is shown in Figure LABEL:LC2MILL (LC
propositional symbols are treated as binary predicate symbols). This provides
a conservative embedding of LC into MILL1 [MP01].

##  3\. MILL1 grammars and linguistic fragment

###  3.1. MILL1 grammars

Translation from LC suggests defining MILL1 grammars similar to Lambek
grammars.

Let a finite alphabet $T$ of terminal symbols be given. Assume for convenience
that our first order language contains two special variables (or constants)
$l,r$. Given a terminal alphabet $T$, a MILL1 lexical entry (over $T$) is a
pair $(w,A)$, where $w\in T^{*}$ is nonempty, and $A$ is a MILL1 formula with
one occurrence of $l$ and one occurrence of $r$ and no other free variables.
For the formula $A$ occurring in a lexical entry we will write
$A[x;y]=A[\nicefrac{{x}}{{l}}][\nicefrac{{y}}{{r}}]$ (so that $A=A[l;r]$).

A MILL1 grammar $G$ (over $T$) is a pair $(\mathit{Lex},s)$, where
$\mathit{Lex}$ is a finite set of MILL1 lexical entries, and $s$ is a binary
predicate symbol. The language $L(G)$ generated by $G$ or, simply, the
language of $G$ is defined by

$L(G)=\bigg{\\{}w_{1}\cdots
w_{n}\bigg{|}\begin{array}[]{l}~{}(w_{1},A_{1}),\ldots,(w_{m},A_{n})\in
Lex,\\\ ~{}A_{1}[c_{0};c_{1}],\ldots,A_{n}[c_{n-1};c_{n}]\vdash_{\bf
MILL1}s(c_{0},c_{n})\end{array}\bigg{.}\bigg{\\}}.$ (2)

It seems clear that, under such a definition, Lambek grammars translate
precisely to MILL1 grammars generating the same language (compare (2) with
(1)).

It has been shown [Moo14a], [Moo14b] that MILL1 allows representing more
complex systems such as displacement calculus, abstract categorial grammars,
hybrid type-logical grammars. This suggests that the above definition should
be generalized to allow more complex lexical entries, corresponding to word
tuples rather than just words. (To the author’s knowledge, no explicit
definition of a MILL1 grammar has been given in the literature, but this
concept is implicit in the above cited works).

Now let us isolate the fragment of first order logic that is actually used in
translations of linguistic systems.

###  3.2. Linguistic fragment

A language of MLL1 is linguistically marked if each $n$-ary predicate symbol
$p$ is equipped with valency $v(p)\in{\mathbb{N}}^{2}$,
$v(p)=(v_{l}(p),v_{r}(p))$, where $v_{l}(p)+v_{r}(p)=n$, such that
$v(\overline{p})=(v_{r}(p),v_{l}(p))$. When $v(p)=(k,m)$ we say that first $k$
occurrences $x_{1},\ldots,x_{k}$ in the atomic formula $p(x_{1},\ldots,x_{n})$
are left occurrences or have left polarity, and $x_{k+1},\ldots,x_{n}$ are
right occurrences, with right polarity. For a variable occurrence $x$ in a
compound formula in a linguistically marked language $F$ we define the
polarity of $x$ in $F$ by induction. If $F=A\Box B$, where
$\Box\in\\{\otimes,\parr\\}$, and $x$ occurs in $A$, respectively $B$, then
the polarity of $x$ in $F$ is the same as the polarity of $x$ in $A$,
respectively $B$. If $F=QxA$, where $Q\in\\{\forall,\exists\\}$, then the
polarity of a variable occurrence $x$ in $F$ is the same as the polarity of
$x$ in $A$, If $\Gamma=A_{1},\ldots,A_{n}$ is a context, and $x$ is a variable
occurrence in $A_{i}$ for some $i\in\\{1,\ldots,n\\}$, then the polarity of
$x$ in the context $\Gamma$ and in the sequent $\vdash\Gamma$ is the same as
the polarity of $x$ in $A_{i}$. For a MILL1 sequent $\Gamma\vdash F$, the
polarity of its variable occurrences is determined by the translation to MLL1.

Given a linguistically marked MLL1 language, a formula, context or sequent is
linguistically marked if every quantifier binds exactly one left and one right
variable occurrence. An MLL1 derivation $\pi$ is linguistically marked if all
sequents occurring in $\pi$ are linguistically marked.

A linguistically marked formula or context is linguistically well-formed if,
furthermore, it has at most one left and at most one right occurrence of any
free variable. A linguistically marked sequent is linguistically well-formed
if each of its free variables has exactly one left and one right occurrence. A
MILL1 grammar is well-formed if the formula in every lexical entry is
linguistically well-formed with $l$ and $r$ occurring with left and right
polarity respectively.

######  Proposition 1.

Any cut-free derivation of a linguistically marked MLL1 sequent is
linguistically marked. $\Box$

Evidently, if we understand MILL1 as a fragment of MLL1, then the translation
of LC in Figure LABEL:LC2MILL has precisely the linguistically well-formed
fragment as its target (with $v(p)=(1,1)$ for all $p\in\mathit{Pred}$), and
Lambek grammars translate to linguistically well-formed ones. Similar
observations apply to translations in [Moo14a], [Moo14b].

However, the standard sequent calculus formulation of MLL1 is not intrinsic to
the linguistic fragment. For an illustration, a basic LC derivable sequent
$A,B\vdash A\bullet B$ translates to MILL1 as
$A(c_{0},c_{1}),B(c_{1},c_{2})\vdash\exists xA(c_{0},x)\otimes B(x,c_{2})$.
The latter, obviously, is derivable in ${\bf MLL1}$ by the $(\exists)$ rule
applied to the sequent $A(c_{0},c_{1}),B(c_{1},c_{2})\vdash
A(c_{0},c_{1})\otimes B(c_{1},c_{2})$, which itself is not in the linguistic
fragment. Thus, in order to derive a linguistically well-formed sequent in
MLL1 we have to use “linguistically ill-formed” ones at intermediate steps.

Our goal is to provide the linguistic fragment with an intrinsic deductive
system.

####  3.2.1. Occurrence nets

$\vdash a(e,t),\overline{a}(t,e)\otimes a(e,s),\overline{a}(s,e)$

$(\exists)$$\Longrightarrow$$\vdash a(e,t),\exists x(\overline{a}(t,x)\otimes
a(x,s)),\overline{a}(s,e)$

Figure 2. Occurrence net example

Let us introduce some convenient format and terminology for derivations of
linguistically well-formed sequents. An occurrence net of a linguistically
marked MLL1 sequent $\vdash\Gamma$ is a perfect matching $\sigma$ between left
and right free occurrences in $\Gamma$, such that each pair (link) in $\sigma$
consists of occurrences of the same variable. Basically, occurrence nets are
rudiments of proof-nets. To each cut-free linguistically marked derivation
$\pi$ with conclusion $\vdash\Gamma$ we will assign an occurrence net
$\sigma(\pi)$, which is an occurrence net of $\vdash\Gamma$. (Note that for a
linguistically well-formed sequent there is only one occurrence net possible.)
The occurrence net $\sigma(\pi)$ of a cut-free linguistically marked
derivation $\pi$ is constructed by induction on $\pi$.

  * •

If $\pi$ is the axiom $\vdash\overline{X},X$, where
$X={p}(e_{1},\ldots,e_{n})$, the net is defined by matching each occurrence
$e_{i}$ in $X$ with the occurrence $e_{i}$ in
$\overline{X}=\overline{p}(e_{n},\ldots,e_{1})$.

  * •

If $\pi$ is obtained from a derivation $\pi^{\prime}$ by the $(\parr)$ rule,
then $\sigma(\pi)=\sigma(\pi^{\prime})$.

  * •

If $\pi$ is obtained from derivations $\pi_{1}$, $\pi_{2}$ by the $(\otimes)$
rule, $\sigma(\pi)=\sigma(\pi_{1})\cup\sigma(\pi_{2})$.

  * •

If $\pi$ is obtained from some $\pi^{\prime}$ by the $(\forall)$ rule applied
to a formula $A^{\prime}=A[\nicefrac{{v}}{{x}}]$ and introducing the formula
$\forall xA$, then
$\sigma(\pi)=\sigma(\pi^{\prime})\setminus\\{(v_{l},v_{r})\\}$, where
$v_{l},v_{r}$ are the two occurrences of $v$ in $A^{\prime}$. (The variable
$v$ has no free occurrences in the premise other than those in $A^{\prime}$,
and, since all sequents are linguistically marked, there must be precisely one
left and one right occurrence of $v$ in $A^{\prime}$. It follows that
$(v_{l},v_{r})\in\sigma(\pi^{\prime})$.)

  * •

If $\pi$ is obtained from $\pi^{\prime}$ by the $(\exists)$ rule applied to a
formula $A^{\prime}=A[\nicefrac{{v}}{{x}}]$ and introducing the formula
$\exists xA$, there are two cases depending on $\sigma(\pi^{\prime})$. Let
$v_{l}$ and $v_{r}$ be, respectively, the left and the right occurrence of $v$
in $A^{\prime}$ corresponding to the two occurrences of $x$ in $A$ bound by
the existential quantifier.

    * –

If $(v_{l},v_{r})\in\sigma(\pi^{\prime})$, then
$\sigma(\pi)=\sigma(\pi^{\prime})\setminus\\{(v_{l},v_{r})\\}$.

    * –

Otherwise let $v_{l}^{\prime}$, $v_{r}^{\prime}$ be such that
$(v_{l}^{\prime},v_{r}),(v_{l},v_{r}^{\prime})\in\sigma(\pi^{\prime})$. Then

$\sigma(\pi)=(\sigma(\pi^{\prime})\setminus\\{(v_{l}^{\prime},v_{r}),(v_{l},v_{r}^{\prime})\\})\cup\\{(v_{l}^{\prime},v_{r}^{\prime})\\}.$

(If we see occurrence nets geometrically as bipartite graphs, then the
$(\parr)$ rule does not change the graphs, the $(\otimes)$ rule takes the
disjoint union of two graphs. The $(\forall)$ rule erases the link
corresponding to the two occurrences that become bound by the universal
quantifier. The $(\exists)$ rule has two cases: it erases a link in the first
case and glues two links into one in the second case. An example for the
second case of the $(\exists)$ rule is shown in Figure 2.)

In what follows we will use a number of times the operation of replacing a
free variable occurrence in an expression with another variable. So we
introduce some notation generalizing familiar notation for substitution. Let
$\Phi$ be a context or a formula, let $x$ be a free variable occurrence in
$\Phi$ and $v\in\mathit{Var}$. Then $\Phi[\nicefrac{{v}}{{x}}]$ is the
expression obtained from $\Phi$ by replacing $x$ with $v$. We will also use
the notation
$\Phi[\nicefrac{{v_{1}}}{{x_{1}}},\ldots,\nicefrac{{v_{n}}}{{x_{n}}}]=\Phi[\nicefrac{{v_{1}}}{{x_{1}}}]\ldots[\nicefrac{{v_{n}}}{{x_{n}}}]$
for iterated substitutions, where it is assumed implicitly that
$x_{1},\ldots,x_{n}$ are pairwise distinct occurrences, so that the
substitutions commute with each other.

Finally, we will use for an induction parameter the size of a cut-free
derivation defined in the following natural way. 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$.

######  Proposition 2.

If $\Gamma$, $\Gamma^{\prime}$ are linguistically marked contexts differing
from each other only by renaming bound variables and the sequent
$\vdash\Gamma$ is MLL1 derivable with a cut-free derivation $\pi$, then
$\vdash\Gamma^{\prime}$ is derivable with a cut-free derivation $\pi^{\prime}$
of the same size and with the same occurrence net,
$\mathit{size}(\pi^{\prime})=\mathit{size}(\pi)$,
$\sigma(\pi^{\prime})=\sigma(\pi)$.

######  Proof 3.1.

Induction on $\pi$.

######  Proposition 3.

Let $\pi$ be a linguistically marked cut-free MLL1 derivation with conclusion
$\vdash\Gamma$, and assume that $(e_{l},e_{r})\in\sigma(\pi)$. Let
$v\in\mathit{Var}$ be such that $e_{l},e_{r}$ are not in the scope of a
quantifier $Qv$, $Q\in\\{\forall,\exists\\}$, and let
$\widehat{\Gamma}=\Gamma[\nicefrac{{v}}{{e_{l}}},\nicefrac{{v}}{{e_{r}}}]$.
Then $\vdash\widehat{\Gamma}$ is derivable in MLL1 with a linguistically
marked cut-free derivation $\widehat{\pi}$ of the same size as $\pi$.
Moreover, if $v_{l},v_{r}$ are occurrences of $v$ in $\widehat{\Gamma}$
replacing, respectively, the occurrences $e_{l},e_{r}$ in $\Gamma$, then
$\sigma(\widehat{\pi})=(\sigma(\pi)\setminus\\{(e_{l},e_{r})\\})\cup\\{(v_{l},v_{r})\\}$.

######  Proof 3.2.

Induction on $\mathit{size}(\pi)$. The most involved step is when $\pi$ is
obtained from a derivation $\pi^{\prime}$ of some sequent
$\vdash\Gamma^{\prime}$ by the $(\exists)$ rule and
$(e_{l},e_{r})\not\in\sigma(\pi^{\prime})$.

This means that $\Gamma^{\prime}$ contains some formula $A$, while $\Gamma$
contains the formula $\exists xA^{\prime}$, where
$A=A^{\prime}[\nicefrac{{e}}{{/}}{x}]$, and the occurrences $e_{l}^{\prime}$,
$e_{r}^{\prime}$ of $e$ in $A$ that correspond to the two occurrences of $x$
in $A^{\prime}$ are linked in $\sigma(\pi^{\prime})$ to, respectively,
$e_{r}$, $e_{l}$, i.e.
$(e_{l},e_{r}^{\prime}),(e_{l}^{\prime},e_{r})\in\sigma(\pi^{\prime})$. Note
that

$A^{\prime}=A[\nicefrac{{x}}{{e_{l}^{\prime}}},\nicefrac{{x}}{{e_{r}^{\prime}}}].$
(3)

Observe from (3) that the context
$\widehat{\Gamma}=\Gamma[\nicefrac{{v}}{{e_{l}}},\nicefrac{{v}}{{e_{r}}}]$ can
be obtained as follows.

Let
$\Theta=\Gamma^{\prime}[\nicefrac{{v}}{{e_{l}^{\prime}}},\nicefrac{{v}}{{e_{r}}},\nicefrac{{v}}{{e_{l}}},\nicefrac{{v}}{{e_{r}^{\prime}}}]$,
and let $v_{l}^{\prime},v_{r},v_{l},v_{r}^{\prime}$ be the occurrences of $v$
in $\Theta$ replacing, respectively, the occurrences
$e_{l}^{\prime},e_{r},e_{l},e_{r}^{\prime}$ in $\Gamma^{\prime}$. Let $B$ be
the formula in $\Theta$ that corresponds to $A$ in $\Gamma^{\prime}$. Put

$\widehat{A}=\exists
xB[\nicefrac{{x}}{{v_{l}^{\prime}}},\nicefrac{{x}}{{v_{r}^{\prime}}}].$ (4)

Then $\widehat{\Gamma}$ is obtained from $\Theta$ by replacing $B$ with
$\widehat{A}$.

Moreover, the sequent $\vdash\widehat{\Gamma}$ is derivable from
$\vdash\Theta$ by the $(\exists)$ rule. It follows that, if the occurrences
$e_{l}^{\prime},e_{r},e_{l},e_{r}^{\prime}$ in $\Gamma^{\prime}$ are not in
the scope of a quantifier $Qv$, $Q\in\\{\forall,\exists\\}$, then, by the
induction hypothesis (applied twice), we have that $\vdash_{\bf MLL1}\Theta$,
hence $\vdash_{\bf MLL1}\widehat{\Gamma}$. However, the above condition may
fail, and then we cannot apply the induction hypothesis directly. Therefore,
in a general case, we need some more work.

By renaming bound variables if necessary, we can obtain from $\Gamma^{\prime}$
a linguistically marked context $\Gamma^{\prime\prime}$ such that the
occurrences $e_{l}^{\prime},e_{r},e_{l},e_{r}^{\prime}$ are not in the scope
of a quantifier $Qv$, $Q\in\\{\forall,\exists\\}$. By the preceding
proposition the sequent $\vdash\Gamma^{\prime\prime}$ is derivable with a cut-
free derivation $\pi^{\prime\prime}$, where
$\mathit{size}(\pi^{\prime\prime})=\mathit{size}(\pi^{\prime})$,
$\sigma(\pi^{\prime\prime})=\sigma(\pi^{\prime})$. Then we put
$\Theta^{\prime\prime}=\Gamma^{\prime\prime}[\nicefrac{{v}}{{e_{l}^{\prime}}},\nicefrac{{v}}{{e_{r}}},\nicefrac{{v}}{{e_{l}}},\nicefrac{{v}}{{e_{r}^{\prime}}}]$.
Now the induction hypothesis can be applied for sure and the sequent
$\vdash\Theta^{\prime\prime}$ is derivable with a linguistically marked cut-
free derivation $\rho$, and
$\mathit{size}(\rho)=\mathit{size}(\pi^{\prime\prime})=\mathit{size}(\pi^{\prime})$.
Moreover,

$\sigma(\rho)=(\sigma(\pi^{\prime})\setminus\\{(e_{l}^{\prime},e_{r}),(e_{l},e_{r}^{\prime})\\})\cup\\{(v_{l}^{\prime},v_{r}),(v_{l},v_{r}^{\prime})\\},$
(5)

where $v_{l}^{\prime},v_{r},v_{l},v_{r}^{\prime}$ are the occurrences of $v$
in $\Theta^{\prime\prime}$ replacing, respectively, the occurrences
$e_{l}^{\prime}$, $e_{r}$, $e_{l}$, $e_{r}^{\prime}$ in
$\Gamma^{\prime\prime}$.

Let $A^{\prime\prime}$ be the formula in $\Gamma^{\prime\prime}$ corresponding
to $A$ in $\Gamma^{\prime}$, and $B^{\prime\prime}$ be the formula in
$\Theta^{\prime\prime}$ obtained from $A^{\prime\prime}$ in
$\Gamma^{\prime\prime}$. Let $\widehat{B}=\exists
xB^{\prime\prime}[x/v_{l}^{\prime},x/v_{r}^{\prime}]$. The formula
$\widehat{A}$ in (4) may differ from $\widehat{B}$ only by renaming bound
variables. Let $\widehat{\Theta}$ be the context obtained from
$\Theta^{\prime\prime}$ by replacing $B^{\prime\prime}$ with $\widehat{B}$.
Then $\widehat{\Theta}$ and $\widehat{\Gamma}$, as well, may differ only by
renaming bound variables. But $\vdash\widehat{\Theta}$ is derivable from
$\vdash\Theta^{\prime\prime}$ by the $(\exists)$ rule, i.e. the derivation
$\widehat{\rho}$ of $\vdash\widehat{\Theta}$ is obtained from $\rho$ by
attaching the $(\exists)$ rule. Since
$\mathit{size}(\rho)=\mathit{size}(\pi^{\prime})$, it follows that
$\mathit{size}(\widehat{\rho})=\mathit{size}(\pi)$, and the occurrence net
$\sigma(\widehat{\rho})$ is computed from (5). Applying Proposition 2 once
more, we obtain the desired result.

####  3.2.2. Linguistic derivations

Let $\vdash\Gamma$ be a linguistically well-formed MLL1 sequent containing a
formula $A$ and let $s,t\in Var$, $s\not=t$, have, respectively, a left and a
right free occurrences in $A$, denoted as $s_{l}$ and $t_{r}$. Let $s_{r}$ be
the unique right occurrence of $s$ in $\Gamma$, and $t_{l}$ be the unique left
occurrence of $t$. Let $x,v\in\mathit{Var}$ be such that $x$ does not occur in
$A$ freely, and $s_{r},t_{l}$ do not occur in $\Gamma$ in the scope of a
quantifier $Qv$, $v\in\\{\forall,\exists\\}$.

Let $A^{\prime}=\exists xA[\nicefrac{{x}}{{t_{r}}},\nicefrac{{x}}{{s_{l}}}]$,
and the context $\Gamma^{\prime}$ be obtained from $\Gamma$ by replacing $A$
with $A^{\prime}$. Finally, let
$\widehat{\Gamma}=\Gamma^{\prime}[\nicefrac{{v}}{{t_{l}}},\nicefrac{{v}}{{s_{r}}}]$.
Then the sequent $\vdash\widehat{\Gamma}$ is obtained from $\vdash\Gamma$ by
the $(\exists^{\prime})$ rule. An example of the $(\exists^{\prime})$ rule is
the following

$\cfrac{\vdash\overline{a}(t,z),a(y,s)\parr(\overline{a}(s,y)\otimes
a(z,t))}{\vdash\overline{a}(v,z),\exists
x(a(y,v)\parr(\overline{a}(x,y)\otimes a(z,x)))}~{}(\exists^{\prime}),$ (6)

where the valency $v(a)=(1,1)$. In the notation of the above definition, the
sequents in (6) have the following structure:

$\begin{array}[]{rl}A=a(y,s)\parr(\overline{a}(s,y)\otimes
a(z,t)),&\Gamma=\overline{a}(t,z),a(y,s)\parr(\overline{a}(s,y)\otimes
a(z,t)),\\\ A^{\prime}=\exists x(a(y,s)\parr(\overline{a}(x,y)\otimes
a(z,x))),&\Gamma^{\prime}=\overline{a}(t,z),\exists
x(a(y,s)\parr(\overline{a}(x,y)\otimes a(z,x))),\\\ \widehat{A}=\exists
x(a(y,v)\parr(\overline{a}(x,y)\otimes
a(z,x))),&\widehat{\Gamma}=\overline{a}(v,z),\exists
x(a(y,v)\parr(\overline{a}(x,y)\otimes a(z,x))),\end{array}$

where we also indicated the formula $\widehat{A}$ in the context
$\widehat{\Gamma}$ that corresponds to the formula $A$ in the context
$\Gamma$.

######  Proposition 4.

If $\vdash\Gamma$ is an MLL1 derivable linguistically well-formed sequent and
the sequent $\vdash\widehat{\Gamma}$ is obtained from $\vdash\Gamma$ by the
$(\exists^{\prime})$ rule, then $\vdash\widehat{\Gamma}$ is linguistically
well-formed and MLL1 derivable.

######  Proof 3.3.

Let the notation be as in the definition above. By Proposition 1 any cut-free
derivation $\pi$ of $\vdash\Gamma$ is linguistically marked so it has an
occurrence net $\sigma(\pi)$. Moreover, since $\vdash\Gamma$ is linguistically
well-formed, there are only two occurrences of $s$ and $t$ in $\Gamma$, which
implies $(s_{l},s_{r}),(t_{l},t_{r})\in\sigma(\pi)$.

By renaming, if necessary, bound variables of $A$ we can obtain from $\Gamma$
a linguistically well-formed context $\Theta$ such that $s_{l},t_{r}$ in
$\Theta$ are not in the scope of a quantifier $Qv$,
$Q\in\\{\forall,\exists\\}$. By Proposition 2, the sequent $\vdash\Theta$ is
cut-free derivable with a linguistically marked derivation $\rho$ such that
$\sigma(\rho)=\sigma(\pi)$, i.e. $(s_{l},s_{r}),(t_{l},t_{r})\in\sigma(\rho)$.
It follows from Proposition 3 that $\vdash_{\bf MLL1}\Theta^{\prime}$, where
$\Theta^{\prime}=\Theta[\nicefrac{{v}}{{t_{l}}},\nicefrac{{v}}{{t_{r}}},\nicefrac{{v}}{{s_{l}}},\nicefrac{{v}}{{s_{r}}}]$.

Let $B$ be the formula in $\Theta$ corresponding to $A$ in $\Gamma$ and
$B^{\prime}$ be the formula in $\Theta^{\prime}$ corresponding to $B$ in
$\Theta$. Finally, let $v_{l},v_{r}^{\prime},v_{l}^{\prime},v_{r}$ be the
occurrences of $v$ in $\Theta^{\prime}$ replacing the occurrences
$t_{l},t_{r},s_{l},s_{r}$ in $\Theta$ respectively, and let
$\widehat{B}=\exists
xB^{\prime}[\nicefrac{{x}}{{v_{l}^{\prime}}},\nicefrac{{x}}{{v_{r}^{\prime}}}]$.
It follows from the definition that the formulas $\widehat{B}$ and
$\widehat{A}$, where $\widehat{A}$ is the formula in $\widehat{\Gamma}$
corresponding to $A^{\prime}$ in $\Gamma^{\prime}$, may differ only by
renaming bound variables. Let $\widehat{\Theta}$ be obtained from
$\Theta^{\prime}$ by replacing $B^{\prime}$ with $\widehat{B}$. Then the
sequent $\vdash\widehat{\Theta}$ is derivable from $\vdash\Theta^{\prime}$ by
the $(\exists)$ rule. But $\widehat{\Theta}$, again, may differ from
$\widehat{\Gamma}$ only by renaming bound variables, and the statement follows
from Proposition 2. That $\vdash\widehat{\Gamma}$ is linguistically well-
formed is obvious from counting free left and right occurrences.

Note that on the level of occurrence nets, seen as bipartite graphs, the
$(\exists^{\prime})$ rule does the same gluing as $(\exists)$; only vertex
labels are changed. Derivations of linguistically well-formed sequents using
rules of MLL1 and the $(\exists^{\prime})$ rule and involving only
linguistically well-formed sequents are linguistic derivations.

######  Lemma 5.

Any cut-free MLL1 derivation $\pi$ of a linguistically well-formed sequent
$\vdash\Gamma$ translates to a linguistic derivation.

######  Proof 3.4.

By Proposition 1 the derivation $\pi$ is linguistically marked. We use
induction on $\mathit{size}(\pi)$.

The main case is when the last step in $\pi$ is the $(\exists)$ rule applied
to a cut-free linguistically marked derivation $\pi^{\prime}$ of some non-
linguistically well-formed $\vdash\Gamma^{\prime}$. This means that
$\Gamma^{\prime}$ has four free occurrences of some free variable $v$ (two of
which are renamed when the quantifier is introduced in $\Gamma$). Let
$v_{l}^{\prime},v_{r}^{\prime}$ be, respectively, the left and the right
occurrences of $v$ in $\Gamma^{\prime}$ that become bound in $\Gamma$, and let
$v_{l},v_{r}$ be, respectively, the remaining left and right occurrence of $v$
in $\Gamma^{\prime}$ (inherited by $\Gamma$). We have that $\Gamma^{\prime}$
contains a formula $A$ in which $v_{l}^{\prime},v_{r}^{\prime}$ are located
and $\Gamma$ is obtained from $\Gamma^{\prime}$ by replacing $A$ with the
formula $A^{\prime}=\exists
xA[\nicefrac{{x}}{{v_{r}^{\prime}}},\nicefrac{{x}}{{v_{l}^{\prime}}}]$.

The derivation $\pi^{\prime}$ still has an occurrence net
$\sigma(\pi^{\prime})$. If
$(v_{l}^{\prime},v_{r}^{\prime})\in\sigma(\pi^{\prime})$, then, by Proposition
3, the sequent $\vdash\Gamma^{\prime\prime}$, where
$\Gamma^{\prime\prime}=\Gamma^{\prime}[\nicefrac{{e}}{{v_{l}^{\prime}}},\nicefrac{{e}}{{v_{r}^{\prime}}}]$
and $e\in\mathit{Var}$ is fresh, is derivable with the derivation of the same
size as $\pi^{\prime}$. But $\vdash\Gamma$ is equally well derivable from
$\vdash\Gamma^{\prime\prime}$ by the ($\exists$) rule, and the statement
follows from the induction hypothesis. Otherwise we have
$(v_{l},v_{r}^{\prime}),(v_{l}^{\prime},v_{r})\in\sigma(\pi^{\prime})$. Let
$u,w\in\mathit{Var}$ be fresh and let
$\Gamma^{\prime\prime}=\Gamma^{\prime}[\nicefrac{{u}}{{v_{l}}},\nicefrac{{u}}{{v_{r}^{\prime}}},\nicefrac{{w}}{{v_{l}^{\prime}}},\nicefrac{{w}}{{v_{r}}}]$.
Then $\vdash\Gamma^{\prime\prime}$ is, again by Proposition 3, derivable with
a derivation of the same size as $\pi^{\prime}$. But $\vdash\Gamma$ can be
obtained from $\vdash\Gamma^{\prime\prime}$ by the ($\exists^{\prime}$) rule,
and the statement follows.

Thus, adding the $(\exists^{\prime})$ rule, we obtain a kind of intrinsic
deductive system for the linguistically well-formed fragment. It might seem
though that the usual syntax of first order sequent calculus is not very
natural for such a system. It is not even clear how to write the
$(\exists^{\prime})$ rule in the sequent calculus format concisely. Arguably,
some other representation might be desirable.

##  4\. Tensor type calculus

We assume that we are given an infinite set $\mathit{Ind}$ of indices. They
will be used in all kinds of syntactic objects (terms, types, typing
judgements) that we consider.

Indices will have upper or lower occurrences, which may be free or bound. (The
exact meaning of free and bound occurrences for different syntactic objects
will be defined below.) Following the practice of first order logic, we will
write $e^{[\nicefrac{{i}}{{j}}]}$, respectively $e_{[\nicefrac{{i}}{{j}}]}$,
for the expression obtained from $e$ by replacing the upper, respectively
lower, free occurrence(s) of the index $j$ with $i$, implicitly stating by
this notation that the substituted occurrences of $i$ are free in the resulted
expression. We will write ${I^{\bullet}}(e)$ and ${I_{\bullet}}(e)$ for the
sets of upper and lower indices of $e$ respectively, and $I(e)$ for the pair
$(I^{\bullet}(e),I_{\bullet}(e))$; similarly,
$FI(e)=(FI^{\bullet}(e),FI_{\bullet}(e))$ for sets of free indices.

For pairs of index sets $W_{i}=(U_{i},V_{i})$, $i=1,2$, we write binary
operations componentwise, e.g. $W_{1}\cup W_{2}=(U_{1}\cup U_{2},V_{1}\cup
V_{2})$. We write $W_{1}\perp W_{2}$ for $U_{1}\cap U_{2}=V_{1}\cap
V_{2}=\emptyset$. We also write $(i,j)\perp(U,V)$ for $i\not\in U$, $j\not\in
V$ and $(i,j)\in(U,V)$ for $i\in U$, $j\in V$. Finally, for $W=(U,V)$, we
write $W^{\dagger}=(V,U)$ and $|W|=U\cup V$.

###  4.1. Tensor terms

Given an alphabet $T$ of terminal symbols, tensor terms (over $T$) are the
elements of the free commutative monoid (written multiplicatively with the
unit denoted as 1) generated by the sets

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

satisfying the constraint that any index has at most one lower and one upper
occurrence.

Generating set (7) elements of the form $[w]_{i}^{j}$ are elementary regular
tensor terms and those of the form $[w]$ are elementary singular tensor terms.
(The adjective “tensor” will often be omitted in the following.)

It follows from the definition, that an index in a term cannot occur more than
twice. An index occurring in a 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$. A term is $\beta$-reduced if it has no bound
indices. Terms $t,t^{\prime}$ that can be obtained from each other by renaming
bound indices are $\alpha$-equivalent, $t\equiv_{\alpha}t^{\prime}$.
$\beta$-Reduction of tensor terms is generated by the relations

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

where $\epsilon$ denotes the empty word. Terms related by $\beta$-reduction
are $\beta$-equivalent, notation: $t\equiv_{\beta}s$. The meaning of
$\beta$-reduction will be discussed shortly in Section 4.1.1.

It is easy to see that free indices are invariant under $\beta$-equivalence
and that any term is $\beta$-equivalent to a $\beta$-reduced one. Note also
that $\alpha$-equivalent terms are automatically $\beta$-equivalent, because
their $\beta$-reduced forms coincide. A $\beta$-reduced term is regular if it
is the product of elementary regular terms. A general tensor term is regular
if it is $\beta$-equivalent to a $\beta$-reduced regular term. A tensor term
that is not regular is singular.

The elementary term $[\epsilon]^{j}_{i}$ is denoted as $\delta^{j}_{i}$, more
generally, we write $\delta^{i_{1}\ldots i_{k}}_{j_{1}\ldots j_{k}}$ for the
term $\delta^{i_{1}}_{j_{1}}\cdots\delta^{i_{k}}_{j_{k}}$. When all indices
$i_{1},\ldots,i_{k},j_{1},\ldots,j_{k}$ are pairwise distinct, the term
$\delta^{i_{1}\ldots i_{k}}_{j_{1}\ldots j_{k}}$ is called Kronecker delta.

A term $t$ is lexical if it is regular and not $\beta$-equivalent to some term
of the form $\delta^{i}_{j}\cdot t^{\prime}$ with $(i,j)\in FI(t)$.
Multiplication by Kronecker deltas amounts to renaming indices: if $t$ is a
term with $(i,j)\in FI(t)$ and $(i^{\prime},j^{\prime})\perp I(t)$, then
$\delta_{i}^{i^{\prime}}\cdot
t\equiv_{\beta}t^{[\nicefrac{{i^{\prime}}}{{i}}]}$ and
$\delta_{j^{\prime}}^{j}\cdot
t\equiv_{\beta}t_{[\nicefrac{{j^{\prime}}}{{j}}]}$. For the case of $i=j$, we
have from (8) that $\delta^{i}_{i}\equiv_{\beta}1$.

As for lexical terms they can be equivalently characterized as
$\beta$-equivalent to regular $\beta$-reduced ones of the form
$[w_{1}]^{i_{1}}_{j_{1}}\cdots[w_{k}]^{i_{k}}_{j_{k}}$ where all
$w_{1},\ldots,w_{k}$ are nonempty.

####  4.1.1. Geometric representation

$i$$j$ab$j$$k$cd$\to_{\beta}$abcd$i$$k$ (a)

$i$$i$abc$\to_{\beta}$abc (b)

$\to_{\beta}$${\emptyset}$ (c)

Figure 3. Meaning of $\beta$-reductions

We think of regular terms as bipartite graphs having indices as vertices and
edges labeled with words, the direction of edges being from lower indices to
upper ones.

A regular term $[w]_{i}^{j}$, $i\not=j$, corresponds to a single edge from $i$
to $j$ labeled with $w$, the product of two terms without common indices is
the disjoint union of the corresponding graphs, and a term with repeated
indices corresponds to the graph obtained by gluing edges along matching
vertices. The unit $1$ corresponds to the empty graph. As for singular terms,
such as $[w]^{i}_{i}$, they correspond to closed loops (with no vertices)
labeled with cyclic words (this explains the last relation in (8)). These
arise when edges are glued cyclically. Singular terms are pathological, but we
need them for consistency of definitions. Note however our convention that
when there are no labels, loops evaporate ($\delta^{i}_{i}\equiv_{\beta}1$),
so that the singularity does not arise. The correspondence between terms and
edge-labeled graphs is illustrated in Figure 3. We emphasize that this
geometric representation is an invariant of $\beta$-equivalence.

Finally, we note that a Kronecker delta is a bipartite graph with no edge
labels, and a lexical term, vice versa, is a graph whose every edge has a
nonempty label.

(We also remark that in the system introduced in [Sla21b], which preceded this
work, empty loops were not factored out. This was adequate for problems
considered there.)

####  4.1.2. Remarks on binding and multiplication

We emphasize that binding in terms is global, not restricted to some “scope”.
If $t$ is a subterm (a factor) in a term $s$ and $t$ has a bound index $i$,
then $i$ is bound everywhere in $s$. In particular, if $t$ and $t^{\prime}$
both have a bound index $i$ then the expression $tt^{\prime}$ simply is not a
term (it has four occurrences of $i$). In general, because term multiplication
is only partially defined (concretely, the expression $ts$ is a term if
$I(t)\perp I(s)$), we have to be careful when commuting multiplication with
$\beta$\- or $\alpha$-equivalence. It can be that $t\equiv_{\beta}t^{\prime}$,
but for some term $s$ the product $ts$ is well-defined, while $t^{\prime}s$ is
not a term at all because of index collisions.

As a compensation, multiplication of terms is strictly associative whenever
defined: if $(ts)k$ is a term then $t(sk)$ is also a term and the two are
strictly equal. Also, if $t\to_{\beta}t^{\prime}$, $s\to_{\beta}s^{\prime}$,
$k\to_{\beta}k^{\prime}$ and the expression $tsk$ is a term then
$t^{\prime}s^{\prime}k^{\prime}$ is also a term and
$tsk\to_{\beta}t^{\prime}s^{\prime}k^{\prime}$. Passing to equivalence classes
we have the following: if $t\equiv_{\beta}t^{\prime}$,
$s\equiv_{\beta}s^{\prime}$, $k\equiv_{\beta}k^{\prime}$ and both expressions
$tsk$, $t^{\prime}s^{\prime}k^{\prime}$ are well-defined terms, then
$tsk\equiv_{\beta}t^{\prime}s^{\prime}k^{\prime}$; the same property holds for
$\alpha$-equivalence.

(On the other hand, one could argue that some amount of non-associativity, in
the case of linguistic applications, might be an advantage rather than a
drawback. Such an observation might suggest possible directions for
refinements and modifications for the system introduced in this paper.)

###  4.2. Tensor formulas and types

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}$, the set
$\widetilde{\mathit{Fm}}$ of tensor pseudoformulas is built according to the
grammar in Figure 4, 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 atomic pseudoformulas.

$\begin{array}[]{c}\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}_{-}.\\\\[5.69046pt]
\widetilde{\mathit{At}}=\\{p_{j_{1}\ldots j_{n}}^{i_{1}\ldots
i_{m}}|~{}p\in\mathit{Lit},v(p)=(m,n),i_{1},\ldots,i_{m},j_{1},\ldots,j_{n}\in\mathit{Ind}\\}.\\\\[5.69046pt]
\widetilde{\mathit{Fm}}::=\widetilde{\mathit{At}}|(\widetilde{\mathit{Fm}}\otimes\widetilde{\mathit{Fm}})|(\widetilde{\mathit{Fm}}\parr\widetilde{\mathit{Fm}})|\nabla^{i}_{j}\widetilde{\mathit{Fm}}|\triangle^{i}_{j}\widetilde{\mathit{Fm}},~{}i,j\in\mathit{Ind},~{}i\not=j.\\\\[5.69046pt]
\overline{p^{i_{1},\ldots,i_{n}}_{j_{1},\ldots,j_{m}}}=\overline{p}_{{i_{n}},\ldots,{i_{1}}}^{{j_{m}},\ldots,{j_{1}}}.\\\\[5.69046pt]
\overline{A\otimes B}=\overline{B}\wp\overline{A},\quad\overline{A\wp
B}=\overline{B}\otimes\overline{A},\quad\overline{\nabla_{i}^{j}A}=\triangle^{i}_{j}\overline{A},\quad\overline{\triangle_{i}^{j}A}=\nabla^{i}_{j}\overline{A}.\end{array}$

Figure 4. ETTC Language

Duality $\overline{(.)}$ is not a connective or operator, but is definable.
The symbols $\nabla,\triangle$ are binding operators. They bind indices
exactly in the same way as quantifiers bind variables. The operator
$Q\in\\{\nabla,\triangle\\}$ in front of an expression $Q^{i}_{j}A$ has $A$ as
its scope and binds all lower occurrences of $i$, respectively, upper
occurrences of $j$ in $A$ that are not already bound by some other operator. A
pseudoformula $A$ is well-formed when any index has at most one free upper and
one free lower occurrence in $A$, and every binding operator binds exactly one
lower and one upper index occurrence. A well-formed pseudoformula $A$ is a
tensor formula or a pseudotype. If moreover $FI^{\bullet}(A)\cap
FI_{\bullet}(A)=\emptyset$ then $A$ is a tensor type. Note that definitions of
free and bound indices for tensor terms and tensor formulas are different. In
particular, unlike terms, general tensor formulas (that are not tensor types)
may have repeated free indices (i.e. an index may have both an upper and a
lower free occurrence). Also, unlike the case of terms, binding in tensor
formulas is local, visible only in the scope of a binding operator.

Tensor formulas that can be obtained from each other by renaming bound indices
are $\alpha$-equivalent. The set of atomic types (i.e. coming from atomic
pseudoformulas) is denoted as $\mathit{At}$.

A tensor pseudotype context $\Gamma$, or, simply, a tensor context is a finite
multiset of pseudotypes such that for any two distinct $A,B\in\Gamma$ we have
that $FI(A)\perp FI(B)$. The pseudotype context $\Gamma$ is a type context if
$FI^{\bullet}(\Gamma)\cap FI_{\bullet}(\Gamma)=\emptyset$, where
$FI(\Gamma)=\bigcup\limits_{A\in\Gamma}FI(A)$.

An ordered tensor context $\Gamma$ is defined identically with the difference
that $\Gamma$ is a sequence rather than a multiset. Again, in a pseudotype
context an index can have two free occurrences, once as a lower one and once
as an upper one. For example the expression $a^{i},\overline{a_{i}}$ is a
legitimate pseudotype context, but not a type context.

###  4.3. Sequents and typing judgements

A pseudotyping judgement $\Sigma$ is an expression of the form $t::\Gamma$,
where $\Gamma$ is a tensor context and $t$ is a tensor term such that

$I(t)\perp FI(\Gamma),\mbox{ }FI(t)\cup FI(\Gamma)=(FI(t)\cup
FI(\Gamma))^{\dagger}.$ (9)

When $\Gamma$ is a type (not just pseudotype) context, we say that $\Sigma$ is
a tensor typing judgement.

A tensor sequent is an expression of the form $\vdash\Sigma$, where $\Sigma$
is a pseudotyping judgement.

An ordered pseudotyping judgement and ordered tensor sequent are defined
identically with the difference that the tensor context should be ordered. (In
the paper [Sla21b] preceding this work we used a slightly different notation
for tensor sequents with the term to the left of the turnstile.)

Spelling out defining relation (9): if we erase from $\Sigma$ all bound
indices of $\Gamma$, then every remaining index has exactly one upper and one
lower occurrence. When $\Sigma$ is a tensor typing judgement, we have
$FI(t)=FI(\Gamma)^{\dagger}$, i.e. every index occurring in $\Sigma$ freely
has exactly one free occurrence in $\Gamma$ and one in $t$. In this case we
read $\Sigma$ as “$t$ has type $\Gamma$”. A pseudotyping judgement is not a
genuine typing judgement if there are repeated free indices in the tensor
context (i.e. some index in the tensor context has both an upper and a lower
free occurrence). When $t=1$ we write the judgement $\Sigma$ simply as
$\Gamma$. When $\Gamma$ consists of a single formula $F$, we write $\Sigma$ as
$t:F$. When $t$ is $\beta$-reduced or lexical we say that $\Sigma$ is,
respectively, $\beta$-reduced or lexical.

The ordered and unordered contexts and sequents correspond to two possible
formulations of sequent calculus. We will generally use the unordered version,
but for geometric representation of tensor sequents and sequent rules we need
to consider explicit Exchange rule. The definitions below apply to both
versions.

If $t,t^{\prime}$ are terms with $t\equiv_{\beta}t^{\prime}$ then the
pseudotyping judgements $t::\Gamma$ and $t^{\prime}::\Gamma$ are
$\beta$-equivalent, $t::\Gamma\equiv_{\beta}t^{\prime}::\Gamma$.

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

$\begin{array}[]{c}t\equiv_{\alpha}t^{\prime},F\equiv_{\alpha}F^{\prime}\Rightarrow
t::\Gamma,F\equiv_{\alpha}t^{\prime}::\Gamma,F^{\prime},\\\ i\in
FI^{\bullet}(t)\cup FI^{\bullet}(\Gamma),~{}j\mbox{ fresh }\Rightarrow
t::\Gamma\equiv_{\alpha}(t::\Gamma)^{[\nicefrac{{j}}{{i}}]}_{[\nicefrac{{j}}{{i}}]}.\end{array}$

$\eta$-Expansion of pseudo-typing judgements is the transitive closure of the
relation defined by

$i\in FI^{\bullet}(\Gamma)\cap FI_{\bullet}(\Gamma),~{}j\mbox{ fresh
}\Rightarrow
t::\Gamma\to_{\eta}\delta^{i}_{j}t::\Gamma^{[\nicefrac{{j}}{{i}}]},~{}t::\Gamma\to_{\eta}\delta_{i}^{j}t::\Gamma_{[\nicefrac{{j}}{{i}}]}.$

$\eta$-Reduction of judgements is the opposite relation of $\eta$-expansion,
$\eta$-equivalence ($\equiv_{\eta}$) is the symmetric closure of
$\eta$-expansion.

Tensor sequents $\vdash\Sigma$, $\vdash\Sigma^{\prime}$ are, respectively
$\alpha$-, $\beta$\- or $\eta$-equivalent iff $\Sigma$ and $\Sigma^{\prime}$
are. $\eta$-Expansion removes from the tensor context free index repetitions
by renaming them and, simultaneously, adds Kronecker deltas to the term as a
compensation. Typing judgements have no repeated free indices in the tensor
context and are, thus, $\eta$-long in the sense that they cannot be
$\eta$-expanded. A general pseudotyping judgement could be thought as a
shorthand notation for its $\eta$-expansion; the sequent $\vdash
a^{i},\overline{a}_{i}$ “morally” is a short for
$\vdash\delta^{j}_{i}::a^{i},\overline{a}_{j}$. Lexical pseudotyping
judgements, on the contrary, are $\eta$-reduced in the sense that they are not
$\eta$-expansions of anything, for having no Kronecker deltas in the term.
Lexical typing judgements, at once ${\eta}$-long and $\eta$-reduced, will have
natural interpretation as nonlogical axioms. It is easy to see that any
pseudotyping judgement has (many $\alpha\beta$-equivalent) $\eta$-long and
$\eta$-reduced forms.

####  4.3.1. Geometric representation

$\gamma\delta$$\beta\alpha$$\overbrace{i}$${a}$$j$$\overbrace{~{}\quad
k\quad}$$l$${b}$$k$$\overbrace{~{}\quad\quad~{}}$$m$${c}$$\Leftrightarrow$$[\gamma\delta]_{m}^{i}\cdot[\beta\alpha]_{j}^{l}::a_{i}\otimes
b^{j}_{kl},c^{km}$ Figure 5. Tensor sequent

If tensor terms can be thought as edge-labeled graphs, then ordered
pseudotyping judgements or tensor sequents correspond to particular pictorial
representations of these graphs. Especially natural the representation is for
genuine typing judgements, so we discuss it first.

Let $\Sigma=t::\Gamma$, where $t$ is $\beta$-reduced, be an ordered typing
judgement, i.e. such that $FI(t)=FI(\Gamma)^{\dagger}$. (When the term is not
$\beta$-reduced, we replace it with its $\beta$-reduced form.) We interpret
free indices of $\Gamma$ as vertices. For a pictorial representation we equip
the set of vertices with a particular ordering corresponding to their
positioning in $\Gamma$. Say, indices occurring in the same formula are
ordered from left to right, from top to bottom (first come the upper indices,
then come the lower ones), and the whole set of free indices occurring in
$\Gamma$ is ordered lexicographically according to the ordering of formulas in
$\Gamma$, i.e. indices occurring in $A$ come before indices occurring in $B$
if $A$ comes before $B$ in $\Gamma$. We depict them aligned, say, horizontally
in this order.

The edge-labeled graph on these vertices is constructed as follows. Free
indices in $\Gamma$ are in bijection with free indices/vertices of $t$ and we
connect them with labeled edges corresponding to factors of $t$. That is, for
any index $\mu\in FI^{\bullet}(\Gamma)$ we have that $\mu\in FI_{\bullet}(t)$
and there is unique $\nu\in FI^{\bullet}(t)$ such that $t$ has the form
$t=[w]^{\nu}_{\mu}t^{\prime}$, so that $t$, seen as a graph, contains and edge
from $\mu$ to $\nu$ labeled with the word $w$. It follows that $\nu\in
FI_{\bullet}(\Gamma)$, and we draw an edge from $\mu$ to $\nu$ with the label
$w$. In this way every index/vertex in $FI(\Gamma)$ becomes adjacent to a
(unique) edge.

The constructed graph is a specific geometric representation of the graph
corresponding to $t$, the representation being induced by a particular
ordering of vertices. Note that the direction of edges is from upper indices
of $\Gamma$ to lower ones (upper indices of $\Gamma$ correspond to lower
indices of $t$ and vice versa). Also, note that bound indices of $\Gamma$ are
not in the picture.

When $\Sigma=t::\Gamma$ is only a pseudo-typing judgement, i.e. there are
repeated free indices in $\Gamma$, we treat it as a short expression for its
$\eta$-long expansion $t^{\prime}::\Gamma^{\prime}$. Any pair of repeated free
index occurrences in $\Gamma$ corresponds to a Kronecker delta, i.e. an edge
in $t^{\prime}$, connecting two distinct vertices and carrying no label. In
this case, for geometric representation of $\Sigma$, we take as vertices the
set of free index occurrences rather than indices in $\Gamma$ and order them
in the same way a above. In the picture, we connect every pair of repeated
free indices/vertices of $\Gamma$ with an edge carrying no label and directed
from the upper occurrence to the lower one. The prescription for the remaining
indices has already been described. An example of a concrete pseudotyping
judgement representation is given in Figure 5.

Observe that $\alpha\beta\eta$-equivalent pseudo-typing judgements or sequents
have identical geometric representation (up to vertex labeling). Usually it is
convenient to erase indices from the picture, avoiding notational clutter. For
example, the pseudotyping judgement
$[xy]_{m^{\prime}}^{i^{\prime}}\cdot[ba]_{j}^{l}::a_{i^{\prime}}\otimes
b^{j}_{k^{\prime}l},c^{k^{\prime}m^{\prime}}$ is $\alpha$-equivalent to the
one in Figure 5, while
$[xy]_{m}^{i}\cdot[ba]_{j}^{l}\cdot\delta_{k}^{\mu}::a_{i}\otimes b^{j}_{\mu
l},c^{km}$ is an $\eta$-expansion of the latter. Also, we note that lexical
typing judgements correspond to pictures where every edge has a non-empty
label.

###  4.4. Sequent calculus

####  4.4.1. Rules

We defined tensor sequents in order to define tensor grammars, which generate
languages from a given lexicon of typing judgements. But at first, we
introduce the underlying purely logical system of extended tensor type
calculus (ETTC). (The title “extended”, introduced in [Sla21b], refers to
usage of binding operators, which extend plain types of MLL.) The system of
ETTC, being cut-free, does not use any non-logical axioms and is independent
from terminal alphabets.

Our default formulation involves unordered tensor sequents. For geometric
representation of the rules one needs an ordered formulation with the explicit
rule for exchange; this will be discussed in the next subsection. The system
of extended tensor type calculus (ETTC) is given by the rules in Figure
LABEL:ETTC, where sequents are unordered, and it is assumed that all
expressions are well-formed, i.e. there are no forbidden index repetitions and
upper occurrences match lower ones.

The requirement that all expressions in Figure LABEL:ETTC must be well-formed
is not to be overlooked. It imposes severe restrictions on the rule premises.
These are spelled out in Figure LABEL:restrictions (recall our shorthand
notation for pairs of sets introduced in the beginning of this section).

$\begin{array}[]{c}\cfrac{A\in\mathit{At}}{\vdash
A,\overline{A}}({\rm{Id}})~{}~{}~{}\cfrac{\vdash t::\Gamma,A~{}\vdash
s::\overline{A},\Theta}{\vdash
ts::\Gamma,\Theta}({\rm{Cut}})~{}~{}~{}\cfrac{\vdash
t::\Gamma,~{}t\equiv_{\beta}t^{\prime}}{\vdash
t^{\prime}::\Gamma}~{}(\equiv_{\beta})\\\\[11.38092pt] \cfrac{\vdash
t::\Gamma}{\vdash\delta^{i}_{j}t::\Gamma^{[\nicefrac{{j}}{{i}}]}}(\alpha\eta^{\to})~{}~{}~{}\cfrac{\vdash\delta^{i}_{j}t::\Gamma^{[\nicefrac{{j}}{{i}}]}}{\vdash
t::\Gamma}(\alpha\eta^{\leftarrow})~{}~{}~{}\cfrac{\vdash
t::\Gamma}{\vdash\delta^{j}_{i}t::\Gamma_{[\nicefrac{{j}}{{i}}]}}(\alpha\eta_{\to})~{}~{}~{}\cfrac{\vdash\delta^{i}_{j}t::\Gamma_{[\nicefrac{{i}}{{j}}]}}{t\vdash\Gamma}(\alpha\eta_{\leftarrow})\\\\[11.38092pt]
\cfrac{\vdash t::\Gamma,A,B}{\vdash t::\Gamma,A\parr
B}(\parr)~{}~{}~{}\cfrac{\vdash t::\Gamma,A~{}\vdash s::B,\Theta}{\vdash
ts::\Gamma,A\otimes
B,\Theta}(\otimes)~{}~{}~{}\cfrac{\vdash\delta_{\nu}^{\mu}t::\Gamma,A}{\vdash
t::\Gamma,\nabla^{\mu}_{\nu}A}(\nabla)~{}~{}~{}\cfrac{\vdash
t::A,\Gamma}{\vdash\delta^{\nu}_{\mu}t::\triangle_{\nu}^{\mu}A,\Gamma}(\triangle)\end{array}$

(a)

$\begin{array}[]{c}(\alpha\eta^{\to}):~{}i\in
FI^{\bullet}(\Gamma),~{}j\not\in|I(t)|\cup|FI(\Gamma)|.\quad\quad(\alpha\eta_{\to}):~{}i\in
FI_{\bullet}(\Gamma),~{}j\not\in|I(t)|\cup|FI(\Gamma)|.\\\\[2.84544pt]
(\otimes):~{}|I(t)|\cap|I(s)|=|FI(\Gamma,A)|\cap|FI(B,\Theta)|=\emptyset,~{}I(t)\perp
FI(B,\Theta),~{}I(s)\perp FI(\Gamma,A).\\\\[2.84544pt]
(\mbox{Cut}):~{}I(t)\perp I(s),~{}FI(\Gamma)\perp FI(\Theta),~{}FI(t)\cap
FI(s)^{\dagger}\subseteq FI(\Gamma)^{\dagger}\cap FI(\Theta)\subseteq
FI(A).\\\\[2.84544pt] (\nabla),(\triangle):~{}(\nu,\mu)\in FI(A).\end{array}$

(b)

Figure 6. ETTC sequent calculus

######  Proposition 6.

The rules in Figure LABEL:ETTC transform well-formed tensor sequents to well-
formed tensor sequents iff the premises satisfy the conditions in Figure
LABEL:restrictions.

######  Proof 4.1.

  * •

$(\alpha\eta^{\to})$, $(\alpha\eta_{\to})$: Sufficiency is obvious. The rule
adds two matching occurrences of the fresh index $j$, and one free occurrence
of $i$ in the tensor context gets moved to the term without changing the
polarity. Let us check necessity. For definiteness, consider the
$(\alpha\eta^{\to})$ rule, the other case being identical.

There are two possibilities for the term in the conclusion of the rule to be
well-formed. Either $i\in FI_{\bullet}(t)$, $i\not\in I^{\bullet}(t)$ or
$i\not\in|I(t)|$. If the first possibility holds, then it must be that $i\in
FI^{\bullet}(\Gamma)$ for the premise to be well-formed. Assume that the
second possibility holds. Then it must be that $i\in
FI_{\bullet}(\Gamma^{[\nicefrac{{j}}{{i}}]})=FI_{\bullet}(\Gamma)$ for the
conclusion of the rule to be well-formed. But $i\in FI_{\bullet}(\Gamma)$ and
$i\not\in|I(t)|$ implies, again, $i\in FI^{\bullet}(\Gamma)$ or the premise is
not well-formed. Thus, in both cases the condition $i\in FI^{\bullet}(\Gamma)$
must hold.

Consider the second condition, $j\not\in|I(t)|\cup|FI(\Gamma)|$. We note that
the conclusion of the rule has a free upper occurrence of $j$ located in the
tensor context (the one replacing $i$ in $\Gamma$) and an occurrence of $j$ in
the term located in the factor $\delta^{i}_{j}$. If $j\in|FI(\Gamma)|$ then
there is a third occurrence of $j$ in the conclusion located in the tensor
context, and if $j\in|I(t)|$ then there is a third occurrence of $j$ in the
conclusion located in the term. In both cases the conclusion is not well-
formed.

  * •

$(\otimes):$ Sufficiency is very easy. We also need to check that all
conditions are indeed necessary. Consider, for example, the first one that
$|I(t)|\cap|I(s)|=\emptyset$. Assume, for a contradiction, that
$i\in|I(t)|\cap|I(s)|$. For the term $ts$ in the conclusion to be well-formed,
it must be that $i$ occurs in $t$ and in $s$ freely (without repetitions) and
with opposite polarities. It follows that $i$ also has free occurrences in the
contexts $\Gamma,A$ and $B,\Theta$, otherwise the premises of the rule are not
well-formed pseudo-typing judgements. But then the conclusion of the rule is
not well-formed, because $(i,i)\in I(ts)\cap FI(\Gamma,A\otimes B,\Theta)$.
The other conditions are obtained similarly.

  * •

$(\mbox{Cut})$: Similar to the $(\otimes)$ case.

  * •

$(\nabla),(\triangle)$: The condition is necessary simply for the formula in
the conclusion to be well-formed. For sufficiency we observe that there are
also an upper and a lower free occurrence of $\mu$ and $\nu$ respectively in
the premise, and a simple analysis shows that indices in the conclusion match
correctly.

####  4.4.2. Geometric meaning

$A$$\overline{A}$$({\rm{Id}})$$t$$s$$\Gamma$$A$$\Theta$$\overline{A}$$\Rightarrow$$t$$\Gamma$$s$$\Theta$$(\mbox{Cut})$$t$$\Gamma$$A$$\Theta$$B$$\Rightarrow$$t$$\Gamma$$A$$\Theta$$B$$(\mbox{Ex})$

(a)

$t$$\Gamma$$\overbrace{~{}~{}\quad~{}~{}}$$\overbrace{\quad\quad\quad}$$A$$\nu$$\mu$$\Rightarrow$$t$$\Gamma$$\overbrace{~{}~{}\quad~{}~{}}$$\nabla_{\nu}^{\mu}A$$\overbrace{\quad\quad\quad}$
(b)

$t$$\Gamma$$\overbrace{~{}~{}\quad~{}~{}}$$\overbrace{\quad\quad\quad}$$A$$\nu$$\mu$$\Rightarrow$$t$$\Gamma$$\overbrace{~{}~{}\quad~{}~{}}$$\overbrace{\quad\quad\quad}$$\triangle_{\nu}^{\mu}A$
(c)

Figure 7. Pictures for ETTC

In order to give geometric representation of the ETTC rules we need to
consider ordered sequents and enrich the system with the rule of exchange

$\cfrac{\vdash t::\Gamma,A,B,\Theta}{\vdash
t::\Gamma,B,A,\Theta}~{}({\rm{Ex}}).$

Clearly, this results in an equivalent formulation. Then, using geometric
representation of tensor sequents, the rules of ETTC can be illustrated as in
Figure 7.

The identity/structure group $\\{({\rm{Id}}),({\rm{Cut}}),({\rm{Ex}}))\\}$ is
schematically illustrated in Figure LABEL:structural_rules_picture. As for the
multiplicative group, the $(\otimes)$ rule puts two graphs together in the
disjoint union and the $(\parr)$ rule does nothing in the picture. The
$(\equiv_{\beta})$ and $(\alpha\eta)$ rules do not change the picture either
(except for vertex labels); they could be thought of as coordinate
transformations.

Finally, the $(\triangle)$ rule glues together two indices/vertices, and the
$(\nabla)$ rule is applicable only in the case when the corresponding
indices/vertices are connected with an edge carrying no label. Then this edge
is erased from the picture completely (the information about the erased edge
is stored in the introduced type). This is illustrated in Figures
LABEL:nabla_geometrically, LABEL:delta_geometrically (the lines of dots denote
that there might be other vertices around).

####  4.4.3. Towards first order translation

We will discuss the exact relationship of ETTC with the linguistic fragment of
MLL1 in due course, but the outline of their correspondence is the following.
Indices in tensor formulas correspond to variables in predicate formulas, with
upper/lower polarities of indices corresponding to left/right polarities of
variables. Multiplicative connectives translate to themselves, while the
binding operators $\nabla/\triangle$ of ETTC correspond to the
$\forall/\exists$ quantifiers in the linguistic fragment. A quantifier in the
linguistic fragment binds exactly two variable occurrences of opposite
polarities. These two bound occurrences in a predicate formula translate to
two different indices bound by the corresponding operator in the tensor
formula: $\forall xA(x,x)$ translates to $\nabla^{i}_{j}A^{j}_{i}$.

Tensor sequents may also contain terms, and these do not translate to the
first order language directly. However, we note that Kronecker deltas behave
much like (some rudimentary versions of) equalities to the left of the
turnstile. Typically, the tensor sequent $\vdash\delta^{i_{1}\ldots
i_{k}}_{j_{1}\ldots j_{k}}::\Gamma$ could be thought intuitively as the
sequent

$j_{1}=i_{1},\ldots,j_{k}=i_{k}\vdash\Gamma$

in a first order language with equality. At least, the $(\alpha\eta)$ rules
are consistent with such an interpretation. And the $(\equiv_{\beta})$ rule,
in the absence of terminal symbols, amounts to the equivalences
$\delta^{i}_{j}\delta^{j}_{k}\equiv_{\beta}\delta^{i}_{k}$ and
$\delta^{i}_{i}\equiv_{\beta}1$, which, basically correspond to transitivity
and reflexivity of equality (if we translate the term $1$ as the empty
context). This intuition, probably, could be developed more formally.

####  4.4.4. Properties

The crucial property of cut-elimination in ETTC will be established in a
separate section below. Here we collect some simple observations about the
system.

######  Proposition 7.

In ETTC:

  1. (1)

the sequent $\vdash F,\overline{F}$ is derivable for any formula $F$;

  2. (2)

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

  3. (3)

$\beta\eta$-equivalent sequents are cut-free derivable from each other;

  4. (4)

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

$\mathord{}\ \vdash\ \mathord{}$$\overline{A},A$ ($\alpha\eta^{\to}$)
$\mathord{}\ \vdash\
\mathord{}$$\delta^{\nu}_{y}::\overline{A},A^{[\nicefrac{{y}}{{\nu}}]}$
($\alpha\eta_{\to}$) $\mathord{}\ \vdash\ \mathord{}$$\delta^{x\nu}_{\mu
y}::\overline{A},A^{[\nicefrac{{y}}{{\nu}}]}_{[\nicefrac{{x}}{{\mu}}]}$
($\triangle$) $\mathord{}\ \vdash\ \mathord{}$$\delta^{\mu x\nu}_{\nu\mu
y}::\triangle^{\nu}_{\mu}\overline{A},A^{[\nicefrac{{y}}{{\nu}}]}_{[\nicefrac{{x}}{{\mu}}]}$
($\equiv_{\beta}$) $\mathord{}\ \vdash\
\mathord{}$$\delta^{x}_{y}::\triangle^{\nu}_{\mu}\overline{A},A^{[\nicefrac{{y}}{{\nu}}]}_{[\nicefrac{{x}}{{\mu}}]}$
($\nabla$) $\mathord{}\ \vdash\
\mathord{}$$\triangle^{\nu}_{\mu}\overline{A},\nabla^{x}_{y}(A^{[\nicefrac{{y}}{{\nu}}]}_{[\nicefrac{{x}}{{\mu}}]})$

(a)

$\quad\begin{array}[]{c}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
51.6511pt\hbox{\vbox{\vbox{\hbox{\hskip 4.0pt\hbox{$\mathord{}\ \vdash\
\mathord{}$}\hbox{$t::\Gamma\quad(i,i)\in FI(\Gamma)$}\hskip
4.0pt}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to119.00107pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
3.0pt($\alpha\eta^{\to}$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
0.0pt\hbox{\hskip 4.0pt\hbox{$\mathord{}\ \vdash\
\mathord{}$}\hbox{$\delta^{i}_{j}t::\Gamma^{[\nicefrac{{j}}{{i}}]}$}\hskip
4.0pt}}}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to63.37772pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
3.0pt($\alpha\eta_{\leftarrow}$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
0.0pt\hbox{\hskip 4.0pt\hbox{$\mathord{}\ \vdash\
\mathord{}$}\hbox{$t::\Gamma^{[\nicefrac{{j}}{{i}}]}_{[\nicefrac{{j}}{{i}}]}$}\hskip
4.0pt}}}}\ignorespaces\\\ \\\
\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
51.6511pt\hbox{\vbox{\vbox{\hbox{\hskip 4.0pt\hbox{$\mathord{}\ \vdash\
\mathord{}$}\hbox{$t::\Gamma\quad i\in FI_{\bullet}(t)\cap
FI^{\bullet}(\Gamma)$}\hskip 4.0pt}\vskip-2.8pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox to144.43367pt{\xleaders\hrule\hfill}\lower
2.3pt\hbox{\hskip
3.0pt($\alpha\eta^{\to}$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
0.0pt\hbox{\hskip 4.0pt\hbox{$\mathord{}\ \vdash\
\mathord{}$}\hbox{$\delta^{i}_{j}t::\Gamma^{[\nicefrac{{j}}{{i}}]}$}\hskip
4.0pt}}}\vskip-3.06667pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox to63.37772pt{\xleaders\hrule\hfill}\lower
2.03334pt\hbox{\hskip
3.0pt($\equiv_{\beta}$)}}\vskip-3.06667pt\nointerlineskip\hbox{\hskip
0.0pt\hbox{\hskip 4.0pt\hbox{$\mathord{}\ \vdash\
\mathord{}$}\hbox{$t_{[\nicefrac{{j}}{{i}}]}::\Gamma^{[\nicefrac{{j}}{{i}}]}$}\hskip
4.0pt}}}}\ignorespaces\end{array}$

(b)

Figure 8. To the proof of Proposition 7

######  Proof 4.2.

Claim (i) is easy. Claim (ii) is established by induction on $A$,
$A^{\prime}$, the base cases being $F=Q^{\mu}_{\nu}A$,
$F^{\prime}=Q^{x}_{y}(A^{[\nicefrac{{y}}{{\nu}}]}_{[\nicefrac{{x}}{{\mu}}]})$,
$Q\in\\{\nabla,\triangle\\}$. A derivation for this case is shown in Figure
LABEL:alpha_equiv_formulas_are_equivalent_figure. For claim (iii) note that
$\beta$-equivalent sequents are derivable from each other by the
$(\equiv_{\beta})$ rule, and if $\Sigma^{\prime}$ is a one-step
$\eta$-expansion of $\Sigma$ then $\Sigma^{\prime}$ is derivable from
$\vdash\Sigma$ by the $(\alpha\eta^{\to})$ rule, and $\vdash\Sigma$ from
$\vdash\Sigma^{\prime}$ by the $(\alpha\eta_{\leftarrow})$ rule.

Finally, consider claim (iv). There are two relations generating
$\alpha$-equivalence of sequents. The first one involves sequents of the form
$\vdash t::\Gamma,F$ and $\vdash t^{\prime}::\Gamma,F^{\prime}$, where
$t\equiv_{\alpha}t^{\prime}$, $F\equiv_{\alpha}F^{\prime}$. The statement
follows from (ii), (iii). The second relation involves sequents of the form
$\vdash\Sigma$ and
$\vdash\Sigma^{[\nicefrac{{j}}{{i}}]}_{[\nicefrac{{j}}{{i}}]}$. This has two
subcases: either the index $i$ has two free occurrences in the pseudotype
context in $\Sigma$, or it has one free occurrence in the pseudotype context
and one in the term. Derivations for both situations are shown in Figure
LABEL:Claim_iv.

####  4.4.5. Implicational types

$\overline{A}$$B$string1string2

(a)

$\overline{A}$$B$string

$\overline{A}$$B$string

(b)

$A$st$\overline{A}$$B$$\Longrightarrow$st$B$$=$
ts$A$st$\overline{A}$$B$$\Longrightarrow$st$B$$=$ st (c)

Figure 9. Geometry of implicational types

The implicational types of LC can be translated to ETTC as

$(b/a)^{i}_{j}=\nabla^{\mu}_{\nu}(b^{i}_{\mu}\wp\overline{a}_{j}^{\nu}),\quad(a\backslash
b)^{i}_{j}=\nabla^{\mu}_{\nu}(\overline{a}_{\mu}^{i}\wp b_{j}^{\nu})$ (10)

(compare with translation to MILL1 in Figure LABEL:LC2MILL). Let us dicuss the
geometric meaning of this.

Terms of (pseudo-)type $\nabla^{\mu}_{\nu}A$ encode a particular “subtype” of
$A$: consisting of terms whose indices/vertices corresponding to $\mu$ and
$\nu$ are connected with an edge carrying no label. Let $A,B$ be types with
exactly one free upper and one free lower index. Then regular terms of type
$A$ or $B$ are, essentially, strings. As for the implication type $A\multimap
B$, which we encode in ETTC as $\overline{A}\parr B$ for definiteness (the
alternative encoding is $B\parr\overline{A}$), its terms are rather pairs of
strings, as Figure LABEL:implication_general_form suggests. There are two
“degenerate subtypes”, shown in Figure LABEL:subtypes, where one of the two
strings is empty. (They are degenerate, for example, for having no lexical
terms). These are precisely “subtypes” of the kind encoded by $\nabla$. Now,
it is easy to see that terms of the first “subtype” act on type $A$ terms by
multiplication (concatenation) on the left, and terms of the second one act by
multiplication on the right (see Figure LABEL:slash_action). That is, the two
“degenerate subtypes” of the general, “undirected” implication type correspond
precisely to two implicational types of LC. Note, however, that the
translations in (10) use both possible encodings of the undirected
implication, one for the left LC implication and the other one for the right
implication. This choice seems most natural.

##  5\. Cut-elimination

###  5.1. $\eta$-Long fragment

$\cfrac{p\in Lit}{\vdash\delta_{i_{1}\ldots i_{n}l_{m}\ldots
l_{1}}^{k_{n}\ldots k_{1}j_{1}\ldots j_{m}}::p^{i_{1}\ldots
i_{n}}_{j_{1}\ldots j_{m}},\overline{p}^{l_{1}\ldots l_{m}}_{k_{1}\ldots
k_{n}}}({\rm{Id}}_{\eta_{\to}})~{}\cfrac{\vdash\delta^{i}_{j}t::\Gamma,A_{[\nicefrac{{i}}{{\mu}}]}^{[\nicefrac{{j}}{{\nu}}]}}{\vdash
t::\Gamma,\nabla^{\mu}_{\nu}A}(\nabla_{\equiv_{\alpha}})~{}\cfrac{\vdash
t::A_{[\nicefrac{{i}}{{\mu}}]}^{[\nicefrac{{j}}{{\nu}}]},\Gamma}{\vdash\delta^{j}_{i}t::\triangle^{\mu}_{\nu}A,\Gamma}(\triangle_{\equiv_{\alpha}})$

(a)

$\mathord{\vdash\delta^{i}_{j}t}\ ::\
\mathord{}$$\Gamma,A_{[\nicefrac{{i}}{{\mu}}]}^{[\nicefrac{{j}}{{\nu}}]}$
($\alpha\eta^{\to}$) $\mathord{\vdash\delta^{ji}_{\nu j}t}\ ::\
\mathord{}$$\Gamma,A_{[\nicefrac{{i}}{{\mu}}]}$ ($\alpha\eta_{\to}$)
$\mathord{\vdash\delta^{\mu ji}_{i\nu j}t}\ ::\ \mathord{}$$\Gamma,A$
($\equiv_{\beta}$) $\mathord{\vdash\delta^{\mu}_{\nu}t}\ ::\
\mathord{}$$\Gamma,A$ ($\nabla$) $\mathord{\vdash t}\ ::\
\mathord{}$$\Gamma,\nabla^{\mu}_{\nu}A$

(b)

$\mathord{\vdash t}\ ::\
\mathord{}$$A_{[\nicefrac{{i}}{{\mu}}]}^{[\nicefrac{{j}}{{\nu}}]},\Gamma$
($\alpha\eta^{\to}$) $\mathord{\vdash\delta^{j}_{\nu}t}\ ::\
\mathord{}$$A_{[\nicefrac{{i}}{{\mu}}]},\Gamma$ ($\alpha\eta_{\to}$)
$\mathord{\vdash\delta^{\mu j}_{i\nu}t}\ ::\ \mathord{}$$A,\Gamma$
($\triangle$) $\mathord{\vdash\delta^{\nu\mu j}_{\mu i\nu}t}\ ::\
\mathord{}$$\triangle_{\nu}^{\mu}A,\Gamma$ ($\equiv_{\beta}$)
$\mathord{\vdash\delta^{j}_{i}t}\ ::\
\mathord{}$$\triangle_{\nu}^{\mu}A,\Gamma$

(c)

Figure 10. ${\bf ETTC}_{\eta\to}$

The $\eta$-long fragment ${\bf ETTC}_{\eta\to}$ is ETTC restricted to
$\eta$-long sequents, i.e. to typing judgements. The fragment can be given a
separate axiomatization. The system ${\bf ETTC}_{\eta\to}$ is obtained from
ETTC by removing the $(\alpha\eta)$ rules and replacing the $({\rm{Id}})$
axioms with their $\eta$-long forms $({\rm{Id}}_{\eta_{\to}})$ and the
$(\nabla)$, $(\triangle)$ rules with their closures
$(\nabla_{\equiv_{\alpha}})$, $(\triangle_{\equiv_{\alpha}})$ under
$\alpha$-equivalence shown in Figure LABEL:ETTC_eta-long.

######  Proposition 8.

If a typing judgement $\Sigma$ is derivable in ${\bf ETTC}_{\eta\to}$ then it
is derivable in ${\bf ETTC}$. If the ${\bf ETTC}_{\eta\to}$ derivation of
$\Sigma$ is cut-free, then $\Sigma$ is cut-free derivable in ${\bf ETTC}$.

######  Proof 5.1.

The $({\rm{Id}_{\eta_{\to}}})$ axioms of ${\bf ETTC}_{\eta\to}$ are ETTC
derivable from $({\rm{Id}})$ axioms using $(\alpha\eta)$ rules. The
$(\nabla_{\equiv_{\alpha}})$, $(\triangle_{\equiv_{\alpha}})$ rules are cut-
free emulated in ETTC as shown in Figures LABEL:emulating_nabla_alpha,
LABEL:emulating_triangle_alpha.

(It was precisely the $\eta$-long fragment that was introduced and discussed
in [Sla21b] under the name ETTC, with the exception that in [Sla21b] we did
not have the term reduction $\delta^{i}_{i}\to_{\beta}1$. Also, in [Sla21b]
types were defined as quotiented under $\alpha$-equivalence, so that the rules
$(\nabla)_{\equiv_{\alpha}}$, $(\triangle)_{\equiv_{\alpha}}$ in those
definitions would be identical to the original $(\nabla)$, $(\triangle)$
versions. The enriched ETTC of this work has the advantage of more concise
notation; derivations in the ${\bf ETTC}_{\eta\to}$ tend to become overloaded
with indices and barely readable.)

The $\eta$-long fragment is notationally cumbersome, but is easy to analyze.
In particular, cut-elimination in ${\bf ETTC}_{\eta\to}$ is more or less
routine. For the full system ETTC of this work, cut-elimination is trickier
because of $(\alpha\eta)$ rules.

###  5.2. Cut-elimination for ${\bf ETTC}_{\eta\to}$

######  Proposition 9.

If $\Sigma$, $\Sigma^{\prime}$ are $\alpha$-equivalent typing judgements and
$\pi$ is an ${\bf ETTC}_{\eta\to}$ derivation of $\vdash\Sigma$ then there
exists an ${\bf ETTC}_{\eta\to}$ derivation $\pi^{\prime}$ of
$\vdash\Sigma^{\prime}$, which is obtained from $\pi$ by renaming some
indices.

######  Proof 5.2.

Easy induction on $\pi$.

We define the size of a derivation in ${\bf ETTC}_{\eta\to}$ 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 $\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 an ${\bf ETTC}_{\eta\to}$ derivation with two subderivations $\pi_{1}$,
$\pi_{2}$ of the sequents $\vdash t::\Gamma,A$ and $\vdash
s::\overline{A},\Theta$ respectively followed with the Cut rule, we say that
this application of a cut rule is a principal cut if $\pi_{1}$, respectively
$\pi_{2}$, ends with a rule introducing the formula $A$, respectively
$\overline{A}$. An application of the Cut rule that is not principal is a side
cut.

######  Lemma 10.

There is an algorithm transforming an ${\bf ETTC}_{\eta\to}$ derivation $\pi$
of a sequent $\vdash\Sigma$ to a derivation $\pi^{\prime}$ of the same
sequent, where $\mathit{size}(\pi^{\prime})=\mathit{size}(\pi)$ and all cuts
in $\pi^{\prime}$ principal.

######  Proof 5.3.

Let $\pi_{1},\ldots,\pi_{n}$ be all subderivations of $\pi$ ending with side
cuts and let $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
introducing a side formula. We will consider only one case that seems most
involved, namely, permutation with the $(\nabla_{\equiv\alpha})$ rule when
there is a possibility of index collision. Other cases are similar or easier.

Let a side cut be between sequents $\vdash\Sigma_{1}$, $\vdash\Sigma_{2}$ of
the forms

$\vdash t::\nabla^{\mu}_{\nu}B,\Phi,A,\quad\vdash s::\overline{A},\Theta$

respectively, where $\vdash\Sigma_{1}$ is obtained by the
$(\nabla_{\equiv_{\alpha}})$ rule from the sequent $\vdash\Sigma_{0}$ of the
form
$\vdash\delta^{i}_{j}t::B_{[\nicefrac{{i}}{{\mu}}]}^{[\nicefrac{{j}}{{\nu}}]},\Phi,A$.

The transformation of derivations is shown in Figure LABEL:side_cut_figure,
where in order to avoid possibility of forbidden index repetitions, we use
Proposition 9 and replace the derivation of $\vdash\Sigma_{0}$ with a
derivation with the same size and an $\alpha$-equivalent conclusion obtained
from $\Sigma_{0}$ by renaming $i$, $j$ with fresh indices. The induction
parameter $N$ for the new derivation is smaller at least by 1.

$\begin{array}[]{c}i^{\prime},j^{\prime}\mbox{
fresh},~{}B^{\prime}=B^{[\nicefrac{{j^{\prime}}}{{\nu}}]}_{[\nicefrac{{i^{\prime}}}{{\mu}}]}.\\\\[7.11317pt]
\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
51.17218pt\hbox{\vbox{\hbox{\vbox{\hbox{\hskip
0.1pt\hbox{$\mathord{\vdash\delta^{i}_{j}t}\ ::\
\mathord{}$}\hbox{$B_{[\nicefrac{{i}}{{\mu}}]}^{[\nicefrac{{j}}{{\nu}}]},\Phi,A$}\hskip
0.1pt}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to83.59016pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
3.0pt($\nabla_{\equiv_{\alpha}}$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
6.37372pt\hbox{\hskip 0.1pt\hbox{$\mathord{\vdash t}\ ::\
\mathord{}$}\hbox{$\nabla^{\mu}_{\nu}B,\Phi,A$}\hskip 0.1pt}}}\hbox{\hskip
3.0pt}\hbox{\hskip 0.1pt\hbox{$\mathord{\vdash s}\ ::\
\mathord{}$}\hbox{$\overline{A},\Theta$}\hskip
0.1pt}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
6.37372pt\lower-0.2pt\hbox{}\hbox to157.83978pt{\xleaders\hrule\hfill}\lower
2.3pt\hbox{\hskip
3.0pt(${\rm{Cut}}$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
44.20274pt\hbox{\hskip 0.1pt\hbox{$\mathord{\vdash ts}\ ::\
\mathord{}$}\hbox{$\nabla^{\mu}_{\nu}B,\Phi,\Theta$}\hskip
0.1pt}}}}\ignorespaces\Rightarrow\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
51.6072pt\hbox{\vbox{\vbox{\hbox{\hbox{\hskip
0.1pt\hbox{$\mathord{\vdash\delta^{i^{\prime}}_{j^{\prime}}t}\ ::\
\mathord{}$}\hbox{$B^{\prime},\Phi,A$}\hskip 0.1pt}\hbox{\hskip
3.0pt}\hbox{\hskip 0.1pt\hbox{$\mathord{\vdash s}\ ::\
\mathord{}$}\hbox{$\overline{A},\Theta$}\hskip
0.1pt}}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to129.41208pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
3.0pt(${\rm{Cut}}$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
25.07214pt\hbox{\hskip
0.1pt\hbox{$\mathord{\vdash\delta^{i^{\prime}}_{j^{\prime}}ts}\ ::\
\mathord{}$}\hbox{$B^{\prime},\Phi,\Theta$}\hskip
0.1pt}}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
25.07214pt\lower-0.2pt\hbox{}\hbox to89.43544pt{\xleaders\hrule\hfill}\lower
2.3pt\hbox{\hskip
3.0pt($\nabla_{\equiv_{\alpha}}$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
32.32585pt\hbox{\hskip 0.1pt\hbox{$\mathord{\vdash ts}\ ::\
\mathord{}$}\hbox{$\nabla^{\mu}_{\nu}B,\Phi,\Theta$}\hskip
0.1pt}}}}\ignorespaces\end{array}$

(a)

$\begin{array}[]{c}i^{\prime},j^{\prime}\mbox{
fresh},t^{\prime}=t^{[\nicefrac{{j^{\prime}}}{{l}}]}_{[\nicefrac{{i^{\prime}}}{{k}}]},A^{\prime}=A^{[\nicefrac{{j^{\prime}}}{{\nu}}]}_{[\nicefrac{{i^{\prime}}}{{\mu}}]}.\\\\[7.11317pt]
\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
50.62497pt\hbox{\vbox{\hbox{\vbox{\hbox{\hskip
0.1pt\hbox{$\mathord{\vdash\delta_{j}^{i}s}\ ::\
\mathord{}$}\hbox{$\Gamma,A_{[\nicefrac{{i}}{{\mu}}]}^{[\nicefrac{{j}}{{\nu}}]}$}\hskip
0.1pt}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to70.7494pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
3.0pt($\nabla_{\equiv_{\alpha}}$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
7.07112pt\hbox{\hskip 0.1pt\hbox{$\mathord{\vdash s}\ ::\
\mathord{}$}\hbox{$\Gamma,\nabla^{\mu}_{\nu}A$}\hskip 0.1pt}}}\hbox{\hskip
3.0pt}\vbox{\hbox{\hskip 7.5361pt\hbox{\hskip 0.1pt\hbox{$\mathord{\vdash t}\
::\
\mathord{}$}\hbox{$\overline{A}^{[\nicefrac{{k}}{{\mu}}]}_{[\nicefrac{{l}}{{\nu}}]},\Theta$}\hskip
0.1pt}}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to70.22447pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
3.0pt($\triangle_{\equiv_{\alpha}}$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
0.1pt\hbox{$\mathord{\vdash\delta^{k}_{l}t}\ ::\
\mathord{}$}\hbox{$\triangle^{\nu}_{\mu}\overline{A},\Theta$}\hskip
0.1pt}}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
7.07112pt\lower-0.2pt\hbox{}\hbox to162.41653pt{\xleaders\hrule\hfill}\lower
2.3pt\hbox{\hskip
3.0pt(${\rm{Cut}}$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
56.58156pt\hbox{\hskip 0.1pt\hbox{$\mathord{\vdash s\delta^{k}_{l}t}\ ::\
\mathord{}$}\hbox{$\Gamma,\Theta$}\hskip
0.1pt}}}}\ignorespaces\Rightarrow\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
28.11554pt\hbox{\vbox{\hbox{\hbox{\hskip
0.0pt\hbox{$\mathord{\vdash\delta^{i^{\prime}}_{j^{\prime}}s}\ ::\
\mathord{}$}\hbox{$\Gamma,A^{\prime}$}\hskip 0.0pt}\hbox{\hskip
3.0pt}\hbox{\hskip 0.0pt\hbox{$\mathord{\vdash t^{\prime}}\ ::\
\mathord{}$}\hbox{$\overline{A^{\prime}},\Theta$}\hskip
0.0pt}}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to115.9375pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
3.0pt(${\rm{Cut}}$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
25.39343pt\hbox{\hskip
0.0pt\hbox{$\mathord{\vdash\delta_{j^{\prime}}^{i^{\prime}}st^{\prime}}\ ::\
\mathord{}$}\hbox{$\Gamma,\Theta$}\hskip 0.0pt}}}}\ignorespaces\end{array}$

(b)

Figure 11. Cut-elimination for ${\bf ETTC}_{\eta\to}$

######  Lemma 11.

There is an algorithm transforming an ${\bf ETTC}_{\eta\to}$ derivation $\pi$
of a sequent $\Sigma$ with cuts into an ${\bf ETTC}_{\eta\to}$ derivation
$\pi^{\prime}$ of some sequent $\Sigma^{\prime}$ such that
$\Sigma^{\prime}\equiv_{\beta}\Sigma$ and
$\mathit{size}(\pi^{\prime})<\mathit{size}(\pi)$, provided that all cuts in
$\pi$ are principal.

######  Proof 5.4.

If there is a cut

$\cfrac{\vdash\delta_{i_{1}\ldots i_{n}l_{m}\ldots l_{1}}^{k_{n}\ldots
k_{1}j_{1}\ldots j_{m}}::p^{i_{1}\ldots i_{n}}_{j_{1}\ldots
j_{m}},\overline{p}^{l_{1}\ldots l_{m}}_{k_{1}\ldots
k_{n}}~{}\vdash\delta_{k_{n}\ldots k_{1}t_{m}\ldots t_{1}}^{s_{n}\ldots
s_{1}l_{m}\ldots l_{1}}::p^{k_{n}\ldots k_{1}}_{l_{m}\ldots
l_{1}},\overline{p}^{t_{1}\ldots t_{m}}_{s_{1}\ldots
s_{n}}}{\vdash\delta_{i_{1}\ldots i_{n}l_{m}\ldots l_{1}k_{n}\ldots
k_{1}t_{m}\ldots t_{1}}^{k_{n}\ldots k_{1}j_{1}\ldots j_{m}s_{n}\ldots
s_{1}l_{m}\ldots l_{1}}::p^{i_{1}\ldots i_{n}}_{j_{1}\ldots
j_{m}},\overline{p}^{t_{1}\ldots t_{m}}_{s_{1}\ldots s_{n}}}$

between $({\rm{Id}}_{\eta\to})$ axioms then its conclusion is
$\beta$-equivalent to the $({\rm{Id}}_{\eta\to})$ axiom

$\vdash\delta_{i_{1}\ldots i_{n}t_{m}\ldots t_{1}}^{s_{n}\ldots
s_{1}j_{1}\ldots j_{m}}::p^{i_{1}\ldots i_{n}}_{j_{1}\ldots
j_{m}},\overline{p}^{t_{1}\ldots t_{m}}_{s_{1}\ldots s_{n}}.$

The transformation of a principal cut between a $\triangle$\- and a
$\nabla$-formula is shown in Figure LABEL:cut_triangle/nabla, where, similarly
to Proposition 10, we use Proposition 9 and replace derivations of the
premises with derivations of $\alpha$-equivalent sequents. The conclusion of
the new derivation is $\beta$-equivalent to the conclusion of the original
one, they are obtained from each other by renaming bound indices in the terms.
(That is, the terms are $\alpha$-equivalent, but $\alpha$-equivalent terms are
automatically $\beta$-equivalent).

The case of a $\otimes-$ and a $\parr-$ formula is indistinguishable from the
familiar case of multiplicative linear logic.

######  Corollary 12.

The system ${\bf ETTC}_{\eta\to}$ is cut-free.

######  Proof 5.5.

Combining Lemma 10 and Lemma 11 we prove by induction on the size of an ${\bf
ETTC}_{\eta\to}$ derivation $\pi$ of a sequent $\vdash\Sigma$ that $\pi$
transforms to a cut-free derivation of some $\beta$-equivalent sequent
$\vdash\Sigma^{\prime}$. But $\vdash\Sigma^{\prime}$ is cut-free derivable
from $\vdash\Sigma$ in ${\bf ETTC}_{\eta\to}$ by the $(\equiv_{\beta})$ rule.

###  5.3. Conservativity of ${\bf ETTC}_{\eta\to}$

If $\Gamma$ is a pseudotype context, the degeneracy $D(\Gamma)$ of $\Gamma$ is
the index set

$D(\Gamma)=\\{i|~{}i\in FI^{\bullet}(\Gamma)\cap FI_{\bullet}(\Gamma)\\}.$

If $\Sigma$ is a pseudotyping judgement of the form $t::\Gamma$, the
degeneracy $D(\Sigma)$ of $\Sigma$ is the set $D(\Sigma)=D(\Gamma)$. A typing
judgement $\widetilde{\Sigma}$ is an $\eta$-long representative of $\Sigma$ if
$\widetilde{\Sigma}$ has the form

$\delta^{\mu_{1}\ldots\mu_{n}}_{\nu_{1}\ldots\nu_{n}}t::\Gamma^{[\nicefrac{{\nu_{1}}}{{i_{1}}},\ldots,\nicefrac{{\nu_{n}}}{{i_{n}}}]}_{[\nicefrac{{\mu_{1}}}{{i_{1}}},\ldots,\nicefrac{{\mu_{n}}}{{i_{n}}}]},$

where $\\{i_{1},\ldots,i_{n}\\}=D(\Sigma)$. We will also use the following
notation for pairs of contexts: if $\Gamma,\Theta$ are pseudotype contexts
then

$D(\Gamma;\Theta)=\\{i|i\in FI^{\bullet}(\Gamma)\cap FI_{\bullet}(\Theta)\\},$
(11)

so that

$D(\Gamma,\Theta)=D(\Gamma)\cup D(\Theta)\cup D(\Gamma;\Theta)\cup
D(\Theta;\Gamma).$ (12)

######  Lemma 13.

If $\Sigma$ is a pseudotyping judgement and $\vdash_{\bf ETTC}\Sigma$, then
for any $\eta$-long representative $\widetilde{\Sigma}$ of $\Sigma$ it holds
that $\vdash_{{\bf ETTC}_{\eta\to}}\widetilde{\Sigma}$.

######  Proof 5.6.

Induction on the ETTC derivation of $\Sigma$.

For the base we have that $\eta$-long representatives of $({\rm{Id}})$ axioms
of ETTC are $({\rm{Id}}_{\eta_{\to}})$ axioms of ${\bf ETTC}_{\eta\to}$. If
$\Sigma$ is obtained from a sequent $\Sigma^{\prime}$ by an $(\alpha\eta)$ or
the $(\equiv_{\beta})$ rule then any $\eta$-long representative of $\Sigma$ is
$\alpha$-equivalent to some $\eta$-long representative of $\Sigma^{\prime}$
and the statement follows from the induction hypothesis. The case of the
$(\otimes)$ or the $(\parr)$ rule is very easy.

Let $\vdash\Sigma$ of the form
$\vdash\delta^{\mu}_{\nu}t::\triangle^{\mu}_{\nu}A,\Gamma$ be obtained from
the sequent $\vdash\Sigma^{\prime}$ of the form $\vdash t::A,\Gamma$, where
$(\nu,\mu)\in FI(A)$, by the $(\triangle)$ rule. There are different
possibilities on the structure of $D(\Sigma^{\prime})$, we will consider the
most involved case, when $\mu,\nu\in D(\Sigma^{\prime})$. In this case we have
$\mu,\nu\not\in D(\Sigma)$ (since repetitions of $\mu,\nu$ in the context are
eliminated by the $\triangle$ operator) and, in fact,
$D(\Sigma^{\prime})=D(\Sigma)\cup\\{\mu,\nu\\}$. Any $\eta$-long
representative $\widetilde{\Sigma}$ of $\Sigma$ has the form

$\delta^{\mu_{1}\ldots\mu_{n}}_{\nu_{1}\ldots\nu_{n}}\cdot\delta^{\mu}_{\nu}t::(\triangle^{\mu}_{\nu}A,\Gamma)^{[\nicefrac{{\nu_{1}}}{{i_{1}}},\ldots,\nicefrac{{\nu_{n}}}{{i_{n}}}]}_{[\nicefrac{{\mu_{1}}}{{i_{1}}},\ldots,\nicefrac{{\mu_{n}}}{{i_{n}}}]},$

where $\\{i_{1},\ldots,i_{n}\\}=D(\Sigma)$. It follows that the typing
judgement $\widetilde{\Sigma^{\prime}}$ of the form

$\delta^{\mu_{1}\ldots\mu_{n}}_{\nu_{1}\ldots\nu_{n}}\cdot\delta^{\mu^{\prime}\nu}_{\mu\nu^{\prime}}t::(A^{[\nicefrac{{\nu^{\prime}}}{{\nu}}]}_{[\nicefrac{{\mu^{\prime}}}{{\mu}}]},\Gamma)^{[\nicefrac{{\nu_{1}}}{{i_{1}}},\ldots,\nicefrac{{\nu_{n}}}{{i_{n}}}]}_{[\nicefrac{{\mu_{1}}}{{i_{1}}},\ldots,\nicefrac{{\mu_{n}}}{{i_{n}}}]}$

is an $\eta$-long representative of $\Sigma^{\prime}$, and, by the induction
hypothesis, $\vdash_{{\bf ETTC}_{\eta\to}}\widetilde{\Sigma^{\prime}}$. But
$\vdash\widetilde{\Sigma}$ is ${\bf ETTC}_{\eta\to}$ derivable from
$\vdash\widetilde{\Sigma^{\prime}}$ by the $(\triangle_{\equiv_{\alpha}})$
rule followed by the $(\equiv_{\beta})$ rule. Other possibilities of the
$(\triangle)$ rule are similar or easier. The case of the $(\nabla)$ rule is
analogous to the $(\triangle)$ rule.

The most involved case is that of the Cut rule. Let $\vdash\Sigma$ of the form
$\vdash ts::\Gamma,\Theta$ be obtained from $\vdash\Sigma_{1}$,
$\vdash\Sigma_{2}$ of the forms $\vdash t::\Gamma,A$, $\vdash
s::\overline{A},\Theta$ respectively by the Cut rule.

$\begin{array}[]{c}D(\Gamma)=\\{i_{1},\ldots,i_{k}\\},~{}D(\Theta)=\\{j_{1},\ldots,j_{l}\\},~{}D({\Gamma;\Theta})=\\{k_{1},\ldots,k_{m}\\},~{}D({\Theta;\Gamma})=\\{l_{1},\ldots,l_{n}\\}.\\\\[4.26773pt]
\delta_{\Gamma}=\delta^{x_{1}\ldots x_{k}}_{y_{1}\ldots
y_{k}},\quad\delta_{\Theta}=\delta^{p_{1}\ldots p_{l}}_{q_{1}\ldots
q_{l}},\quad\delta_{\Gamma\Theta}=\delta^{r_{1}\ldots r_{m}}_{s_{1}\ldots
s_{m}},\quad\delta_{\Theta\Gamma}=\delta^{u_{1}\ldots u_{n}}_{v_{1}\ldots
v_{n}},\\\\[4.26773pt]
\Gamma^{\prime}=\Gamma^{[\nicefrac{{y_{1}}}{{i_{1}}},\ldots,\nicefrac{{y_{k}}}{{i_{k}}},\nicefrac{{s_{1}}}{{k_{1}}},\ldots,\nicefrac{{s_{m}}}{{k_{m}}}]}_{[\nicefrac{{x_{1}}}{{i_{1}}},\ldots,\nicefrac{{x_{k}}}{{i_{k}}},\nicefrac{{u_{1}}}{{l_{1}}},\ldots,\nicefrac{{u_{n}}}{{l_{n}}}]},\quad\Theta^{\prime}=\Theta^{[\nicefrac{{q_{1}}}{{j_{1}}},\ldots,\nicefrac{{q_{l}}}{{j_{l}}},\nicefrac{{v_{1}}}{{l_{1}}},\ldots,\nicefrac{{v_{n}}}{{l_{n}}}]}_{[\nicefrac{{p_{1}}}{{j_{1}}},\ldots,\nicefrac{{p_{l}}}{{j_{l}}},\nicefrac{{r_{1}}}{{k_{1}}},\ldots,\nicefrac{{r_{m}}}{{k_{m}}}]}.\\\\[4.26773pt]
D(A)=\\{\xi_{1},\ldots,\xi_{r}\\},\quad\mu_{1},\nu_{1},\ldots\mu_{r},\nu_{r},\sigma_{1},\ldots,\sigma_{m},\tau_{1},\ldots,\tau_{n}\mbox{
fresh},\\\\[4.26773pt] \delta_{\Gamma A}=\delta_{s_{1}\ldots
s_{m}}^{\sigma_{1}\ldots\sigma_{m}},\quad\delta_{\overline{A}\Theta}=\delta^{r_{1}\ldots
r_{m}}_{\sigma_{1}\ldots\sigma_{m}},\quad\delta_{\Theta\overline{A}}=\delta_{v_{1}\ldots
v_{n}}^{\tau_{1}\ldots\tau_{n}},\quad\delta_{A\Gamma}=\delta^{u_{1}\ldots
u_{n}}_{\tau_{1}\ldots\tau_{n}},\\\\[4.26773pt]
\delta_{A}=\delta^{\mu_{1}\ldots\mu_{r}}_{\nu_{1}\ldots\nu_{r}},\quad\delta_{\overline{A}}=\delta_{\mu_{1}\ldots\mu_{r}}^{\nu_{1}\ldots\nu_{r}},\quad
A^{\prime}=A^{[\nicefrac{{\nu_{1}}}{{\xi_{1}}},\ldots,\nicefrac{{\nu_{r}}}{{\xi_{r}}}\nicefrac{{\tau_{1}}}{{l_{1}}},\ldots,\nicefrac{{\tau_{n}}}{{l_{n}}}]}_{[\nicefrac{{\mu_{1}}}{{\xi_{1}}},\ldots,\nicefrac{{\mu_{r}}}{{\xi_{r}}}\nicefrac{{\sigma_{1}}}{{k_{1}}},\ldots,\nicefrac{{\sigma_{m}}}{{k_{m}}}]}.\end{array}$

Figure 12. To the proof of Lemma 13

Any $\eta$-long representative $\widetilde{\Sigma}$ of $\Sigma$ can be written
as

$\delta_{\Gamma}\delta_{\Theta}\delta_{\Gamma\Theta}\delta_{\Theta\Gamma}ts::\Gamma^{\prime},\Theta^{\prime},$
(13)

where $\Gamma^{\prime}$, $\Theta^{\prime}$ are obtained from $\Gamma,\Theta$
respectively by renaming repeated free indices, and $\delta_{\Gamma}$,
$\delta_{\Theta}$, $\delta_{\Gamma\Theta}$, $\delta_{\Theta\Gamma}$ are
Kronecker deltas corresponding to this renaming, respectively, in $D(\Gamma)$,
$D(\Theta)$, $D({\Gamma;\Theta})$, $D({\Theta;\Gamma})$ (see Figure 12 for
explicit expressions with indices).

We are going to construct $\eta$-long representatives
$\widetilde{\Sigma_{1}}$, $\widetilde{\Sigma_{2}}$ of $\Sigma_{1}$,
$\Sigma_{2}$ respectively such that $\widetilde{\Sigma}$, up to
$\beta$-equivalence, is obtained from them by a cut.

Note that we have the equalities

$D({\Gamma;\Theta})=D({\Gamma;A})=D({\overline{A};\Theta}),\quad
D({\Theta;\Gamma})=D(\Theta;\overline{A})=D({A;\Gamma}).$

Indeed, if an index $i$ occurs freely both in $\Gamma$ and $\Theta$, then, in
order for $\Sigma$ to be well formed, it should have just one free occurrence
in $\Gamma$ and one in $\Theta$, and no occurrences in $ts$ whatsoever. Then
in order for $\Sigma_{1}$, $\Sigma_{2}$ to be well-formed, there must be a
free occurrence of $i$ in $A$ (hence in $\overline{A}$) to match the
occurrence in $\Gamma$ for $\Sigma_{1}$ and in $\Theta$ for $\Sigma_{2}$. With
this observation is easy to construct desired $\widetilde{\Sigma_{1}}$,
$\widetilde{\Sigma_{2}}$, respectively of the forms

$\delta_{\Gamma}\delta_{\Gamma
A}\delta_{A\Gamma}\delta_{A}t::\Gamma^{\prime},A^{\prime},\quad\delta_{\Theta}\delta_{\Theta\overline{A}}\delta_{\overline{A}\Theta}\delta_{\overline{A}}s::\overline{A^{\prime}},\Theta^{\prime},$

where we use the same notational convention for Kronecker deltas as in (13),
so that the terms satisfy the relations

$\delta_{\Gamma
A}\delta_{\overline{A}\Theta}\equiv_{\beta}\delta_{\Gamma\Theta},\quad\delta_{\Theta\overline{A}}\delta_{A\Gamma}\equiv_{\beta}\delta_{\Theta\Gamma},\quad\delta_{A}\delta_{\overline{A}}\equiv_{\beta}1.$

Explicit formulas are given in Figure 12.

Then the cut between $\vdash\widetilde{\Sigma_{1}}$,
$\vdash\widetilde{\Sigma_{2}}$ yields a sequent $\beta$-equivalent to
$\vdash\widetilde{\Sigma}$. Since derivability in ${\bf ETTC}_{\eta\to}$ is
closed under $\beta$-equivalence, the statement follows from the induction
hypothesis.

######  Corollary 14.

${\bf ETTC}_{\eta\to}$ is a conservative fragment of ETTC. $\Box$

######  Corollary 15.

ETTC is cut-free.

######  Proof 5.7.

Assume that $\vdash_{\bf ETTC}\Sigma$. Let $\widetilde{\Sigma}$ be an
$\eta$-long form of $\Sigma$. In particular, $\widetilde{\Sigma}$ is an
$\eta$-long representative of $\Sigma$, and, using the preceding lemma and
cut-elimination for ${{\bf ETTC}_{\eta\to}}$, the sequent
$\vdash\widetilde{\Sigma}$ in cut-free derivable in ${\bf ETTC}_{\eta\to}$.
Then, by Proposition 8, the sequent $\vdash\widetilde{\Sigma}$ is cut-free
derivable in ETTC. But $\vdash\Sigma$ is cut-free derivable from
$\vdash\widetilde{\Sigma}$ in ETTC using $(\alpha\eta)$ rules.

##  6\. Natural deduction and grammars

For derivations from nonlogical axioms it seems more convenient to allow
variables standing for tensor terms, in the style of natural deduction
(abbreviated below as “n.d.”). N.d. formulation might also be more convenient
if we want to consider the purely intuitionistic fragment of ETTC that is
restricted to types built using only binding operators, tensor and linear
implication (the latter defined as $A\multimap B=\overline{A}\parr B$ or
$A\multimap B=B\parr\overline{A}$). Given a terminal alphabet $T$ and a
countable set $\mathit{var}_{\otimes}$ of tensor variable symbols of different
valencies, where valency $v(x)$ of the symbol $x$ is a pair of nonnegative
integers, the set $\mathit{Var}_{\otimes}$ of tensor variables is the subset
of

$\\{x^{i_{1}\ldots i_{m}}_{j_{1}\ldots
j_{n}}|~{}x\in\mathit{var}_{\otimes},v(x)=(m,n),~{}i_{1},\ldots,i_{m},j_{1},\ldots,j_{n}\in\mathit{Ind}\\}$

satisfying the constraint that there are no repeated indices. N.d. tensor
terms are defined same as tensor terms in Definition 4.1 except that the set
$\mathit{Var}_{\otimes}$ is added to sets (7) of generators.

$\beta$-Reduction of n.d. tensor terms is defined same as $\beta$-reduction of
tensor terms in Definition 4.1. Lexical n.d. terms are defined as in
Definition 4.1 with the addition that they contain no tensor variables. An
n.d. tensor pseudotyping, respectively typing, judgement is an expression of
the form $t:C$ where $t$ is an n.d. tensor term and $C$ a tensor pseudotype,
respectively type, satisfying the same relation (9) as $t$ and $\Gamma$ in
Definition 4.3 of usual tensor pseudotyping judgement. Lexical,
$\beta$-reduced and $\alpha$-, $\beta$\- or $\eta$-equivalent pseudotyping
judgements are defined as previously in Definition 4.3.

A variable declaration is an n.d. typing judgement $X:A$, where $X$ is a
tensor variable. An n.d. typing context $\Gamma$ is a finite set (rather than
a multiset) of variable declarations that have no common variable symbols and
such that for any two distinct variables $X,Y$ in $\Gamma$ we have $I(X)\perp
I(Y)$.

An n.d. tensor sequent is an expression of the form $\Gamma\vdash\Sigma$,
where $\Gamma$ is an n.d. typing context, and $\Sigma$ an n.d. pseudotyping
judgement. $\alpha$-, $\beta$-, $\eta$-Equivalence of n.d. sequents are
generated by the relation

$\Sigma\equiv_{\xi}\Sigma^{\prime}\Longrightarrow(\Gamma\vdash\Sigma)\equiv_{\xi}(\Gamma\vdash\Sigma^{\prime}),\mbox{
where }\xi\in\\{\alpha,\beta,\eta\\}.$

Natural deduction system ${\bf ETTC}_{n.d.\ }$ is given by the rules in Figure
13 with the usual implicit restriction that all expressions are well-formed.

$\begin{array}[]{lr}X:A\vdash X:A~{}(\rm{Id})&\cfrac{\Gamma\vdash
t:A,~{}t\equiv_{\beta}t^{\prime}}{\Gamma\vdash
t^{\prime}:A}~{}(\equiv_{\beta})\\\\[11.38092pt] \cfrac{\Gamma\vdash
t:A}{\Gamma\vdash\delta^{i}_{j}t:A^{[j/i]}}~{}(\alpha\eta^{\to})&\cfrac{\Gamma\vdash\delta^{i}_{j}t:A^{[j/i]}}{\Gamma\vdash
t:A}~{}(\alpha\eta^{\leftarrow})\\\\[11.38092pt] \cfrac{\Gamma\vdash
t:A}{\Gamma\vdash\delta_{j}^{i}t:A_{[i/j]}}~{}(\alpha\eta_{\to})&\cfrac{\Gamma\vdash\delta^{i}_{j}t:A_{[i/j]}}{\Gamma\vdash
t:A}_{(}\alpha\eta_{\leftarrow})\\\\[11.38092pt] \cfrac{X:A,\Gamma\vdash
tX:B}{\Gamma\vdash t:\overline{A}\parr
B}~{}(\parr{\rm{I}}_{l})&\cfrac{\Gamma\vdash t:{A}\quad\Theta\vdash
s:\overline{A}\parr B}{\Gamma,\Theta\vdash
ts:B}~{}(\parr{\rm{E}}_{l})\\\\[11.38092pt] \cfrac{\Gamma,X:A\vdash
tX:B}{\Gamma\vdash
t:B\parr\overline{A}}~{}(\parr{\rm{I}}_{r})&\cfrac{\Gamma\vdash
s:B\parr\overline{A}\quad\Theta\vdash t:{A}}{\Gamma,\Theta\vdash
st:B}~{}(\parr{\rm{E}}_{r})\\\\[11.38092pt] \cfrac{\Gamma\vdash
t:A\quad\Theta\vdash s:B}{\Gamma,\Theta\vdash ts:A\otimes
B}(\otimes{\rm{I}})&\cfrac{\Theta\vdash s:A\otimes B\quad\Gamma,X:A,Y:B\vdash
tXY:C}{\Gamma,\Theta\vdash ts:C}(\otimes{\rm{E}})\\\\[11.38092pt]
\cfrac{\Gamma\vdash\delta^{\mu}_{\nu}\cdot t:A}{\Gamma\vdash
t:\nabla^{\mu}_{\nu}A}~{}(\nabla{\rm{I}})&\cfrac{\Gamma\vdash
t:\nabla^{\mu}_{\nu}A}{\Gamma\vdash\delta^{\mu}_{\nu}\cdot
t:A}~{}(\nabla{\rm{E}})\\\\[11.38092pt] \cfrac{\Gamma\vdash
t:A}{\Gamma\vdash\delta_{\mu}^{\nu}\cdot
t:\triangle^{\mu}_{\nu}A}~{}(\triangle{\rm{I}})&\cfrac{\Gamma\vdash
t:\triangle^{\mu}_{\nu}A\quad
X:A,\Theta\vdash\delta_{\mu}^{\nu}sX:B}{\Gamma,\Theta\vdash
st:B}~{}(\triangle{\rm{E}})\end{array}$

Figure 13. Natural deduction for ETTC

Note that there are two pairs of introduction/elimination rules for the
$\parr$ connective. They correspond to two different encodings of implication.
If we are interested only in the intuitionistic fragment then one of the two
pairs (depending on the chosen encoding) is not needed.

######  Proposition 16.

In ${\bf ETTC}_{n.d.}$, $\alpha\beta\eta$-equivalent sequents are derivable
from each other.

######  Proof 6.1.

Similar to Proposition 7.

######  Proposition 17.

The system ${\bf ETTC}_{n.d.\ }$ is closed under the following substitution
rule

$\cfrac{\Gamma\vdash t:A\quad X:A,\Theta\vdash X\cdot s:B}{\Gamma,\Theta\vdash
ts:B}({\rm{Sb}})$

######  Proof 6.2.

The rule is emulated with the $(\parr{\rm{I}}_{l})$ rule followed by the
$(\parr{\rm{E}}_{l})$ rule.

We defined typing contexts in n.d. sequents as unordered sets. However,
notationally it will be convenient to consider them as “vectors” with
enumerated components as in the following.

Let $\overrightarrow{X}=\\{X_{(1)},\ldots,X_{(n)}\\}$ be a sequence of tensor
variables and $\Gamma=A_{(1)},\ldots,A_{(n)}$ be an ordered tensor type
context (we put sequence numbers in brackets in order to avoid confusion with
indices). We denote the n.d. typing context
$X_{(1)}:A_{(1)},\ldots,X_{(n)}:A_{(n)}$ as $\overrightarrow{X}:\Gamma$. Given
a term $t$, we denote the term $tX_{(1)}\cdots X_{(n)}$ as
$t\overrightarrow{X}$. Finally, we write $\overline{\Gamma}$ for the ordered
type context $\overline{A_{(n)}},\ldots,\overline{A_{(1)}}$. (As usual, it is
implicitly assumed that all these expressions are well-formed). An n.d. tensor
sequent is standard if it has the form $\overrightarrow{X}:\Gamma\vdash
t\overrightarrow{X}:B$.

######  Proposition 18.

Any sequent derivable in ${\bf ETTC}_{n.d.\ }$ is standard. $\Box$

######  Proposition 19 (“Deduction theorem”).

Consider a finite set

$\Xi=\\{\tau_{(1)}:A_{(1)},\ldots,\tau_{(n)}:A_{(n)}\\}$

of n.d. lexical typing judgements with $FI(A_{(i)})\perp FI(A_{(j)})$ for
$i\not=j$, $i,j=1,\ldots,n$.

An n.d. sequent $\Sigma$ of the form $\Gamma\vdash t:B$ is ${\bf ETTC}_{n.d.\
}$ derivable from $\Xi$ using each element of $\Xi$ exactly once iff there
exist an n.d. sequent $\Sigma^{\prime}$ of the form

$X_{(1)}:A_{(1)},\ldots,X_{n}:A_{(n)},\Gamma\vdash t^{\prime}X_{(1)}\ldots
X_{(n)}:B$ (14)

derivable in ${\bf ETTC}_{n.d.\ }$ without nonlogical axioms such that

$t^{\prime}\cdot\tau_{(1)}\ldots\tau_{(n)}\equiv_{\beta}t.$ (15)

######  Proof 6.3.

If there is $\Sigma^{\prime}$ satisfying (14), (15), then $\Sigma$ is ${\bf
ETTC}_{n.d.\ }$ derivable from $\Xi$ and $\Sigma^{\prime}$ by a series of
substitution rules using each element of $\Xi$ exactly once. Thus, if
$\vdash_{{\bf ETTC}_{n.d.\ }}\Sigma^{\prime}$ then $\Sigma$ is ${\bf
ETTC}_{n.d.\ }$ derivable from $\Xi$ as required. The other direction is
proven by an easy induction on the n.d. derivation of $\Sigma$.

###  6.1. Translation to sequent calculus

######  Proposition 20.

Given a standard n.d. sequent $\Xi$ of the form
$\overrightarrow{X}:\Gamma\vdash t\overrightarrow{X}:A$, the expression
$\Xi^{\prime}$ of the form $t::A,\overline{\Gamma}$ is a well-defined tensor
pseudotyping judgement.

######  Proof 6.4.

Let us denote $\widetilde{t}=t\overrightarrow{X}$ and
$\Theta=A,\overline{\Gamma}$.

The n.d. type context $\overrightarrow{X}:\Gamma$, by definition, consists of
variable declarations. In any variable declaration $Y:F$ we have that
$FI(Y)=FI^{\dagger}(F)$, because it is an n.d. typing judgement, and we have
$I(Y)=FI(Y)$, because $Y$, being a tensor variable, has no repeated indices.
It follows that, for
$FI(\overrightarrow{X})=\bigcup\limits_{Y\in\overrightarrow{X}}FI(Y)$, we have
$I(\overrightarrow{X})=FI^{\dagger}(\Gamma)=FI(\overline{\Gamma})$.

Since $\widetilde{t}$ is a well-formed term we have that $I(t)\perp
I(\overrightarrow{X})$, $I(Y)\perp I(Y^{\prime})~{}\forall
Y,Y^{\prime}\in\overrightarrow{X}$. Since $\Sigma$ is a well-defined n.d.
pseudotyping judgement we have $I(\widetilde{t})\perp FI(A)$,
$FI(\overrightarrow{X})\perp FI(A)$. It follows that
$FI(\overline{\Gamma})\perp FI(A)$, $FI(F)\perp FI(F^{\prime})~{}\forall
F,F^{\prime}\in\overrightarrow{\Gamma}$, $I(t)\perp FI(\overline{\Gamma})$,
and $I(t)\perp FI(A)$. The first two conditions mean that $\Theta$ is a well-
defined pseudotype context, and the last two mean that $I(t)\perp FI(\Theta)$.

In order for $\Xi^{\prime}$ to be a pseudotyping judgement it remains to show
that $I^{\bullet}(t)\cup FI^{\bullet}(\Theta)=I_{\bullet}(t)\cup
FI_{\bullet}(\Theta)$. Again, since $\Sigma$ is an n.d. pseudotyping
judgement, we have that $I^{\bullet}(\widetilde{t})\cup
FI^{\bullet}(A)=I_{\bullet}(\widetilde{t})\cup FI_{\bullet}(A)$. But
$I(\widetilde{t})=I(t)\cup I(\overrightarrow{X})=I(t)\cup
FI(\overline{\Gamma})$ and $FI(\Theta)=FI(\overline{\Gamma})\cup FI(A)$. The
desired equality follows.

In the notation of Proposition 20, the tensor sequent $\vdash\Xi^{\prime}$ is
the sequent calculus translation of a standard n.d. sequent $\Xi$.

######  Lemma 21.

A standard n.d. sequent is derivable in ${\bf ETTC}_{n.d.\ }$ whenever its
sequent calculus translation is derivable in ${\bf ETTC}$.

$\begin{array}[]{c}\cfrac{\vdash\delta^{i}_{j}t::A,\overline{\Theta},(\overline{B})^{[\nicefrac{{j}}{{i}}]}}{\vdash
t::A,\overline{\Theta},(\overline{B})}~{}(\alpha\eta^{\leftarrow})\quad\Longrightarrow\\\
\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
74.55331pt\hbox{\vbox{\vbox{\hbox{\vbox{\hbox{\hskip
0.0pt\hbox{$\mathord{Z:B}\ \vdash\ \mathord{}$}\hbox{$Z:B$}\hskip
0.0pt}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to83.02637pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
3.0pt($\alpha\eta_{\to}$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
0.0pt\hbox{\hskip 0.0pt\hbox{$\mathord{Z:B}\ \vdash\
\mathord{}$}\hbox{$\delta^{j}_{i}Z:B_{[\nicefrac{{j}}{{i}}]}$}\hskip
0.0pt}}}\hbox{\hskip 14.45377pt}\vbox{\hbox{\hskip 54.15839pt\hbox{\hskip
0.0pt\hbox{\it{(Ind.~{}hyp.)}}\hskip 0.0pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to115.51306pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip
0.0pt\hbox{$\mathord{Y:B_{[\nicefrac{{j}}{{i}}]},\overrightarrow{X}:{\Theta},}\
\vdash\ \mathord{}$}\hbox{$\delta^{i}_{j}tY\overrightarrow{X}:A$}\hskip
0.0pt}}}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to237.93332pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
3.0pt(Sb)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip 62.73225pt\hbox{\hskip
0.0pt\hbox{$\mathord{Z:B,\overrightarrow{X}:\Theta}\ \vdash\
\mathord{}$}\hbox{$\delta^{j}_{i}\delta^{i}_{j}tZ\overrightarrow{X}:A$}\hskip
0.0pt}}}\vskip-3.06667pt\nointerlineskip\hbox{\hskip
62.73225pt\lower-0.2pt\hbox{}\hbox to112.46883pt{\xleaders\hrule\hfill}\lower
2.03334pt\hbox{\hskip
3.0pt($\equiv_{\beta}$)}}\vskip-3.06667pt\nointerlineskip\hbox{\hskip
62.73225pt\hbox{\hskip 0.0pt\hbox{$\mathord{Z:B,\overrightarrow{X}:\Theta}\
\vdash\ \mathord{}$}\hbox{$tZ\overrightarrow{X}:A$}\hskip
0.0pt}}}}\ignorespaces\\\ \\\
\cfrac{\vdash\delta^{\mu}_{\nu}t::A,\overline{\Theta},\overline{B}}{\vdash
t::A,\overline{\Theta},\nabla^{\mu}_{\nu}\overline{B}}~{}(\nabla)\quad\Longrightarrow\\\
\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
50.91664pt\hbox{\vbox{\hbox{\hbox{\hskip
0.1pt\hbox{$\mathord{Z:\triangle^{\nu}_{\mu}B}\ \vdash\
\mathord{}$}\hbox{$Z:\triangle^{\nu}_{\mu}B$}\hskip 0.1pt}\hbox{\hskip
14.45377pt}\vbox{\hbox{\hskip 44.91525pt\hbox{\hskip
0.1pt\hbox{\it{(Ind.~{}hyp.)}}\hskip 0.1pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to108.01494pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip
0.1pt\hbox{$\mathord{Y:B,\overrightarrow{X}:{\Theta}}\ \vdash\
\mathord{}$}\hbox{$\delta^{\mu}_{\nu}tY\overrightarrow{X}:A$}\hskip
0.1pt}}}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to215.56902pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
3.0pt($\triangle{\rm{E}}$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
52.34491pt\hbox{\hskip
0.1pt\hbox{$\mathord{Z:\triangle^{\nu}_{\mu}B,\overrightarrow{X}:\Theta}\
\vdash\ \mathord{}$}\hbox{$tZ\overrightarrow{X}:A$}\hskip
0.1pt}}}}\ignorespaces\\\ \\\ \cfrac{\vdash
t::A,\overline{\Theta},\overline{B}}{\vdash\delta^{\mu}_{\nu}t::A,\overline{\Theta},\triangle_{\mu}^{\nu}\overline{B}}~{}(\triangle)\quad\Longrightarrow\\\
\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
49.22499pt\hbox{\vbox{\hbox{\vbox{\hbox{\hskip
0.1pt\hbox{$\mathord{Z:\nabla_{\nu}^{\mu}B}\ \vdash\
\mathord{}$}\hbox{$Z:\nabla_{\nu}^{\mu}B$}\hskip
0.1pt}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to91.98923pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
3.0pt($\nabla{\rm{E}}$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
0.0pt\hbox{\hskip 0.1pt\hbox{$\mathord{Z:\nabla_{\nu}^{\mu}B}\ \vdash\
\mathord{}$}\hbox{$\delta^{\mu}_{\nu}Z:B$}\hskip 0.1pt}}}\hbox{\hskip
14.45377pt}\vbox{\hbox{\hskip 44.91525pt\hbox{\hskip
0.1pt\hbox{\it{(Ind.~{}hyp.)}}\hskip 0.1pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to100.19623pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip
0.1pt\hbox{$\mathord{Y:B,\overrightarrow{X}:{\Theta}}\ \vdash\
\mathord{}$}\hbox{$tY\overrightarrow{X}:A$}\hskip
0.1pt}}}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to232.55595pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
3.0pt(Sb)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip 57.20679pt\hbox{\hskip
0.1pt\hbox{$\mathord{Z:\nabla_{\nu}^{\mu}B,\overrightarrow{X}:\Theta}\ \vdash\
\mathord{}$}\hbox{$t\delta^{\mu}_{\nu}Z\overrightarrow{X}:A$}\hskip
0.1pt}}}}\ignorespaces\\\ \\\ \cfrac{\vdash
t::A,\overline{\Theta},\overline{B}\quad\vdash
s::\overline{C},\overline{\Psi}}{\vdash
ts::A,\overline{\Theta},\overline{B}\otimes\overline{C},\overline{\Psi}}~{}(\otimes)\quad\Longrightarrow\\\
\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
70.6611pt\hbox{\vbox{\hbox{\vbox{\hbox{\vbox{\hbox{\hskip
16.30077pt\hbox{\hskip 0.1pt\hbox{\it`{(Ind.~{}hyp.)}}\hskip 0.1pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to66.77528pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip
0.1pt\hbox{$\mathord{\overrightarrow{X}:{\Psi}}\ \vdash\
\mathord{}$}\hbox{$s\overrightarrow{X}:\overline{C}$}\hskip
0.1pt}}\hbox{\hskip 14.45377pt}\hbox{\hskip 0.1pt\hbox{$\mathord{Y:C\parr B}\
\vdash\ \mathord{}$}\hbox{$Y:C\parr B$}\hskip
0.1pt}}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to185.85503pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
3.0pt($\parr{\rm{E}}_{l}$)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
30.47633pt\hbox{\hskip 0.1pt\hbox{$\mathord{\overrightarrow{X}:{\Psi},Y:C\parr
B}\ \vdash\ \mathord{}$}\hbox{$s\overrightarrow{X}\cdot Y:{B}$}\hskip
0.1pt}}}\hbox{\hskip 14.45377pt}\vbox{\hbox{\hskip 44.12012pt\hbox{\hskip
0.1pt\hbox{\it{(Ind.~{}hyp.)}}\hskip 0.1pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to98.60596pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip
0.1pt\hbox{$\mathord{T:B,\overrightarrow{Z}:{\Theta}}\ \vdash\
\mathord{}$}\hbox{$tT\overrightarrow{Z}:A$}\hskip
0.1pt}}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
30.47633pt\lower-0.2pt\hbox{}\hbox to296.87233pt{\xleaders\hrule\hfill}\lower
2.3pt\hbox{\hskip 3.0pt(Sb)}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
97.85545pt\hbox{\hskip 0.1pt\hbox{$\mathord{\overrightarrow{X}:{\Psi},Y:C\parr
B,\overrightarrow{Z}:{\Theta}}\ \vdash\
\mathord{}$}\hbox{$ts\overrightarrow{X}\cdot
Y\cdot\overrightarrow{Z}:A$}\hskip 0.1pt}}}}\ignorespaces\end{array}$

Figure 14. From ${\bf ETTC}$ to ${\bf ETTC}_{n.d.\ }$: “side” rule cases

######  Proof 6.5.

Let the n.d. sequent in question be $\overrightarrow{X}:\Gamma\vdash
t\overrightarrow{X}:A$. Use induction on the ETTC derivation of the
translation $\vdash t::A,\overline{\Gamma}$. A rule introducing or modifying
the “principal” formula $A$ directly translates to the corresponding n.d. rule
(with two variations for the $(\parr)$ rule), the same applies to the
$(\equiv_{\beta})$ rule. A “side” rule, i.e. modifying a formula in
$\overline{\Gamma}$, typically, is emulated using the substitution rule and an
elimination rule for the dual connective. Basic cases of the
$(\alpha\eta^{\leftarrow})$, $(\nabla)$, $(\triangle)$ and $(\otimes)$ rules
are collected in Figure 14, the remaining ones are treated similarly or
easier. Note that for the $(\otimes)$ rule there is also a case mirror-
symmetric to that in the figure, namely, when the “principal” formula $A$ in
the conclusion comes from the right premise of the rule. In this situation the
n.d. translation is obtained using the $(\parr{\rm{E}}_{r})$ rule.

######  Lemma 22.

If a standard sequent is derivable in ${\bf ETTC}_{n.d.\ }$ then its sequent
calculus translation is derivable ${\bf ETTC}$.

######  Proof 6.6.

For the axioms of ${\bf ETTC}_{n.d.\ }$ use Proposition 7, claim (i). The
introduction rules, $(\alpha\eta)$ rules and the $(\equiv_{\beta})$ rule of
${\bf ETTC}_{n.d.\ }$ translate to ETTC directly. The elimination rules
$(\nabla{\rm{E}})$ and $(\parr{\rm{E}}_{l})$ are emulated in ETTC using cuts
with ETTC derivable sequents
$\vdash\delta^{\alpha}_{\beta}::\triangle^{\beta}_{\alpha}\overline{A},A$ and
$\vdash\overline{B}\otimes A,\overline{A},B$ respectively. The
$(\parr{\rm{E}_{r}})$ rule is similar to the $(\parr{\rm{E}}_{l})$ rule. The
remaining elimination rules are emulated very easily, using ETTC rules for the
corresponding dual connectives and the Cut rule.

######  Corollary 23.

A standard sequent is derivable in ${\bf ETTC}_{n.d.\ }$ iff its sequent
calculus translation is derivable ${\bf ETTC}$. $\Box$

###  6.2. Geometric representation

Translating to sequent calculus we can obtain geometric representation for
n.d. sequents and derivations. Namely, the standard n.d. sequent
$\overrightarrow{X}:\Gamma\vdash t\overrightarrow{X}:F$ can be depicted as the
ordered tensor sequent $\vdash t::F,\overline{\Gamma}$.

In this case, however, it seems natural to deform the graph of the sequent
calculus translation, so that indices corresponding to to the left and to the
right of the turnstile in the n.d. sequent appear on two parallel vertical
lines. That is, we depict indices of $F$ aligned vertically, from the top to
the bottom on one line, and indices of $\overline{\Gamma}$ aligned from the
bottom to the top on another line to the left. (This is the same as to say
that the indices occurring in $F$ are depicted on the right vertical line,
aligned from the top to the bottom, and those occurring in $\Gamma$ depicted
on the left vertical line, also ordered from the top to the bottom, but with
opposite polarities.) The prescription for drawing labeled edges is the same
as in the sequent calculus. An example of such a representation is shown in
Figure LABEL:n.d._sequent_geometric_representation.

In Figure LABEL:n.d._geometric_representation we show schematically geometric
representations of some n.d. rules, namely introduction/elimination for the
$\parr$ connective and elimination rules for the binding operators. Note that
$\parr$-introduction rules do not change the graph, but change its pictorial
representation by a continuous deformation.

$A$$\\{$$B$$\\{$$C$$\\{$$i$$j$$j$$k$$l$$s$$t$$k$$\\}$$F$$\\}$$G$$\alpha$$\beta$$\Leftrightarrow$$x^{i}_{j}:A^{j}_{i},y^{jk}:B_{jk},z_{l}:C^{l}\vdash[\alpha]^{s}_{i}[\beta]^{l}_{t}x^{i}_{j}y^{jk}z_{l}:F_{s}\parr
G^{t}_{k}$ (a)

$\begin{array}[]{c}{\scalebox{0.9}{ \leavevmode\hbox to210.71pt{\vbox
to46.22pt{\pgfpicture\makeatletter\hbox{\hskip 7.25282pt\lower-37.20558pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{
\pgfsys@beginscope\pgfsys@invoke{ }{{}} \pgfsys@beginscope\pgfsys@invoke{
}{{}} {}{{}}{} {}{{}}{}{}{}{}{{}}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{}\pgfsys@moveto{21.33957pt}{-28.45276pt}\pgfsys@moveto{21.33957pt}{-28.45276pt}\pgfsys@lineto{21.33957pt}{-7.11319pt}\pgfsys@lineto{49.79233pt}{-7.11319pt}\pgfsys@lineto{49.79233pt}{-28.45276pt}\pgfsys@closepath\pgfsys@moveto{49.79233pt}{-7.11319pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{33.76039pt}{-20.85837pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$t$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{}\pgfsys@moveto{7.11319pt}{-11.38113pt}\pgfsys@lineto{21.33957pt}{-11.38113pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\par{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.91982pt}{-14.79779pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$A$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{}\pgfsys@moveto{7.11319pt}{-24.1848pt}\pgfsys@lineto{21.33957pt}{-24.1848pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.66982pt}{-27.60146pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\Gamma$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \par{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{}\pgfsys@moveto{49.79233pt}{-17.78297pt}\pgfsys@lineto{64.0187pt}{-17.78297pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{67.55171pt}{-21.19963pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$B$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{95.83466pt}{-31.87257pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\Longrightarrow$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{88.46494pt}{-18.1518pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$(\parr{\rm{I}}_{l})$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\par\par\pgfsys@beginscope\pgfsys@invoke{ }{{}}{}{{}}{}
{}{{}}{}{}{}{}{{}}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{}\pgfsys@moveto{145.82039pt}{-28.45276pt}\pgfsys@moveto{145.82039pt}{-28.45276pt}\pgfsys@lineto{145.82039pt}{-7.11319pt}\pgfsys@lineto{174.27315pt}{-7.11319pt}\pgfsys@lineto{174.27315pt}{-28.45276pt}\pgfsys@closepath\pgfsys@moveto{174.27315pt}{-7.11319pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{158.24121pt}{-20.85837pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$t$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{} {}{} {{}{}}{{}}
{{{}}{{}}}{{}}{{{}}{{}}}{}{{}}{}{}{} {{}{}}{{}}
{{{}}{{}}}{{}}{{{}}{{}}}{}{{}}{}{}{} {}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{}\pgfsys@moveto{145.82039pt}{-11.38113pt}\pgfsys@lineto{131.59401pt}{-11.38113pt}\pgfsys@curveto{128.02951pt}{-11.38113pt}{125.90355pt}{-7.83244pt}{125.90355pt}{-4.26794pt}\pgfsys@curveto{125.90355pt}{-0.70345pt}{128.02951pt}{2.84523pt}{131.59401pt}{2.84523pt}\pgfsys@lineto{188.49953pt}{2.84523pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{192.03253pt}{0.00635pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\overline{A}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \par\par{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{}\pgfsys@moveto{145.82039pt}{-24.1848pt}\pgfsys@lineto{131.59401pt}{-24.1848pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{121.811pt}{-27.60146pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\Gamma$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \par\par{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{}\pgfsys@moveto{174.27315pt}{-17.78297pt}\pgfsys@lineto{188.49953pt}{-17.78297pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{192.03253pt}{-21.19963pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$B$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \par
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope }
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}
}}{\quad\quad\quad\scalebox{0.9}{ \leavevmode\hbox to214.54pt{\vbox
to44.85pt{\pgfpicture\makeatletter\hbox{\hskip-220.09145pt\lower-11.72878pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{
\pgfsys@beginscope\pgfsys@invoke{ }{{}}\pgfsys@beginscope\pgfsys@invoke{ }{{}}
{}{{}}{} {}{{}}{}{}{}{}{{}}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{}\pgfsys@moveto{248.96164pt}{18.49432pt}\pgfsys@moveto{248.96164pt}{18.49432pt}\pgfsys@lineto{248.96164pt}{32.7207pt}\pgfsys@lineto{277.4144pt}{32.7207pt}\pgfsys@lineto{277.4144pt}{18.49432pt}\pgfsys@closepath\pgfsys@moveto{277.4144pt}{32.7207pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{261.38246pt}{22.53212pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$t$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{}\pgfsys@moveto{277.4144pt}{25.60751pt}\pgfsys@lineto{291.64078pt}{25.60751pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\par{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{295.17378pt}{22.19086pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$A$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{}\pgfsys@moveto{234.73526pt}{25.60751pt}\pgfsys@lineto{248.96164pt}{25.60751pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\par{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{224.95226pt}{22.19086pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\Gamma$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope