BRICS RS-96-61 S. Soloviev: Proof of a Conjecture of S. Mac Lane

BRICS

Basic Research in Computer Science

Proof of a Conjecture of S. Mac Lane

Sergei Soloviev

BRICS Report Series RS-96-61 ISSN 0909-0878 December 1996 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1996, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through World Wide Web and anonymous FTP:

http://www.brics.dk/
ftp://ftp.brics.dk/

This document in subdirectory RS/96/61/

Proof of a Conjecture of S. Mac Lane

S. Soloviev ^{∗}Department of Computer Science Durham University South Road, Durham DH1 3LE, U.K. e-mail Sergei.Soloviev@durham.ac.uk

December, 1996

Abstract

Some sufficient conditions on a Symmetric Monoidal Closed category K are obtained such that a diagram in a free SMC category generated by the set A of atoms commutes if and only if all its interpretations in K are commutative. In particular, the category of vector spaces on any field satisfies these conditions (only this case was considered in the original Mac Lane conjecture). Instead of diagrams, pairs of derivations in Intuitionistic Multiplicative Linear logic can be considered (together with categorical equivalence). Two derivations of the same sequent are equivalent if and only if all their interpretations in K are equal. In fact, the assignment of values (objects of K) to atoms is defined constructively for each pair of derivations. Taking into account a mistake in R. Voreadou’s proof of the “abstract coherence theorem” found by the author, it was necessary to modify her description of the class of noncommutative diagrams in SMC categories; our proof of S. Mac Lane conjecture proves also the correctness of the modified description.

1 Preface

Since the notion of Symmetric Monoidal Closed (SMC) Category, in its axiomatic formulation, was introduced, the category of vector spaces over a field was considered as one of its principal models (see, e.g., [4]). The structure of an SMC category includes tensor product and internal hom-functor, and corresponding natural transformations. A diagram commutes in the free SMC category, iff it commutes in all its models, including vector spaces. But “how faithfully” does the notion of SMC category capture the categorical properties of a model?

For example,

Does a diagram commute in a free SMC category (and hence in all SMC categories) iff all instantiations by vector spaces give a commutative diagram?

The positive answer would mean, that the equality of morphisms in a free SMC category is complete with respect to the model of vector spaces.

The positive answer to this question will be called the Mac Lane’s conjecture. (The reason for this name will be explained in the end of the preface, when we shall recall briefly the history of the question.)

A similar result concerning free Cartesian Closed (CC) Categories and the category of finite sets was proved in the beginning of 80’s (Statman [16], Soloviev [14]), and is known as Statman’s finite completeness theorem.

∗This work was supported under the ESPRIT project CLICS-II, and mostly carried out while the author was employed by BRICS, a centre of the Danish National Research Foundation, Computer Science Department, Aarhus University, Denmark. He has been working on the final version during his visit to Ecole Normale Superieure, Paris, in 1996. The final version of this paper was completed when the author was supported by a British EPSRC grant and employed by Durham University (on leave from S.-Petersburg Institute for Informatics of the Russian Academy of Sciences).

The question above was not settled and thus remained a conceptual challenge.

Connection with the coherence problem

A straightforward idea to prove the conjecture of S. Mac Lane would be to take the class of all non-commutative diagrams in a free SMC category and then find, for each such diagram, some vector spaces (depending on the diagram), such that the corresponding instance of this diagram will be non-commutative in the category of vector spaces. Clearly, such a proof would rely on the description of commutative (and non-commutative) diagrams in a free category. This description constitutes a coherence problem.

A partial coherence theorem was proved by Kelly and Mac Lane [9] (1971): every diagram, that does not contain “essential” occurrences of tensor unit I (i.e., such that all occurrences of I can be eliminated by canonical isomorphisms) is commutative.

An important contribution was made by R. Voreadou [18]. She proposed a new and very fruitful idea: to give an exhaustive description of the non-commutative diagrams in a free SMC category as a class W generated recursively by application of functors and some other operations to the diagrams of certain “initial class” W_{0}, whose diagrams are non-commutative in a more or less obvious way. To prove non-commutativity of all the diagrams from W, she constructed a complex combinatorial model. The principal role in her description of W_{0} is played by the scheme of “twisted” application of evaluation, when hom-objects, used in each application, switch their roles in a “mirror-symmetrical” way (we will deal with this later in detail) ^{1}.

The proof in [18] of commutativity of diagrams in the complement D − W (in Voreadou’s terminology, the “abstract coherence theorem”) proceeds by straightforward induction on the construction of diagrams, since the “twisted” evaluation is to capture exactly the case when this induction would not go through. The whole construction seems appropriate for some (recursive) procedure for the assignement of vector spaces to variables (providing a non-commutative diagram in vector spaces), though this was out of the scope of Voreadou’s paper.

Recently we discovered a counterexample to an important technical proposition of Voreadou (proposition 2, p.3 of [18]). It destroyed her inductive proof of commutativity of the diagrams from D − W (making possible some “semi-twisted” cases).

In this paper we show that it is possible to prove correctness of a modified description: the definition of W_{0} is left essentially unchanged, while the recursive procedure generating W is replaced by the condition that the diagram could be “projected” into W_{0} by instantiation of the constant I for some variables.

Actually, the correctness of the modified description is a consequence of our main result, though the redefined classes of Voreadou play a principal role in our proof. (A recursive algorithm checking commutativity of a diagram can be extracted.)

The following remark should be made. We have used the description of non-commutative diagrams, suggested by Voreadou in our paper [15]. The main results of [15] remain valid in spite of necessary modifications in their proofs (we are going to show it elsewhere). In this paper several computational lemmas from [15] are used. They do not depend on Voreadou’s work.

Main Result.

Our main result is more general than the conjecture formulated above. We describe axiomatically a class of ”test-categories” and show that if K is a test-category, then a diagram is commutative in the free SMC category F(A) (generated by a set of atoms A) if and only if all its interpretations in K are commutative. We show also that the category of vector spaces over any field I is a test-category.

Methods.

Throughout the paper we use proof-theoretical language. This is based on the possibility to introduce a structure of free SMC category on the Multiplicative Intuitionistic Linear Logic. (The connection between categories with structure and logical calculi was first described by J.Lambek [10].)

Let us recall that, for this connection, it is useful to keep in mind the following correspondence between notions of category theory and proof theory:

1See examples 3.6, 5.1 and section 7

• Formulas are objects;

• Equivalence classes of derivations of the sequent A → B are morphisms from A to B (the equivalence relation is generated by axioms of equality in SMC categories);

• Logical connectives are functors (on objects);

• Inference rules in sequential calculus represent operations on morphisms, and functors (on morphisms) are represented by derived rules introducing the same connective simultaneously at the left and right side of arrow;

• The ”Cut” rule represents composition of morphisms;

• A pair of derivations of the same sequent represents a diagram.

• The “twisted evaluation”, mentioned above, is represented by two applications of the rule −↪ in sequential calculus with the same conclusion having the following form^{2}:

\frac{Γ_{11}, A − B → A′ B′, Γ_{12} → C}{Γ, A − B A′ − B′ → C} \frac{Γ_{21}, A′ − B′ → A B, Γ_{22} → C}{Γ, A − B A′ − B′ → C}

with Γ_{11} ∩ Γ_{12} = Γ_{21} ∩ Γ_{22} = Γ (and some conditions on the derivations of the premises, excluding trivial cases).

The structure of this paper

In section 1 we describe the free SMC category F(A) on a set of atoms A and give a precise formulation of our main result.

Sections 2-4 contain some known facts about F(A), the description of the corresponding sequent calculus L(A) and its properties with respect to the equivalence of proofs determined by the SMC structure. A diagram in F(A) is commutative iff the corresponding derivations in L(A) are equivalent. The derivations in L(A) can be studied by the methods of proof theory. Main tools from traditional arsenal are cut-elimination and permutation of rules. We use only wellestablished results on cut-elimination or facts about permutation of rules which can be checked by direct computation.

The principal part of the proof begins in section 5. First, we reduce the problem to the similar problem considering only so called 2-sequents (i.e., the ”nesting” of connectives/functors is essentially bounded by 2).

In section 6 we define the (modified) classes W′_{0} and W′ of Voreadou, and prove our version of the Abstract Coherence Theorem (two derivations of the same sequent, which do not belong to the ”exception class” W′ are equivalent in L(A) - cf. [18]).

In section 7 we describe ”saturated sequents and derivations” (a subsystem of multiplicative linear logic). It turns out, that the derivations from W′_{0} are obtained from saturated ones by a single introduction of implication at the left with different main formulas (this will allows us to show that their interpretations are different).

In section 8 we prove the main lemma (that every saturated derivation ends by one of 13 inferences such that the subderivations of its premises are saturated, which provides an inductive argument). Here permutations of rules from section 4 are essentially used.

In section 9 we give the axiomatic definition of test-category, and check (in section 10) that the category of vector spaces over a field satisfies this definition.

The notion of test-category is essentially an abstract version of that of the SMC subcategory of the category of vector spaces generated by three objects: a countable-dimensional space V, the field I and zero 0, but only few arrows, necessary to check non-commutativity. (Roughly speaking, in vector spaces the principal “test-arrow” distinguishes between the infinite diagonal matrix id_{V} ∈ Hom(V, V) and the matrixes with a finite number of non-zero rows.)

2This presentation corresponds to original case considered by Voreadou, in our modified definition we need less general form.

In section 11 necessary identities between arrows in a test-category are derived.

The assignement of objects of a test-category is rather straightforward: for every pair of derivations of W′_{0} we assign the object V (countable-dimensional space in case of vector spaces) to every variable; for a pair from W′ to some variables is assigned I (in accordance with substitution, ”projecting” it into W′_{0}). The difficult part is to prove that the resulting diagram is non-commutative.

Via this assignment each implicative formula is interpreted as a hom-object in the test-category. The axioms for a test-category provide sufficient number of elements in these hom-objects and a mechanism of evaluation, which allows to show that certain ”values” of arrows, corresponding to non-equivalent derivations are different (0 and non-0).

Together with our abstract coherence theorem, this proves that W′ is exactly the class of pairs of non-equivalent derivations with the same final sequent.

The history of the question. According to S. Mac Lane (in a letter to the author), he has been discussing the question whether a diagram is commutative in SMC categories iff all its instances in the category of vector spaces (say, over real or rational numbers) are commutative since about 1963. Although in this way the problem became more or less generally known, I am unaware of a published record.

M. Barr (e-mail to the author) suggested a similar question (not published) independently about 1970.

In ”Algebra of Proofs” by M.E.Szabo [17], chapter 8, one can find an assertion that a diagram is commutative in a free SMC category iff every its interpretation in the SMC category of real Banach spaces is commutative.

The following statement can be found in [1] (1979):

\underline{Theorem} A diagram commutes in all closed symmetric monoidal categories iff it commutes in the category of real vector spaces.

It is formulated in the appendix (by Po-Hsuang Chu, introducing the ”Chu construction”) with the reference to a paper ”Commutativity in Closed Categories” by Szabo, apparently never published. However, soon after the appearance of [17] it was realized that its proofs contained flaws, and the “Theorem” published in [1] remained a conjecture.

Furthermore, in a recent paper [7] C.B. Jay has shown that normalization result in chapter 8 is non-correct.

The detailed analysis of the proofs presented in chapters 7 and 8 of [17] (concerning nonsymmetric and symmetric monoidal closed categories respectively) shows, that the case-analysis there is incomplete ^{3}. M.E. Szabo considered only several particular concrete cases of “twisted evaluation” (in his and our terminology, “left-introduction of implication”), corresponding to wellknown non-commutative diagrams (without any fully general scheme, in difference from [18] or our paper, and without any reduction process to his particular cases). Other cases considered by M.E. Szabo were not related to “twisted evaluation” at all ^{4}.

For these reasons, we would suggest calling the theorem, formulated above, “Mac Lane’s conjecture”.

Aknowledgements. The author first has heard about the conjecture of S. Mac Lane from G.Mints in St.Petersburg, to whom is due his long-lasting interest in applications of proof theory to categories. He is very much obliged to Saunders Mac Lane himself, with whom he had the opportunities to discuss the matter during his two visits to St.Petersburg in 80’s, during one author’s visit to the University of Chicago at 1990, organized by professor Mac Lane, and later, in Denmark at 1993 and in Cambridge at 1995. The excellent working conditions at BRICS, Aaarhus, Denmark, were very helpful in carrying out the main part of this work. I am very grateful to all BRICS people (and especially Glynn Winskel). I am grateful to Anders Kock for useful discussions in the early stages of this work, and for all people and institutions that helped me to complete it during various visits (G. Longo, ENS, Paris, H. Schwichtenberg, Ludwig-Maximilan University, Munchen, I. Moerdijk, Utrect University, P. Damphousse, Tours University, and, finally, Zhaohui Luo and the University of Durham). I would thank Michael Barr for important information, clarifying the history of the question.

3It is easy to compare with our paper, since in [17] the proof-theoretical approach is used.

4For example, he considered the arrows that have in fact different graphs of naturality conditions [9], [18]. It can be shown, that already the instances of such arrows in 2-dimensional vector spaces are distinct

2 Statement of Result

The free symmetric monoidal closed category (SMC) F(A) over a set of atoms A can be represented by the calculus with formulas built in the ordinary way from elements of A and from the constant I by connectives ⊗ and −, and with the following axioms and rules. (This definition does not differ essentially from the definition of the “labelled deductive system” in [17].)

Axioms:

For all formulas A, B, C

id_{A} : A → A;
a_{ABC} : (A ⊗ B) ⊗ C → A ⊗ (B ⊗ C), a_{ABC}^{−1} : A ⊗ (B ⊗ C) → (A ⊗ B) ⊗ C;
b_{A} : A ⊗ I → A, b_{A}^{−1} : A → A ⊗ I; c_{AB} : A ⊗ B → B ⊗ A;
e_{AB} : (A − B) ⊗ A → B, d_{AB} : A → B − A ⊗ B.

Rules

\frac{φ : A → B ψ : C → D}{(φ ⊗ ψ) : A ⊗ C → B ⊗ D}(⊗), \frac{φ : A → B ψ : C → D}{(φ − ψ) : B − C → A − D}(−)

\frac{φ : A → B ψ : B → C}{(ψ ∘ φ) : A → C}(cut).

A similar calculus was called the “labelled deductive system” in [17]. Its derived objects are “labelled sequents” φ : A → B, where φ is a term built from a, a^{−1}, b, b^{−1}, c, e, d with appropriate indices. Taking into account the categorical meaning of these derived objects, we shall call them canonical maps.

Remark 2.1 The whole tree-form derivation in F(A) is actually encoded in (and can be reconstructed) from the label of its final sequent. Thus, we can, at will, consider only labels, labelled sequents (canonical maps) or tree-form derivations. If f : A → B is a canonical map, and f_{0} is obtained by erasing some indices in f, then often f can be reconstructed from f_{0} and A → B. When there is no confusion, we’ll sometimes omit indices in the labels of canonical maps.

Notation. b′_{A} will denote the b_{A} ∘ c_{IA} : I ⊗ A → A and z_{AB} the

(id − (b′ ∘ ((e ⊗ id) ∘ (a^{−1} ∘ ((id ⊗ c) ∘ a))))) ∘ d_{((B− I)⊗A)B} : (B − I) ⊗ A → (B − A)

.

In F(A) the formulas play the role of objects, and the morphisms from A to B are the equivalence classes of canonical maps φ : A → B, where the equivalence relation ≡ is the smallest relation, satisfying the following conditions (taking into account remark 2.1 we write only the equations between labels):

(i) F(A) is a category with cut as composition and axioms id_{A} : A → A as identity morphisms, i.e., for all derivations ψ : A → B, φ : B → C, χ : C → D,

id_{B} ∘ ψ ≡ ψ ∘ id_{A}; (χ ∘ φ) ∘ ψ ≡ χ ∘ (φ ∘ ψ);

(ii) ⊗ and − (considered as operations on formulas and morphisms) are functors, i.e., for all derivations

ψ : A → B, ψ′ : B → C, φ : A′ → B′, φ′ : B′ → C′

(ψ′ ∘ ψ) ⊗ (φ ∘ φ′) ≡ (ψ′ ⊗ φ′) ∘ (ψ ⊗ φ)

(ψ′ ∘ ψ) − (φ ∘ φ′) ≡ (ψ − φ′) ∘ (ψ′ − φ)

1_{A⊗B} ≡ 1_{A} ⊗ 1_{B}; 1_{A− B} ≡ 1_{A} − 1_{B};

(iii) the a, b, c are isomorphisms (with inverse a^{−1}, b^{−1}, c):

a_{ABC} ∘ a_{ABC}^{−1} ≡ id_{(A⊗B)⊗C}, a_{ABC}^{−1} ∘ a_{ABC} ≡ id_{A⊗(B⊗C)};
b_{A} ∘ b_{A}^{−1} ≡ id_{A}, b_{A}^{−1} ∘ b_{A} ≡ id_{A⊗I}; c_{AB} ∘ c_{BA} ≡ id_{A⊗B};

(iv) ordinary naturality conditions for each parameter of the a, c, b, e.g., if we take the first parameter of c, then for all ψ : A → C,

c_{CB} ∘ (ψ ⊗ 1_{B}) ≡ (1_{B} ⊗ ψ) ∘ c_{AB},

(we shall not write all these naturality conditions);

(v) ordinary naturality conditions for the second parameter of e and for the first parameter of d, and the following generalized naturality conditions for the first parameter of e and the second parameter of d: for all formulas A,B,C,D and ψ : A → D, e_{DC} ∘ (id_{D− C} ⊗ ψ) ≡ e_{AC} ∘ ((ψ − id_{C}) ⊗ id_{A}); ((id_{A} − id_{B}) ⊗ ψ) ∘ d_{BA} ≡ (ψ − id_{B⊗D}) ∘ d_{BD}, or, in the form of diagrams,

[figure: \begin{matrix}(D − C) ⊗ A & (D − C) ⊗ D \\ (A − C) ⊗ A & C \end{matrix}; (id_{D}− C)⊗ψ; (ψ− id_{C})⊗id_{A}; e_{DC}; e_{AC}]

[figure: \begin{matrix}B & D − B ⊗ D \\ A − B ⊗ A & A − B ⊗ D \end{matrix}; d_{BD}; d_{BA}; (ψ− id_{B}⊗id_{D}); id_{A}− id_{B}⊗ψ]

(vi) the so-called Kelly-Mac Lane coherence conditions for a, b, c e, d are satisfied:

a_{AB(C⊗D)} ∘ a_{(A⊗B)CD}≡(id_{A} ⊗ a_{BCD}) ∘ a_{A(B⊗C)D} ∘ (a_{ABC} ⊗ id_{D});
a_{BCA} ∘ c_{A(B⊗C)} ∘ a_{ABC}≡(id_{B} ⊗ c_{AC}) ∘ a_{BAC} ∘ (c_{AB} ⊗ id_{A});
b_{A⊗B}≡(id_{A} ⊗ b_{B}) ∘ a_{ABI};
(id_{A} − e_{AB}) ∘ d_{(A− B)A}≡id_{A− B};
e_{B(A⊗B)} ∘ (d_{AB} ⊗ id_{B})≡id_{A⊗B}.

(vii) ≡ satisfies the axiom ψ ≡ ψ, (viii) is closed under the rules

\frac{ψ ≡ φ}{φ ≡ ψ} \frac{ψ ≡ ψ′ ψ′ ≡ ψ′′}{ψ ≡ ψ′′}

(≡ is equivalence);

(ix) and the rules

\frac{φ ≡ φ′ ψ ≡ ψ′}{(φ ⊗ ψ) ≡ (φ′ ⊗ ψ′)} \frac{φ ≡ φ′ ψ ≡ ψ′}{(φ − ψ) ≡ (φ′ − ψ′)} \frac{φ ≡ φ′ ψ ≡ ψ′}{(φ ∘ ψ) ≡ (φ′ ∘ ψ′)}

where ψ, ψ′, ψ′′ : A → B, φ, φ′ : C → D, and, in the rule for composition, C = B (≡ is ”congruence”).

Since ≡ is defined as smallest relation, satisfying these conditions, ψ ≡ φ holds if and only if it is derivable from conditions of the groups (i)-(vii) by the rules of the groups (viii) and (ix).

The next two lemmas are immediate consequences of the definition of ≡.

Lemma 2.2 Equivalent maps always have the same type.

Let us denote by S[A_{1}/a_{1}, ..., A_{n}/a_{n}] the substitution of the formulas A_{1}, ..., A_{n} for the atoms a_{1}, ..., a_{n} respectively, in an arbitrary syntactic expression (in F(A) and in the other calculi considered below). If

ψ : A → B

is canonical map, then

ψ[A_{1}/a_{1}, ..., A_{n}/a_{n}] : A[A_{1}/a_{1}, ..., A_{1}/a_{1}] → B[A_{1}/a_{1}, ..., A_{1}/a_{1}]

is canonical map.

Lemma 2.3 If ψ ≡ φ : A → B then

ψ[A_{1}/a_{1}, ..., A_{n}/a_{n}] ≡ φ[A_{1}/a_{1}, ..., A_{n}/a_{n}]

for every formulas A_{1}, ..., A_{n} and atoms a_{1}, ..., a_{n}.

There is no need to give here the detailed definition of SMC category in general, since it will reproduce almost literally the definition above. The differences to be mentioned are that 1)the category itself (its objects, morphisms etc) is not necessarily described in any constructive way; 2)instead of formulas we have to consider arbitrary objects, I being just a distinguished object, and instead of canonical maps arbitrary morphisms; 3)⊗ : K × K → K, − : K^{op} × K → K are distinguished functors; 4) a_{ABC}, ..., d_{AB} are components of distinguished natural transformations a, ..., d (families of morphisms indexed by objects and satisfying naturality conditions); 5)the equality of morphisms in K should satisfy the conditions of the definition of ≡ (with = instead of ≡) except that of being minimal.

The category F(A) is free in the sense that for every SMC category K, every assignment J : A → Ob(K) can be extended to the unique structure-preserving functor

| − |_{J} : F(A) → K.

As a consequence, given two canonical maps ψ, φ : A → B, ψ ≡ φ iff |ψ|_{J} = |φ|_{J} for all assignments J in all possible SMC categories K.

Definition 2.4 Let K be an SMC category. We shall say that K has test-property if for all canonical maps ψ, φ : A → B with ψ non-equivalent to φ, there exists an assignment J in K such that |ψ|_{J} ≠ |φ|_{J}.

Thus, K is a complete model with respect to equality in SMC categories.

Definition 2.5 (Sign or variance of an occurrence.) (i) The sign of C in C is + (the occurrence is covariant).

(ii) ⊗ does not change signs (variances).

(iii) The signs (variances) of the occurrences in A− B are the same as in B for the occurrences lying in B, and for the occurrences lying in A + is changed to − and − to + (covariant became contravariant and vice versa).

(iv) The sign (variance) of an occurrence in the sequent A_{1}, ..., A_{n} → B is the same as in A_{1} ⊗ (... ⊗ A_{n})...) − B.

Definition 2.6 The sequent S is called balanced if every atom, occurring in S, occurs exactly twice and with opposite variances.

Often only the interpretations (or even only one canonical interpretation) in the category N(K) of functors and natural transformations over a category K were considered [9], [18]. This “lifting” is closely connected with the interpretations | − |_{J}, because |ψ|_{J} always is a component of natural transformation in N(K)). Meanwhile, in general not all the components of the natural transformation, corresponding to ψ have the form |ψ|_{J} for some J, because the structure of ψ could impose some “extra” identifications of variables in |ψ|_{J}. For example, take ψ = c_{A}A : A ⊗ A → A ⊗ A. (Naturality conditions in N(K) divide atoms (even identical) into independent pairs, see for details [9], [18]). Considering only the the interpretations in N(K), one will obtain a different notion of test-property (distinguishing more arrows in F). For arbitrary K, it will coincide with the notion defined above only for ψ, ϕ : A → B with balanced A → B. (Because for balanced A → B the identifications imposed by sintactical structure and by naturality conditions coincide.) This modified notion of test-property may be called “balanced test-property”.

Lemma 2.7 Let K be a category with biproduct (i.e., product coinciding with coproduct). Then K has test-property iff it has balanced test-property.

Proof is based on the possibility of obtaining any component of a natural transformation

F (A_{1}A_{2}..A_{n}) → G(A_{1}A_{2}...A_{n})

from the component

F (AA..A) → G(AA...A)

with A = A_{1} ∘ ... ∘ A_{n} using canonical projections and injections

A_{i} → A_{1} ∘ ... ∘ A_{n} → A_{i}

and naturality conditions (∘ denoting biproduct).□

Note that the SMC category of vector spaces over a field or modules over a commutative ring has biproducts.

The conjecture of S.Mac Lane may be formulated as follows:

The category of real vector spaces has the test-property.

Since S.Mac Lane usually considered interpretations in N(K), it would be somewhat more close to his original formulation to take here balanced test-property, but, as we see from the lemma above, at least for such categories as vector spaces or modules, balanced and full test-property are equivalent.

In section 10, we define axiomatically a “test-category” V.

This is an abstract analog of the SMC subcategory of the category of vector spaces over a field I, generated by three objects: I, zero-space 0, and the space V of countable dimension. (The main difference from the corresponding subcategory of the category of vector spaces is that unnecessary arrows are omitted.)

Theorem 1 If an SMC category K contains an SMC subcategory V, which satisfies the axioms of test-category in section 10, then K has balanced test-property. If K has biproducts, then it has also full test-property. In particular, the category of vector spaces over a field I has the test-property.

3 Some known results about F(A)

Definition 3.1 Canonical maps, obtained from a_{ABC}, a_{ABC}^{−1}, b_{A}, b_{A}^{−1}, c_{AB}, id_{A} by (⊗) and composition are called central isomorphisms.

Proposition 3.2 (Coherence of centrals, [9]) All central isomorphisms ψ, φ : A → B with balanced A → B are equivalent.

A formula is constant if it does not contain atoms (is built only from constant I).

Proposition 3.3 (Coherence for closed categories, [9]) Let ψ, φ : A → B be canonical maps and the sequent A → B be balanced and do not contain occurrences of the subformulas of the form C − D with D constant and C non-constant. Then ψ ≡ φ.

There is also a “cut-elimination” theorem, proved by Kelly and Mac Lane, [9], Theorem 6.5, see also [8]. (It allows actually some “controlled” use of cut.)

Definition 3.4 Let ψ : A → B, φ : A ⊗ B → C, φ′ : A → B − C be arbitrary canonical maps. Then denote

< ψ >⇀ ↽ e_{BC} ∘ (id_{B− C} ⊗ ψ) : (B − C) ⊗ A ⟶ C,
π_{ABC}(φ) ⇀ ↽ (id_{A} − φ) ∘ d_{AB} : A → B − C,
π_{ABC}^{−1}(φ′) ⇀ ↽ e_{BC} ∘ (φ′ ⊗ id_{B}) : A ⊗ B → C.

(Using π for adjunction we follow Kelly and Mac Lane [9].)

Proposition 3.5 Every canonical map ψ : A → B is equivalent to some canonical map φ : A → B, which is derivable in the calculus with the rules (⊗),

\frac{ψ : A ⊗ B → C}{π_{ABC}(ψ) : A → (B − C)} and \frac{ψ : A → B φ : C ⊗ D → E}{φ ∘ (< ψ > ⊗id_{D}) : ((B − C) ⊗ A) ⊗ D → E},

and cut only in case when one of its premises is central isomorphism.

Example 3.6 The following is an example of a non-commutative diagram in F(A) :

[figure: (((a − I) − I) − I) ⊗ ((a − I) − I); <π(e_{aI}∘c)− id_{I}>∘c; e; I]

(cf. the diagram (1.4) from [9], that can be obtained by application of π). Note that one e uses right, and another left factor as function space (“twisted evaluation”). Any interpretation | − |_{J} in the category of vector spaces with J(a) = V, where V is a vector space of infinite dimension, renders this diagram non-commutative, because the factors have different dimension.

4 The calculus L(A) and its connection with F(A).

The formulas of L(A) are the same as in F(A). It is defined by the following axioms and rules. (This definition does not differ essentially from the definition of the “unlabelled deductive system” in [17], though deductive systems for SMC categories can be found in earlier works [11], [13]. The calculus may be considered also as the multiplicative intuitionistic linear logic, see [5].)

Axioms

\overline{A → A} (identity)  \overline{→ I} (unit)

Structural Rules

\frac{Γ → A A, Δ → B}{Γ, Δ → B} (cut) \frac{Δ ⟶ I Σ ⟶ A}{Δ, Σ ⟶ A} (wkn)

Logical rules

\frac{Γ → A Δ → B}{Γ, Δ → A ⊗ B} (→⊗) \frac{A, B, Γ → C}{A ⊗ B, Γ → C} (⊗→)

\frac{A, Γ → B}{Γ → A − B} (→−)  \frac{Γ → A B, Δ → C}{Γ, A − B, Δ → C} (−↪)

Derived objects of L(A) are unlabelled sequents. Here Σ, Γ, Δ are multisets of formulas; A, B, C formulas. The “wkn” is an abbreviation for weakening (this form of weakening in presence of cut is equivalent to “restricted weakening”, where only the constant I can be added). If not stated otherwise, we shall always suppose (wkn) to be non-trivial (i.e., with Δ non-empty).

As usual, in logical rules A, B are called their “side formulas” , and A− B, A⊗B their “main” formulas. (Other formulas are parametric.) A is the main formula of cut; we shall often call it the “cut-formula”. ”Cut” has no side formulas. Other formulas are called parametric.

In the system L⃗(A) left sides of the sequents are lists (not multisets) of formulas. It has the same rules as L, but Γ, Σ, Δ are understood as lists, and the following rule of permutation

\frac{Γ → C}{Γ′ → C} (perm),

is added (where Γ′ is any non-trivial permutation of Γ).

The transformations D of F(A)-derivations into L⃗(A)-derivations and C of L⃗(A)-derivations into equivalence classes of F(A)-derivations can be described. Both are defined by induction on the process of construction of a derivation.

Thus, D(id_{A} : A → A) = A → A, other axioms of F(A) are replaced (after deleting their labels) by their obvious cut-free derivations, and if D is already defined for derivations of the premises of a rule, then

D(\frac{ψ : A → B φ : C → D}{(ψ ⊗ φ) : A ⊗ C → B ⊗ D})  = \frac{\frac{A ⟶^{D(ψ)} B C ⟶^{D(φ)} D}{A, C ⟶ B ⊗ D}}{A ⊗ C ⟶ B ⊗ D}

D(\frac{ψ : A → B φ : C → D}{(ψ − φ) : B − C → A − D}) = \frac{\frac{A ⟶^{D(ψ)} B C ⟶^{D(φ)} D}{A, B − C ⟶ D}}{B − C ⟶ A − D}

D(\frac{ψ : A → B φ : B → D}{(ψ ∘ φ) : A → D})  = \frac{A ⟶^{D(ψ)} B B ⟶^{D(φ)} D}{A → D}

The description of C is more complex (cf. [17]). Let a_{1}, ..., a_{n} be different atoms. For any two formulas C, C′ built by ⊗ from a_{1}, ..., a_{n}, taken in arbitrary order (each atom used in each formula exactly once), with arbitrary order of brackets, and, possibly, with addition of some I, there exists unique (up to ≡) central isomorphism ζ : C → C′. (“Coherence of centrals.”)

If D, D′ are built from formulas A_{1}, ..., A_{n} in similar way (one can write

[A_{1}/a_{1}, ..., A_{n}/a_{n}]C = D, [A_{1}/a_{1}, ..., A_{n}/a_{n}]C′ = D′,

with C, C′ as above) then the instance

[A_{1}/a_{1}, ..., A_{n}/a_{n}]ζ : D → D′

also is a central isomorphism.

Let Φ(Γ⃗) denote the formula A_{1} ⊗ (... ⊗ A_{n})...) for Γ non-empty, and I otherwise. In the definition below, ψ, φ are L⃗-derivations, and ζ denotes the central isomorphism, defined

as above (maybe, different in different places).

• C(A → A) = b_{A} : A ⊗ I → A;

• C(→ I) = id_{I} : I → I;

• C(\frac{A, Γ →^{ψ} B}{Γ → A − B}) = π(C(ψ) ∘ ζ ∘ c_{Φ(Γ)A}) : Φ(Γ) → (A − B),

with ζ : A ⊗ Φ(Γ) → Φ(A, Γ);

• C(\frac{Γ →^{ψ} A B, Δ →^{φ} C}{Γ, A − B, Δ → C}) =

= (C(φ) ∘ (< C(ψ) > ⊗id_{Φ(Δ)}) ∘ ζ : Φ(Γ, A − B, Δ) → C, ζ : Φ(Γ, A − B, Δ) → ((A − B) ⊗ Φ(Γ)) ⊗ Φ(Δ);

• C(\frac{Γ →^{ψ} A Δ →^{φ} B}{Γ, Δ → A ⊗ B} (→ ⊗)) = (C(ψ) ⊗ C(φ) ∘ ζ : Φ(Γ, Σ) → B ⊗ A,

ζ : Φ(Γ, Δ) → Φ(Γ) ⊗ Φ(Δ);

• C(\frac{A, B, Γ →^{ψ} C}{A ⊗ B, Γ → C} (⊗ →)) = C(ψ) ∘ a_{ABΦ(Γ)} : Φ((A ⊗ B), Γ) → C,

note that Φ(A, B, Γ) = A ⊗ (B ⊗ Φ(Γ));

• C(\frac{Δ →^{ψ} I Σ →^{φ} B}{Δ, Σ → B} (wkn)) = b′_{B} ∘ ((C(ψ) ⊗ C(φ)) ∘ ζ) : Φ(Σ, Γ) → B, ζ : Φ(Γ, Σ) → Φ(Γ) ⊗ Φ(Σ);

• C(\frac{Γ →^{ψ} B}{Γ′ → B} (perm)) = C(ψ) ∘ ζ : Φ(Γ′) → B,

ζ : Φ(Γ′) → Φ(Γ), Γ′ is permutation of Γ;

• C(\frac{Γ →^{ψ} A A, Δ →^{φ} B}{Γ, Δ → B} (cut)) = (C(φ) ∘ (C(ψ) ⊗ 1_{Φ(Δ)})) ∘ ζ : Φ(Γ, Δ) → B, ζ : Φ(Γ, Δ) → Φ(Γ) ⊗ Φ(Δ).

Of course, one can use diagrams to represent resulting derivations of FA, for instance, in case of

C(\frac{Γ →^{ψ} A B, Δ →^{φ} C}{Γ, A − B, Δ → C} (−↪))

we have

Φ(Γ, A − B, Δ)

((A − B) ⊗ Φ(Γ)) ⊗ Φ(Δ)

B ⊗ Φ(Δ)

Φ(B, Δ)

C

central

<C(ψ)>⊗id_{Φ(Δ)}

central

C(φ)

Lemma 4.1 For every ψ : A → B in F(A), C(D(ψ)) ≡ ψ.

D can be used also to define the transformation of canonical maps into derivations in the calculus L(A) with unordered antecedents (it is enough to “forget” the ordering).

Every derivation ψ of Γ → A in L(A) can be transformed in a derivation in L⃗(A) by ordering of antecedents and inserting necessary inferences of perm. C can be used to transform it further in a canonical map. Taking into account “coherence of centrals”, one can easily check, that only the ordering of the antecedent of its final sequent influences the equivalence class of resulting canonical map, and if this ordering is changed, the canonical map is composed with an instance of central isomorphism, depending only on the change of ordering, and not on ψ. Thus, one can correctly define CΓ⃗ on the derivations of Γ → A (depending on this ordering).

Lemma 4.2 Let ψ, φ be two derivations of Γ → A in L(A), and Γ⃗′, Γ⃗′′ be two orderings of Γ. Then

CΓ⃗′(ψ) ≡ CΓ⃗′(φ) ⟺ CΓ⃗′′(ψ) ≡ CΓ⃗′′(φ).

Definition 4.3 Let φ, φ′ be derivations of the same sequent in L⃗(A). Then φ ≡ φ′ ⟺ C(φ) ≡ C(φ′).

Lemma 4.2 also justifies the following definition:

Definition 4.4 Let φ, φ′ be derivations of Γ → A in L(A). Then φ ≡ φ′ ⟺ CΓ⃗(φ) ≡ CΓ⃗(φ′) for some ordering Γ⃗.

By lemma 4.1 it will be enough to consider L(A)-derivations.

The interpretation | − |_{J} for L(A) is defined as composition of already defined interpretation of F(A) with C. ( To avoid ambiguity, we assume that some ordering of antecedent of each final sequent is fixed; as we explained above,it doesn’t matter what was concrete choice of that ordering.)

5 Some facts about derivations in L(A).

Example 5.1 The non-commutative diagram from 3.6 is represented by the following pair of derivations:

\frac{(a − I) − I → (a − I) − I I → I}{((a − I) − I) − I, (a − I) − I → I}

and

\frac{\frac{\frac{\frac{\frac{a → a I → I}{(a − I), a → I}}{a → (a − I) − I} \overline{I → I}}{((a − I) − I) − I, a → I}}{((a − I) − I) − I → (a − I)} \overline{I → I}}{((a − I) − I) − I, (a − I) − I → I}.

This pair represents also an example of “twisted applications” of −↪.

These facts are based mostly on the definition of ≡ for sequent derivations and known facts about F(A). For other methods that can be used to check ≡ see, e.g., [6], [13]. Proposition 5.2 (Cut-elimination theorem, cf. [9], [8].) Every derivation in L is equivalent to a cut-free derivation of the same sequent. Proposition 5.3 (Kelly-Mac Lane coherence theorem for L). Let S be balanced sequent which does not contain occurrences of formulas of the form C − D with D constant (containing only I) and C non-constant. Then all its derivations in L are equivalent. Lemma 5.4 If a subderivation ψ of some derivation φ is equivalent to ψ′ then the derivation φ′ obtained from φ by replacement of ψ by ψ′ is equivalent to φ. Definition 5.5 We shall call a derivation ψ in L atomic if it contains only the axioms of the forms a → a, I → I, and → I. Lemma 5.6 Every derivation ψ in L is equivalent to an atomic derivation of the same sequent.

Proof. For every axiom A → A there exists an equivalent atomic derivation (it can be proved directly by induction or using coherence theorem). Replace all axioms in ψ by their atomic derivation. □ Lemma 5.7 Let the sequent S = A_{1}, ..., A_{n} → B contain odd number of occurrences of an atom a. Then S is not derivable in L.

Proof. By induction (consider cut-free derivations).□ Lemma 5.8 Every cut-free derivation ψ of a balanced sequent in L contains only balanced sequents.

Proof by induction, using lemma 5.7. □ Lemma 5.9 In any cut-free derivation of a balanced sequent the premises of each rule have no atoms in common.

Permutation of rules with “cut”.

Lemma 5.10 Let (r) be some rule and let us consider the derivations of the following structure

(1)\frac{\frac{\frac{ψ}{S_{0}}}{S_{1}} (r) \frac{ξ}{S_{2}}}{S}(cut) ; (2)\frac{\frac{\frac{ψ}{S_{0}} \frac{φ}{S_{1}}}{S_{2}} (r) \frac{ξ}{S_{3}}}{S}(cut)

(3)\frac{\frac{ξ}{S_{2}} \frac{\frac{ψ}{S_{0}}}{S_{1}} (r)}{S}(cut) ; (4)\frac{\frac{ξ}{S_{3}} \frac{\frac{ψ}{S_{0}} \frac{φ}{S_{1}}}{S_{2}} (r)}{S}(cut),

where ψ, φ, ξ are arbitrary derivations. If the cut-formula in these derivations is not at the same time the main formula of the rule (r), then they are equivalent respectively to the derivations

(1′)\frac{\frac{\frac{ψ}{S_{0}} \frac{ξ}{S_{2}}}{S′_{1}}(cut)}{S}(r) (2′)\frac{\frac{ψ}{S_{0}} \frac{\frac{φ}{S_{1}} \frac{ξ}{S_{3}}}{S′_{2}} (cut)}{S}(r)

(3′)\frac{\frac{\frac{ξ}{S_{2}} \frac{ψ}{S_{0}}}{S′_{1}}(cut)}{S}(r) (4′)\frac{\frac{\frac{ξ}{S_{3}} \frac{ψ}{S_{0}}}{S′_{2}} (cut) \frac{φ}{S_{1}}}{S}(r) or (4′′)\frac{\frac{\frac{ξ}{S_{3}} \frac{φ}{S_{1}}}{S′_{2}} (cut) \frac{ψ}{S_{0}}}{S}(r)

where new inferences have the same main and cut-formulas as in (1)-(4).

Remark 5.11 Some inferences in this lemma are excluded by the condition that the main formulas of (r) and (cut) do not coincide. For example, if the left premise of (cut) is the conclusion of (r) (as in cases (1), (2)), (r) cannot be (→ −) or (→ ⊗).

Corollary 5.12 Every cut can be moved up to the application of rule which has cut-formula as its main formula in such a way, that resulting derivation is equivalent to original one.

The following two lemmas are particular cases of cut-elimination procedure:

Lemma 5.13 For every two derivations ψ of Γ → A and φ of B, Δ → C,

\frac{\frac{Γ →^{ψ} A B → B}{Γ, A − B → B} \frac{φ}{B, Δ → C}}{Γ, A − B, Δ → C} ≡ \frac{Γ →^{ψ} A B, Δ →^{φ} C}{Γ, A − B, Δ → C}

Lemma 5.14 For every derivations ξ of B′ → B, ψ of Γ → A and φ of B, Δ → C,

\frac{\frac{\frac{A → A B′ →^{ξ} B}{A, A − B′ → B}}{A − B′ → A − B} \frac{Γ →^{ψ} A B, Δ →^{φ} C}{Γ, A − B, Δ → C}}{Γ, A − B′, Δ → C} ≡ \frac{\frac{ψ}{Γ → A} \frac{B′ →^{ξ} B B, Δ →^{φ} C}{B′, Δ → C}}{Γ, A − B′, Δ → C}.

Permutation of rules, different from “cut”.

Lemma 5.15 Every derivation ψ of the sequent A⊗B, Γ → C is equivalent to a cut-free derivation which ends by an application of (⊗ →).

Proof. Make cut with

\frac{A → A B → B}{A, B → A ⊗ B},

and then apply the rule ⊗ →. From definition of C and “coherence of centrals” follows that the result is equivalent to ψ. Eliminate cut (this doesn’t influence last ⊗ →). By cut-elimination theorem the result is again equivalent to ψ. □

Lemma 5.16 Every derivation ψ of the sequent Γ → A − B is equivalent to a cut-free derivation which ends by an application of (→ −).

Proof. Make cut with

\frac{A → A B → B}{A, A − B → B},

and apply → −. The rest as in previous lemma.□

Lemma 5.17 Let S = Δ → A be an arbitrary balanced sequent. If Δ = Δ_{1}, Δ_{2} and the list Δ_{1} is balanced, then for every derivation ψ of S there exist derivations ψ_{1} of the sequent Δ_{1} → I and ψ_{2} of Δ_{2} → A, such that

ψ ≡ \frac{Δ_{1} →^{ψ_{1}} I Δ_{2} →^{ψ_{2}} A}{Δ_{1}, Δ_{2} → A} (wkn).

Proof by induction on the length of the final sequent of ψ (one can assume that ψ is cut-free). It is easy to check applicability of the induction hypothesis to the premise(s). The computations, necessary for the inductive step, should be done in F(A) using C and the definition of ≡. They are relatively lenghty, and can be found in [15], where a reformulation of this lemma for F(A) is proved directly (lemma 19). □

Taking into account lemmas 5.8 and 5.9, one can derive the following corollaries.

Corollary 5.18 Let S = Δ → A be an arbitrary balanced sequent.If some derivation of S ends by wkn, with the premises Δ_{1} → I and Δ_{2} → A then Δ_{1} is balanced and every derivation of S is equivalent to a derivation ending by wkn with the same premises.

Corollary 5.19 Let S = Δ → A ⊗ B be a balanced sequent such that there exist two derivations of S ending by applications of (→ ⊗) with different premises. Then every derivation of S is equivalent to a derivation which ends by (non-trivial) wkn.

Proof. Let Δ_{1} → A, Δ_{2} → B and Δ′_{1} → A, Δ′_{2} → B be the premises of ⊗ → in question. At least one of multisets Δ_{1} ∩ Δ′_{2}, Δ′_{1} ∩ Δ_{2} is non-empty. It has to be balanced, else one of the premises will be unbalanced. Now lemma 5.17 can be applied.□

Corollary 5.20 Let S = Σ → C − D be balanced sequent. If the sequent S^{−} = Σ, C → D has two derivations ending by different applications of wkn, then every derivation of S is equivalent to a derivation ending by wkn.

Corollary 5.21 Let S = Δ → C − D be a balanced sequent which has no derivation ending by wkn. Then for S^{−} = Δ, C → D the following alternative holds: (i)it has no derivation ending by wkn; (ii)or it has a derivation ending by wkn, and all its derivations are equivalent to some derivation ending by the same wkn with left premise of the form C, Δ_{1} → I.

Lemma 5.22 Let S = Δ → A ⊗ B be an arbitrary derivable balanced sequent. If Δ can be presented as Δ_{1}, Δ_{2} with S_{1} = Δ_{1} → A and S_{2} = Δ_{2} → B balanced sequents, then for every derivation ψ of S there exist derivations ψ_{1} of the sequent Δ_{1} → A and ψ_{2} of Δ_{2} → B, such that

ψ ≡ \frac{Δ_{1} →^{ψ_{1}} A Δ_{2} →^{ψ_{2}} B}{Δ_{1}, Δ_{2} → A ⊗ B} (→ ⊗).

Proof by induction on the length of the final sequent of ψ. (For computations see citesol90).□

One has much less freedom with permutations of −↪.

By the following lemma we can sometimes “pull down” a −↪.

Lemma 5.23 Let ψ be a derivation of the form

\frac{\frac{Δ →^{ψ_{1}} A B, Σ →^{ψ_{2}} C}{Δ, A − B, Σ → C}(−↪) [\frac{ψ_{3}}{S_{1}}]}{S}(r)

with arbitary rule (r)(the part in the square brackets is absent when (r) has only one premise). If the main formula of (r) does not belong to Δ, A − B, then

ψ ≡ \frac{\frac{ψ_{1}}{Δ → A} \frac{\frac{ψ_{2}}{B, Σ → C} [ \frac{ψ_{3}}{S_{1}} ]}{S′}(r)}{S}(−↪).

Proof. Direct calculation, using definition of ≡.□

Lemma 5.24 Every derivation ending by −↪ is equivalent to a derivation ending by “minimal” application of the same rule, i.e., −↪ such that the subderivation of its left premise is not equivalent to any derivation ending by −↪.

Proof by induction on the length of the left premise of the last −↪, taking into account that if the derivation of this premise also ends by −↪, then the conditions of the previous lemma will be satisfied. □

Lemma 5.25 Let in the sequent S = Γ → A the formula A be a or a ⊗ b with a, b being variables or I. Let Γ not contain formulas of the form C ⊗ D and contain at least one formula of the form C − D. Then every derivation of S is equivalent to a derivation ending by an application of the rule (−↪).

Proof by induction on the length of φ (see [15], lemma 16).□

6 Reduction to 2-sequents.

We do not give detailed proofs in this section, since the reduction is described in detail in our paper [15] (including categorical aspects).

Definition 6.1 The sequent Γ → A will be called a 2-sequent if A contains no more than one connective, and each member of Γ no more than two connectives.

As follows from this definition, A has one of the forms a, a ⊗ b, a − b and the members of the list Γ have one of the forms a, a ⊗ b, a ⊗ (a ⊗ b), (a ⊗ b) ⊗ c, a − b, a − (b ⊗ c), (a ⊗ b) − c, a − (b − c), (a − b) − c, where a, b, c denote atoms and possibly the constant I. Some members of these lists are not necessary, as the study in [15] shows (for example, one of (a ⊗ b) − c, a − (b − c) can be eliminated, since they are isomorphic). This motivates the following

Definition 6.2 The sequent Γ → A will be called pure 2-sequent if A has one of the following forms (a, b, c denote only atoms, and NOT the constant I):

I, a, a ⊗ b, a − I, a − b

and the members of Γ have one of the forms

a, a ⊗ b, a − I, a − b, a − (b ⊗ c), (a ⊗ b) − I, (a ⊗ b) − c,
(b − I) − I, (b − a) − I, (b − I) − c, (b − a) − c

Lemma 6.3 Cut-free derivation of any balanced pure 2-sequent contains only balanced pure 2sequents.

Proposition 6.4 Let S = Γ → B be any balanced sequent. There exist a balanced pure 2-sequent S_{0} = Γ_{0} → b, such that for every derivations ψ, ψ′ of S in L(A) there exist some derivations ψ_{0}, ψ′_{0} of S_{0} and

ψ ≡ ψ′ ⟺ ψ_{0} ≡ ψ′_{0}.

For every SMC category K similar equivalence holds for corresponding natural transformations

∥ψ∥ = ∥ψ′∥ ⟺ ∥ψ_{0}∥ = ∥ψ′_{0}∥.

Let us explain the general idea of the reduction (it comes from proof theory).

1) Every derivation ψ of a sequent Γ → B can be transformed into the derivation

ψ_{1} = \frac{Γ →^{ψ} B p → p}{Γ, B − p → p}

Here p is an atom which does not occur in Γ → B. This transformation is invertible, because we can obtain a derivation equivalent to ψ by substitution [B/p] in ψ′ and then use cut with the sequent → B − B.

If we apply this transformation to two derivations ψ, ψ′ then for the resulting derivations ψ_{1} ≡ ψ′_{1} will hold iff ψ ≡ ψ′.

2) Let A(p) be a formula containing a single occurrence of an atom p. Then, depending on the sign of p in A(p), one of the following sequents is derivable for every C:

A(p), p − C → A(C) (p positive) and

A(p), C − p → A(C) (p negative) In both cases there exist canonical derivation ζ(A(p), C).

If the list Γ in the sequent Γ → B contains a member A(C) (C can stand for any (single) occurrence of a subformula) then this subformula can be “extracted” by cut with ζ(A(p), C). If p does not occur in Γ → B, then this transformation (applied to a derivation ψ of Γ → B) is also invertible: we can return to ψ by substitution of C and cut with → C − C.

Applying 1) and then iterating 2) we can transform every derivation of an arbitrary sequent S into a derivation of some 2-sequent. Note, that this sequent does depend only on S (not on derivations) Balancedness is preserved. We can obtain pure 2-sequent by applications of cut with the derivations representing canonical isomorphisms. (Of course, cut always can be eliminated afterward.)

This construction can be generalized to natural transformations over any given SMC category K, since instead of cut one can take composition, and substitution is interpreted as ”vertical” composition with functor (i.e., one uses the structure of 2-category of functors and natural transformations).

Theorem 2 Let ψ, φ : Γ → A be some derivations of a balanced sequent, and ψ′, φ′ be corresponding derivations of a balanced pure 2-sequent. If for some assignment J : A → ObK |ψ′|_{J} ≠ |φ′|_{J} then for the same assignment |ψ|_{J} ≠ |φ|_{J}.

The following two lemmas show how reduction to pure 2-sequents can help with permutation of rules.

Lemma 6.5 Let ψ be a cut-free derivation of a balanced pure 2-sequent, and S be some sequent, occurring in ψ. If some antecedent member of S has the form A − B, then it is not side formula in any rule below this occurrence of S in ψ.

Proof. By lemma 6.3, all sequents in ψ are balanced pure 2-sequents. If an antecedent member A − B is a side formula of a rule, then the conclusion of this rule contains A − B as proper subformula of a formula. By definition of pure 2-sequent, this formula can be only (A − B) − C and lie at the left side of arrow. It is possible only if A− B is the succedent of one of the premises. Contradiction. □

Lemma 6.6 Let ψ be a cut-free derivation of a balanced pure 2-sequent, and the left premise of an application (r) of −↪ in ψ be of the form

C_{1} − D_{1}, ..., C_{k} − D_{k} → A.

Then ψ is equivalent to a derivation, ending by an application of −↪ with the same left premise.

Proof. By previous lemma and lemma 5.23. □

We shall need also a particular case of one lemma from [15] (reformulated for L and pure 2-sequents).

Let D(a) be any antecedent formula of a pure 2-sequent, containing exactly one negative occurence of an atom a (see the list of possible D(a) above). Denote by D̃(I) the result of replacement of a by the constant I and, if necessary, reduction to an isomorphic formula of the form, permitted by the definition of pure 2-sequent. For example, if D(a) = a − b, D̃(I) = b, and if D(a) = (b − a) − I, D̃(I) = (b − I) − I) = [I/a]D(a) (no reduction needed). In all cases there exists a derivation ε_{D(a)} : D(a), a → D̃(I). (It is enough to consider cut-free derivations. All possible derivations differ only in unessential permutations of wkn, and uniqueness up to ≡ can be checked in straightforward way.)

For example, if D(a) = a − b, then the derivation is

\frac{a → a b → b}{a − b, a → b}.

Lemma 6.7 (See [15], lemma 24) Every derivation ψ(a) of a balanced pure 2-sequent D(a), a, Γ → A is equivalent to the derivation

\frac{D(a), a ⟶^{ε_{D(a)}} D̃(I) D̃(I), Γ →^{ψ̃(I)} A}{D(a), a, Γ → A}.

7 Abstract coherence theorem.

In [18] R.Voreadou presented a description all non-equivalent pairs of canonical maps (noncommutative diagrams in F(A) ) in terms of two classes W_{0} and W. The class W_{0} was the class of “generating” pairs, in the sense, that all the pairs of W were obtained from the pairs belonging to W_{0} by certain rules. According to R.Voreadou, two canonical maps are not equivalent iff they belong to W.

R.Voreadou’s method was 1) to prove an “abstract coherence theorem” (in our terms, that if two derivations ψ, φ with the same final sequent do not belong to W, then they are equivalent) and 2) to build a model (also a syntactic calculus, posessing an SMC structure, in Voreadou’s case) where the pairs ψ, φ belonging to W are interpreted as non-commutative diagrams. In general we follow her ideas. One novelty is that building the calculus used as a model we connect it from the beginning with a certain subcategory of the category of vector spaces.

The proposition 2, p.3 [18] is an important part of her proof of the“abstract coherence theorem”. In our terminology it says that every derivation ψ of a sequent of the form Γ, A− B, Δ → C under certain conditions is equivalent to a derivation ending by the rule −↪. The conditions of the proposition are too permissive, and it allows a couneterexample ^{5}.

We need, of course, some lemmas describing the behaviour of −↪. Our lemmas 5.23, 5.25, 6.5, 6.6 and (implicitely) 6.7 treat some sides of this problem. Yet they are weaker than the statement of Voreadou’s proposition 2.

In this work we had to modify the definition of R.Voreadou’s classes in such a way, that the scheme of her proof could be applied. Our proof of the conjecture of Mac Lane will provide at the same time a new proof of R.Voreadou’s main theorem (with modified classes.) It is not clear, whether our class W′ is different from the class W of R.Voreadou (but it can be shown, that it contains W). By theorem 2 it is enough to consider pure 2-sequents, and for the sake of simplicity we give all definitions only for this case ^{6}.

Definition 7.1 The pair of derivations ζ_{1}, ζ_{2} of the same balanced 2-sequent S = Δ, A − I, A′ − I → I is called critical if

1.

ζ_{1} = \frac{Δ, A − I →^{ξ_{1}} A′ I → I}{Δ, A − I, A′ − I → I} ζ_{2} = \frac{Δ, A′ − I →^{ξ_{2}} A I → I}{Δ, A − I, A′ − I → I},

2. cut-free derivation of S can end only by (some) application of −↪, but

3. the subderivations ξ_{1}, ξ_{2} are not equivalent to derivations ending by −↪.

The critical pair will be called minimal, if Δ doesn’t contain single atoms as its members.

The class W′_{0} is the class of minimal critical pairs.

Lemma 7.2 Δ has no members of the form C ⊗ D.

Proof. Use definition and lemma 5.15.□

Lemma 7.3 The formulas A, A′ in ζ_{1}, ζ_{2} have one of the forms a − b, a − I and a′ − b′, a′ − I respectively.

5One of two non-equivalent derivations of the sequent ((a − I) − I) − b, (a − I) − I → (b − I) − I is NOT ending by −↪. One can easily obtain a version for canonical maps or corresponding version for 2-sequents.

6Probably, it is curious to note, that the reduction of the example 5.1 to 2-sequents provides the pair of derivations related to so called “Arens’ multiplication” (another well-known example of non-commutative diagram in SMC categories)

Proof. Because we consider pure 2-sequents, possible forms for A are a, a ⊗ b, a − I and a − b, and similarly for A′ (a, b variables, not I). The left side of the sequent

Δ, A − I, A′ − I → I

does not contain members of the form C ⊗ D.

Then in cases A = a, a ⊗ b by lemma 5.25 it should exist a derivation of the sequent

Δ, A′ − I → A

ending by (−↪) and equivalent to ξ_{2}. That contradicts the definition of critical pairs.

For A′ the proof is analoguous.

□

Substitutions of I and their action on sequents and derivations.

Definition 7.4 Let α = [I/a_{1}, ..., I/a_{n}] be a substitution, and ψ be a derivation of some balanced pure 2-sequent S = Γ → A. Let us denote by α ∗ ψ a derivation, obtained by:

1)application of α to ψ;

2)cuts (with isomorphisms) making the final sequent of the derivation [I/a_{1}, ..., I/a_{n}]ψ pure;

3)elimination of cuts.

Remark 7.5 The operation ∗ is defined here in a “non-deterministic” way, because the order of cuts is not fixed. For our purposes it is not relevant: we shall assume only, that when ∗ is applied to two derivations ψ, φ of the same sequent, the order of cuts is the same. The same, of course, will be the new final sequent of α ∗ ψ and α ∗ φ. Meanwhile, it can be shown that α ∗ ψ is uniquely determined up to ≡.

Definition 7.6 The class W′ consists of all pairs ζ_{1}, ζ_{2} of the same balanced pure 2-sequent S, such that for some substitution α of I for some variables

(α ∗ ζ_{1}, α ∗ ζ_{2}) ∈ W′_{0}.

The following lemma shows why we have used “minimal critical pairs” instead of “critical pairs” in this definition.

Lemma 7.7 Let

ζ_{1} = \frac{Δ, A − I →^{ξ_{1}} A′ I → I}{Δ, A − I, A′ − I → I} ζ_{2} = \frac{Δ, A′ − I →^{ξ_{2}} A I → I}{Δ, A − I, A′ − I → I}

be a critical pair. If a_{1}, ..., a_{n} are elements of Δ, which are single atoms, and α is the substitution [I/a_{1}, ..., I/a_{n}], then the pair (α ∗ ζ_{1}, α ∗ ζ_{2}) is minimal and critical.

Proof by induction on n.

Base. (n=1)

Let a be the member of Δ being single variable.

Because the sequent

Δ, A − I, A′ − I → I

is balanced, there is another occurrence of a with opposite variance, lying in some other member D(a) of

Δ, A − I, A′ − I → I.

The a should be negative in D(a), and D(a) can have one of the forms a − I, a − b, a − b ⊗ c, a ⊗ b − c, b ⊗ a − c, (b − a) − c or (b − a) − I.

The variants D(a) = a − I, a − b, a − b ⊗ c are excluded. Using lemma 6.7, one easily shows that, with such D(a), the ξ_{1} or ξ_{2} will be equivalent to a derivation ending by −↪ with a → a as the left premise. That contradicts the condition that ζ_{1}, ζ_{2} is critical pair.

Consider ζ̃_{1} = [I/a] ∗ ζ_{1}, ζ̃_{2} = [I/a] ∗ ζ_{2}.

When D(a) is one of the formulas A − I or A′ − I, [I/a]D(a) = (b − I) − I or (b′ − I) − I. So, it is not to be changed to an isomprphic one.

All applications of “technical” (cut) (“purifying” the result of substitution) can be moved above the last (−↪) in both ζ_{1}, ζ_{2} by the lemma 5.10. After that (cut) can be eliminated by cut-elimination property.

Resulting derivations (let us denote them by ζ′_{1}, ζ′_{2}) end by pure 2-sequent.

Δ̃, Ã − I, Ã′ − I → I.

Here the member a of Δ disappeared and one the others or, maybe, A − I or A′ − I (former D(a)) is changed.

ζ′_{1} = \frac{Δ̃, Ã − I →^{ξ̃_{1}} Ã′ I → I}{Δ̃, Ã − I, Ã′ − I → I} ζ′_{2} = \frac{Δ̃, Ã′ − I →^{ξ̃_{2}} Ã I → I}{Δ̃, Ã − I, Ã′ − I → I}.

Assume this pair is not critical.

There is no members in the antecedent of the form C ⊗ C′, and the succedent is I. So, the last rule in any derivation cannot be (⊗ →), (→ −) or (→ ⊗). Suppose there exists a derivation of

Δ̃, Ã − I, Ã′ − I → I

which ends by (wkn).

The premises of this (wkn) are some sequents Σ_{1} → I and Σ_{2} → I. Both Σ_{1}, Σ_{2} are balanced and one (which does not contain D̃) consists only of the formulas which are also members of Δ, A − I, A′ − I. Hence there exist a derivation of the sequent

Δ, A − I, A′ − I → I

which ends by wkn with the same premise (lemma 5.17). Contradiction, because the pair ζ_{1}, ζ_{2} is critical.

Let us consider the subderivations [I/a] ∗ ξ_{1}, [I/a] ∗ ξ_{2} of the left premises of ζ′_{1}, ζ′_{2}. Assume that one of them is equivalent to a derivation, ending by −↪. Suppose its left premise is Σ → C̃. There are three possibilities: D̃ is in Σ, D̃ is the main formula (and C̃ its subformula), or D̃ lies in the right premise.

In the first case we add a to Σ and replace D̃ by D(a) The resulting sequent will be derivable because D̃, a → D(a) is derivable.

In the second case we add a to Σ and replace C̃ by C (corresponding subformula of D(a)), i.e., we replace I by a or b by b ⊗ a or by a ⊗ b. The resulting sequent can be derived by adding an application of (→ ⊗) or (wkn).

In the third case we do not change the sequent.

In all cases using lemma 6.7 we easily show, that these derivations are equivalent to the corresponding subderivation of ζ_{i}.

This contradicts the condition that the pair ζ_{1}, ζ_{2} is critical.

Inductive step in this lemma is trivial. □.

Lemma 7.8 Let (ψ, φ) be cut-free derivations of a balanced pure 2-sequent. Assume that they have the same last rule. If (ψ, φ) is not in W′, then the subderivations (ψ′, φ′) of each premise of this rule in (ψ, φ) also do not belong to W′.

Proof. Assume that, to the contrary, subderivations of one of the premises belong to W′, i.e., there is a substitution α such that (α ∗ ψ′, α ∗ φ′) ∈ W′.

In case of the rule with one premise, apply the same substitution to (ψ, φ). (Take into account that the side formulas of ⊗ →, → − cannot contain connectives, because we consider pure 2sequents.)

In case of the rules with two premises, take into account that the premises have no variables in common, and α can be extended by substitution of I for all atoms of the other premise.

This, together with the definition of minimal critical pair, makes side formulas constant, as above.

Thus, a minimal critical pair can be obtained also from (ψ, φ) . Contradiction. □

Remark 7.9 Now one can easily derive, that original Voreadou’s class W is a subclass of (possibly, coinciding with) our class W′.

The following lemma is obvious.

Lemma 7.10 If the pair (ψ, φ) of cut-free derivations of a pure-2-sequent does not belong to W′, then for every substitution α of I for some variables the pair (α ∗ ψ, α ∗ φ) also does not belong to W′.

Theorem 3 (Abstract coherence theorem.) If the pair (ψ, φ) of cut-free derivations of a balanced pure 2-sequent S does not belong to the class W′, then ψ ≡ φ.

Proof by induction on the length of the sequent.

By lemma 5.6 one can assume, that the derivations are atomic.

Base. Shortest possible derivable balanced pure 2-sequents are axioms a → a, → I. They do not belong to W′, and have unique cut-free derivations.

Inductive Step. Assume (ψ, φ) not in W. Consider the last rules in ψ and φ.

Because the derivations are atomic, the case when one of derivations is an axiom is already considered as base case.

If at least in one of them (say, φ) the last rule is different from −↪, then the other derivation (i.e., ψ) is equivalent to a derivation ψ′, ending with the same rule and with the same premises as φ (lemma 5.15 for ⊗ →, 5.16 for → −, 5.17 for wkn and 5.22 for → ⊗).

By lemma 7.8 the inductive hypothesis can be applied to the derivations of the premise or premises of this rule in φ and ψ′.

They should be equivalent, and this implies ψ ≡ φ.

If in both ψ, φ the last rule is −↪ and its premises are the same, then again inductive hypothesis can be applied.

Let us consider the case when in both ψ, φ the last rule is −↪, but its premises are different.

ψ = \frac{Γ_{1}, [A′ − B′] → A B, Γ_{2}, [A′ − B′] → C}{Γ, A − B, A′ − B′ → C},

φ = \frac{Γ′_{1}, [A − B] → A′ B′, Γ′_{2}, [A − B] → C}{Γ, A − B, A′ − B′ → C}.

(The formulas in square brackets are actually present only in ONE of the premises.)

We can assume that the subderivations of left premises are not equivalent to derivations ending by −↪ (lemma 5.24).

Let

Γ_{11} = Γ_{1} ∩ Γ′_{1}, Γ_{12} = Γ_{1} ∩ Γ′_{2}, Γ_{21} = Γ_{2} ∩ Γ′_{1}, Γ_{22} = Γ_{2} ∩ Γ′_{2}.

(Subcase)A − B and A′ − B′ belong to the left premises.

ψ = \frac{Γ_{11}, Γ_{12}, A′ − B′ →^{ψ_{1}} A B, Γ_{21}, Γ_{22} →^{ψ_{2}} C}{Γ_{11}, ..., Γ_{22}, A − B, A′ − B′ → C},

φ = \frac{Γ_{11}, Γ_{21}, A − B →^{φ_{1}} A′ B′, Γ_{12}, Γ_{22} →^{φ_{2}} C}{Γ_{11}, ..., Γ_{22}, A − B, A′ − B′ → C}.

Taking into account that the different premises have no variables in common, we see, that B, Γ_{21}; C, Γ_{22}; B′, Γ_{12}; A, A′, Γ_{11} have no common variables.

As a consequence, the sequents B, Γ_{21} → I; B′, Γ_{12} → I; Γ_{22} → C; Γ_{11}, A − I, A′ − I → I are balanced.

The sequent Γ_{11}, Γ_{12}, Γ_{21}, A − B, A′ − B′ → I is also balanced, and, if Γ_{22} → C ≠ → I then, by lemma 5.17 both φ and ψ are equivalent to some derivations ψ′, φ′, ending by the same wkn.

This case has been already considered. Assume that Γ_{22} → C =→ I. Thus, S = Γ_{11}, Γ_{12}, Γ_{21}, A − B, A′ − B′ → I.

ψ = \frac{Γ_{11}, Γ_{12}, A′ − B′ →^{ψ_{1}} A B, Γ_{21} →^{ψ_{2}} I}{Γ_{11}, Γ_{12}, Γ_{21}, A − B, A′ − B′ →}I,

φ = \frac{Γ_{11}, Γ_{21}, A − B →^{φ_{1}} A′ B′, Γ_{12} →^{φ_{2}} I}{Γ_{11}, Γ_{12}, Γ_{21}, A − B, A′ − B′ → I}.

Let at least one of the sequents B, Γ_{21} → I; B′, Γ_{12} → I be different from I → I. (For example, let it be B, Γ_{21} → I.)

Because S is pure, we can assume that Γ_{21} is non-constant; B also can be considered as non-constant, because otherwise by lemma 5.17 we would have an already considered case.

Let α substitute I for all variables occurring in B, Γ_{21}. The final sequent of α ∗ ψ, α ∗ φ is Γ_{11}, Γ_{12}, A − I, A′ − B′ → I, and it has smaller length than

S.

By lemma 7.10, the pair (α ∗ ψ, α ∗ φ) cannot belong to W′. Hence, by inductive hypothesis, α ∗ ψ ≡ α ∗ φ.

α ∗ ψ = \frac{Γ_{11}, Γ_{12}, A′ − B′ →^{ψ_{1}} A I→I}{Γ_{11}, Γ_{12}, A − I, A′ − B′ → I},

α ∗ φ = \frac{Γ_{11}, A − I →^{α∗φ_{1}} A′ B′, Γ_{12} →^{φ_{2}} I}{Γ_{11}, Γ_{12}, A − I, A′ − B′ → I}.

Let ψ′_{2} denote the derivation

\frac{\frac{A → A B, Γ_{21} →^{ψ_{2}} I}{A, A − B, Γ_{21} → I}}{A − B, Γ_{21} → A − I}.

Lemma 7.11

ψ ≡ \frac{Γ_{21}, A − B →^{ψ′_{2}} A − I \frac{Γ_{11}, Γ_{12}, A′ − B′ →^{ψ_{1}} A I→I}{Γ_{11}, Γ_{12}, A − I, A′ − B′ → I}}{Γ_{11}, Γ_{12}, Γ_{21}, A − B, A′ − B′ → I}(cut).

Proof. (Direct calculation.)

Apply now cut with ψ′_{2} to α ∗ ψ and α ∗ φ. Because α ∗ ψ ≡ α ∗ φ, the resulting derivations are equivalent and by lemma 5.10

ψ ≡ \frac{\frac{Γ_{21}, A − B →^{ψ′_{2}} A − I Γ_{11}, A − I →^{α∗φ_{1}} A′}{Γ_{11}, Γ_{21}, A − B → A′} B′, Γ_{12} →^{φ_{2}} I}{Γ_{11}, Γ_{12}, Γ_{21}, A − B, A′ − B′ → I}.

Thus, if at least one of B, B′ is different from I, and one of Γ_{12}, Γ_{21} is non-empty, the situation is reduced to the case of the last −↪ having the same premises in ψ and φ.

If B = B′ = I, and Γ_{12}, Γ_{21} are empty, then ψ, φ cannot be a critical pair (because by lemma 7.7 a minimal critical pair could be obtained by substitution of I).

If they do not form a critical pair, then one of conditions 2), 3) of definition 7.1 is violated. If it is 2), i.e., ψ or φ ends by an application of a rule different from −↪, then we have an

already considered case.

If it is 3), we have contradiction with the assumption that the derivations of the left premises do not end by −↪.

(Subcase)Both A − B and A′ − B′ belong to the right premises.

ψ = \frac{Γ_{11}, Γ_{12} →^{ψ_{1}} A B, A′ − B′, Γ_{21}, Γ_{22} →^{ψ_{2}} C}{Γ_{11}, ..., Γ_{22}, A − B, A′ − B′ → C},

φ = \frac{Γ_{11}, Γ_{21} →^{φ_{1}} A′ B′, , A − B, Γ_{12}, Γ_{22} →^{φ_{2}} C}{Γ_{11}, ..., Γ_{22}, A − B, A′ − B′ → C}.

By the same reasons as above, Γ_{11}; Γ_{12}, A; Γ_{21}, A′ and B, B′, Γ_{22}, C have no common variables. If Γ_{11} is non-empty, it is balanced, and ψ, φ will be equivalent to some derivations ending by

the same wkn (see above).

If it is empty, let α be the substitution of I for all variables of Γ_{12}, A.

α ∗ ψ ≡ B, Γ_{21}, A′ − B′, Γ_{22} →^{ψ_{2}} C.

α ∗ φ ≡ \frac{Γ_{21} →^{φ_{1}} A′ B′, B, Γ_{22} →^{α∗φ_{2}} C}{B, Γ_{21}, A′ − B′, Γ_{22} → C}

.

Because the pair ψ, φ does not belong to W′, the pair α ∗ ψ, α ∗ φ also doesn’t. By inductive hypothesis, ψ_{2} is equivalent to α ∗ φ.

Now, replacing ψ_{2} by its presentation, and moving down −↪ with φ_{1} in the left premise (this preserves equivalence, lemma 5.23) we have reduced the situation to the case already considered.

(Subcase) One of the formulas (say, A − B ) is going to the left, and one to the right premise.

ψ = \frac{Γ_{11}, Γ_{12} →^{ψ_{1}} A B, A′ − B′, Γ_{21}, Γ_{22} →^{ψ_{2}} C}{Γ_{11}, ..., Γ_{22}, A − B, A′ − B′ → C},

φ = \frac{Γ_{11}, Γ_{21}, A − B →^{φ_{1}} A′ B′, Γ_{12}, Γ_{22} →^{φ_{2}} C}{Γ_{11}, ..., Γ_{22}, A − B, A′ − B′ → C}.

In this case Γ_{12} should be empty (else wkn).

Let α be substitution of I for all variables of Γ_{11} → A. As above, we derive

ψ_{2} ≡ \frac{Γ_{21}, B →^{α∗φ_{1}} A′ B′, Γ_{22} →^{φ_{2}} C}{Γ_{21}, B, A′ − B′, Γ_{22} → C}.

Replacing ψ_{2} in ψ by its presentation, moving −↪ from this premise down and then to the left premise (this preserves equivalence lemma 5.23), we reduce the problem to an already considered case. □

8 Main Lemma

Definition 8.1 Let us call a derivation φ of a balanced pure 2-sequent S saturated if:

(i) S = σ, Δ → A, where σ is non-empty set of (different) atoms, and Δ is (possibly empty) set of formulas of the form C − D;

(ii) there is no derivation φ′ ≡ φ of S with (non-trivial) wkn as its last rule;

(iii) in every derivation φ′ ≡ φ of S, ending by an application of (→ ⊗), both premises of this application satisfy (i);

(iv) in every derivation φ′ ≡ φ of S, ending by an application of (−↪), left premise of this application satisfies (i).

Since the sequents under consideration are balanced pure 2-sequents, A can have one of five forms: I, a, a ⊗ b, a − I, a − b.

Antecedent members have the forms

a, a ⊗ b, a − I, a − b, a − (b ⊗ c), (a ⊗ b) − I, (a ⊗ b) − c,
(a − I) − I, (a − b) − I, (a − I) − c, (a − b) − c.

(This will be very important for case analysis below.)

In the following section, where we shall prove the main lemma, formulated below, it will be very important to analyse the structure of applications of (−↪) .

We shall distinguish three main cases: the main formula of (−↪) is of the form C − I, of the form C − d or of the form c − D where D is neither I nor an atom. Here d, c are atoms, C can have the forms a, a ⊗ b, a − I, a − b (I is impossible because we consider balanced pure 2-sequents). D can only be d_{1} ⊗ d_{2} with d_{1}, d_{2} atoms.

Not all combinations of C and D are actually possible. When D = d_{1} ⊗ d_{2}, it should be C = c. When D = I, d all four variants of C are actually possible.

The following lemma explains to some extent why we are so interested in saturated sequents.

Lemma 8.2 Let (η_{1}, η_{2}) ∈ W′_{0}

η_{1} ≡ \frac{\frac{c, Δ, (a − b) − I →^{ξ_{1}} d}{Δ, (a − b) − I → (c − d)} (→ −) \overline{I → I}}{Δ, (a − b) − I, (c − d) − I → I} (−↪)

η_{2} ≡ \frac{\frac{a, Δ, (c − d) − I →^{ξ_{2}} b}{Δ, (c − d) − I → (a − b)} (→ −) \overline{I → I}}{Δ, (a − b) − I, (c − d) − I → I} (−↪).

Then the derivations ξ_{1}, ξ_{2} are saturated.

Proof. By definition 7.1, Δ consists of the formulas of the form C − D.

In the sequents c, Δ, (a − b) − I → d and a, Δ, (c − d) − I → b one antecedent member is an atom. Thus, the condition (i) of the definition of saturated derivations is satisfied.

If one of the sequents c, Δ, (a − b) − I → d and a, Δ, (c − d) − I → b would have a derivation, ending by non-trivial wkn, then its antecedent will contain some balanced proper subset of formulas(corollary 5.18).

If this subset does not contain c (resp., a), then the same members will form a balanced subset of the antecedent of the sequent c, Δ, (a − b) − I → d (resp., a, Δ, (c − d) − I → b), and it will contradict to the definition of W′_{0}.

If it does contain a (c), then another premise of this wkn has the form Δ′ → d (resp., Δ′ → b) with Δ′ consisting only of implicative formulas, and by lemma 5.25 the subderivation of this premise will be equivalent to a derivation ending by −↪.

Moreover, the antecedent of the left premise of this −↪ will contain only implicative formulas. Because our sequents are balanced pure 2-sequents, lemma 6.6 can be applied (this −↪ can be moved down), and we obtain contradiction with definition of minimal critical pairs.

Hence, (ii) is satisfied.

By the same lemma, if ξ_{1} or ξ_{2} is equivalent to a derivation, ending by (−↪), then the left premise of this (−↪) must contain a (c). Hence, (iv) is satisfied.

There is no derivation of these sequents ending by (→ ⊗) because their succedent is an atom or I. Hence (iii) is satisfied.

□

Lemma 8.3 (”Main Lemma”) Let φ be saturated derivation of a balanced pure 2-sequent

S = σ, Δ → A.

Then φ is equivalent to a derivation, ending by an inference of one of the following forms, where the subderivations of all sequents on the top also are saturated:

Forms of inference:

1.Case A = I.

1.1 \frac{σ_{1}, Δ_{1} → C σ_{2}, d, Δ_{2} → I}{\underbrace{σ_{1}, σ_{2}}_{σ}, \underbrace{C − d, Δ_{1}, Δ_{2}}_{Δ} → I}(−↪), 1.2 \frac{σ, Δ_{1} → C I → I}{σ, \underbrace{C − I, Δ_{1}}_{Δ} → I}.(−↪)

1.3 \frac{\overline{σ_{1}, Δ_{1} → c} \frac{σ_{2}, d_{1}, d_{2}, Δ_{2} → I}{σ_{2}, d_{1} ⊗ d_{2}, Δ_{2} → I}(⊗ →)}{\underbrace{σ_{1}, σ_{2}}_{σ}, \underbrace{c − d_{1} ⊗ d_{2}, Δ_{1}, Δ_{2}}_{Δ} → I} (−↪),

1.4 \frac{\overline{σ_{1}, Δ_{1} → c} \frac{\frac{σ_{21}, d_{1}, Δ_{21} → I σ_{22}, d_{2}, Δ_{22} → I}{σ_{2}, d_{1}, d_{2}, Δ_{2} → I}(wkn)}{σ_{2}, d_{1} ⊗ d_{2}, Δ_{2} → I}(⊗ →)}{\underbrace{σ_{1}, σ_{2}}_{σ}, \underbrace{c − d_{1} ⊗ d_{2}, Δ_{1}, Δ_{2}}_{Δ} → I} (−↪),

(1.4’) same as (1.4) with d_{1} going to the right, and d_{2} to the left premise of (wkn).

2. Case A = a.

2.1 \frac{σ_{1}, Δ_{1} → C σ_{2}, d, Δ_{2} → a}{\underbrace{σ_{1}, σ_{2}}_{σ}, \underbrace{C − d, Δ_{1}, Δ_{2}}_{Δ} → a} (−↪),

2.2 \frac{\overline{σ_{1}, Δ_{1} → c} \frac{σ_{2}, d_{1}, d_{2}, Δ_{2} → a}{σ_{2}, d_{1} ⊗ d_{2}, Δ_{2} → a}(⊗ →)}{\underbrace{σ_{1}, σ_{2}}_{σ}, \underbrace{c − d_{1} ⊗ d_{2}, Δ_{1}, Δ_{2}}_{Δ} → a} (−↪)

2.3 \frac{\overline{σ_{1}, Δ_{1} → c} \frac{\frac{σ_{21}, d_{1}, Δ_{21} → I σ_{22}, d_{2}, Δ_{22} → a}{σ_{2}, d_{1}, d_{2}, Δ_{2} → a}(wkn)}{σ_{2}, d_{1} ⊗ d_{2}, Δ_{2} → a}(⊗ →)}{\underbrace{σ_{1}, σ_{2}}_{σ}, \underbrace{c − d_{1} ⊗ d_{2}, Δ_{1}, Δ_{2}}_{Δ} → a} (−↪),

(2.3’) same as (2.3) with d_{1} going to the right, and d_{2} to the left premise of (wkn).

3. Case A = a ⊗ b.

3.1 \frac{σ_{1}, Δ_{1} → C σ_{2}, d, Δ_{2} → a ⊗ b}{\underbrace{σ_{1}, σ_{2}}_{σ}, \underbrace{C − d, Δ_{1}, Δ_{2}}_{Δ} → a ⊗ b} (−↪),

3.2 \frac{\overline{σ_{1}, Δ_{1} → c} \frac{σ_{2}, d_{1}, d_{2}, Δ_{2} → a ⊗ b}{σ_{2}, d_{1} ⊗ d_{2}, Δ_{2} → a ⊗ b}(⊗ →)}{\underbrace{σ_{1}, σ_{2}}_{σ}, \underbrace{c − d_{1} ⊗ d_{2}, Δ_{1}, Δ_{2}}_{Δ} → a ⊗ b} (−↪)

3.3 \frac{\overline{σ_{1}, Δ_{1} → c} \frac{\frac{σ_{21}, d_{1}, Δ_{21} → I σ_{22}, d_{2}, Δ_{22} → a ⊗ b}{σ_{2}, d_{1}, d_{2}, Δ_{2} → a ⊗ b}(wkn)}{σ_{2}, d_{1} ⊗ d_{2}, Δ_{2} → a ⊗ b}(⊗ →)}{\underbrace{σ_{1}, σ_{2}}_{σ}, \underbrace{c − d_{1} ⊗ d_{2}, Δ_{1}, Δ_{2}}_{Δ} → a ⊗ b} (−↪),

(3.3’) same as (3.3) with d_{1} going to the right, and d_{2} to the left premise of (wkn),

3.4 \frac{a → a b → b}{a, b → a ⊗ b}(→ ⊗)

4. Case A = a − I.

4.1 \frac{a, σ, Δ → I}{σ, Δ → (a − I)} (→ −)

5. Case A = a − b.

5.1 \frac{a, σ, Δ → b}{σ, Δ → (a − b)} (→ −)

5.2\frac{\frac{a, σ_{1}, Δ_{1} → I σ_{2}, Δ_{2} → b}{a, σ, Δ → b}(wkn)}{σ, Δ → (a − b)} (→ −)

9 Proof of Main Lemma.

In the proof we are going to show that every derivation reduces to an equivalent derivation of one of the forms, considered above. The proof consists in case analysis, depending on the structure of A and of the main formula of the last rule in ψ.

When A ≠ a − I, a − b, by lemma 5.25 every derivation of S is equivalent to a derivation, ending by (−↪). Consider first this case.

Case: right side A = I, a, a ⊗ b.

Lemma 9.1 (Left premises of (−↪) ) Let ψ be saturated derivation of the sequent S = σ, Δ → A. Assume that ψ ends by the rule (−↪). Then the subderivation of the left premise of this rule is saturated.

Proof. The left premise is S_{1} = σ_{1}, Δ_{1} → C, where σ_{1} is part of σ and Δ_{1} is part of Δ; σ_{1} is non-empty by condition (iv) of the definition 8.1.

S_{1} is balanced pure 2-sequent. Thus, the condition (i) of the definition 8.1 is satisfied for the subderivation of S_{1}. Suppose that the subderivation of S_{1} is equivalent to a derivation which ends by wkn. Then its left premise is σ_{11}, Δ_{11} → I. It is balanced, hence σ_{11}, Δ_{11} is balanced. σ_{11}, Δ_{11} is balanced part of the antecedent of S as well, so, by lemma 5.17, ψ is equivalent to

a derivation which ends by wkn. This contradicts (ii) for S Hence, S_{1} satisfies (ii). Suppose that the subderivation of S_{1} is equivalent to a derivation which ends by (→ ⊗), and

one of its premises (for example, the left one) does not contain elements of σ_{1}. This premise has the form

S_{11} = Δ_{11} → c

for some atom c.

Δ_{11} contains only formulas of the form C′ − C′′ and is non-empty. (Else the sequent will be underivable.)

By lemma 5.25, its subderivation is equivalent to some derivation, ending by (−↪). Left premise of this (−↪) does not contain members which are atoms (all its antecedent

members are members of Δ_{11}).

Hence, this (−↪) can be moved down (lemma 6.6, and we obtain a derivation, which is equivalent to ψ and ends by (−↪) with the same left premise, which is not possible, as ψ is saturated. Contradiction.

Thus, (iii) is satisfied.

If the subderivation of S_{1} is equivalent to a derivation which ends by (−↪), and its left premise does not contain members of σ_{1}, then again, by lemma 5.25, ψ will be equivalent to a derivation ending by (−↪) with forbidden left premise.

Hence, (iv) is satisfied. □

To analyse the structure of derivations of right premises, we shall consider subcases depending on the form of main formula of (−↪).

Subcase: main formula is C − d or C − I.

Lemma 9.2 (Right premises of 1.1-1.3.) Let ψ be saturated derivation of the sequent S = σ, Δ → A. Assume that ψ ends by the rule (−↪), and in its main formula is C − d . Then the subderivation of the right premise of this (−↪) is saturated.

Proof. The right premise is balanced pure 2-sequent and has the form d, σ_{2}, Δ_{2} → A.

The condition (i) is satisfied because the variable d is present.

Suppose that the subderivation of S_{2} is equivalent to a derivation which ends by wkn.

Then its left premise is

S_{21} = σ_{21}, Δ_{21} → I

(σ_{21} does not contain d), or

S_{21} = d, σ_{21}, Δ_{21} → I

In the first case, by lemma 5.17 applied to

σ_{21}, Δ_{21}

and

σ_{1}, Δ_{1}, C − d, σ_{22}, Δ_{22}

(both are balanced and

σ, Δ = σ_{21}, Δ_{21}, σ_{1}, Δ_{1}, C − d, σ_{22}, Δ_{22}),

the condition (ii) cannot be satisfied for S.

In the second case, by lemma 5.17, applied to σ_{1}, Δ_{1}, C − d, σ_{21}, Δ_{21} and σ_{22}, Δ_{22}, once more condition (ii) for S is violated.

Hence (ii) is satisfied for S_{2}.

We have to check (iii) only in case when A = a ⊗ b.

If the subderivation of

S_{2} = d, σ_{2}, Δ_{2} → a ⊗ b

is equivalent to a derivation which ends by (→ ⊗), and one of its premises does not contains members of d, σ_{2}, then, applying lemma 5.22 we obtain contradiction with (iii) for S.

Suppose that the subderivation of S_{2} = d, σ_{2}, Δ_{2} → A does not satisfy (iv).

It means, that it is equivalent to a derivation which ends by (−↪), whose left premise does not contain members of σ_{2}, d.

We apply lemma 5.25 and obtain a contradiction. □

Lemma 9.3 (Right premise of 1.2) Let ψ be saturated derivation of the sequent S = σ, Δ → I. Suppose it ends by the rule (−↪), and in its main formula is C − I . Then the right premise of this (−↪) is I → I.

Proof. In general the left premise of (−↪) is σ_{1}, Δ_{1} → C and the right premise is I, σ_{2}, Δ_{2} → I.

Both σ_{1}, Δ_{1}, C − I and σ_{2}, Δ_{2} are balanced,

σ, Δ = σ_{1}, Δ_{1}, C − I, σ_{2}, Δ_{2},

and applying lemma 5.17 we derive that there exists a derivation (equivalent to ψ), ending by (wkn).

If σ_{2}, Δ_{2} is non-empty, then we have contradiction with (ii) of the definition of saturated derivation (for ψ). □

Subcase: main formula of (−↪) is c − d_{1} ⊗ d_{2} The right premise has the form

S_{2} = d_{1} ⊗ d_{2}, σ_{2}, Δ_{2} → A.

By lemma 5.15, every derivation of S_{2} is equivalent to some derivation which has (⊗ →) as its last rule.

The subderivation of its premise is saturated sequent or not. If it is, then we have inference of the form 1.3, 2.2 or 3.2. If it is not, then ψ is equivalent to some derivation which ends by an inference of the form

\frac{\overline{σ_{1}, Δ_{1} → c} \frac{σ_{2}, d_{1}, d_{2}, Δ_{2} → A}{σ_{2}, d_{1} ⊗ d_{2}, Δ_{2} → A}(⊗ →)}{\underbrace{σ_{1}, σ_{2}}_{σ}, \underbrace{C_{1} − C_{2}, Δ_{1}, Δ_{2}}_{Δ} → A} (−↪),

where A = I, a, a ⊗ b and the subderivation ψ′ of the sequent

S′_{2} = σ_{2}, d_{1}, d_{2}, Δ_{2} → A

is NOT saturated.

Obviously, S′_{2} satisfies (i) of the definition of saturated sequent. ψ′ should satisfy (iii) and (iv) of this definition, because (using, respectively, lemma 6.6 and

lemma 5.22 ) we can show that, if these conditions for ψ′ are not satisfied, they are not satisfied also for ψ.

Hence, only the condition (ii) can be violated. I.e., ψ′ is equivalent to some derivation ending by non-trivial (wkn). If we can show that d_{1}, d_{2} always belong to different premises of this wkn, and the subderiva-

tions of both its premises are saturated (it covers forms of inference 1.4, 2.3, 2.3’, 3.3, 3.3’), then the proof in cases A = I, a, a ⊗ b will be completed.

Lemma 9.4 Let the subderivation φ of S′_{2} above satisfy (i), (iii), (iv) of the definition 8.1. Assume that it ends with (wkn). Then d_{1} and d_{2} lie in different premises of this (wkn).

Proof. If d_{1} and d_{2} lie in one premise, then there are two possibilities.

a) Left premise is

d_{1}, d_{2}, σ_{21}, Δ_{21} → I

and right premise is

σ_{22}, Δ_{22} → A.

b) Left premise is

σ_{21}, Δ_{21} → I

and right premise is

d_{1}, d_{2}, σ_{22}, Δ_{22} → A.

In case a)

σ_{1}, Δ_{1}, c − d_{1} ⊗ d_{2}, σ_{21}, Δ_{21}

is balanced subset of σ, Δ, and by lemma 5.17 we obtain a contradiction with (ii) for ψ.

In case b)

σ_{21}, Δ_{21}

is balanced, and again lemma 5.17 can be used to obtain a contradiction with (ii) for psi. Hence, d_{1} and d_{2} are lying in different premises. □

Lemma 9.5 Let the subderivation φ of S′_{2} above satisfy (i), (iii), (iv) of the definition 8.1. Assume that it ends with (wkn). Then the derivations of both premises of this (wkn) saturated.

Proof. In the case under consideration φ ends by an inference of the form

\frac{d_{1}, σ_{21}, Δ_{21} → I d_{2}, σ_{22}, Δ_{22} → A}{d_{1}, d_{2}, σ_{2}, Δ_{2}, → A}(wkn).

(Or the same with permutation of d_{1} and d_{2}.)

The premises of (wkn) in this inference satisfy the condition (i) of the definition of saturated sequent because each contains one of d_{1} and d_{2}.

Consider the subderivation φ_{1} of the left premise (let it contain d_{1}):

S_{21} = d_{1}, σ_{21}, Δ_{21} → I.

Assume that it is equivalent to a derivation ending by non-trivial wkn. At least one of its premises will not contain d_{1}. But then the antecedent of this premise will be balanced subset of the antecedent of S and by

lemma 5.17 we shall obtain a contradiction with (ii) for the derivation ψ.

Hence, φ_{1} satisfies (ii). φ_{1} satisfies (iii), because the succedent of S_{21} is I, and hence, (→ ⊗) is not possible. If φ_{1} is equivalent to a derivation, ending by (−↪), and its left premise contains only im-

plicative formulas, then, using lemma 5.25, we obtain (as above) a contradiction with (iv) for S.

Hence, (iv) is also satisfied, and φ_{1} is saturated. Consider the subderivation φ_{2} of the right premise

S_{22} = d_{2}, σ_{22}, Δ_{22} → A.

Suppose it is equivalent to a derivation ending by (wkn). Then the union of the antecedent of its left premise with d_{1}, σ_{21}, Δ_{21} is a balanced subset of

σ, Δ, and using lemma 5.17 we obtain a contradiction with (ii) for ψ.

Suppose that (iii) is not satisfied, i.e., φ_{2} is equivalent to a derivation ending by (→ ⊗), and one premise of this (→ ⊗) does not contain elements of d_{1}, σ_{22}.

Using lemma 5.22 we obtain a contradiction with (iii) for S. Suppose (iv) is not satisfied, i.e., φ_{2} is equivalent to a derivation, ending by (−↪), such that

the left premise of this (−↪) contains only implicative formulas.

Applying lemma 5.25, we obtain a contradiction with (iv) for S. Hence, (iv) is satisfied and φ_{2} also is saturated. □ Case: the right side is A = a − I or a − b. In this case by lemma 5.16 every derivation of S is equivalent to a derivation which ends by

(→ −) with A as its main formula.

Subcase A = a − I.(4.1) It is enough to show that if ψ ends by the inference

\frac{a, σ, Δ → I}{σ, Δ → (a − I)} (→ −),

then the subderivation of

S′ = a, σ, Δ → I

is saturated.

(i) is satisfied because the antecedent of S′ contains the atom a. Suppose (ii) is not satisfied, i.e., the subderivation ψ′ of S′ is equivalent to a derivation, which

ends by non-trivial wkn.

Then both its premises have I as their succedent, and at least one does not contain a. Using lemma 5.17, we obtain a contradiction with (ii) for S. The succedent of S′ is I, so, (iii) is satisfied trivially. If (iv) is not satisfied, we apply lemma 5.25 and obtain a contradiction with (iv) for S. □ Subcase A = a − b.(5.1, 5.2) We can suppose that ψ ends by the inference

\frac{a, σ, Δ → b}{σ, Δ → (a − b)} (→ −).

If the subderivation ψ′ of its premise is saturated, then we have the form of inference (5.1). If it is not, then, again, (i) and (iii) are satisfied trivially, and (iv) is satisfied by lemma 5.25. Hence, only (ii) is, possibly, not satisfied. If (ii) is not satisfied, then by corollary 5.18, every derivation of S′ is equivalent to some

derivation ending by (wkn).

We have to show only that the premises of such (wkn) satisfy the conditions on the inference (5.2).

By corollary 5.21, a belongs to its left premise. Hence we have to show only that the subderivations of both premises of this (wkn) are satu-

rated.

Without loss of generality we can suppose that ψ end by the inference

\frac{\frac{a, σ_{1}, Δ_{1} → I σ_{2}, Δ_{2} → b}{a, σ, Δ → b}(wkn)}{σ, Δ → (a − b)} (→ −).

Lemma 9.6 Let the subderivation ψ′ of the S′_{2} above satisfy (i), (iii), (iv) of definition of saturated derivation. Assume that it is ending by (wkn) . Then the subderivations of both premises of this (wkn) are saturated.

Proof follows the proof of lemma 9.5 (with some simplifications: for example, (iii) is satisfied trivially because succedents do not contain ⊗). □

This completes the proof of lemma 8.3. □

10 Definition of test-category

The main examples of non-commutative diagrams in free SMC category become commutative when they are interpreted in the SMC category of finite dimensional vector spaces. Thus, to test non-commutativity, infinite dimensional spaces are necessary. All calculations with infinite dimensional hom-spaces are extremely difficult. Following the same reductionist heuristics, as in our reduction to 2-sequents, we shall perform ”partial evaluation” of linear functions, in order to eliminate all hom-spaces. It is possible only when at least one arrow in each hom-space can be constructed in some way. We have only finite list of possible types of hom-spaces, corresponding to the members of 2-sequent. Their structure partly motivates our choice of arrows in abstract definition of ”test-category”, given below.

The rest (motivation for ”test-arrows” and constraints imposed on all data) comes from a close analysis of examples of non-commutative diagrams and the known mechanisms of their verification in the category of vector spaces.

The (obvious) presence of elements of algebra and coalgebra structure seems suggestive, but we have not general motivation, except the direct use of appropriate mechanisms in our proof.

Let V be an SMC category, containing at least two objects V and 0 ^{7} and the following arrows (satisfying the conditions described below).

1. Comultiplication, counit and “Kronecker’s delta”:

Δ : V → V ⊗ V ; ϵ : V → I; δ : V ⊗ V → V; .

Remark 10.1 One may try to complete the structure, making of δ a multiplication in an algebra, but, as we shall see, in vector spaces it will be Kronecker’s “delta”, and it will not even admit any “unit”.

2. Nul-object and arrows.

0^{X} : 0 → X, 0_{X} : X → 0 ,

for all X ∈ Ob(V).

7As SMC category, V contains also I and all objects which can be obtained from V, 0 and I by ⊗, −.

Before describing next group of arrows, we introduce the following abbreviations: 0_{X}^{Y} ⇀ ↽ 0^{Y} ∘ 0_{X} : X → Y,

δ̃ ⇀ ↽ ϵ ∘ δ : V ⊗ V → I,
δ^{+} ⇀ ↽ π(δ) : V → (V − V),
δ̃^{+} ⇀ ↽ π(δ̃) : V → (V − I),
Δ^{+} ⇀ ↽ π(Δ ∘ b′_{V}) : I → (V − V ⊗ V)
ϵ^{+} ⇀ ↽ π(ϵ ∘ b′_{V}) : I → V − I,
δ^{++} ⇀ ↽ π_{I(V ⊗V)V} (δ ∘ b′_{(V ⊗V)}) : I → (V ⊗ V − V),
δ̃^{++} ⇀ ↽ π_{I(V ⊗V)I}(δ̃ ∘ b′_{(V ⊗V)}) : I → (V ⊗ V − I),

3. Retractions. β : (V − V) → V ; β̃ : (V − I) → V. As abbreviations we introduce also:

γ ⇀ ↽ ϵ ∘ β : (V − V) → I ,

γ̃ ⇀ ↽ ϵ ∘ β̃ : (V − I) → I ,
β^{+} ⇀ ↽ π(β) : I → (V − V) − V ,
β̃^{+} ⇀ ↽ π(β̃) : I → (V − I) − V ,
γ^{+} ⇀ ↽ π(ϵ ∘ β) : I → (V − V) − I ,
γ̃^{+} ⇀ ↽ π(ϵ ∘ β̃) : I → (V − I) − I .

4. Two “test-arrows”: θ : (V − V) → I; θ̃: (V − I) → I, As above, we introduce abbreviations for the arrows obtained by adjunctions: θ^{+} : I → (V − V) − I ⇀ ↽ π(θ ∘ b′_{(V − V)}) : I → (V − V) − I, θ̃^{+} : I → (V − V) − I ⇀ ↽ π(θ̃ ∘ b′_{(V − V)}) : I → (V − I) − I. These data satisfy the following conditions:

(1) δ is one-side inverse of Δ:

δ ∘ Δ = id_{V};

(2) the following “absorption laws”:

c_{V V} ∘ Δ = Δ ,
δ ∘ c_{V V} = δ ,
b′_{V} ∘ (ϵ ⊗ id_{V}) ∘ Δ = id_{V}
b_{V} ∘ (id_{V} ⊗ ϵ) ∘ Δ = id_{V}
δ ∘ (δ ⊗ id_{V}) = δ ∘ (id_{V} ⊗ δ) ∘ a_{V V V}
(id_{V} ⊗ δ) ∘ a_{V V V} ∘ (Δ ⊗ id_{V}) = Δ ∘ δ .

Thus, Δ and δ are commutative, ϵ is counit (in respect to comultiplication Δ), δ is associative. Meanwhile, δ is not a multiplication (there is no unit), and we do not need associativity of Δ, being close, but not exactly in the scope of the notions of algebra and coalgebra structure (which yet could be helpful in understanding calculations we do below).

The “laws” above, of course, one may represent by diagrams, e.g., last three of them by

[figure: \begin{matrix}V ⊗ V & V ⊗ I \\ V & V \end{matrix}; id_{V} ⊗ϵ; b_{V}; Δ; _{id_{V}}] ,

[figure: \begin{aligned}V ⊗ (V ⊗ V) & & V ⊗ V \\ (V ⊗ V) ⊗ V & & V \\ & V ⊗ V \end{aligned}; id_{V} ⊗δ; δ; a_{V V V}; δ⊗id_{V}; δ] ,

[figure: \begin{matrix}(V ⊗ V) ⊗ V & & V ⊗ (V ⊗ V) \\ V ⊗ V & V & V ⊗ V \end{matrix}; a_{V V V}; id_{V} ⊗δ; Δ⊗id_{V}; δ; Δ]

(3) 0 is zero-object in V, i.e., for all morphisms ψ : X → 0, φ : 0 → Y,

ψ = 0_{X} : X → 0 , φ = 0^{Y} : 0 → Y;

(4) β and β̃ are one-side inverses to δ^{+}, δ̃^{+}, i.e.,

β ∘ δ^{+} = β̃ ∘ δ̃^{+} = id_{V} : V → V ,

(5) and, moreover (with z : (V − I) ⊗ V → (V − V) being standard canonical map) ,

β ∘ (z_{V V} ∘ (δ̃^{+} ⊗ id_{V})) = δ : V ⊗ V → V ,

and

β ∘ ((z_{V V} ∘ (ϵ^{+} ⊗ id_{V})) ∘ (b′_{V})^{−1}) = id_{V} : V → V.

I.e., the following diagrams are commutative:

[figure: \begin{matrix}(V − I) ⊗ V & (V − V) \\ V ⊗ V & V \end{matrix}; z_{V V}; β; δ̃⊗id_{V}; δ];

[figure: \begin{matrix}(V − I) ⊗ V & (V − V) \\ I ⊗ V \\ V & V \end{matrix}; z_{V V}; β; ϵ^{+}⊗id_{V}; (b′_{V} )^{−1}; _{id_{V}}] .

(6)The following diagrams are commutative:

[figure: \begin{aligned}& (V − V) & & & (V − I) \\ V & & I & V & & I \\ & 0 & & & 0 \end{aligned}; θ; θ̃; δ^{+}; 0_{V}; δ̃^{+}; 0_{V}; 0^{I}; 0^{I}],

[figure: \begin{matrix}(V − I) ⊗ V & & (V − V) \\ V ⊗ V & 0 & I \end{matrix}; z_{V V}; θ; δ̃^{+}⊗id_{V}; 0_{V}; 0^{I}] .

[figure: \begin{matrix}(V − I) ⊗ V & & (V − V) \\ I ⊗ V \\ V & 0 & I \end{matrix}; z_{V V}; θ; ϵ^{+}⊗id_{V}; (b′_{V} )^{−1}; 0_{V}; 0^{I}] .

In equational form,

(θ ∘ δ^{+}) = (0_{I} ∘ 0^{V}), , (θ̃ ∘ δ̃^{+}) = (0_{I} ∘ 0^{V}) ,

θ ∘ (z_{V V} ∘ (δ̃^{+} ⊗ id_{V})) = (0^{I} ∘ 0_{V ⊗V}) , θ ∘ (z_{V V} ∘ ((ϵ^{+} ⊗ id_{V}) ∘ (b′_{V})^{−1}) = (0^{I} ∘ 0_{V}).

7. The following diagrams are not commutative:

[figure: \begin{aligned}& (V − V) & & & (V − I) \\ I & & I & I & & I \\ & 0 & & & 0 \end{aligned}; θ; θ̃; _{id{+ \atop V}}; 0_{I}; ϵ^{+}; 0_{I}; 0^{I}; 0^{I}].

Remark 10.2 We shall need a lot of derived equalities, which follow from those of groups (1)

- (6) above. Some of immediate consequences we may present here. The following variants of “absorption laws” (2) are easily derived:

b ∘ (ϵ ⊗ ϵ) ∘ Δ = b′ ∘ (ϵ ⊗ ϵ) ∘ Δ = ϵ ,
δ ∘ (id_{V} ⊗ δ) = δ ∘ (id_{V} ⊗ δ) ∘ a_{V V V}^{−1} ,
(δ ⊗ id_{V}) ∘ a_{V V V}^{−1} ∘ (id_{V} ⊗ Δ) = Δ ∘ δ,
b ∘ (id_{V} ⊗ δ̃) ∘ a_{V V V} ∘ (Δ ⊗ id_{V}) = id_{V}
b′ ∘ (δ̃ ⊗ id_{V}) ∘ a_{V V V}^{−1} ∘ (id_{V} ⊗ Δ) = id_{V} .

(The first using naturality of b′, b, the second by composition of its analogue above with a^{−1} etc.)

¿From the equalities of groups (4), (5) follow:

γ ∘ δ^{+} = γ̃ ∘ δ̃^{+} = ϵ : V → I ,
γ ∘ (z_{V V} ∘ (δ̃^{+} ⊗ id_{V})) = δ̃: V ⊗ V → V ,
γ ∘ ((z_{V V} ∘ (ϵ^{+} ⊗ id_{V})) ∘ (b′_{V})^{−1}) = ϵ : V → I.

(Since γ = ϵ ∘ β.)

11 Vector spaces as a test-category.

Let K be the SMC category of vector spaces over a field I.

Let us take the space {0} as 0, and V = ⊕_{n∈N}I.

Let 1 ∈ I be the unit element of the field I. We shall suppose that in V the basis {v_{i}}_{i=1}^{i=∞} is fixed, where v_{j} = {0, ..., 1, 0, ...} (with 1 at j-th place).

Tensor product of two vector spaces with fixed bases can be described as the vector space freely generated by tensor products of their basic vectors.

In particular, V ⊗ V has as a basis the set

{v_{i} ⊗ v_{j}}_{i,j=1}^{i,j=∞}

A linear function on a vector space is completely determined by its values on basis vectors. So, we define:

• for all i, Δ(v_{i}) = v_{i} ⊗ v_{i};

• δ(v_{i} ⊗ v_{j}) = 0, if i ≠ j and v_{i} if i = j;

• ϵ(v_{i}) = 1 for all i;

• with this definition we have δ̃(v_{i} ⊗ v_{j}) = 0, if i ≠ j and 1 if i = j.

We easily check, that equalities (1), ((2) of section 10) hold.

One may note, that no “unit” ι : I → V for the “multiplication” δ is possible, since from

V ≅ I ⊗ V ⟶^{ι⊗id_{V}} V ⊗ V ⟶^{δ} V

will follow that ι(1) is 1 ∈ I in each component of V = ⊕_{n∈N}I.

The space V − I consists of linear functionals on V. Each functional f is determined by its values on basis vectors, so, to it corresponds an infinite sequence of scalars {f_{i}} where f_{i} = f(v_{i}). This sequence does not necessarily have finite support.

Vice versa, to each sequence {f_{i}} of scalars corresponds a functional f from V − I, defined by condition f(x) = ∑ f_{i}x_{i} where x = {x_{i}}_{i=1}^{i=∞}.

This definition is correct because x is a sequence with finite support.

Meanwhile, there is an important subspace consisting of all functionals represented by sequences with finite support, and we shall suppose that its basis consists of the same elements (sequences with 1 at i-th place, and 0 elsewhere) as in V. For clarity, we shall denote them by ṽ_{i}. Let us denote corresponding subspace by (V − I)_{fin}.

• Obviously, δ̃^{+}(v_{i}) = ṽ_{i}.

An important example of an element of V − I, which does not belong to this subspace, is the sequence with all elements equal to 1.

Note, that

• ϵ^{+}(1) = {1, ..., 1, ..., 1, ...}.

Let us consider (V − V). Its elements (linear endomorphisms of V) are determined by their values on basis vectors.

This value is always a sequence of scalars with finite support (an element of V).

Each linear endomorphism g can be represented by a matrix {g_{ij}}_{i,j=1}^{i,j=∞} whose i-th (say) column is the value of g on i-th basic vector. It is a sequence with finite support, hence, each column of the matrix has finite number of non-zero elements.

¿From the other side, to each matrix {g_{ij}}_{i,j=1}^{i,j=∞} with this property corresponds a linear function, whose application to the vector x = {x_{i}}_{i=1}^{i=∞} (written horizontally) is defined by right matrix multiplication, i.e., y = g(x) is defined by

y_{j} = ∑_{i=1}^{∞} x_{i}g_{ij}.

There is no good description of a basis in the whole (V − V). But there are several important subspaces.

One subspace is that of diagonal matrices with finite support.

We shall fix its basis consisting of the matrices with one unit element g_{ii} = 1 and other elements equal to 0. We shall denote these basis matrixes by v_{ii} and subspace by (V − V)_{d−fin}. It is isomorphic to V.

• δ^{+}(v_{i}) = v_{ii}.

Another important subspace consists of all matrixes with finite support. We shall fix its basis consisting of all matrixes with one unit element g_{ij} = 1 and other elements equal to 0. We shall denote these matrixes by v_{ij} and corresponding subspace by (V − V)_{fin}.

Third subspace we shall consider consists of all matrixes with finite number of non-zero rows. We shall denote this subspace by (V − V)_{r−fin}.

(V − V)_{d−fin} ⊂ (V − V)_{fin} ⊂ (V − V)_{r−fin}.

Note that infinite diagonal matrix

E = {g_{ij}}_{i,j=1}^{i,j=∞}, g_{ii} = 1, g_{ij} = 0, i ≠ j

does not belong to these subspaces.

Let r_{i} be the matrix whose i − th row consists of 1, and other elements are 0.

For every f ∈ V − I, z_{V V} (f ⊗ v_{j}) = g ∈ V − V, where g(v_{k}) = f(v_{k}) · v_{j} (here · means ordinary multiplication of a vector by scalar).

In particular, if f = ṽ_{i}, then f(v_{k}) = 0 if i ≠ k, and f(v_{k}) = 1 if i = k, i.e.,

ṽ_{i}(v_{k}) = δ̃(v_{i} ⊗ v_{k}).

If f = ϵ, then f(v_{k}) = 1 for all k. Also

(z_{V V} (ṽ_{i} ⊗ v_{j}))(v_{k}) = δ̃(v_{i} ⊗ v_{k}) · v_{j}, δ̃^{+}(v_{i}) = ṽ_{i}.

Thus, we have

• z_{V V} ∘ (δ̃^{+} ⊗ id_{V}))(v_{i} ⊗ v_{j}) = v_{ij} ∈ (V − V)_{fin}

• z_{V V} ∘ ((ϵ^{+} ⊗ id_{V}) ∘ (b′_{V})^{−1})(v_{i}) = r_{i} ∈ (V − V)_{r−fin}.

¿From the other side,

• id_{V}^{+}(1) = E.

To define β, β̃, θ, θ̃ we need the following extension lemma.

Lemma 11.1 Let V_{0} be a subspace of a vector space V_{1}, and f_{0} be a linear function from V_{0} to V_{2}. Then there is a linear function f : V_{1} → V_{2} such that f|_{V_{0}} = f_{0}.

We need it only in application to certain subspaces of V − I and V − V (playing the role of V_{1}) and V or I as V_{2}.

Interpretations β and β̃ of retractions β, β̃ are defined on (V − V)_{r−fin} and (V − I)_{fin} respectively and then extended (in arbitrary way) according to extension lemma.

For f ∈ (V − I)_{fin}:

• β̃(f) = ∑_{i=1}^{i=∞} f_{i}.

For g ∈ (V − V)_{r−fin}:

• β(g) = ∑_{i=1}^{i=∞} g_{ii}v_{i}.

The equivalences of the groups (4) and (5) of the previous section become true equalities with this interpretation of morphisms. For example,

β ∘ (z_{V V} ∘ (δ̃^{+} ⊗ id_{V}))(v_{i} ⊗ v_{j}) = β(v_{ij}) = δ(v_{i} ⊗ v_{j}),

and

β ∘ (z_{V V} ∘ (ϵ^{+} ⊗ id_{V}) ∘ (b′_{V})^{−1})(v_{i}) = β(r_{i}) = v_{i}.

To interpret test-arrows we apply extension lemma to the function

θ(f) = 0, f ∈ (V − V)_{r−fin}, θ(E) = 1.

This definition is correct, because E does not belong to (V − V)_{r−fin}. Now θ on the whole (V − V) is defined as an arbitrary extension of the function above.

θ̃ is defined similarly, as an extension of the function

θ̃(f) = 0, f ∈ (V − I)_{fin}, θ̃(ϵ^{+}) = 1.

The commutativity of diagrams of the group (6) follows from this definition of θ, θ̃ immediately.

The following lemma explain the name “test-arrows”.

Lemma 11.2 The diagrams two diagrams in one

[figure: \begin{aligned}& (V − V) & & & (V − I) \\ I & & I & I & & I \\ & 0 & & & 0 \end{aligned}; θ; θ̃; id^{+}V; 0_{I}; ϵ^{+}; 0_{I}; 0^{I}; 0^{I}]

are not commutative in the category of vector spaces.

Proof.θ(E) = 1 ≠ 0, θ̃(ϵ^{+}) = 1 ≠ 0. □

Theorem 4 The SMC subcategory of the category of vector spaces over arbitrary field I, generated by the vector space V = ⨁_{n∈N} I, and by the space 0 satisfies the axioms of test-category.

Corollary 11.3 The definition of the test-category is consistent (in particular, the conditions of the groups (1)-(6) do not imply commutativity of the diagrams of the group (7)).

12 Extended calculi F_{V}(A) and L_{V}(A).

To make the rest of the proof more general, we shall consider two intermediate calculi: the SMC category FV(A) and related sequent calculus LV(A).

The formulas of FV(A) are built from atoms and three constants V, I and 0 in the same way as in F(A).

The axioms, corresponding to all arrows of V are added:

Δ : V → V ⊗ V, ......, θ : (V − V) → I, θ̃: (V − I) → I.

The rules are the same as in F(A).

We shall use the same abbreviations for derived arrows as in the definition of test-category.

The equivalence relation ≡_{V} on derivations is the minimal equivalence relation defined by all axioms,defining ≡, plus the new axioms corresponding to the conditions of the groups (1) - (6) in section 10.

Taking into account corollary 11.3, we obtain the following lemma:

Lemma 12.1 The calculus FV(A) is a non-trivial SMC category, and the diagrams of the group (7), section 10, are non-commutative in FV(A).

¿From the construction, we have also:

Lemma 12.2 Let K be an SMC category, containing a subcategory V, satisfying the definition of test-category. For every assignment

J : A → Ob(K)

there exists the unique structure-preserving functor

| − |′_{J} : FV(A) → K

such that

|a|′_{J} = J(a), |V |′_{J} = V ∈ Ob(K), |0|′_{J} = 0 ∈ Ob(K),
|Δ|′_{J} = Δ ∈ Mor(K), ..., |θ̃|′_{J} = θ̃ ∈ Mor(K).

The sequent calculus LV(A) is obtained from L(A) by extending the class of formulas as in FV(A) and adding new axioms, corresponding to

Δ : V → V ⊗ V, ..., θ̃: V − I → I.

Taking into account, that new arrows all have different domains and codomains, we can avoid use of labels: i.e., new axioms are just

V → V ⊗ V, ....., V − I → I.

Translations D and C are obtained by trivial extension of corresponding definitions for F(A) and L(A).

The relation ≡_{V} on sequential derivations is defined in the same way as for L(A).

As syntactical calculi, the systems F(A), L(A) are merely subsystems of FV(A), LV(A). Since the equivalence ≡_{V} is not weaker than ≡, all results, concerning the transformations of derivations in which new axioms were not used, still hold (for example, cut-elimination theorem or coherence theorems).

The RULES of FV(A), LV(A) coincide with these of F(A), L(A). This, together with the stronger equivalence relation ≡_{V} implies that most of the lemmas about permutation of rules (except these where we used unrestricted cut-elimination) also hold. We shall use them with appropriate care.

13 Calculations in F_{V}(A).

The interpretation | − |_{V} of the category FV(A) in itself is defined by the assignment

V(a) = V for all a ∈ A.

Below | − | means | − |_{V}.

We shall denote by | − | = | − |_{V} also the interpretation of the calculus LV(A) in itself defined by the same assignment .

This interpretation can be defined directly by substitution of V for all atoms in formulas and derivations.

Let A be a formula, built from atoms and I by applications of ⊗.

Let δ_{|A|} : |A| → V be the morphism, defined inductively in the following way.

(i) δ_{|I|} = id_{I} : I → I, δ_{|a|} = id_{V} : V → V , δ_{|a⊗b|} = δ : V ⊗ V → V; (ii) δ_{|I⊗C|} = δ_{|C|} ∘ b′, δ_{|C⊗I|} = δ_{|C|} ∘ b; (iii) δ_{|B⊗C|} = δ ∘ (δ_{|B|} ⊗ δ_{|C|}) : |B ⊗ C| → V (B, C ≠ I).

We shall denote by δ̃_{|A|} the morphism ϵ ∘ δ_{|A|}.

Let us define a “formal expanded instance” (cf.[18]) of an arrow

χ : B → C

of FV(A) to be any label ψ of the form

ψ = A[χ/a, id_{A_{1}}/a_{1}, ..., id_{A_{n}}/a_{n}, id_{I}/I],

where A is a formula, containing exactly one occurrence of the atom a, and A_{1}, ..., A_{n} are arbitrary formulas.

Obviously, the sequent

ψ : A[B/a, A_{1}/a_{1}, ..., A_{n}/a_{n}] → A[C/a, A_{1}/a_{1}, ..., A_{n}/a_{n}]

(in case a covariant in A), and the sequent

ψ : A[C/a, A_{1}/a_{1}, ..., A_{n}/a_{n}] → A[B/a, A_{1}/a_{1}, ..., A_{n}/a_{n}]

(in case a contravariant) is derivable in FV(A) and hence represents an arrow of FV(A).

If A_{1} = a_{1}, ..., A_{n} = a_{n}, we shall write sometimes

A[χ/a] : A[B/a] → A[C/a]

or

A[χ/a] : A[C/a] → A[B/a].

In multiple tensor products we shall suppose that brackets are grouped to the left.

Lemma 13.1 Let A be some tensor product of atoms and constant I, containing exactly one occurence of an atom a. Then

1.

δ_{|A[B/a]|} ≡V δ_{|A|} ∘ |A[δ_{|B|}/a]|.

2. For every central isomorphism ψ : A → A′:

ψ[V/a] ∘ (A[δ_{|B|}/a]) ≡_{V} (A′[δ_{|B|}/a]) ∘ (ψ[|B|/a]) : A[|B|/a] → A′[V/a],

|ψ| ∘ |A[δ_{|B|}/a]| ≡_{V} |A′[δ_{|B|}/a]| ∘ |ψ[B/a]| : |A[B/a]| → |A′[V/a]|.

3. If

f = (δ_{|A_{1}|} ⊗ ... ⊗ δ_{|A_{n}|}) ∘ |ψ| ∘ |B[δ_{|C|}/b]|,^{8}

where A, B, C, A_{1}, ..., A_{n} are tensor products of atoms and I, b occurs exactly once in B, and ψ : B → A_{1} ⊗ ... ⊗ A_{n}

is central isomorphism, then, for some i, 1 ≤ i ≤ m, f ≡V (δ_{|A_{1}|} ⊗ ... ⊗ δ_{|A_{i}[C/b]|} ⊗ δ_{|A_{n}|}) ∘ |ψ[C/b]|.

8In FV(A) “=” will be reserved for syntactic identity.

Proof. By associativity and commutativity of δ, and natuarlity of central isomorphisms. □

Lemma 13.2 (Absorption of central isomorphisms.) Let A, A′ be some formulas, built from atoms and I by ⊗. For every central isomorphism

ψ : A′ → A,

the composite δ_{|A|} ∘ |ψ|

|A′| →^{|ψ|} |A| →^{δ_{|A|}} V

is equal to δ_{|A′|}.

Proof. We proceed by induction on the number of b, b′, b^{−1}, b′^{−1}, a, a^{−1}, c in the label ψ.

Base: If ψ = b, b′, b^{−1}, b′^{−1}, use definition of δ_{|A|}. If ψ = a, a^{−1}, c, use associativity and commutativity of δ (see “absorption laws” from section 10).

Inductive step.

In case ψ ≡V ψ_{1} ∘ ψ_{2} inductive step is trivial. (Use associativity of composition and inductive hypothesis.)

In case ψ = ψ_{1} ⊗ ψ_{2}, A ≡V A_{1} ⊗ A_{2}, δ_{|A|} ≡V δ ∘ (δ_{|A_{1}|} ⊗ δ_{|A_{2}|}, and we can apply inductive hypothesis to δ_{|A_{1}|} and ψ_{1}, δ_{|A_{2}|} and ψ_{2} separately.

□

Corollary 13.3 In the conditions of lemma13.2, δ̃_{|A|} ∘ |ψ| ≡V δ̃_{|A′|}.

Corollary 13.4 In the conditions of the lemma 13.2

δ_{|A|} ∘ |ψ| ≡V δ_{|A′|} ∘ |ψ_{0}|,

where ψ_{0} is central isomorphism built only from b, b′, and A′ does not contain I.

Proof. By coherence of centrals, ψ can be represented as a composite ψ_{1} ∘ ψ_{0}, where ψ_{1} does not contain b, b′ (because A does not contain I), and ψ_{0} consists only of b, b′. Now apply lemma 13.2. □

Remark 13.5 It is easier to follow the proofs in this section, if one has in mind the case when V is the vector space of countable dimension (and all other data are interpreted as in section 11).

In this case one can prove the lemmas without complex calculations.

For example, consider lemma 13.2.

Let A be built from the atoms a_{1}, ..., a_{n} and I, and let v_{i_{1}}, ..., v_{i_{n}} be some basis vectors in |a_{1}| = V, ..., |a_{n}| = V. Then

δ_{|A|} : |A| → V

is equal to v_{i} if v_{i_{1}} = ... = v_{i_{n}} = v_{i} and is 0- vector otherwise. Obviously, this is not influenced by composition with any central isomorphism.

Lemma 13.6 (“Sewing” of two δ by Δ.) Let A be some non-constant formula, built by ⊗ from atoms and I, containing exactly one occurrence of an atom c, A_{1}, A_{2} be non-constant formulas, built from atoms and I by ⊗, and

ψ : A[(d_{1} ⊗ d_{2})/c] → A_{1} ⊗ A_{2}

be some central isomorphism, such that one of d_{1}, d_{2} occurs in A_{1} and another in A_{2}.

Then the composite

(δ_{|A_{1}|} ⊗ δ_{|A_{2}|}) ∘ |ψ| ∘ |A[Δ/c]| : |A| → V ⊗ V,

is equal to Δ ∘ δ_{|A|}.(Cf.the last diagram illustrating “absorption laws”, (2), section 10.)

Proof. Taking into account lemma 13.2 and coherence of centrals, it is enough to prove the lemma in the case when A = c ⊗ A′ and ψ is

(d_{1} ⊗ d_{2}) ⊗ A′ ⟶^{id⊗ψ′} (d_{1} ⊗ d_{2}) ⊗ (A′_{1} ⊗ A′_{2}) ⟶^{φ} (A′_{1} ⊗ d_{1}) ⊗ (d_{2} ⊗ A′_{2}).

Also by coherence of centrals,

φ ≡ a^{−1} ∘ c ∘ (a ⊗ id) ∘ a^{−1} : (d_{1} ⊗ d_{2}) ⊗ (A′_{1} ⊗ A′_{2}) ⟶ (A′_{1} ⊗ d_{1}) ⊗ (d_{2} ⊗ A′_{2}). (Indices can easily be reconstructed.)

By definition,

δ_{|A′_{1}⊗d_{1}|} ≡V δ ∘ (δ_{|A′_{1}|} ⊗ id), δ_{|(d_{2}⊗A′_{2})|} ≡V δ ∘ (id ⊗ δ_{|A′_{2}|}).

Using these facts, previous lemma, naturality of centrals, and functoriality of ⊗, we obtain

(δ_{|A′_{1}⊗d_{1}|} ⊗ δ_{|d_{2}⊗A′_{2}|}) ∘ |ψ| ∘ (Δ ⊗ id_{|A′|}) ≡V ((δ ∘ (δ_{|A′_{1}|} ⊗ id)) ⊗ (δ ∘ (id ⊗ δ_{|A′_{2}|}))) ∘ (a^{−1} ∘ c ∘ (a ⊗ id) ∘ a^{−1})∘ (id ⊗ ψ′) ∘ (Δ ⊗ id_{|A|}) ≡V (δ ⊗ δ) ∘ (a^{−1} ∘ c ∘ (a ⊗ id) ∘ a^{−1})∘ (Δ ⊗ (id_{V} ⊗ id_{V})) ∘ (id_{V} ⊗ (δ_{|A′_{2}|} ⊗ δ_{|A′_{1}|})) ∘ (id_{V} ⊗ ψ′) (here we have used naturality , note , that it changes the indexes of a, a^{−1}, c) ≡V (δ ⊗ id_{V}) ∘ (a^{−1} ∘ c) ∘ ((id_{V} ⊗ δ) ⊗ id_{V}) ∘ (a ⊗ id_{V})∘ ((Δ ⊗ id_{V}) ⊗ id_{V}) ∘ a^{−1} ∘ (id_{V} ⊗ (δ_{|A′_{2}|} ⊗ δ_{|A′_{1}|})) ∘ (id_{V} ⊗ ψ′) (because (id_{V} ⊗ δ) ∘ a ∘ (Δ ⊗ id_{V}) ≡V Δ ∘ δ) ≡V (δ ⊗ id_{V}) ∘ (a^{−1} ∘ c) ∘ (Δ ⊗ id_{V}) ∘ (δ ⊗ id_{V}) ∘ a^{−1}∘ (id_{V} ⊗ (δ_{|A′_{2}|} ⊗ δ_{|A′_{1}|})) ∘ (id_{V} ⊗ ψ′) ≡V (δ ⊗ id_{V}) ∘ (a^{−1} ∘ (id_{V} ⊗ Δ))∘ c ∘ (δ ⊗ id_{V}) ∘ a^{−1} ∘ (id_{V} ⊗ (δ_{|A′_{2}|} ⊗ δ_{|A′_{1}|})) ∘ (id_{V} ⊗ ψ′) ≡V Δ ∘ δ ∘ c ∘ (δ ⊗ id_{V}) ∘ a^{−1} ∘ (id_{V} ⊗ (δ_{|A′_{2}|} ⊗ δ_{|A′_{1}|})) ∘ (id_{V} ⊗ ψ′) ≡V Δ ∘ δ ∘ (δ ⊗ id_{V}) ∘ a^{−1} ∘ (id_{V} ⊗ (δ_{|A′_{2}|} ⊗ δ_{|A′_{1}|})) ∘ (id_{V} ⊗ ψ′) ≡V Δ ∘ δ ∘ (id_{V} ⊗ δ) ∘ (id_{V} ⊗ (δ_{|A′_{2}|} ⊗ δ_{|A′_{1}|})) ∘ (id_{V} ⊗ ψ′) ≡V Δ ∘ δ_{|c⊗(A′_{1}⊗A′_{2})|} ∘ (id_{V} ⊗ ψ′) ≡V Δ ∘ δ_{|c⊗A′|}.

□ Corollary 13.7 (“Sewing” with absorption of Δ.) In the conditions of previous lemma, the following equalities hold:

(i) b′_{|A_{2}|} ∘ (δ̃_{|A_{1}|} ⊗ δ_{|A_{2}|}) ∘ |ψ| ∘ (|A[Δ/c]|) ≡V δ_{|A|} : |A| → V,
(ii) b_{|A_{2}|} ∘ (δ_{|A_{1}|} ⊗ δ̃_{|A_{2}|}) ∘ |ψ| ∘ (|A[Δ/c]|) ≡V δ_{|A|} : |A| → V,
(iii) b_{I} ∘ (δ̃_{|A_{1}|} ⊗ δ̃_{|A_{2}|}) ∘ |ψ| ∘ (|A[Δ/c]|) ≡V δ̃_{|A|} : |A| → I,
(iv) b′_{I} ∘ (δ̃_{|A_{1}|} ⊗ δ̃_{|A_{2}|}) ∘ |ψ| ∘ (|A[Δ/c]|) ≡V δ̃_{|A|} : |A| → I,

Proof. We use previous lemma and “absorption laws” for b′, b from section 10. □

Let σ be a set of atoms. We shall denote

δ_{|a|}^{+} ⇀ ↽ π(δ_{|a|} ∘ b′_{V}) = id_{V}^{+} : I → (V − V),
δ_{|σ|⊗|a|}^{+} ⇀ ↽ π(δ_{|σ|⊗|a|}) : |σ| → (V − V) (n > 1),
δ̃_{|a|}^{+} ⇀ ↽ π(δ̃_{|a|} ∘ (b′_{V}) = ϵ^{+} : I → (V − I),
δ̃_{|σ|⊗|a|}^{+} ⇀ ↽ π(δ̃_{|σ|⊗|a|}) : |σ| → (V − I) (n > 1).

Using conditions of the groups (4) and (5) of section 10, we derive the following equalities (generalizations of equalities in (4), (5) of section 10). Let σ, τ be arbitrary non-empty sets of atoms:

(i) \begin{matrix}β ∘ δ_{|σ|⊗|a|}^{+} ≡V δ_{|σ|}, β̃ ∘ δ̃_{|σ|⊗|a|}^{+} ≡V δ_{|σ|}, \\ β ∘ z_{V V} ∘ (δ̃_{|σ|⊗|a|}^{+} ⊗ δ_{|τ|}) ≡V δ_{|σ|⊗|τ|} \\ β ∘ z_{V V} ∘ (δ̃_{|a|}^{+} ⊗ δ_{|τ|}) ∘ (b′_{|τ|})^{−1} ≡V \\ β ∘ z_{V V} ∘ (ϵ^{+} ⊗ δ_{|τ|}) ∘ (b′_{|τ|})^{−1} ≡V δ_{|τ|} \end{matrix} .

Using properties of evaluation e, we derive (for all non-empty σ, τ):

(ii) \begin{matrix}e_{V V} ∘ (Δ^{+} ⊗ δ_{|σ|}) ∘ (b′_{|σ|})^{−1} ≡V Δ ∘ δ_{|σ|}, \\ e_{V V} ∘ (id_{V}^{+} ⊗ δ_{|σ|}) ∘ (b′_{|σ|})^{−1} ≡V δ_{|σ|}, \\ e_{V I} ∘ (ϵ^{+} ⊗ δ_{|σ|}) ∘ (b′_{|σ|})^{−1} ≡V δ̃_{|σ|}, \\ e_{(V − V)V} ∘ (β^{+} ⊗ δ_{|σ|⊗|a|}^{+}) ∘ (b′_{|σ|})^{−1} ≡V δ_{|σ|}, \\ e_{(V − I)V} ∘ (β̃^{+} ⊗ δ̃_{|σ|⊗|a|}^{+}) ∘ (b′_{|σ|})^{−1} ≡V δ_{|σ|}, \\ e_{(V − V)I} ∘ (γ^{+} ⊗ δ_{|σ|⊗|a|}^{+}) ∘ (b′_{|σ|})^{−1} ≡V δ̃_{|σ|}, \\ e_{(V − I)I} ∘ (γ̃^{+} ⊗ δ̃_{|σ|⊗|a|}^{+}) ∘ (b′_{|σ|})^{−1} ≡V δ̃_{|σ|}, \\ e_{(V ⊗V)I} ∘ (δ̃^{++} ⊗ (δ_{|σ|} ⊗ δ_{|τ|})) ∘ (b′_{|σ|⊗|τ|})^{−1} ≡V δ̃_{|σ|⊗|τ|}, \\ e_{(V ⊗V)V} ∘ (δ^{++} ⊗ (δ_{|σ|} ⊗ δ_{|τ|})) ∘ (b′_{|σ|⊗|τ|})^{−1} ≡V δ_{|σ|⊗|τ|}, \\ e_{(V ⊗V)I} ∘ (δ̃^{++} ⊗ (Δ ∘ δ_{|σ|})) ∘ (b′_{|σ|})^{−1} ≡V δ̃_{|σ|}, \\ e_{(V ⊗V)V} ∘ (δ^{++} ⊗ (Δ ∘ δ_{|σ|})) ∘ (b′_{|σ|})^{−1} ≡V δ_{|σ|}, \end{matrix} .

At the same time the following generalizations of equalities (6) of section 10 hold for all non-empty σ, τ,

(iii) \begin{matrix}θ ∘ δ_{|σ|⊗|a|}^{+} ≡V 0_{|σ|}^{I}, θ̃ ∘ δ̃_{|σ|⊗|a|}^{+} ≡V 0_{|σ|}^{I}, \\ θ ∘ z_{V V} ∘ (δ̃_{|σ|⊗|a|}^{+} ⊗ δ_{|τ|}^{+}) ≡V 0_{|σ|⊗|τ|}^{I}, \\ θ ∘ z_{V V} ∘ (ϵ^{+} ⊗ δ_{|σ|}^{+}) ∘ (b′_{|σ|})^{−1} ≡V 0_{|σ|}^{I}, \\ e_{(V − V)I} ∘ (θ^{+} ⊗ δ_{|σ|⊗|a|}^{+}) ≡V 0_{|σ|}^{I}, \\ e_{(V − I)I} ∘ (θ̃^{+} ⊗ δ̃_{|σ|⊗|a|}^{+}) ≡V 0_{|σ|}^{I}, \\ e_{(V − V)I} ∘ (θ^{+} ⊗ (z_{V V} ∘ (δ̃_{|σ|⊗|a|}^{+} ⊗ δ_{|τ|}^{+}))) ∘ (b′_{|σ|⊗|τ|})^{−1} ≡V 0_{|σ|⊗|τ|}^{I}, \\ e_{(V − I)V} ∘ (θ^{+} ⊗ z_{V V} ∘ (ϵ^{+} ⊗ δ_{|σ|}^{+}) ∘ (b′_{|σ|})^{−1}) ≡V 0_{|σ|}^{I}, \end{matrix}

but also the following inequalities hold:

(iv) \begin{matrix}θ ∘ δ_{|a|}^{+} ≡V θ ∘ id_{V}^{+} ≠ 0, θ̃ ∘ ϵ^{+} ≠ 0, \\ e_{(V − I)V} ∘ (θ^{+} ⊗ δ_{|a|}^{+}) ∘ (b′_{I})^{−1} ≡V \\ e_{(V − I)V} ∘ (θ^{+} ⊗ id_{V}^{+}) ∘ (b′_{I})^{−1} ≠ 0 \\ e_{(V − I)V} ∘ (θ̃^{+} ⊗ ϵ^{+}) ∘ (b′_{I})^{−1} ≠ 0. \end{matrix}

Two lemmas about 0:

Lemma 13.8 If 0 occurs in a formula A, then |A| is isomorphic to 0.

Proof.(Trivial)

Lemma 13.9 Let ψ : A → B in FV(A), and some φ, such that

|φ| ≡V 0_{|C|}^{|D|},

occurs in ψ. Then

|ψ| ≡V 0_{|A|}^{|B|} : |A| → |B|.

Proof.(Trivial.)

14 Associated arrows and associated derivations

Definition 14.1 (Associated arrows.) Let S = σ, Σ → A be some balanced pure 2-sequent, where σ is non-empty set of atoms, and Σ consists of formulas of the form C − D.

We shall call associated arrows of S the following arrows of K (depending on σ and on the form of A).

(i) A = I.

δ̃_{|σ|} : |σ| → I.

(ii) A = a.

δ_{|σ|} : |σ| → V.

(iii) A = a ⊗ b (two kinds of arrows):

Δ ∘ δ_{|σ|} : |σ| → V ⊗ V

and

δ_{|σ_{1}|} ⊗ δ_{|σ_{2}|} : |σ_{1}| ⊗ |σ_{2}| → V ⊗ V ,

where σ_{1}, σ_{2} are non-empty disjoint subsets of σ, and σ = σ_{1} ∪ σ_{2};

(iv) A = a − I.

δ̃_{|σ|⊗|a|}^{+} : |σ| → V − I.

(v) A = a − b (two kinds of arrows):

δ_{|σ|⊗|a|}^{+} and z_{V V} ∘ (δ̃_{|σ_{1}|⊗|a|}^{+} ⊗ δ_{|σ_{2}|}) : |σ| → V − V,

where σ_{1}, σ_{2} are disjoint subsets of σ, at least σ_{2} is non-empty, and σ = σ_{1} ∪ σ_{2}.

We shall also call associated arrows of S all arrows that are ≡_{V} -equivalent to the arrows above and their compositions with central isomorphisms

|B| → |σ|,

where B is a tensor product of atoms of σ (each atom taken exactly once), and, maybe, some copies of I.

If h is an arrow associated with S, we shall write

S >> h.

If, for some derivation φ of a sequent S in LV(A), S >> |φ|, we shall say that φ is an associated derivation of S.

Definition 14.2 (Associated arrows of implicative formulas.) With each type of implicative formula B = C − D, which occur in balanced pure 2-sequents, we shall associate the following arrow g^{|B|}.

\begin{matrix}B & |B| & g^{|B|} \\ c − I & V − I & ϵ^{+} : I → V − I \\ c − d & V − V & id_{V}^{+} : I → (V − V) \\ c − d_{1} ⊗ d_{2} & V − (V ⊗ V) & Δ^{+} : I → V − (V ⊗ V) \\ c_{1} ⊗ c_{2} − d & (V ⊗ V) − V & δ^{++} : I → (V ⊗ V) − V \\ c_{1} ⊗ c_{2} − I & (V ⊗ V) − I & δ̃^{++} : I → (V ⊗ V) − I \\ (c_{1} − c_{2}) − d & (V − V) − V & β^{+} : I → (V − V) − V \\ (c − I) − d & (V − I) − V & β̃^{+} : I → (V − I) − V \\ (c_{1} − c_{2}) − I & (V − V) − I & γ^{+} : I → (V − V) − I \\ (c − I) − I & (V − I) − I & γ̃^{+} : I → (V − I) − I \end{matrix}

Remark 14.3 Remember that we have translations in both directions FV(A) → LV(A) and FV(A) → LV(A). So, all the arrows of FV(A) we consider have as their counterparts certain derivations of LV(A). We shall call them associated derivations(and sometimes denote them by the same symbols).

Between these derivations the same equivalences hold.

Theorem 5 For every saturated derivation ξ of a sequent

S = a_{1}, ..., a_{n}, A_{1}, ..., A_{m} → A

the derivation, obtained from the derivation |ξ| of

V, ..., V, |A_{1}|, ..., |A_{m}| → |A|

by cuts with g^{|A_{i}|}, is an associated derivation of S.

Proof by induction on the number of implications in S.

Base. (No implications.)

Because S is balanced pure 2-sequent, S can be an axiom a → a or be of the form a, b → a ⊗ b.

There is unique cut-free derivation φ in each case, and |φ| = b_{V} = δ_{1} ∘ b_{V} and (δ_{1} ⊗ δ_{1}) ∘ (id_{V} ⊗ b_{1}) respectively.

These arrows are associated arrows of S.

Inductive step. By lemma 8.3 we can assume without loss of generality that ξ ends by one of forms of inference, described there, and that the subderivations of the sequents on the top of these inferences are saturated.

Note that the last rule of the inferences we consider now is either −↪ or → −.

There is no problem to show that inductive hypothesis is applicable to the derivations of premises (top-sequents) of each inference: each cut with g^{|A_{i}|}, except the one where |A_{i}| is main formula of the last (−↪), can be moved up to these premises (by lemmas about permutations with cut).

To prove inductive step, we have to consider the “action” of each inference on associated arrows of these premises. It is essential, how the newly introduced function g^{|A_{i}|} (corresponding to the last −↪) is evaluated.

In case of the last rule (→ −) we automatically obtain an arrow in one of the forms, given in the definition of associated arrows, from the associated arrows of premises (top-sequents).

For example, in case 5.1 it will be (up to central isomorphism)

δ_{|σ|⊗|a|}^{+} : |σ| → V − V.

In the case 5.2 it will be

\begin{matrix}π(b′_{V} ∘ (δ_{|a|⊗|σ_{1}|} ⊗ δ_{|σ_{2}|}) ∘ χ) = \\ π(b_{V} ∘ (δ_{|σ_{rp}|} ⊗ δ_{|a|⊗|σ_{1}|}) ∘ χ_{1}) = z_{V V} ∘ (δ_{|σ_{rp}|} ⊗ δ_{|a|⊗|σ_{1}|}) ∘ χ_{2} \end{matrix} ,

where χ, χ_{1}, χ_{2} are appropriate central isomorphisms. If the last rule is (−↪), then by lemma 5.13 it can be replaced by the following (cut):

\frac{\frac{σ_{1}, Σ_{1} →^{ξ_{1}} C D → D}{σ_{1}, Σ_{1}, C − D → D} (−↪) \frac{ξ_{2}}{D, σ_{2}, Σ_{2} → A}}{\underbrace{σ_{1}, σ_{2}}_{σ}, \underbrace{C − D, Σ_{1}, Σ_{2}}_{σ} → A} (cut),

where ξ_{1} and ξ_{2} are the subderivations of left and right premises of ξ.

Let ξ′_{1} denote the derivation

\frac{σ_{1}, Σ_{1} →^{ξ_{1}} C D → D}{σ_{1}, Σ_{1}, C − D → D} (−↪).

Using equalities (i), (ii) in the end of section 13, we see, that, composing |ξ′_{1}| with an appropriate expanded instance of g^{|C− D|} and central isomorphism, we receive an arrow, associated with σ_{1} and D.

When the derivation of the right premise is saturated (cases 1.1, 2.1), we use equalities from lemma 13.1 and absorption of centrals (lemma 13.2), and, if main formula is c → d_{1} ⊗ d_{2}, also Δ-absorption (corollary 13.7).

In case 1.2 (the right premise I → I) it is enough to use appropriate equalities from (ii), section 13 (depending on main formula).

If the derivation of the right premise of (−↪) is not saturated (all remaining cases), then still the arrow in F(V), obtained from associated arrows of “top-sequents” (the premises of considered inference) is simple combination of these arrows and some central isomorphisms (it can be written in routine way).

For example, in case 1.4 it is

b_{II} ∘ (δ̃_{|σ_{21}|⊗|d_{1}|} ⊗ δ̃_{|σ_{22}|⊗|d_{2}|}) ∘ χ

with χ central.

In case 3.3 it is

b′_{V} ∘ (δ̃_{|σ_{21}|⊗|d_{1}|} ⊗ h) ∘ χ,

where h is Δ ∘ δ_{|σ_{22}|} or (δ_{|σ_{221}|} ⊗ δ_{|σ_{222}|}) ∘ χ_{1}.

To show, that its composition with the arrow, obtained from the derivation of the left premise will give an arrow, associated with the final sequent, we have to use:

• in case 3.1, (3) of lemma 13.1;

• in cases 1.3, 2.2, 3.2, absorption of centrals (lemma 13.2), equalities of lemma 13.1, and also absorption of Δ (lemma 13.7);

• in all remaining cases, i.e., the cases 1.4, 2.3, 2.3’, 3.3, 3.3’ all these lemmas and (this is essential) “sewing” lemma and its corollary (lemma 13.6, corollary 13.7).

It is essential that in the last group of cases the d_{1}, d_{2} of the main formula c − d_{1} ⊗ d_{2} go to different premises (top-sequents) of considered inference.

This allows to apply “sewing” lemmas, and provide “closedness” of the system of associated arrows with respect to the “evaluation process”, determined by saturated derivations. □

Remark 14.4 The arrow, described in theorem 5, can be represented by the following diagram:

|a_{1} ⊗ ... ⊗ a_{n}|

|a_{1} ⊗ ... ⊗ a_{n} ⊗ I ⊗ ... ⊗ I|

|a_{1} ⊗ ... ⊗ a_{n} ⊗ A_{1} ⊗ ... ⊗ A_{m}|

|A|

|κ|

id_{V} ⊗...⊗id_{V} ⊗g^{|A1|}⊗...⊗g^{|Am|}⊗id_{I}

|ξ|

Theorem 6 Under the conditions of the previous theorem, assume that one of A_{i} has the form (a− b)− I, with a an atom and b an atom or I. Consider |ξ| and apply “cut” with the cut-formula |(a− b)− I| and with the left premise θ^{+} : I → (V − V)− I if b is an atom or θ̃^{+} : I → (V − I)− I if b is I. Make “cuts” with g^{|A_{k}|} for all other implicative members A_{k}. The resulting derivation is equivalent to 0 in LV(A).

Proof by induction on the number of applications of the rule −↪ between the introduction of − in A_{i} and the final sequent.

Without loss of generality we can assume that i = m Base. The implication in A_{m} = (a − b) − I was introduced by the last rule.

The derivation |ξ| has the form

|ξ| = \frac{V, ...V, |A_{1}|, ...|A_{m−1}| → (V − V) I → I}{V, ...V, |A_{1}|, ...|A_{m−1}|, (V − V) − I → I}.

By lemma 5.10 all cuts except the one with θ^{+} or θ̃^{+} can be moved up to the left premise. By the previous theorem the resulting derivation of the left premise is equivalent to

z_{V V} ∘ (δ̃_{|σ_{1}|⊗|a|}^{+} ⊗ δ_{|σ_{2}|}) : |σ| → (V − V)

or to

δ_{|σ|⊗|a|}^{+} : |σ| → (V − V).

In both cases, by the equalities (iii) of section 13 the result will be equivalent to 0.

Inductive Step. We consider the forms of inference as in the previous theorem. If the last application of −↪ has not A_{m} as main formula, then by lemma 5.10, the cut with θ^{+} (θ̃^{+}) can be moved up to one of the premises, and inductive hypothesis can be applied (again using lemma 8.3). □

Let us consider a pair of derivations (η_{1}, η_{2}) ∈ W′_{0}.

η_{1} ≡ \frac{\frac{c, Σ, (a − b) − I →^{ξ_{1}} d}{Σ, (a − b) − I → (c − d)} (→ −) \overline{I → I}}{Σ, (a − b) − I, (c − d) − I → I} (−↪)

η_{2} ≡ \frac{\frac{a, Σ, (c − d) − I →^{ξ_{2}} b}{Σ, (c − d) − I → (a − b)} (→ −) \overline{I → I}}{Σ, (a − b) − I, (c − d) − I → I} (−↪).

The derivation ξ_{1} is saturated, and, as its final sequent contains exactly one atom c as antecedent member, the corresponding associated arrow is id_{V} (when d is also an atom) or ϵ, when it is I. The same may be said about ξ_{2}.

Theorem 7

¬(|η_{1}| ≡V |η_{2}|).

Proof. Let Σ = A_{1}, ..., A_{m}.

Let ω_{i} (i=1,2) be the derivations, obtained from |η_{i}| by cuts with the derivations

I \underrightarrow{g^{|A_{1}|}} |A_{1}|, ... , I \underrightarrow{g^{|An|}} |A_{n}|,

I \underrightarrow{g^{|(a− b)− I|}} |(a − b) − I|,

I ⟶^{θ^{+}} |(c − d) − I|.

(in case d = I we take θ̃^{+} instead of θ^{+}). Obviously, if ¬(ω_{1} ≡_{V} ω_{2}) then ¬(|η_{1}| ≡_{V} |η_{2}|).

In ω_{1} all cuts except the one with θ^{+} (θ̃^{+}) can be moved up at least to the final sequent of |ξ_{1}|. The cut with θ^{+} (θ̃^{+}) cannot be moved because its cut-formula is at the same time the main formula of the last −↪.

The result of these cuts with |ξ_{1}| will be associated arrow, which is, in this particular case, id_{V} or ϵ. Direct calculation gives

ω_{1} ≡_{V} θ^{+} ∘ id^{+},

or

ω_{1} ≡_{V} θ̃^{+} ∘ ϵ^{+}.

As to ω_{2}, cut with θ^{+} (θ̃^{+}) can be moved up to the final sequent of |ξ_{2}| instead of cut with g^{|(a− b)− I|}. By theorem 6, the result will be equivalent to 0. □

Corollary 14.5 If an SMC category K contains a subcategory V, satisfying the definition of testcategory, and J is the assignment of V ∈ ObK to every atom, then for every pair (η_{1}, η_{2}) ∈ W′_{0},

|η_{1}|_{J} ≠ |η_{2}|_{J}.

Proof. Obviously, | − |_{J} can be represented as the composition of the following interpretations: 1)L(A) in LV(A), defined by identity on atoms; 2)| − |_{V} of LV(A) in itself; 3)| − |′_{J} from LV(A) to K. By the theorem 7, in LV(A) one of the derivations is interpreted as θ^{+} ∘ id^{+} or θ̃^{+} ∘ ϵ^{+} and

another as 0. This difference will be preserved by | − |′_{J} by definition of this interpretation. □ Now our Theorem 1 If SMC category K contains an SMC subcategory V, satisfying the axioms of test-

category, then for every two canonical maps ψ, φ : A → B with balanced A → B the equivalence ψ ≡ φ holds iff for all interpretations | − |_{J} in K, |ψ|_{J} = |φ|_{J}.

can be proved as follows. Proof. If ψ ≡ φ then automatically |ψ|_{J} = |φ|_{J}. Assume that ¬(ψ ≡ φ). Consider the corresponding pair of derivations in L(A). By theorem 2, we can assume that the derivations under consideration are the derivations of

a pure 2-sequent.

By abstract coherence theorem 3, they should belong to the class W′. By definition of the class W′, there exists a substitution α of I for some atoms, such that

(α ∗ η_{1}, α ∗ η_{2}) ∈ W′_{0}.

If K contains subcategory being test-category, the interpretation, defined by the assignment of V to remaining atoms makes α ∗ η_{1} and α ∗ η_{2} distinct morphisms of K.

Obviously, the assignment of I to the atoms such that I was substituted for them by α, and the assignment of V to the rest, will have the same effect as the use of α with subsequent assignment of V to all atoms.

Hence there exists an assignment, making η_{1} and η_{2} distinct in K. □ The following corollary is a modified version of the main theorem of R.Voreadou.

Corollary 14.6 Let (η_{1}, η_{2}) be derivations of the same balanced pure 2-sequent. Then η_{1} ≡ η_{2} iff the pair (η_{1}, η_{2}) does not belong to the class W′.

References

[1] . M. Barr. *-Autonomous Categories (with Appendix by Po-Hsuang Chu). Lect. Notes in Mathematics, 752, 1979.

[2] G.Bierman. Ph.d. Thesis, Oxford, 1994.

[3] S.Eilenberg and G.M.Kelly. A generalization of the functorial calculus.-J.of Algebra, 1966.

[4] S.Eilenberg and G.M.Kelly. Closed Categories. - Proceedings of the Conference on Categorical Algebra, La Jolla, 1965, 421-562, N.-Y., Springer, 1966.

[5] G.-Y. Girard, Y. Lafont. Linear logic and lazy computation. In: Proc.TAPSOFT 87 (Pisa), v.2, p.52-66, Lecture Notes in Comp.Sci. v.250 , 1987.

[6] C.B. Jay. The structure of free closed categories. Journal of Pure and Applied Algebra, 66(3):271–287, 1990.

[7] C.B. Jay. Coherence in Category Theory and the Church-Rosser property. To appear in: Notre Dame Journal of Formal Logic, also accessible from the WWW-site: linus.socs.uts.edu.au/ cbj.

[8] G.M.Kelly. A cut-elimination theorem. Ibid., 196-213.

[9] G.M. Kelly and S. Mac Lane. Coherence in Closed Categories. Journal of Pure and Applied Algebra, 1(1):97–140, 1971.

[10] J. Lambek. Deductive Systems and Categories. I. Math. Systems Theory, 2, 287-318, 1968.

[11] J. Lambek. Deductive Systems and Categories. II. Lecture Notes in Math., 86: 76–122, 1969.

[12] S. Mac Lane. Topology and Logic as a Source of Algebra. Bull. Amer. Math. Soc., 82, 1, 1976.

[13] G.E. Mints. Closed categories and Proof Theory. Journal of Soviet Mathematics, 15, 45–62, 1981.

[14] S. V. Soloviev. The category of finite sets and cartesian closed categories. Zapiski Nauchnych Seminarov Leningradskogo Otdelenya Matematicheskogo Instituta im.V.A. Steklova AN SSSR, 105:174-194, 1981 (English translation in: Journal of Soviet Mathematics, 22(3): 1387– 1400, 1983).

[15] S.V. Soloviev. On the conditions of full coherence in closed categories. Journal of Pure and Applied Algebra, 69:301-329, 1990.

[16] R.Statman. Completeness, Invariance and λ -definability. J.of Symb. Logic, 47, 1, 1982.

[17] M.E. Szabo. Algebra of Proofs. Studies in Logic and the Foundations of Mathematics, 88(1978), North-Holland P.C.

[18] R. Voreadou. Coherence and non-commutative diagrams in closed categories. Memoirs of the AMS, v.9, issue 1, No 182 (last of two numbers), January 1977.

Recent Publications in the BRICS Report Series

RS-96-61 Sergei Soloviev. Proof of a Conjecture of S. Mac Lane. December 1996. 53 pp. Extended abstract appears in Pitt, Rydeheard and Johnstone, editors, Category Theory and Computer Science: 6th International Conference, CTCS ’95 Proceedings, LNCS 953, 1995, pages 59�80.

RS-96-60 Johan Bengtsson, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Uppaal in 1995. December 1996. 5 pp. Appears in Margaria and Steffen, editors, Tools and Algorithms for The Construction and Analysis of Systems: 2nd International Workshop, TACAS ’96 Proceedings, LNCS 1055, 1996, pages 431�434.

RS-96-59 Kim G. Larsen, Paul Pettersson, and Wang Yi. Compositional and Symbolic Model-Checking of Real-Time Systems. December 1996. 12 pp. Appears in 16th IEEE Real-Time Systems Symposium, RTSS ’95 Proceedings, 1995.

RS-96-58 Johan Bengtsson, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Uppaal � a Tool Suite for Automatic Veri�cation of Real�Time Systems. December 1996. 12 pp. Appears in Alur, Henzinger and Sontag, editors, DIMACS Workshop on Veri�cation and Control of Hybrid Systems, HYBRID ’96 Proceedings, LNCS 1066, 1996, pages 232�243.

RS-96-57 Kim G. Larsen, Paul Pettersson, and Wang Yi. Diagnostic Model-Checking for Real-Time Systems. December 1996. 12 pp. Appears in Alur, Henzinger and Sontag, editors, DIMACS Workshop on Veri�cation and Control of Hybrid Systems, HYBRID ’96 Proceedings, LNCS 1066, 1996, pages 575�586.

RS-96-56 Zine-El-Abidine Benaissa, Pierre Lescanne, and Kristoffer H. Rose. Modeling Sharing and Recursion for Weak Reduction Strategies using Explicit Substitution. December 1996. 35 pp. Appears in Kuchen and Swierstra, editors, 8th International Symposium on Programming Languages, Implementations, Logics, and Programs, PLILP ’96 Proceedings, LNCS 1140, 1996, pages 393�407.