Linear Läuchli Semantics

R. F. Blute P. J. Scott

Dept. of Mathematics University of Ottawa Ottawa, Ontario CANADA

March 20, 1995

Dedicated to the memory of Moez Alimohamed

Abstract

We introduce a linear analogue of Läuchli’s semantics for intuitionistic logic. In fact, our result is a strengthening of Läuchli’s work to the level of proofs, rather than provability. This is obtained by considering continuous actions of the additive group of integers on a category of topological vector spaces. The semantics, based on functorial polymorphism, consists of dinatural transformations which are equivariant with respect to all such actions. Such dinatural transformations are called uniform. To any sequent in Multiplicative Linear Logic (MLL), we associate a vector space of “diadditive” uniform transformations. We then show that this space is generated by denotations of cut-free proofs of the sequent in the theory MLL+MIX. Thus we obtain a full completeness theorem in the sense of Abramsky and Jagadeesan, although our result differs from theirs in the use of dinatural transformations.

As corollaries, we show that these dinatural transformations compose, and obtain a conservativity result: diadditive dinatural transformations which are uniform with respect to actions of the additive group of integers are also uniform with respect to the actions of arbitrary cocommutative Hopf algebras. Finally, we discuss several possible extensions of this work to noncommutative logic.

It is well known that the intuitionistic version of Läuchli’s semantics is a special case of the theory of logical relations, due to Plotkin and Statman. Thus, our work can also be viewed as a first step towards developing a theory of logical relations for linear logic and concurrency.

Contents

1 Introduction 3

2 Proof Nets 4 2.1 Cut Elimination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.2 The MIX Rule . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.3 Coherence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.4 Simple Sequents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8

3 Logical Relations and Logical Permutations 9 3.1 Definitions and Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 3.2 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11

4 Läuchli Semantics 12 4.1 G-Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 4.2 Läuchli’s Theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13

5 ∗-Autonomous Categories and Vector Spaces 14 5.1 Linear Topology . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 5.2 Quotients and Direct Sums . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

6 Representations of Groups 18 6.1 Z-Actions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 6.2 Symmetric Monoidal Closed Structure . . . . . . . . . . . . . . . . . . . . . 18

7 Functorial Polymorphism 19 7.1 Interpreting ⊗, −∘ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 7.2 Interpreting MLL Sequents . . . . . . . . . . . . . . . . . . . . . . . . . . . 23

8 Dinaturals on Vector Spaces 24 8.1 Uniform Dinaturals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 8.2 Linear Structure of Uniform Dinaturals . . . . . . . . . . . . . . . . . . . . . 25

9 Completeness 25

10 Full Completeness 30 10.1 Binary Sequents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 10.2 Nonbinary Sequents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 10.3 Main Result . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38

11 Hopf Algebras 38 11.1 Definition and Categorical Structure . . . . . . . . . . . . . . . . . . . . . . 38 11.2 Conservativity Theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41

12 Conclusion 41

1 Introduction

In the 1930’s, Heyting introduced a “proof” interpretation of intuitionistic logic. This informal semantics has become increasingly influential, both in logic and more recently in computer science. Indeed, attempts to develop a rigorous mathematical framework for Heyting’s ideas led the way to many fundamental discoveries, for example Kleene’s Realizability, Gödel’s Dialectica Interpretation , and (more recently) the Curry-Howard Isomorphism ([21]). However somewhat less familiar is Läuchli’s seminal work in the 1960’s [30]: this was the first attempt to give both an abstract model of “proof” for intuitionistic logic and a Completeness Theorem for provability.

Läuchli’s viewpoint models a formula by a set: intuitively, by its set of (abstract) proofs. Ordinary sets, however, have insufficient structure to obtain a completeness theorem of this type. Lauchli’s modelling used a more sophisticated notion of “set” and “element”:

Formula = set with a distinguished permutation on it
Proof  = invariant element.

A set with a distinguished permutation may be identified with a Z-set (a set with an action of the free cyclic group Z). Thus, from this viewpoint, Läuchli’s abstract models are nothing more than Z-set models [23]. Läuchli’s Completeness Theorem says: a formula is provable if and only if its interpretation in every abstract model contains an invariant element (i.e. an “abstract proof”).

Läuchli’s semantics also has a categorical interpretation. The category of Z-sets is a cartesian closed category (= ccc), and so interprets simply-typed λ-calculus as in [29], or equivalently deductions in a fragment of intuitionistic logic. A categorical presentation can be found in [23].

While Läuchli’s semantics is a semantics of proofs, Läuchli’s theorem is finally about provability, rather than genuine proofs. Thus, we might ask for a better result: can one find a notion of abstract model which characterizes proofs themselves? This is the full completeness problem [2]. From the Curry-Howard viewpoint, which identifies formulas with types and (natural deduction) proofs with typed λ−terms, we are asking for a typed lambda model E with a surjective interpretation function − : L → E. Thus every function in such a model is the denotation of some proof.

From a Computer Science viewpoint, full completeness theorems are similar to full abstraction theorems, since lambda terms correspond to programs. Thus one is attempting to characterize operational or syntactic behaviour of program terms using a more “mathematical” model. Indeed, the fundamental full completeness results of Abramsky and Jagadeesan [2] for multiplicative linear logic (= MLL) using game semantics recently led to a solution of the full abstraction problem for PCF [3], a fundamental problem in denotational semantics for many years [34].

Finally, from a categorical viewpoint, full completeness theorems are asking for a full representation of a certain kind of free category, say C, into a model category E. In this sense, a full completeness theorem is a strong kind of representation theorem. Of course for such a result to be sensible, the model E should not itself be too syntactic, but rather be a “genuine” mathematical structure not built from C. For example, the Yoneda embedding [29] Y : C → Set^{C^{op}} is well-known to give a fully faithful representation for ccc’s, but it fails to yield an independent model E in our sense: Set^{C^{op}}depends too much on C.

The first full completeness result that we know of is due to Plotkin [39]. Inspired by Läuchli’s work, Plotkin attempted to characterize lambda definability of set-theoretic functions in the full type hierarchy (= a full sub-ccc of Sets) generated from an infinite atomic set. This characterization involved invariance under certain kinds of logical relations. For a detailed discussion, see Section 4 below. As such, we believe that the work presented in this paper may be viewed as the beginnings of a theory of logical relations for linear logic and concurrency.

In this paper, we present a semantics based upon an extension of functorial polymorphism [5, 9, 22] to the linear setting. In this setting, types are definable multivariant functors on a category of topological vector spaces. We then interpret terms, i.e. deductions in the theory MLL+MIX as certain dinatural transformations between such functors. The key property is that these transformations be uniform, in other words, equivariant with respect to certain continuous actions of the additive group of integers. In the case of sequents which are balanced but not binary, we add an additional criterion known as diadditivity. This says that the transformation is a linear combination of substitution instances of dinaturals interpreting binary sequents. This is in keeping with the philosophy that in a (cut-free) proof structure it is the axiom links which behave as variables, and one should be allowed to substitute distinct variables for two variables not connected by axiom links.

The use of dinaturality and functorial polymorphism is a substantial difference between our work and previous such theorems. For example, function spaces have a natural interpretation as certain multivariant functors. This work also suggests the notion of group action may be fundamental to future results of this sort.

Our full completeness theorem (Section 10) takes the following strong form: interpreting formulas as definable functors F, F′, the set of uniform diadditive dinatural transformations has a vector space structure, with basis the cut-free proofs in MLL + MIX. This yields several interesting corollaries (see Section 10):

- Such dinaturals compose. When one is constructing a semantics based on functorial polymorphism [5], one must show that the dinatural transformations representing the terms compose. This is because dinatural transformations, unlike natural transformations, do not compose in general.

- A conservativity result: if a proof (= diadditive dinatural) is uniform with respect to the additive group of integers, it is uniform with respect to arbitrary cocommutative Hopf algebras.

Finally, we point out that our treatment appears to be extendible to other theories, notably theories of non-commutative linear logics, by generalizing groups to general Hopf algebras. At the same time, the categories of vector spaces we deal with are complete and co-complete, suggesting the interpretation of far more than just MLL.

2 Proof Nets

In this section, we review basic properties of proof nets, and their relationship to ∗- autonomous categories. We assume that the reader is familiar with linear sequent calculus.

If not, the reader might consult [19] or [47].

Notation Convention We shall write ⊢ Γ to denote a one-sided sequent, and say that ⊢ Γ is derivable (correct or provable) if there is a sequent calculus proof of it. We will use similar terminology for two-sided sequents.

Proof nets are a graph-theoretic natural deduction proof system for the multiplicative fragment of linear logic, introduced by Girard in [19]. The remarkable property of proof nets is the interaction between a global correctness criterion and a local normalization process. It is this interaction which makes nets useful in analyzing coherence problems in ∗-autonomous categories [9].

The version of proof net we present is a simplification due to Danos and Regnier [14]. We first define the notion of proof structure. These are certain graphs whose nodes are labelled by formulas (or better, formula occurrences). Proof structures are constructed inductively from four types of links:

AXIOM LINKS TENSOR LINKS

A  A^{⊥}

[figure: A; B; A ⊗ B]

PAR LINKS CUT LINKS

[figure: A; B; A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B]

[figure: A; A^{⊥}; CUT]

Each link has a multiset of hypotheses and conclusions. The axiom link has no hypotheses and A, A^{⊥} as conclusions, while Cut has the dual situation: A, A^{⊥} are hypotheses and no conclusion; the tensor and par links have A, B as hypotheses, and the appropriate formula as conclusion. Tensor and Par links are not symmetric w.r.t. interchanging hypotheses; on the other hand, axiom and cut are symmetric w.r.t. interchanging conclusions (resp. hypotheses). Proof structures are subject to the obvious restrictions, i.e. an occurrence of a formula is the conclusion of exactly one link, and the premise of at most one link. We will also add the condition that one may only introduce axiom links for which the conclusions are literals, i.e. atoms or negations of atoms. This has no effect on expressive power and allows us to avoid the expansion rules of [12].

There is a straightforward translation from sequent deductions to proof structures. We wish to identify those structures which correspond to derivable sequents. One of the advantages of this system over other natural deduction systems is that there is an intrinsic graph-theoretic criterion on proof structures which determines if the structure corresponds to a derivable sequent deduction.

A switching for a proof structure is obtained by removing one of the two edges from each .^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} -link. A proof structure is a proof net if, for all switchings, the resulting graph is acyclic and connected.

The following two theorems [19, 47] show that this is a correct notion of deduction for MLL.

Theorem 2.1 (Girard) There is a canonical translation procedure which takes sequent calculus deductions in MLL to proof structures. If a proof structure is in the image of this translation, it is a proof net.

Theorem 2.2 (Girard) Given a proof net with conclusions {A_{1}, …, A_{n}}, there is a sequent calculus proof of ⊢ A_{1}, …, A_{n} mapped to it under the translation procedure.

This last result is refered to as the sequentialization theorem.

Finally, note that proof nets take no account of the order of the rules in a deduction: sequent proofs which are equivalent modulo commutative reductions have the same proof net.

2.1 Cut Elimination

As previously remarked, the cut elimination procedure is especially important for analyzing the structure of ∗-autonomous categories. For proof nets, it is accomplished by the following procedure. The advantage of this procedure is that it is local in nature, so that each cut can be eliminated independently, as follows.

The cut:

[figure: B; C; B^{⊥}; C^{⊥}; B ⊗ C; B^{⊥}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} C^{⊥}; CUT]

reduces to the two cuts:

[figure: B; B^{⊥}; C; C^{⊥}; CUT; CUT]

The cut:

[figure: A; A^{⊥}; A; CUT]

reduces to the single formula:

A

The following is due to Girard [19].

Theorem 2.3 The theory MLL satisfies cut elimination. The cut elimination process for proof nets is confluent and strongly normalizing. Given a derivable sequent deduction in MLL, its cut-free proof net is uniquely determined.

This last statement follows from the elementary observation that a cut-free proof structure is uniquely determined by its axiom links. The portion of the net below the axiom links corresponds to the subformula tree of the formulas in the sequent.

2.2 The MIX Rule

An important variant of MLL is obtained by considering the MIX rule. Not only is this an interesting extension of linear logic with a natural computational interpretation [15], but the MIX rule is valid in most models. For example, the coherence spaces of [19] as well as the category RT VEC defined below validate it. The MIX rule is stated as follows:

\begin{matrix}⊢ Γ & ⊢ Δ \\ ⊢ Γ, Δ \end{matrix} MIX

This rule is not correct for MLL, so to accommodate the larger theory MLL + MIX, we simply alter the correctness criterion by requiring only that for each switch setting the graph be acyclic. Then all of the above results easily extend. This is described in [15].

In our models, we have a strong version of the MIX rule, which is obtained by equating the two multiplicative units, i.e. ⊤ = ⊥. It is straightforward to verify that MLL with the usual unit rules and this equation implies the MIX rule. For this theory, it is straightforward to incorporate units into the nets, whereas for MLL, one requires weakening links [12].

2.3 Coherence

While the observation that a cut-free net is uniquely determined by its axiom links is obvious, it has several important consequences. In particular it is used to derive the coherence theorem for ∗-autonomous categories. Under the Lambek equivalence between deductions in a deductive system and morphisms in a free category, a morphism in the free ∗-autonomous category (without units) can be interpreted as a proof net. In this interpretation, proof nets are viewed as a graph-theoretic syntax for specifying morphisms in the free ∗-autonomous category (without units). The fact that they form a confluent, strongly normalizing rewrite system suggests that nets can be viewed as a typed λ-calculus for ∗-autonomous categories, analogous to the work of [29]. With this interpretation in mind, it is straightforward to derive:

Theorem 2.4 (Blute) Two morphisms f, g: A → B are equal if and only if f and g have the same interpretation as cut-free proof nets.

This result is proved in [9], as part of a stronger theorem precisely characterizing those extensions of the theory of ∗-autonomous categories which satisfy such a criterion. (Among theories which satisfy this criterion is the theory of ∗-autonomous categories satisfying the MIX rule.) It allows us to interpret nets semantically. Thus, when we refer to the denotation of a proof, we mean the denotation of the corresponding net.

2.4 Simple Sequents

We here record some proof-theoretic results, due to Abramsky and Jagadeesan [2], which will be crucial in the sequel. We begin with some definitions.

Definition 2.5 A sequent ⊢ Γ is balanced if each atom occurs an even number of times, with proper variance. A balanced sequent is binary if each atom occurs exactly twice. It is simple if all of the formulas of Γ are literals or a tensor product of two literals.

A monotone context is a sequent with a “hole” (as in contexts for λ-calculus) such that the hole does not appear in the scope of a negation. Such contexts will be denoted Γ = D[·]

If a sequent is balanced, we can associate to it a cut-free proof structure. The fact that it is balanced allows us to establish axiom links, at which point the structure is uniquely determined, as previously remarked. If the sequent is binary, then there is a unique associated cut-free structure. Thus one can unambiguously ask whether a binary sequent is correct.

One of the crucial results of [2] simplifies the process of proving a full completeness theorem by allowing one to only consider the simple sequents:

Theorem 2.6 (Abramsky, Jagadeesan) Suppose ⊢ Γ is a binary sequent. Then there exists a finite list of binary simple sequents ⊢ Γ_{1}, …, ⊢ Γ_{n} such that:

• ⊢ Γ −∘ Γ_{i} is derivable for all i.

• ⊢ Γ is derivable if and only if, for all i, ⊢ Γ_{i} is.

To prove the result, we require two technical lemmas, both of which appear with proofs in [2].

Lemma 2.7 Let Γ = D[A ⊗ (B^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} C)] be a binary sequent. Let Γ_{1} = D[(A ⊗ B)^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} C] and Γ_{2} = D[(A ⊗ C)^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B]. Then we have:

• For all i = 1, 2 ⊢ Γ −∘ Γ_{i} is derivable.

• ⊢ Γ is derivable if and only if ⊢ Γ_{i} is derivable for i = 1, 2.

Lemma 2.8 Let Γ = D[A ⊗ (B ⊗ C)] be a binary sequent. Let Γ_{1} = D[A ⊗ (B^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} C)] and Γ_{2} = D[A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} (B ⊗ C)]. Then we have:

• For all i = 1, 2 ⊢ Γ −∘ Γ_{i} is derivable.

• ⊢ Γ is derivable if and only if ⊢ Γ_{i} is derivable for i = 1, 2.

The set of sequents mentioned in the above theorem is then obtained by using three canonical morphisms which exist in any model of MLL + MIX. These are the weak distributivity [13] and the MIX morphism [15]:

δ: A ⊗ (B^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} C)→(A ⊗ B)^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} C

δ′: A ⊗ (B^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} C)→(A ⊗ C)^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B

ξ: A ⊗ B→A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B

One now proves the theorem by using the first lemma to push a par down the proof structure so that it is the outermost connective of the formula it appears in. Then replace it with a comma.

Then given a nested occurrence of tensor, use the second lemma to replace it with a par. Then use the first lemma to eliminate it. Iteration of this process eventually leads to a finite family of simple binary sequents.

It is important to note that the set of simple sequents is obtained by left composition with the three canonical morphisms described above.

3 Logical Relations and Logical Permutations

Logical relations play an important role in the recent proof theory and semantics of typed lambda calculi [35, 39, 40, 43]. We begin with logical relations on Henkin models; for further developments see [5, 35, 37, 38].

3.1 Definitions and Examples

Consider a simply typed lambda calculus with product types. A Henkin model is a wellpointed cartesian closed category (ccc). Equivalently, a Henkin model is a type-indexed family of sets A = {A_{σ} | σ a type } where A_{1} = {∗}, A_{σ×τ} = A_{σ} × A_{τ}, A_{σ⇒τ} ⊆ A_{τ}^{A_{σ}} which forms a ccc with respect to restriction of the usual ccc structure of Set. In the case of atomic base types b, A_{b} is some fixed but arbitrary set.

Given two Henkin models A and B, a logical relation from A to B is a family of binary relations R = {R_{σ} ⊆ A_{σ} × B_{σ} | σ a type } satisfying:

1. R_{1}(∗, ∗)

2. (a, b)R_{σ×τ}(a′, b′) if and only if aR_{σ}a′ and bR_{τ}b′, for any a, a′ ∈ A_{σ}, b, b′ ∈ B_{τ}.

i.e. ordered pairs are related exactly when their components are.

3. For any f, g ∈ A_{σ⇒τ}, fR_{σ⇒τ} g if and only if for all a, a′ ∈ A_{σ} (aR_{σ}a′ implies fa R_{τ} ga′ ) i.e. functions are related when they map related inputs to related outputs.

For each (atomic) base type b, fix a binary relation R_{b} ⊆ A_{b} × B_{b} . Then: there is a smallest family of binary relations R = {R_{σ} ⊆ A_{σ} × B_{σ} | σ a type } defined inductively from the R_{b}’s by 1,2,3 above. That is, any property (relation) at base-types can be inductively lifted to a family R at all higher types, satisfying 1, 2, 3 above. If a, b ∈ A_{σ}, we write R(a, b) to denote R_{σ}(a, b). If R is a logical relation from A to itself, we say an element a is invariant under R if R(a, a).

The fundamental property of logical relations is the Soundness Theorem. Let M(x⃗) : σ denote a term M of type σ with free variables (i.e. in context) x⃗ : Γ, sometimes denoted x⃗ : Γ ▷ M : σ. Consider Henkin models A, B, with assignments for variables η_{A}, η_{B} in the respective models. Let M _{η_{A}} denote the meaning of M in model A w.r.t. the given variable assignment.

Theorem 3.1 ([39, 43, 35]) Let R ⊆ A × B be a logical relation between Henkin models A, B . Let x⃗ : Γ ▷ M : σ. Suppose the interpretations of the free variables are related, i.e. for all i, R(η_{A}(x_{i}), η_{B}(x_{i})). Then R( M _{η_{A}}, M _{η_{B}}).

In particular, if A = B and M is a closed term (i.e. contains no free variables), its meaning M in a model A is invariant under all logical relations.

This observation has been used by Plotkin, Statman, et. al [39, 43, 44] to show certain elements (of models) are not lambda definable: it suffices to find some logical relation on A for which the element in question is not invariant.

An important special case for us is the following example:

Example 3.2 Consider a Henkin model A, with a specified permutation π_{b} : A_{b} → A_{b} at each base type b. We extend π to all types as follows: (i) on product types we extend componentwise: π_{σ×τ} = π_{σ} × π_{τ} : A_{σ×τ} → A_{σ×τ} ; (ii) on function spaces, extend by conjugation: π_{σ⇒τ}(f) = π_{τ}^{o}f^{o}π_{σ}^{−1} , where f ∈ A_{σ⇒τ}. We build a logical relation R on A by letting R_{σ} = the graph of permutation π_{σ} : A_{σ} → A_{σ}, i.e. R_{σ}(a, b) ⇔ π_{σ}(a) = b. Members of R will be called hereditary permutations. R−invariant elements a ∈ A_{σ} are simply fixed points of the permutation: π_{σ}(a) = a. Further discussion of this example is in the next section.

There is no reason to restrict ourselves to binary logical relations: one may speak of n-ary logical relations, which relate n Henkin models [43]. Indeed, since Henkin models are closed under products, it suffices to consider unary logical relations, known as logical predicates.

3.2 Soundness

The original use of unary logical relations stemmed from Tait’s computability predicates in proof theory [21]. Unfortunately, our previous definition of logical relations, based on Henkin models, does not directly apply to the syntax, since syntactic term models are not always Henkin models (cf. [29] p. 263, Corollary 2.12). Statman [43] and Mitchell [35] extended the notion of logical relation to certain applicative typed structures A for which (i) appropriate meaning functions on the syntax, M _{η_{A}}, are well-defined, and (ii) all logical relations R are (in a suitable sense) congruence relations on the syntax. Following [35] we call them admissible logical relations. In this situation, the Soundness Theorem above is still valid:

Theorem 3.3 (Soundness) Let {A_{i}}_{i≤n} be a family of typed applicative structures. Let x⃗ : Γ▷M : σ and suppose M _{η_{A_{i}}} is a well-defined meaning function which interprets term M in A_{i} with respect to variable assignment η_{A_{i}}. Suppose R ⊆ Π_{i≤n}A_{i} is an n-ary admissible logical relation . If the interpretations of the variables are all related, i.e. for all variables x_{i}, R(η_{A_{1}}(x_{i}), …, η_{A_{j}}(x_{i}), … η_{A_{n}}(x_{i})), then R( M _{η_{A_{1}}}, …, M _{η_{A_{j}}} , …, M _{η_{An}}).

As pointed out by Mitchell [35] and Statman [43] this permits obtaining many interesting soundness theorems for the syntax. For example, let A be a term model for the lambda theory T . To apply the previous discussion, note that the usual (Tarski) interpretation of a term M, M _{η_{A}}, is a well-defined meaning function in our previous sense. For example, letting η be the identity, M _{η_{A}} simply refers to the type assignment x⃗ : Γ ▷ M : σ, while the satisfaction relation A ⊧_{η} M = N : σ means “provable equality in theory T ”.

Corollary 3.4 (“All terms are computable”.) Let T be the pure theory of simply typed λcalculus. Suppose B is an applicative typed structure, and R is an admissible logical predicate on B. Then for any term x⃗ : Γ ▷ M : σ and variable assignment η_{B}, R( M _{η_{B}}).

This corollary may be extended to applied lambda theories with additional constants, base types, type- and/or term-constructors, etc. by appropriate modifications to the notion of structure and interpretation. Indeed, as a special case of the above result, let B be the term model for typed lambda calculus, and R be Tait’s computability predicates ([21], Chapter 6); we obtain Tait’s Soundness Theorem ([21], p. 46). As another special case, let B be a Henkin model and let R be the hereditary permutations on B, starting from some basic types. Then the above corollary says: the meaning of any term is invariant under all hereditary permutations.

The above corollary is itself a consequence of the usual universal property of free cartesian closed categories: any interpretation of the nodes of a (discrete) graph G into a ccc E has a unique extension to an E-valued representation of the free ccc generated G. We may then pick E to be an appropriate category of logical relations [37]. For example, in the next section, we discuss Läuchli’s semantics, in which we pick E = Set^{G}, the category of G-sets.

4 Läuchli Semantics

4.1 G-Sets

Definition 4.1 Let G be a group and X a set. A G-set X, or a left action of G on X, is a group homomorphism G → Sym(X) to the symmetric group on X. Equivalently, a G-set is a pair (X,.) where . : G × X → X is a map satisfying, for all g_{i} ∈ G, x ∈ X,

(g_{1}g_{2}).x = g_{1}.(g_{2}.x)
1.x = x

A G-set morphism from (X,._{X}) to (Y,._{Y}) is a function ϕ : X → Y preserving the actions, i.e. ϕ(g.x) = g.ϕ(x) (we omit indexing the actions). Such maps are sometimes called equivariant maps.

Theorem 4.2 The category Set^{G}, the category of G-sets and G-set morphisms is a cartesian closed category (= ccc) [29].

Proof. The ccc structure is as follows:

Terminal object: any one point set, with trivial action.

Products of G-sets : given two G-Sets X, Y their product is the cartesian product X × Y with pointwise action. Exponentials of G-sets : given two G-Sets X, Y their exponential (function space) Y^{X} is given by the ordinary set-theoretic function space, with “conjugate” or “contragredient” action: for any g ∈ G, h ∈ Y^{X}, (g.h)(x) = g.h(g^{−1}.x) □

In the above proof, we see two important examples of group actions: (i). the trivial or discrete action given by second projection: g.x = x, for all g ∈ G, x ∈ X and (ii). the historically important case of a group G acting on itself by conjugation. We will be primarily interested in the case where G = Z, the additive group of integers. In this case, we have the following equivalence of categories, which follows from the fact that Z is the free cyclic group.

Theorem 4.3 The category of Z-sets is equivalent to the category whose objects are sets equipped with a permutation and whose maps are set-theoretic maps commuting with the distinguished permutations.

Thus maps which commute with the given permutations are frequently called equivariant maps, while a Z-set with trivial action corresponds to a set with the identity permutation.

The notions of hereditary permutations and soundness may be usefully understood from the above viewpoint [29, 23]. Let G be a set, considered as a discrete graph, and consider ⟨G⟩ = the free ccc generated by G. Let G be any group, and consider the topos of left G-sets Sets^{G}, a Henkin model. The universal property of ⟨G⟩ implies the following: for any graph morphism F : G → Set^{G}, there is a unique extension to a ccc-functor − _{F} : ⟨G⟩ → Set^{G}.

⟨G⟩ \overline{− _{F}_{}}Set^{G}
[figure: F]
G^{}

In other words, given any interpretation F of basic atomic types (= nodes of G) as Gsets, there is a unique extension to a G-set interpretation − _{F} of the entire typed lambda calculus generated by G, modulo β, η, and product equations (this is the free ccc ⟨G⟩).

In particular, by the Curry-Howard correspondence, lambda terms (which denote proofs) are interpreted as G-set morphisms, i.e. equivariant maps. That is, let F be an initial assignment of G-sets to atomic types. Then a closed term M : σ, qua proof of formula σ, qua ⟨G⟩-arrow M : 1 → σ, corresponds to a G-set map M _{F} : 1 → σ _{F} . Such maps are fixed points under the action. In particular, letting G = Z, we obtain the notion of hereditary permutation, and the associated Soundness Theorem. In terms of provability it says: A formula σ of intuitionistic propositional calculus is provable only if for every F, its Set^{Z}-interpretation σ _{F} has an invariant element.

4.2 Läuchli’s Theorem

In fact, the above viewpoint extends to the language {⊤, ∧, ⇒, ∨}^{1}. Consider B(G), the free ccc with binary coproducts generated by G. Sets^{G} has coproducts, so there is a unique extension of the interpretation of the base types to a structure-preserving functor

− _{F} : B(G) → Set^{G}

hence the meaning map − interprets {⊤, ∧, ⇒, ∨}-proofs via hereditary permutations: a closed term M : 1 → σ corresponds to an invariant lambda term in Sets^{G} (now for the extended lambda calculus with binary coproduct types.) This is the viewpoint of Läuchli [30]. The Läuchli Completeness Theorem is a converse to Soundness, for the case G = Z:

Theorem 4.4 (Lauchli [30]) A formula σ of intuitionistic propositional calculus is provable if and only if for every interpretation F of the base types, its Set^{Z}-interpretation σ _{F} has an invariant element.

Indeed, Harnik and Makkai extend Läuchli’s theorem to a representation theorem. Recall, a functor Φ is weakly full if Hom(A, B) being empty implies Hom(Φ(A), Φ(B)) is empty.

Theorem 4.5 (Harnik, Makkai [23]) Let A be a countable free ccc with binary coproducts. There is a weakly full representation of A into a countable power of Set^{Z}. If in addition A has the disjunction property, there is a weakly full representation into Set^{Z}.

1As emphasized in [30, 23], we ignore ⊥ in what follows, i.e. only consider non-trivial coproducts.

Letting A = ⊤, i.e. the terminal object, we see the existence of such a weakly full representation of A corresponds to completeness with respect to provability: i.e. Hom_{Set^{Z}}(⊤, Φ(B)) nonempty implies Hom_{A}(⊤, B) non-empty, so B is provable.

We are interested in full completeness theorems–i.e. completeness with respect to proofs (not just non-emptiness of the hom-sets). This is connected with fullness of the functor − _{F} above. In the case of simply typed lambda calculus generated from a fixed base type (= the free ccc on one object), Plotkin proved the following related result. Consider the Henkin model T_{B} = the full type hierarchy over a set B, i.e. the full sub-ccc of Sets generated by some set B. Thus in T_{B} we have B_{σ⇒τ} = B_{σ} ⇒ B_{τ} , the full function space. Recall ([39]) the rank of a type is defined inductively: rank(b) = 0 , where b is a base type, rank(σ ⇒ τ) = max { rank(σ) + 1, rank(τ)}, rank(σ × τ) = max { rank(σ), rank(τ)}. The rank of an element f ∈ B_{σ} in T_{B} is the rank of the type σ.

Theorem 4.6 (Plotkin, [39]) In the full type hierarchy T_{B} over an infinite set B, all elements f of rank ≤ 2 satisfy: if f is invariant under all logical relations, then f is lambda definable.

This result has been extended and discussed by Statman [43], but the same question for terms of arbitrary rank is still open. However Plotkin [39] did prove the above result for lambda terms of arbitrary rank, by moving to the category of Kripke Logical Relations rather than Set-based logical relations. For a categorical reformulation, in terms of toposes of the form Sets^{P}, P a poset, see [36, 37].

Finally, we also mention recent work of R. Loader [32]. Loader proves the undecidability of the Plotkin-Statman problem: in any model of simply typed lambda calculus over a finite base type, is it decidable whether a function is lambda definable or not? In particular, as pointed out in the Appendix to [32], this undecidability result actually implies that Plotkin’s theorem is false over finite base types: logical relations fail to characterize lambda definability (in terms of invariance) on T_{B}, for B finite.

Interestingly, a similar problem occurs if we restrict our semantics to finite dimensions: our Completeness and Full Completeness results for MLL depend crucially on having infinite dimensional spaces.

5 ∗-Autonomous Categories and Vector Spaces

Since the category of G-sets is cartesian closed, it provides a model of intuitionistic logic. To model linear logic, it is natural to replace sets with vector spaces. This leads to the classical subject of group representation theory as described for example in [18]. However, we must build a ∗-autonomous category of vector spaces, in order to be able to model the involutive negation of classical linear logic.

Recall that a symmetric monoidal closed category is ∗-autonomous if, for all objects V, the canonical morphism μ: V →(V −∘⊥) −∘⊥ is an isomorphism. Here ⊥ is a fixed object, called the dualizing object. In our example, the dualizing object will be the base field. In an arbitrary symmetric monoidal closed category, objects for which μ is an isomorphism are called reflexive, or more precisely reflexive with respect to ⊥.

5.1 Linear Topology

The approach we use goes back to the work of Lefschetz [31], and has been studied by Barr [6] and the first author [10]. The idea is to add to the linear structure an additional topological structure, and then define the dual space to be the linear continuous maps. This serves to decrease the size of the dual space and thus create a large class of reflexive objects, i.e. objects which are canonically isomorphic to their second dual. The categorical structure so arising was studied by Barr in [6], where he shows that the resulting category is ∗-autonomous. In [10], the first author examines this category as a model of linear logic, and considers the representations of groups and Hopf algebras in such spaces. This theory leads to a large class of new models of commutative linear logic [19], noncommutative linear logic [4, 28], and braided linear logic [11]. Proofs of all of the following results can be found in [6] and [10].

Definition 5.1 Let V be a vector space over a discrete field k. A topology, τ, on V is linear if it satisfies the following three properties:

• Addition and scalar multiplication are continuous, when the field k is given the discrete topology.

• τ is hausdorff.

• 0 ∈ V has a neighborhood basis of open linear subspaces.

The first requirement means that we have a topological vector space in the sense of [24] (except that most texts take the field to be the real or complex numbers with its usual topology). The third requirement is quite stringent. For example, it implies that the only linear topology on a finite dimensional vector space is the discrete topology.

Let T VEC denote the category whose objects are vector spaces equipped with linear topologies, and whose maps are linear continuous morphisms.

The vector space V −∘_{LT} W of linear continuous maps is endowed with the topology of pointwise convergence, i.e. as a subspace of the cartesian product W^{V}. Given this, the tensor product can be endowed with a linear topology to obtain an autonomous category. The next theorem follows from an application of the special adjoint functor theorem. Here the base field acts as cogenerator.

Theorem 5.2 (Barr) Given V in T VEC, the functor V −∘_{LT} − has a left adjoint, denoted − ⊗_{LT} V.

Corollary 5.3 (Barr) T VEC is an autonomous (symmetric monoidal closed) category.

It is important to note that while the monoidal structure exists for abstract reasons, it is possible to prove that the underlying vector space of V ⊗_{LT} W is the usual algebraic tensor product. This issue is discussed in Barr’s note [8], which is an appendix to [10].

We now define duality for this category. Given an object V in T VEC we define V^{⊥} to be V −∘_{LT} k where the base field k is topologized discretely. Lefschetz proves:

Theorem 5.4 (Lefschetz) The map μ: V → V^{⊥⊥} is a bijection, for all V.

Thus linear topology has served to decrease the size of the second dual space to the correct extent. While this map is a bijection, it need not be an isomorphism as the inverse map may not be continuous. Barr gives a characterization of the reflexive objects:

Theorem 5.5 (Barr) A space is reflexive if and only if every discrete linear subspace is finite dimensional.

Definition 5.6 Let RT VEC denote the full subcategory of reflexive objects.

The fundamental result is:

Theorem 5.7 (Barr) RT VEC is a ∗-autonomous category.

The proof of this theorem follows from two lemmas.

Lemma 5.8 For any V in T VEC, the space V^{⊥} is reflexive.

Lemma 5.9 The inclusion RT VEC ↪ T VEC has a left adjoint (−)^{⊥⊥}: T VEC → RT VEC.

Intuitively, the adjoint (−)^{⊥⊥} is adjusting the topology to make the inverse of μ continuous. Note that the tensor product in RT VEC of two objects, V and W, is given by (V ⊗ W)^{⊥⊥}.

Thus RT VEC provides a model of multiplicative linear logic. While the category of finitedimensional spaces is also ∗-autonomous, RT VEC provides a richer model since it does not equate the two multiplicative connectives, ⊗ and ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} . It is well known that if V and W are finite dimensional spaces, we have an isomorphism:

(V ⊗ W)^{⊥} ≅ V^{⊥} ⊗ W^{⊥}

Thus we cannot hope for any kind of completeness theorem. RT VEC does not satisfy such an identity. This point is discussed in [10].

5.2 Quotients and Direct Sums

We now discuss quotients and direct sums of topological vector spaces. More complete discussions can be found in [24] and [41]. Given a topological vector space V and an arbitrary linear subspace U, it is readily seen that the quotient topology on the quotient space V/U gives a topological vector space. It is not generally the case however that when an object of T VEC is quotiented by an arbitrary subspace that we get an object of T VEC. This is seen by the following lemma, which is proved in the above two references.

Lemma 5.10 The quotient space V/U is hausdorff if and only if U is closed.

We also observe that if U is an open linear subspace, then V/U will be discrete. This leads to the following standard result.

Lemma 5.11 An open linear subspace is also closed.

We now wish to consider direct sums. In particular, for (non-topological) vector spaces, we have the following canonical isomorphism:

V ≅ V/U ⊕ U

To what extent, does this hold topologically, or more precisely, does V have the product topology in the above expression? We have the following definition:

Definition 5.12 Let V be a topological vector space, which algebraically is the direct sum V ≅ M ⊕ N. We say that V is the topological direct sum of M and N if the linear map

ϱ: M × N→V

is an isomorphism of topological vector spaces. Here, M × N has the product topology.

Note that if we quotient an object of T VEC by a nonclosed subspace, then clearly the above isomorphism is not a topological direct sum.

We have the following result, proved in [24] and [41]:

Lemma 5.13 If V is the algebraic direct sum of M and N, then V is their topological direct sum if and only if the canonical projections onto M and N are continuous. (Here we mean projections in the sense of linear algebra, a morphism from V to V projecting onto the M (or N) component).

Finally, we will need the following lemma:

Lemma 5.14 Let V be an object of T VEC, and U an open linear subspace. Then V is the topological direct sum:

V ≅ V/U ⊕ U

Proof. The morphism p_{1} : V →V/U is continuous, since this is the quotient map. Now for any vector space, this map splits, and the splitting is continuous, as V/U is discrete. This induces a continuous endomorphism of V, call it q, which is the projection onto the V/U component. Then the other projection onto U is also continuous as it can be defined as 1_{V} − q. □

This particular lemma will be quite important in what follows. When defining actions on RT VEC, one must always make sure they are continuous. Given any point in V, one can find an open linear subspace not containing the point. This follows from the definition of linear topology. The quotient will be discrete, so continuity is automatic on this factor of the direct sum. Since the above composition is a topological direct sum, it is possible to define an action on V componentwise.

6 Representations of Groups

We will first consider representations of groups in discrete spaces.

Definition 6.1 Let G be a group and V a vector space. A representation of G on V is given by a group homomorphism ϱ : G → Aut(V), the group of linear automorphisms of V. Equivalently, a G-module is a vector space V equipped with a linear automorphism v ↦ g.v for each g ∈ G. These automorphisms must satisfy the obvious analogue of the equations of a G-set. Let MOD(G) denote the category of G-modules with linear maps commuting with the G-action as morphisms.

6.1 Z-Actions

The group we are primarily interested in is the additive group of integers Z, which can act on a complex vector space V in many ways; we shall give some useful examples.

Examples 6.2 The following are actions of Z on V:

1. For each nonzero complex number p define the action n.v = p^{n}v, for all v ∈ V. These are sometimes called “p-actions”.

2. Suppose V = C[Z], the complex vector space generated by the elements of Z. Thus V has as basis {e_{i}}_{i∈Z}. For each basis vector e_{i}, define the action n.e_{i} = e_{i+n} .

3. More generally, for any space V with basis {e_{i}}_{i∈I}, choose any permutation σ of the set I, and define an action by n.e_{i} = e_{σ^{n}(i)}.

Of course, these actions can be combined in various ways using direct sums and tensor products.

6.2 Symmetric Monoidal Closed Structure

The category MOD(G) has the appropriate structure to model intuitionistic multiplicative linear logic.

Theorem 6.3 For any group G, the category MOD(G) is symmetric monoidal closed.

Proof. If V and W are G-modules, we define a G-action on V ⊗ W by

g.(v ⊗ w) = g.v ⊗ g.w (1)

The exponential, V −∘ W in this category is the space of all k-linear maps from V to W with action defined by:

(g.f)(v) = g.f(g^{−1}.v) (2)

□

Equation 2 is generally refered to as the contragredient representation [18]. Note the obvious similarity to the structure of the category of G-sets (cf. Theorem 4.2).

To model the involutive negation of classical linear logic, we must consider representations of groups in RT VEC.

Definition 6.4 Let G be a group. A continuous G-module is a linear action of G on a space V in T VEC, such that for all g ∈ G, the induced map g.( ) : V → V is continuous. Let T MOD(G) denote the category of continuous G-modules and continuous equivariant maps. Let RT MOD(G) denote the full subcategory of reflexive objects.

We have the following result, which in fact holds in the more general context of Hopf algebras [10].

Theorem 6.5 The category T MOD(G) is symmetric monoidal closed. The category RT MOD(G) is ∗-autonomous, and a reflective subcategory of T MOD(G) via the functor ( )^{⊥⊥}. Furthermore the forgetful functor to RT VEC preserves the ∗-autonomous structure.

7 Functorial Polymorphism

We shall give a further development of the theory of Functorial Polymorphism applied to linear logic, following [5, 9, 22]. For other developments of the general theory, cf [16, 17]. Recall that in functorial polymorphism, the types of a λ-calculus are interpreted directly as certain multivariant functors, while terms are an appropriate multivariant version of natural transformation known as a dinatural transformation:

Definition 7.1 Let C be a category, and F, G : C^{op} × C → C functors. A dinatural transformation is a family of C-morphisms θ = {θ_{A} : F AA → GAA | A ∈ C} satisfying (for any f : A → B):

F AA  \overline{θ_{A}  ^{}}GAA
[figure: F fA; GAf]
F BA  GAB
[figure: F Bf; GfB]
F BB  \overline{θ_{B}  ^{}}GBB

More generally, we can consider multivariant functors F, G : (C^{op})^{n} × C^{n} → C , where n ≥ 1, and dinatural transformations between them. In this case, then A and B above denote vectors of objects and f denotes a vector of morphisms.

Denote dinatural transformations by θ : F ⟶^{..} G.

A fundamental difficulty is that dinatural transformations do not generally compose [5]; however, in certain known cases they do. When composition is well-defined, the dinatural calculus permits interesting “parametric” interpretations of the relevant lambda calculus (cf. [40]).

For example:

1. In [5] it was shown that certain uniform dinaturals between “logically definable” functors over Per (the category of partial equivalence relations on the natural numbers) do compose. In this case, one obtains a parametric model of Girard’s second order lambda calculus, system F.

2. Also, in the case of logical syntax, for certain freely generated categories and “logically definable” functors, there is a notion of uniform dinatural transformation, for which again composition is well-defined. More specifically, one shows that the interpretations of cut-free proofs yield dinatural transformations. This is done by induction on the complexity of the derivation. Compositionality then follows by cut-elimination. This approach was applied to simply typed lambda calculus in [22] and to linear logic in [9].

In this paper we shall develop another notion of uniformity, in this case for certain dinatural transformations on a category of vector spaces. Again we shall show compositionality of uniform dinaturals between appropriate definable functors as a consequence of a more general “Full Completeness Theorem” below.

7.1 Interpreting ⊗, −∘

We shall first work in the theory of symmetric monoidal closed (= smc) categories without units, equivalently in intuitionistic MLL without units [20, 9]. Thus formulas are built from atoms, using the connectives ⊗, −∘. Following the lead of functorial polymorphism (loc cit), we interpret formulas as multivariant functors over an smc category C, using the following functorial operations on n-ary multivariant functors F, G : (C^{op})^{n} × C^{n} → C:

(3)  (F ⊗ G)(AB) ≡ F (AB) ⊗ G(AB)
(4)  (F −∘ G)(AB) ≡ F (BA) −∘ G(AB)

Here AB ∈ (C^{op})^{n} × C^{n} denotes an object consisting of a vector of n contravariant variables A and n covariant variables B. Note the “twisted” order of arguments in exponentiation. The operations F ⊗ G and F −∘ G again yield n-ary multivariant functors.

Formulas are interpreted functorially: associated to each formula ϕ(α_{1}, …, α_{n}), with type variables (or atoms) α_{1}, …, α_{n}, its interpretation ϕ(α_{1}, …, α_{n}) : (C^{op})^{n} × C^{n} → C is given as follows:

1. If ϕ(α_{1}, …, α_{n}) ≡ α_{i}, then ϕ (AB) = B_{i}, the (covariant) projection functor onto the i-th component of B. We denote this i-th covariant projection functor by Π_{i}

2. If ϕ = c, a constant interpreted as an object of C, then ϕ = K_{c}, the constant multivariant functor with value c.

3. If ϕ = ϕ_{1} ⊗ ϕ_{2}, then ϕ = ϕ_{1} ⊗ ϕ_{2} .

4. If ϕ = ϕ_{1} −∘ ϕ_{2}, then ϕ_{1} −∘ ϕ_{2} = ϕ_{1} −∘ ϕ_{2} .

Thus formulas are thought of as schemas with n slots (atoms) into which other formulas can be plugged.

Similarly, a sequent between formulas with n atoms

σ_{1}, …, σ_{k} ⊢ τ

is interpreted as a dinatural transformation between n-ary multivariant functors. Indeed, letting the atoms be α_{1}, …, α_{n} and σ_{i}(α_{1}, …, α_{n}) = F_{i} : (C^{op})^{n} × C^{n} → C and τ(α_{1}, …, α_{n}) = G : (C^{op})^{n} × C^{n} → C then the sequent σ_{1}, …, σ_{k} ⊢ τ interprets as a dinatural transformation θ : F_{1} ⊗ … ⊗ F_{k} ⟶^{..} G.

Example 7.2 The above inductive definitions yield the following:

1. The axiom sequent α ⊢ α is interpreted as a dinatural transformation σ : Π_{1} ⟶^{..} Π_{1} : C^{op}×C → C, where Π_{1}AB = B is the (covariant) projection. Thus (letting σ_{A} =_{def} σ_{AA}) we have a family of maps

σ_{A} : Π_{1}AA → Π_{1}AA ≡ σ_{A} : A → A.

One such dinatural family is given by choosing each σ_{A} to be the identity on A. We call this the identity dinatural. Since the sequent α ⊢ α is actually provable, this identity dinatural is the “standard” interpretation, cf.[22].

More generally, note that any dinatural transformation σ : Π_{1} ⟶^{..} Π_{1} : C^{op} × C → C must satisfy the following square (= degenerate hexagon); for any f : A → B

A  \overline{σ_{A}  ^{}}A
[figure: id; f]
A  B
[figure: f; id]
B  \overline{σ_{B}  ^{}}B

That is, σ_{B}^{o}f = f^{o}σ_{A} .

2. Given the sequent α −∘ β ⊢ α −∘ β, its dinatural interpretation is in general of the form F ⟶^{..} F : (C^{op})^{2} × C^{2} → C, where F = α −∘ β = Π_{1} −∘ Π_{2}, with Π_{i} = the projection onto the ith covariant variable (i = 1, 2). Thus (using semicolon to separate contravariant and covariant variables),

F (AA′; BB′) = Π_{1}(BB′; AA′) −∘ Π_{2}(AA′; BB′) = A −∘ B′.

Any dinatural θ = {θ_{AA′} : F (AA′; AA′) → F (AA′; AA′) |(A, A′) ∈ B^{2} } interpreting this sequent must satisfy the following hexagon, for f : B → A and g : B′ → A′:

A −∘ A′  \overline{θ_{AA′}  ^{}}A −∘ A′
[figure: A −∘ g; f −∘ A′]
A −∘ B′  B −∘ A′
[figure: f −∘ B′; B −∘ g]
B −∘ B′  \overline{θ_{BB′}  ^{}}B −∘ B′

For example, in the above case we could pick the identity dinatural, i.e. each component θ_{AA′} would be the identity.

3. The derivable sequent α, α −∘ β ⊢ β interprets as a dinatural

ev : F ⟶^{..} G : (C^{op})^{2} × C^{2} → C

where F = (α −∘ β) ⊗ α = Π_{1} ⊗ (Π_{1} −∘ Π_{2}), and G = β = Π_{2} . Thus (using semicolon to separate contravariant and covariant variables),

F (BB′; AA′) = Π_{1}(BB′; AA′) ⊗ (Π_{1}(AA′; BB′) −∘ Π_{2}(BB′; AA′))
= A ⊗ (B −∘ A′)
G(AA′; BB′) = Π_{2}(AA′; BB′) = B′.

The dinatural

ev = {ev_{AA′} : F (AA′; AA′) → G(AA′; AA′) |(A, A′) ∈ C^{2} }

must satisfy the following hexagon, for f : A → B and f′ : A′ → B′:

A ⊗ (A −∘ A′) \overline{ev_{AA′}  ^{}}A′
[figure: A × (f −∘ A′); f′]
A ⊗ (B −∘ A′)  B′
[figure: f ⊗ (B −∘ f′); B′]
B ⊗ (B −∘ B′) \overline{ev_{BB′}  ^{}}B′

We refer to ev as the evaluation dinatural. Of course, in the canonical syntactic interpretation [22], as well as in many concrete monoidal closed categories, ev refers to the evaluation map: ev_{AA′}(a ⊗ u) = u(a). In such concrete categories, the hexagon above translates into the following equation: for any a ⊗ g ∈ A ⊗ (B −∘ A′)

f′(ev_{AA′}(a ⊗ g^{o}f)) = ev_{BB′}(f(a) ⊗ f′^{o}g) (5)

A generalization of this example to nested evaluations is in Lemma 10.2 below.

7.2 Interpreting MLL Sequents

Functorial polymorphism can be extended to handle Barr’s ∗-autonomous categories [7], i.e. smc categories C equipped with an involution functor ( )^{⊥} : C^{op} → C given by a dualising object. Such categories interpret the multiplicative fragment of classical linear logic [42, 9].

We modify the functorial interpretation of formulas mentioned earlier to the ⊗, ( )^{⊥} fragment of classical linear logic by modifying the interpretation of atomic clauses. Thus associated to each formula ϕ(α_{1}, …, α_{n}) in ⊗, −∘, ( )^{⊥} , with type variables (or atoms) α_{1}, …, α_{n}, we inductively define its interpretation ϕ(α_{1}, …, α_{n}) : (C^{op})^{n} × C^{n} → C by changing the previous interpretation to:

• If ϕ(α_{1}, …, α_{n}) ≡ α_{i}, then ϕ (AB) = B_{i} , the (covariant) projection onto the ith component of B.

• If ϕ(α_{1}, …, α_{n}) ≡ α_{i}^{⊥}, then ϕ (AB) = A_{i}^{⊥} , the linear negation of the (contravariant) projection onto the ith component of A, denoted Π_{i}^{⊥}

• ⊗ is interpreted as before.

Remember that in MLL, A −∘ B is defined as A^{⊥}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B

Example 7.3 The above inductive definition yields the following:

1. The underivable sequent α −∘ β ⊢ α^{⊥} ⊗ β interprets as a dinatural

θ : F ⟶^{..} G : (C^{op})^{2} × C^{2} → C

where F = α −∘ β = Π_{1} −∘ Π_{2}, and G = α^{⊥} ⊗ β = Π_{1}^{⊥} ⊗ Π_{2} . Here Π_{i} denotes the projection onto the ith covariant variable and Π_{i}^{⊥} denotes the linear negation of the projection onto the ith contravariant variable (i = 1, 2). Thus (using semicolon to separate contravariant and covariant variables),

F (BB′; AA′) = Π_{1}(AA′; BB′) −∘ Π_{2}(BB′; AA′) = B −∘ A′
G(AA′; BB′) = Π_{1}^{⊥}(AA′; BB′) ⊗ Π_{2}(AA′; BB′) = A^{⊥} ⊗ B′.

Any dinatural θ = {θ_{BB′} : F (BB′; BB′) → G(BB′; BB′) |(B, B′) ∈ A^{2} } must satisfy the following hexagon, for f : A → B and g : A′ → B′:

B −∘ B′  \overline{θ_{BB′}  ^{}}B^{⊥} ⊗ B′
[figure: B −∘ g; f^{⊥} ⊗ B′]
B −∘ A′  A^{⊥} ⊗ B′
[figure: f −∘ A′; A ⊗ g]
A −∘ A′  θ_{AA′}  ^{}A^{⊥} ⊗ A′

Remark 7.4 Although dinatural transformations do not compose in general, we note that the composition of a dinatural with a natural transformation does yield a well-defined dinatural transformation (cf. Remark 9.6 below). We shall use this observation later.

Remark 7.5 We end with some notation. Let θ : F ⟶^{..} G : (C^{op})^{n} ×C^{n} → C be a dinatural, with components schematically denoted θα⃗ : F (α⃗; α⃗) → G(α⃗; α⃗), with a semicolon separating the contravariant from the co-variant occurrences of variables. Here α⃗ = (α_{1}, …, α_{n}) are formal variables referring to the n contravariant and n covariant slots in the functors F and G. A genuine component of θ, say θ_{A} : F (A; A) → G(A; A), where A = (A_{1}, …, A_{n}) ∈ C^{n}, is also called an instantiation of θ at A. Such an instantiation arises as a formal simultaneous substitution of A_{i} for α_{i} into the schema θα⃗ . We sometimes denote functors and dinaturals schematically, using variables, as in the above interpretation of MLL sequents. We usually omit the semicolon separating contravariant and covariant slots.

8 Dinaturals on Vector Spaces

8.1 Uniform Dinaturals

The theory of uniform dinaturals is motivated by the following elementary observation. Let MOD(G) be the associated category of modules of a group G. MOD(G) is autonomous, and moreover the forgetful functor

| | : MOD(G) → V ec

is an autonomous functor. An analogous result holds when vector spaces are replaced with spaces equipped with a linear topology, when we instead use the forgetful functor:

| | : RT MOD(G)→RT VEC

Definition 8.1 Let F and F′ be definable functors on RT VEC. A dinatural transformation θ: F →F′ is uniform for a group G if for every V_{1}, …, V_{n} ∈ RT MOD(G), the morphism θ_{|V_{1}|,...,|V_{n}|} is a G-map, i.e. is equivariant with respect to the actions induced (by equations 1,2) from the atoms V_{i}.

In the above definition, the instantiation of the dinatural, θ_{|V_{1}|,...,|V_{n}|}, is certainly a continuous map of topological vector spaces, but there is no a priori reason why it should also be equivariant on the action induced by the actions on the atoms. This is what uniformity requires.

Remark 8.2 We here make some elementary observations that we will need in the sequel.

• Any action on a function space V −∘ V which is induced by an action of V will preserve the identity element.

• By the definition of equivariance, if an element of the domain is fixed under the action induced by the atoms, then it must be mapped to a fixed point.

8.2 Linear Structure of Uniform Dinaturals

We use the following notation: suppose given definable functors F, F′ : (V ec^{op})^{n} × V ec^{n} ⟶ V ec,

(i) Dinat(F, F′) = the set of dinatural transformations from F to F′. (ii) G−Dinat(F, F′) = the set of dinatural transformations from F to F′ which are uniform

for the group G

Proposition 8.3 Dinat(F, F′) is a vector space under pointwise operations. Moreover, for each group G, G−Dinat(F, F′) is a subspace of Dinat(F, F′).

We refer to the elements of G−Dinat(F, F′) as G-uniform dinatural transformations. By analogy to Läuchli semantics, the special case we are interested in is when G = Z, the additive group of integers. We call Z−Dinat(F, F′) the space of proofs associated to the sequent M ⊢ M′, where M = F and M′ = F′. This terminology will be motivated by the full completeness theorem below. In the sequel, we will frequently allow formulas to denote their own interpretation. For example, above we might write Z−Dinat(M, M′).

9 Completeness

We begin by establishing a traditional completeness theorem, which is a direct analogue of the original Läuchli result. Recall that to a binary balanced sequent, we can assign a unique cut-free proof structure. The completeness theorem says that if that proof structure is not a net, then there are no nonzero “abstract proofs”.

Theorem 9.1 (Completeness) Let M ⊢ N be a balanced binary sequent. If the unique cut-free proof structure associated to M ⊢ N is not a proof net for the theory MLL + MIX, then Z − Dinat(M, N) is a zero dimensional vector space.

The following lemma will be crucial in establishing completeness.

Lemma 9.2 Let V be an infinite dimensional object in RT VEC, and let v ≠ 0 be an element of V ⊗ V^{⊥}. Then there exists a Z-action on V such that v is not fixed by the induced action on V ⊗ V^{⊥}.

Proof. Begin by choosing a basis for V, say {e_{i}}_{i∈I}, and a dual basis for V^{⊥}, say {f^{j}}_{j∈J}. Now let v = Σr_{ij}e_{i} ⊗ f^{j}. Note that this is a finite sum. Suppose without loss of generality that e_{1}, e_{2}, …, e_{n} are the n basis vectors appearing in v. Finally, let e_{n+1} be a basis vector not appearing in the list, and set L equal to the list e_{1}, …, e_{n+1}.

Now we must construct U, an open linear subspace of V, such that the images of the elements of L remain linearly independent in V/U. For each e_{i} in L, one can find a U_{i}, an open linear subspace not containing e_{i}. Begin by setting U = U_{1} ∩ U_{2} ∩ … ∩ U_{n+1}. This will not be the final U. Now choose any pair of elements of L, say e_{i} and e_{j}. The subspace U may contain a nonzero element of the form u = r_{i}e_{i} + r_{j}e_{j}. If so, then any other such element must be a scalar multiple of this one. Otherwise e_{i} or e_{j} would be in U. Now find an open linear subspace not containing u and “update” U by intersecting it with this space. Now repeat this procedure for all pairs of basis elements. This establishes pairwise linear independence. Now proceed as above for all 3-tuples, and so on. The process terminates after finitely many intersections, so that U is open.

By construction it is clear that the images of elements of L are linearly independent in V/U. Furthermore since U is open, then V/U will be discrete, and it is possible to rewrite V as the topological direct sum V ≅ V/U ⊕ U by the previous discussion.

We proceed by choosing a basis for V/U such that the elements of L are in the basis. We define an action on V/U which cyclically permutes the elements of L but leaves the other basis elements fixed. Since V/U is discrete, this is continuous. We extend to an action on V by placing a trivial action on U. Clearly v is not fixed by this action.

□

Notice first that infinitely many dimensions are necessary to carry this argument out. For finite V, there are elements which are fixed by arbitrary actions. These are the scalar multiples of the trace element, and arise because the category of finite dimensional representations of a group is compact [26]. Thus, while the category of finite-dimensional vector spaces is a model of multiplicative linear logic, it will not satisfy the appropriate full completeness theorem.

Notice also that this lemma contains the first hint of a completeness theorem. A dinatural interpreting the nonderivable sequent ⊢ α ⊗ α^{⊥} instantiated at V would correspond to a fixed point of V ⊗ V^{⊥}. The above lemma implies that such a dinatural must be 0 on all infinite dimensional instantiations. We will soon see that this implies the dinatural must be identically 0.

Lemma 9.3 Given a binary sequent of the form:

Γ, α_{1} −∘ α_{2}, α_{2} −∘ α_{3}, …, α_{n−1} −∘ α_{n} ⊢ α_{1}^{⊥} ⊗ α_{n} (6) suppose each α_{i} is instantiated at the same space V ∈ RT VEC (The atoms in Γ may be instantiated at any spaces). Let θ be a uniform dinatural transformation interpreting this sequent. Suppose there exist elements a⃗ ∈ Γ, f_{1} ∈ α_{1} −∘ α_{2}, f_{2} ∈ α_{2} −∘ α_{3}, …, f_{n−1} ∈ α_{n−1} −∘ α_{n} such that, at the above instantiation, θ(a⃗, f_{1}, …, f_{n−1}) ≠ 0. Then θ(a⃗, id, …, id) ≠ 0.

Proof. Consider a dinatural θ ∈ Z − Dinat(Γ ⊗ (α_{1} −∘ α_{2}) ⊗ ⋯ ⊗ (α_{n−1} −∘ α_{n}), α_{n}). Such a dinatural is a family of morphisms θ_{A_{1}···A_{n}} satisfying the following diagram: for all n-tuples of objects A_{1}A_{2} ⋯ A_{n}, B_{1}B_{2} ⋯ B_{n} in RT VEC and morphisms f_{i} : A_{i} → B_{i}, the following hexagon commutes

Γ ⊗ (A_{1} −∘ A_{2}) ⊗ ⋯ ⊗ (A_{n−1} −∘ A_{n}) \overline{θ_{A_{1}···A_{n}}  ^{}}A_{1}^{⊥} ⊗ A_{n}
[figure: A_{1}^{⊥} ⊗ f_{n}]
Γ ⊗ (B_{1} −∘ A_{2}) ⊗ ⋯ ⊗ (B_{n−1} −∘ A_{n}) Γ ⊗ (f_{1} −∘ A_{2}) ⊗ ⋯ ⊗ (f_{n−1} −∘ A_{n})^{}A_{1}^{⊥} ⊗ B_{n}
[figure: f_{1}^{⊥} ⊗ B_{n}]
[figure: Γ ⊗ (B_{1} −∘ B_{2}) ⊗ ⋯ ⊗ (B_{n−1} −∘ B_{n}); Γ ⊗ (B_{1} −∘ f_{2}) ⊗ ⋯ ⊗ (B_{n−1} −∘ f_{n}); θ_{B_{1}···B_{n}}; B_{1}^{⊥} ⊗ B_{n}]

Commutativity of this hexagon corresponds to the following equation: for all a⃗ ⊗ g_{2} ⊗ ⋯ ⊗ g_{n} ∈ Γ ⊗ (B_{1} −∘ A_{2}) ⊗ ⋯ ⊗ (B_{n−1} −∘ A_{n}),

A_{1}^{⊥} ⊗ f_{n}(θ_{A_{1}···A_{n}}(a⃗, g_{2}^{o}f_{1}, g_{3}^{o}f_{2} ⋯ g_{n}^{o}f_{n−1})) = (7)

f_{1}^{⊥} ⊗ B_{n}(θ_{B_{1}···B_{n}}(a⃗, f_{2}^{o}g_{2} ⋯ f_{n}^{o}g_{n}))

Recalling that all objects A_{i} and B_{i} (in θ’s components) are instantiated at V, we simply write θ instead of θ_{A_{1}···A_{n}} or θ_{B_{1}···B_{n}}. Consider the element a ⊗ id ⊗ ⋯ ⊗ id ∈ Γ ⊗ (B_{1} −∘ A_{2}) ⊗ ⋯ ⊗ (B_{n−1} −∘ A_{n}). Set f_{n} : A_{n} → B_{n} = id_{V}. Chasing this element around the hexagon (i.e. evaluating equation 7 with f_{n} = g_{2} = ⋯ = g_{n} = id_{V}) we obtain

θ(a⃗, f_{1}, ⋯, f_{n−1}) = f_{1}^{⊥} ⊗ B_{n}(θ(a⃗, f_{2}, ⋯, f_{n−1}, id)) (8)

Since θ(a⃗, f_{1}, ⋯, f_{n−1}) ≠ 0 it follows that θ(a⃗, f_{2}, ⋯, f_{n−1}, id) ≠ 0. Repeating this process, we obtain the statement of the lemma. □

Lemma 9.4 Suppose θ is a uniform dinatural interpreting sequent (6), and suppose each α_{i} is instantiated at V, an infinite dimensional object in RT VEC. Then θ is identically zero for this instantiation.

Proof. Choose v ∈ V ⊗ V^{⊥}, v ≠ 0. We define actions on the spaces instantiating the atoms of sequent (6); these atoms consist of those in Γ together with α_{1}, … α_{n}. The spaces instantiating the atoms in Γ are given the trivial action. V is given an action for which v is not fixed by the induced action on V ⊗ V^{⊥}. By lemma 9.2 , we know such an action exists. Since the identity map is fixed under any action, we conclude that θ(a⃗, id, …, id) ≠ v: this follows since a uniform dinatural takes fixed points to fixed points. Since v is arbitrary, then θ(a⃗, id, …, id) = 0. The result now follows from the previous lemma. □

Lemma 9.5 If θ is a uniform dinatural interpreting (6) then θ is identically zero on all instantiations.

Proof. Consider a dinatural θ ∈ Z − Dinat(Γ ⊗ (α_{1} −∘ α_{2}) ⊗ ⋯ ⊗ (α_{n−1} −∘ α_{n}), α_{1}^{⊥} ⊗ α_{n}), i.e. a family of morphisms satisfying the following diagram: for all n-tuples of objects A_{1}A_{2} ⋯ A_{n}, B_{1}B_{2} ⋯ B_{n} in RT VEC and morphisms f_{i} : A_{i} → B_{i}, the following hexagon commutes

Γ ⊗ (A_{1} −∘ A_{2}) ⊗ ⋯ ⊗ (A_{n−1} −∘ A_{n}) \overline{θ_{A_{1}···A_{n}}  ^{}}A_{1}^{⊥} ⊗ A_{n}
[figure: A_{1}^{⊥} ⊗ f_{n}]
Γ ⊗ (B_{1} −∘ A_{2}) ⊗ ⋯ ⊗ (B_{n−1} −∘ A_{n}) Γ ⊗ (f_{1} −∘ A_{2}) ⊗ ⋯ ⊗ (f_{n−1} −∘ A_{n})^{}A_{1}^{⊥} ⊗ B_{n}
[figure: f_{1}^{⊥} ⊗ B_{n}]
[figure: Γ ⊗ (B_{1} −∘ B_{2}) ⊗ ⋯ ⊗ (B_{n−1} −∘ B_{n}); Γ ⊗ (B_{1} −∘ f_{2}) ⊗ ⋯ ⊗ (B_{n−1} −∘ f_{n}); θ_{B_{1}···B_{n}}; B_{1}^{⊥} ⊗ B_{n}]

In this proof we will consider the upper leg of the diagram. Suppose that the A_{i} are instantiated at arbitrary spaces V_{i}. Set

B ≡ B_{1} = B_{2} = ⋯ = B_{n} = (⨁_{i} V_{i}) ⊕ k[Z]^{⊥⊥}

The purpose is to create an infinite dimensional space into which all the V_{i} embed. (Note that k[Z]^{⊥⊥} is an object of RT VEC, but k[Z] is not.) If one of the V_{i} is already infinite dimensional, the summand k[Z]^{⊥⊥} is unnecessary. Let f_{i} : A_{i}→B be the canonical embedding. Given an arbitrary element a⃗ ⊗ h_{1} ⊗ ⋯ ⊗ h_{n−1} ∈ Γ ⊗ (A_{1} −∘ A_{2}) ⊗ ⋯ ⊗ (A_{n−1} −∘ A_{n}) define an element a⃗ ⊗ d_{1} ⊗ ⋯ ⊗ d_{n−1} ∈ Γ ⊗ (B_{1} −∘ A_{2}) ⊗ ⋯ ⊗ (B_{n−1} −∘ A_{n}) as follows: d_{i} : B→A_{i} is h_{i} on the ith component, 0 elsewhere. By the previous lemma 9.4, we know the lower leg of the diagram is zero. Therefore, chasing the upper leg of the diagram, we conclude that (A_{1}^{⊥} ⊗ f_{n})^{o}θ(a⃗ ⊗ h_{1} ⊗ ⋯ ⊗ h_{n−1}) = 0. Since f_{n} is monic, the result follows. □

Proof. We now prove Theorem 9.1 (the completeness theorem). Suppose we have an underivable binary sequent which is also simple. Since the sequent is not derivable, the associated proof structure has a cycle. Isolate those formulas of the sequent which appear in the cycle. Choose one such formula, and bring all other formulas to the other side of the sequent using linear negation. Then, the first observation is that any such sequent must be of the form (6). Thus the previous lemma establishes the result for underivable simple sequents. Now suppose that we have an arbitrary underivable binary sequent. We reduce to the simple case by repeatedly left-composing with the morphisms:

δ: A ⊗ (B^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} C)→(A ⊗ B)^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} C

δ′: A ⊗ (B^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} C)→(A ⊗ C)^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B

ξ: A ⊗ B→A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B

Since these morphisms are monic, the general case follows (see Remarks below). □

Remark 9.6 The above proof involves a subtlety: we are composing a sequent (interpreted as a dinatural transformation) with one of the maps δ, δ′, ξ; the latter, as sequents, are also dinaturals. How do we know such dinaturals compose? The reason is that in fact these maps δ, δ′, ξ are really natural transformations, and natural transformations do compose with dinaturals.

As an example of this phenomenon in the reduction to simple sequents, consider the composition (using the cut-rule) of the binary, nonsimple sequent

⊢ (α ⊗ β^{⊥}) ⊗ (β ⊗ α^{⊥})

with the mix map ξ (qua sequent)

(α ⊗ β^{⊥}) ⊗ (β ⊗ α^{⊥}) ⊢ (α ⊗ β^{⊥})^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} (β ⊗ α^{⊥}) .

This composition yields the sequent ⊢ (α ⊗ β^{⊥})^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} (β ⊗ α^{⊥}), which is the same as the simple binary sequent ⊢ (α ⊗ β^{⊥}), (β ⊗ α^{⊥}).

Let us examine the dinatural interpretation of this composition in RT VEC:

1. The sequent ⊢ (α ⊗ β^{⊥}) ⊗ (β ⊗ α^{⊥}) interprets as a dinatural

θ : F ⟶^{..} G : (C^{op})^{2} × C^{2} → C

where F = I = k, the constant functor with value the base field (= unit for the tensor) and G = (α ⊗ β^{⊥}) ⊗ (β ⊗ α^{⊥}) = (Π_{1} ⊗ Π_{2}^{⊥}) ⊗ (Π_{2} ⊗ Π_{1}^{⊥}) . Here Π_{i} denotes the projection onto the ith covariant variable and Π_{i}^{⊥} denotes the linear negation of the projection onto the ith contravariant variable (i = 1, 2). Since F is constant, the dinatural hexagon for θ degenerates into a diamond shape (a so-called wedge). We leave it to the reader to calculate the following diagram for θ: for any f : C → A and g : D → B,

(A ⊗ B^{⊥}) ⊗ (B ⊗ A^{⊥})
[figure: θ_{AB}; (A ⊗ g^{⊥}) ⊗ (B ⊗ f^{⊥})]
k  (A ⊗ D^{⊥}) ⊗ (B ⊗ C^{⊥})
[figure: θ_{CD}; (f ⊗ D^{⊥}) ⊗ (g ⊗ C^{⊥})]
(C ⊗ D^{⊥}) ⊗ (D ⊗ C^{⊥})

2. Composing the above diagram for θ with the natural transformation associated to the MIX map ξ, we obtain the following combined commutative diagram, thus a dinatural transformation:

(A ⊗ B^{⊥}) ⊗ (B ⊗ A^{⊥})  \overline{mix} (A ⊗ B^{⊥})^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} (B ⊗ A^{⊥})
[figure: θ_{AB}; (A ⊗ g^{⊥}) ⊗ (B ⊗ f^{⊥}); II]
[figure: k; I; (A ⊗ D^{⊥}) ⊗ (B ⊗ C^{⊥}); mix; (A ⊗ D^{⊥})^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} (B ⊗ C^{⊥}); (A ⊗ g^{⊥})^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} (B ⊗ f^{⊥})]
[figure: θ_{CD}; (f ⊗ D^{⊥}) ⊗ (g ⊗ C^{⊥}); III]
[figure: (C ⊗ D^{⊥}) ⊗ (D ⊗ C^{⊥}); mix; (C ⊗ D^{⊥})^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} (D ⊗ C^{⊥}); (f ⊗ D^{⊥})^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} (g ⊗ C^{⊥})]

In the above diagram, we have omitted the appropriate subscripts on the MIX natural transformation. The commutative diagram II arises since mix is a natural transforma-

tion (A ⊗ (−)) ⊗ (B ⊗ (−)) ⟶^{.} (A ⊗ (−))^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} (B ⊗ (−)). Similarly, III arises since mix

is a natural transformation ((−) ⊗ D^{⊥}) ⊗ ((−) ⊗ C^{⊥}) ⟶^{.} ((−) ⊗ D^{⊥})^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ((−) ⊗ C^{⊥}).

10 Full Completeness

We are interested in Full Completeness, that is, when is a space of dinaturals generated by (the denotations of) syntactic proof terms? In this setting, syntactic proof terms take on the form of proof nets. We begin by establishing that a nonzero uniform dinatural can be assigned axiom links.

Lemma 10.1 Let M, N be MLL formulas. If Z−Dinat(M, N) has dimension greater than 0, then the sequent M ⊢ N is balanced.

Proof. Suppose σ is a nonzero dinatural transformation, and that σ_{A} is an instantiation for which it is nonzero. Let v ∈ M[A] be such that σ_{A}(v) ≠ 0. Let α_{1}, …, α_{n} be the atoms of M ⊢ N, and A = A_{1}, …, A_{n} the corresponding spaces. We define actions on each A_{i} as follows. Pick distinct prime numbers p_{1}, …, p_{n} and define the A_{i} action to be n.v = p_{i}^{n}v, for all v ∈ A_{i}. Since σ is uniform, we know that:

σ(1.v) = 1.σ(v)

Consider for example a positive occurrence of α_{i} in M. Each such occurrence contributes a factor of p_{i} to the left hand side of the equation. For the equation to hold, we conclude that there must either be:

• a negative occurrence of α_{i} in M, which would contribute a factor of p_{i}^{−1}.

• a positive occurrence of α_{i} in N.

A similar claim holds for all occurrences of variables, and it is clear that such occurrences must come in pairs, thus establishing that the sequent is balanced. □

Thus, for a sequent to have a nonzero proof structure, it must be a balanced sequent. So for the remainder of this section we will only consider such sequents. We begin by restricting to binary sequents, that is, sequents where each variable appears exactly twice.

If the sequent M ⊢ N is balanced, then one can associate to it a cut-free proof structure by choosing a pairing of the variables, and viewing this pairing as a set of axiom links. As previously remarked, given a sequent together with its axiom links, the cut-free proof structure is uniquely determined. To a binary sequent, we can only associate one set of axiom links. Thus the sequent is assigned a unique cut-free proof structure. To a nonbinary sequent, we associate a finite set of cut-free proof structures.

10.1 Binary Sequents

We begin by considering simple sequents.

Lemma 10.2 The space of proofs of the derivable binary sequent

α_{1}, α_{1} −∘ α_{2}, α_{2} −∘ α_{3}, …, α_{n−1} −∘ α_{n} ⊢ α_{n} (9)

has dimension 1. That is, the space

Z − Dinat(α_{1} ⊗ (α_{1} −∘ α_{2}) ⊗ ⋯ ⊗ (α_{n−1} −∘ α_{n}), α_{n})

consists of scalar multiples of the canonical dinatural transformation of this shape, which is the dinatural of the form:

(v, f_{1}, f_{2}, …, f_{n−1}) ↦ f_{n−1}(f_{n−2}(… f_{1}(v)) …)

Proof. Consider a dinatural θ ∈ Z − Dinat(α_{1} ⊗ (α_{1} −∘ α_{2}) ⊗ ⋯ ⊗ (α_{n−1} −∘ α_{n}), α_{n}). Such a dinatural is a family of morphisms θ_{A_{1}···A_{n}} satisfying the following diagram: for all n-tuples of objects A_{1}A_{2} ⋯ A_{n}, B_{1}B_{2} ⋯ B_{n} in RT VEC and morphisms f_{i} : A_{i} → B_{i}, the following hexagon commutes

A_{1} ⊗ (A_{1} −∘ A_{2}) ⊗ ⋯ ⊗ (A_{n−1} −∘ A_{n}) \overline{θ_{A_{1}···A_{n}}  ^{}}A_{n}
[figure: f_{n}]
A_{1} ⊗ (B_{1} −∘ A_{2}) ⊗ ⋯ ⊗ (B_{n−1} −∘ A_{n}) A_{1} ⊗ (f_{1} −∘ A_{2}) ⊗ ⋯ ⊗ (f_{n−1} −∘ A_{n})^{}B_{n}
[figure: id]
[figure: B_{1} ⊗ (B_{1} −∘ B_{2}) ⊗ ⋯ ⊗ (B_{n−1} −∘ B_{n}); f_{1} ⊗ (B_{1} −∘ f_{2}) ⊗ ⋯ ⊗ (B_{n−1} −∘ f_{n}); θ_{B_{1}···B_{n}}; B_{n}]

Commutativity of this hexagon corresponds to the following equation (which is a generalization of equation 5): for (v, g_{2} ⋯ g_{n}) ∈ A_{1} ⊗ (B_{1} −∘ A_{2}) ⊗ ⋯ ⊗ (B_{n−1} −∘ A_{n}):

f_{n}(θ_{A_{1}···A_{n}}(v, g_{2}^{o}f_{1}, g_{3}^{o}f_{2} ⋯ g_{n}^{o}f_{n−1})) = θ_{B_{1}···B_{n}}(f_{1}(v), f_{2}^{o}g_{2} ⋯ f_{n}^{o}g_{n}) (10)

We begin by instantiating a θ at a single space V; e.g. in θ_{A_{1}···A_{n}} set A_{1} = A_{2} = ⋯ = A_{n} = V. Given v ∈ V define an action on V which fixes v but has a p-action on a complementary subspace. It can be shown that such actions are continuous, by previous arguments.

We calculate θ_{A_{1}···A_{n}}(v, id, ⋯, id). Since the point (v, id, ⋯, id) is fixed under the above action, we have

θ_{A_{1}···A_{n}}(v, id, ⋯, id) = rv (11)

for some scalar r. We show that r is independent of the choice of v ∈ V.

To this end, consider the above hexagon with all spaces A_{i} = B_{i} = V. Now pick another vector v′ ∈ V, v′ ≠ 0. Choose a continuous involution i_{v′} : V → V satisfying i_{v′}(v) = v′, and i_{v′}^{2} = id. Consider the following element (v, i_{v′}, i_{v′} ⋯ i_{v′}) ∈ A_{1} ⊗ (B_{1} −∘ A_{2}) ⊗ ⋯ ⊗ (B_{n−1} −∘ A_{n}) and let all f_{1} = f_{2} = ⋯ = f_{n−1} = i_{v′}. Chasing around the hexagon, the upper leg gives rv′, whereas the lower gives θ(v′, id, ⋯, id). Thus θ(v′, id, ⋯, id) = rv′, as required.

We now show that in this instantiation of the hexagon (i.e. when all A_{i} and B_{i} equal V):

θ_{A_{1}···A_{n}}(v, f_{1}, ⋯, f_{n−1}) = rf_{n−1}(… f_{1}(v)))

where each f_{i} is an arbitrary endomorphism of V, and for the same r as in equation (11). To prove this, consider the previous hexagon (i.e. with all A_{i} and B_{i} equal V), and set f_{n} = id. Consider (v, id, id ⋯ id) ∈ A_{1} ⊗ (B_{1} −∘ A_{2}) ⊗ ⋯ ⊗ (B_{n−1} −∘ A_{n}). Then going around the upper leg gives θ_{A_{1}···A_{n}}(v, f_{1}, ⋯, f_{n−1}), while going around the lower leg gives θ_{B_{1}···B_{n}}(f_{1}(v), f_{2}, ⋯ f_{n−1}, id). By induction, we conclude that

θ_{V,...V} (v, f_{1}, ⋯, f_{n−1}) = r(f_{n−1}(… f_{1}(v)))

We now show that the scalar r in the equations above is independent of the space V at which we uniformly instantiate. Denote the r above by r_{V}. We shall now show that r_{V} = r_{k}, where k is the base field. Instantiate the hexagon (i.e. equation (10)) at A_{i} = V and B_{i} = k, for all i. Consider the element (v, v̂, ⋯, v̂) ∈ A_{1} ⊗ (B_{1} −∘ A_{2}) ⊗ ⋯ ⊗ (B_{n−1} −∘ A_{n}), where v̂ : k→V is the map sending 1 to v. Choose f : V →k such that f(v) = 1. Set f_{1}, f_{2}, … = f. Now by considering the diagram, the upper leg gives r_{V} and the lower gives r_{k}.

Finally, we need to verify the result on arbitrary instantiations. Consider the instantiation θ_{C_{1}···C_{n}} where each α_{i} is instantiated at C_{i}, an arbitrary object. Next we set each B_{i} = V = ⨁ C_{i}. The maps C_{i} → B_{i} are the canonical inclusions.

Suppose we have c ⊗ f_{1} ⊗ f_{2} … f_{n−1} ∈ C_{1} ⊗ (C_{1} −∘ C_{2}) … (C_{n−1} −∘ C_{n}). Define an element of C_{1} ⊗ (V −∘ C_{2}) ⊗ … ⊗ (V −∘ C_{n}) by defining a map V → C_{i} to be f_{i−1} on C_{i−1} and 0 elsewhere.

The commutativity of the above diagram gives:

θ_{C_{1}···C_{n}}(c, f_{1}, ⋯, f_{n−1}) = r(f_{n−1}(… f_{1}(c)))
□

Theorem 10.3 (Full Completeness for Binary Sequents) If a sequent M ⊢ N is binary, then Z − Dinat(M, N) is zero or 1-dimensional, depending on whether its uniquely determined proof structure is a net.

Proof. If M ⊢ N is not derivable, the result follows from the completeness theorem.

For the other direction, first observe that all of the connected components of a derivable binary simple sequent in the theory MLL+MIX are of the form (9). The disjoint components must have disjoint atoms, since the sequent is binary. Thus the argument establishing the preceding lemma can be carried out “in parallel” on the various pieces. For example, if there are two disjoint components, the codomain of the dinatural will be of the form A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B. If v ∈ A and w ∈ B, then the image of (v, id, ⋯, id, w, id, ⋯, id) will be a scalar multiple of the morphism mapping f ⊗ g to f(v)g(w), where f ∈ A^{⊥} and g ∈ B^{⊥}. (Remember that A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B = (A^{⊥} ⊗ B^{⊥})^{⊥}.) The various diagram chases necessary to establish the previous lemma, go through in this more general setting as well.

Now given a derivable binary sequent, we associate to it a set of simple binary sequents, by the methods described in section 2.4. Since the sequent is derivable, each of these simple sequents must be derivable, and so has a one-dimensional proof space. We know that the proof space of the original sequent is at least one-dimensional, since it will contain the denotation of the cut-free proof. If it were greater than one dimensional, then the proof space of one of the associated simple sequents, would have to also be at least two-dimensional. This is because the associated simple sequents are obtained by left composition with the structure maps described in Lemma 9.5, and these maps are monic, and so have trivial kernels. □

Remark 10.4 The dinatural transformations interpreting binary sequents in the above theorem will be called binary dinatural transformations.

This result establishes full completeness for arbitrary binary sequents. Given a derivable such sequent, we see that the only “abstract proofs” are scalar multiples of the denotation of the unique cut-free proof.

10.2 Nonbinary Sequents

The above result could be seen as the main theorem of the paper as it is the binary sequents which are fundamental in linear logic. Nonbinary balanced sequents are obtained as substitution instances of these. This philosophy is discussed in [9]. In that paper, a general system known as the Autonomous Deductive System (ADS) is presented. An ADS is a method of specifying theories of monoidal categories by the addition of nonlogical axioms to (multiplicative) linear logic. One of the fundamental restrictions in the definition of ADS is that if one wishes to add nonbinary axioms, one must add an associated binary axiom of which it is a substitution instance.

This corresponds to the idea that in a proof net, it is the axiom links themselves which are functioning as variables. An analogue of α-conversion for linear logic should say that in a proof structure, one should be allowed to substitute distinct variables when two variables are not connected by an axiom link. With this interpretation in mind, given a nonbinary balanced sequent, we will only consider those dinaturals which are (linear combinations of) substitution instances of binary dinaturals. Such dinaturals will be called diadditive.

Consider as an example the sequent α ⊗ α ⊢ α ⊗ α. There are two canonical proofs of this sequent. These are modeled in a ∗-autonomous category by the identity morphism and the symmetry map. Thus the proof space associated to this sequent should be a two-dimensional space. In other words, every uniform dinatural of this shape should be a linear combination of the identity dinatural and the “twist” dinatural.

We investigate this question in more detail. First note that to any balanced sequent, say M ⊢ N, we can assign a set of sets of axiom links. This assignment determines a finite list of binary sequents of which M ⊢ N is a substitution instance. Suppose this list is: M_{1} ⊢ N_{1}, M_{2} ⊢ N_{2}, . . .. (The list must be finite.) We define a new vector space, called the associated binary space for the sequent M ⊢ N.

ABS(M, N) = ∐_{i} Z − Dinat(M_{i}, N_{i})

By the completeness theorem, we know that each Z − Dinat(M_{i}, N_{i}) is either 0- or 1dimensional, and in the latter case, the space is generated by the denotation of the unique cut-free proof of the sequent.

Example 10.5 Consider the (derivable) sequent α, α −∘ α ⊢ α . For later purposes, it is convenient to consider this as a left-sided sequent: α, α −∘ α, α^{⊥} ⊢ . There are two associated sets of axiom links:

α, α −∘ α, α^{⊥} ⊢  and  α, α −∘ α, α^{⊥} ⊢

These yield (respectively) the following binary sequents:

(a) α, α −∘ β, β^{⊥} ⊢

(b) α, β −∘ β, α^{⊥} ⊢

The associated binary space ABS of the original sequent α, α −∘ α ⊢ α is the coproduct of the proof spaces associated to (a) and (b). Using full completeness for binary sequents we obtain: for (a), the sequent is derivable; so the space of Z-dinats in this case has dimension 1. For (b), the sequent is not derivable, so the space of Z-dinats in this case has dimension 0. Thus ABS has dimension 1 + 0 = 1, as expected . □

There is a canonical linear map:

φ : ABS(M, N) ⟶ Z − Dinat(M, N)

On basis elements, this is defined by “equating variables” in the associated binary sequents M_{i} ⊢ N_{i}, or more formally, restricting which instantiations we will allow according to the pattern of in M ⊢ N (see the previous example). At the level of dinaturality, this amounts to restricting the acceptable instantiations.

Definition 10.6 We call those elements of Z − Dinat(M, N) of the form φ(S) for a (necessarily unique) S ∈ ABS(M, N) diadditive.

Equivalently, a diadditive dinatural transformation is a transformation which is a linear combination of substitution instances of binary dinaturals.

Note that if the sequent is binary, every Z-uniform dinatural is automatically diadditive.

Example 10.7 In Example 10.5, consider the sequent α ⊗ (α −∘ β) ⊢ β. We will only allow instantiations (in RT VEC) of the form α = β = V. Clearly the resulting dinatural transformation lives in Z − Dinat(M, N).

Given a diadditive element of Z − Dinat(M, N), we give a method for determining the unique S ∈ ABS(M, N).

Suppose that the atom α occurs in the sequent M ⊢ N. We introduce a stock of new variables X_{1}^{α}, X_{2}^{α}, X_{3}^{α}, . . .. We will consider formal expressions of the form: X_{1}^{α} ⊕ X_{2}^{α} ⊕ … ⊕ X_{n}^{α}. This is designed to represent the idea that we will be instantiating the atom α at n-ary coproducts. The variables X_{i}^{α} will represent the summands, which we will allow to vary over arbitrary objects of RT VEC. In such instantiations, we will only consider morphisms of the form

X_{1}^{α} ⊕ X_{2}^{α} ⊕ … ⊕ X_{n}^{α} \overline{f_{1} ⊕ f_{2} ⋯ ⊕ f_{n}_{}}W_{1}^{α} ⊕ W_{2}^{α} ⊕ … ⊕ W_{n}^{α}

Now for the construction. We restrict our attention to left-only sequents, i.e. sequents of the form Γ ⊢. Since we are working in a ∗-autonomous category, this is not a real restriction. Suppose that the atom α occurs 2n times in the sequent Γ, n times covariantly and n times contravariantly. Finally suppose we have θ ∈ Z − Dinat(Γ,). In θ, we will instantiate α at the formal coproduct:

α = X_{1}^{α} ⊕ X_{2}^{α} ⊕ … ⊕ X_{n}^{α}

Repeat this process for all atoms in M ⊢ N.

Given an allowable set of axiom links, number the links connecting α’s 1, ⋯, n. For the two occurrences of α paired by the ith axiom link, restrict X_{1}^{α} ⊕ X_{2}^{α} ⊕ … ⊕ X_{n}^{α} to the ith component (and set the others to 0). If α occurs in the scope of a negation (thus it interprets as a functional) this amounts to ignoring some of the summands of the domain of the functional. Proceed similarly for all atoms in the sequent.

When θ is instantiated in this way, it can be interpreted as a (binary) dinatural θ̂ corresponding to the binary sequent with the chosen set of axiom links. We shall illustrate the construction by an extended example below, but for now continue with the main discussion.

We repeat this process for all choices of allowable axiom links for Γ ⊢. The process yields a finite family of binary dinaturals associated to θ, say {θ̂_{1}, ⋯, θ̂_{m}}, where m is the number of choices of allowable axiom links for Γ ⊢. We then conclude that:

θ = θ̂_{1} + θ̂_{2} + … + θ̂_{m}

We now begin an extended example illustrating the above procedure.

Example 10.8 We consider the sequents in Example 10.5.

(a) Consider the sequent α, α −∘ α, α^{⊥} ⊢ . This sequent is equivalent to the sequent α ⊗ (α −∘ α) ⊗ α^{⊥} ⊢ I , where I is the unit. Let C = RT VEC. The sequent interprets as a dinatural θ : F → G : (C^{op}) × C → C, where F = P_{1} ⊗ (P_{1} −∘ P_{1}) ⊗ P_{1}^{⊥} (with P_{1} = the covariant projection) and G = I = the constant functor with value k, the base field. The reader may verify that θ satisfies the following wedge (= degenerate hexagon [5]): for any h : A → B

A ⊗ (A −∘ A) ⊗ A^{⊥}

[figure: A ⊗ (h −∘ A) ⊗ h^{⊥}; θ_{A}]
A ⊗ (B −∘ A) ⊗ B^{⊥}  k
[figure: h ⊗ (B −∘ h) ⊗ B^{⊥}; θ_{B}]

B ⊗ (B −∘ B) ⊗ B^{⊥}

Thus for any element (a, x, b) ∈ A ⊗ (B −∘ A) ⊗ B^{⊥}, we have the equation

θ_{A}(a, x^{o}h, b^{o}h) = θ_{B}(h(a), h^{o}x, b) (12)

(b) The first set of axiom links in Example 10.5 yield the binary sequent α, α −∘ β, β^{⊥} ⊢ . This latter sequent is equivalent to α ⊗ (α −∘ β) ⊗ β^{⊥} ⊢ I , where I is the unit for the tensor. As above, this sequent interprets as a dinatural θ̂: F → G : (C^{op})^{2} × C^{2} → C, where F = Π_{1} ⊗ (Π_{1} −∘ Π_{2}) ⊗ Π_{2}^{⊥} and G = I = the constant functor with value k, the base field. The reader may verify that θ̂ satisfies the following wedge (= degenerate hexagon [5]): for any h : A → B, h′ : A′ → B′:

A ⊗ (A −∘ A′) ⊗ (A′)^{⊥}
[figure: A ⊗ (h −∘ A′) ⊗ (h′)^{⊥}; θ̂_{AA′}]
A ⊗ (B −∘ A′) ⊗ (B′)^{⊥}  k
[figure: h ⊗ (B −∘ h′) ⊗ (B′)^{⊥}; θ̂_{BB′}]
B ⊗ (B −∘ B′) ⊗ (B′)^{⊥}

Thus for any element (a, l, m) ∈ A ⊗ (B −∘ A′) ⊗ (B′)^{⊥}, we have the equation

θ̂_{AA′}(a, l^{o}h, m^{o}h′) = θ̂_{BB′}(h(a), h′^{o}l, m) (13)

(c) Let θ be a dinatural interpreting the sequent (with axiom links)

α, α −∘ α, α^{⊥} ⊢

and satisfying equation (12) above. We know these axiom links determine the binary sequent α, α −∘ β, β^{⊥} ⊢ . We shall instantiate θ at a coproduct V ⊕ W, yielding a family

θ̂_{V,W} : V ⊗ (V −∘ W) ⊗ W^{⊥} → k

as follows: for the first axiom link, we instantiate at V, letting W = 0 and vice-versa for the second axiom link.

θ̂_{V,W} (v, f, g) =_{def} (14)

θ_{V ⊕W} ( (v, 0) ⊗ [(v̂, ŵ) ↦ (0, f(v̂))] ⊗ [(v̂, ŵ) ↦ g(ŵ)] )

We now show that θ̂ is a dinatural transformation, i.e. satisfies equation (13) above (in which we set, respectively, A = V, A′ = W, B = V′, B′ = W′.) We chase around the above diagram. Consider an element (a, l, m) ∈ V ⊗ (V′ −∘ W) ⊗ (W′)^{⊥}.

The upper leg gives

θ̂_{V,W} (a, l^{o}h, m^{o}h′) = (15)

θ_{V ⊕W} ( (a, 0) ⊗ [(v̂, ŵ) ↦ (0, l(h(v̂)))] ⊗ [(v̂, ŵ) ↦ m(h′(ŵ))] )

The lower leg gives

θ̂_{V′,W′}(h(a), h′^{o}l, m) = (16)

θ_{V′⊕W′}( (h(a), 0) ⊗ [(v̂, ŵ) ↦ (0, h′(l(v̂)))] ⊗ [(v̂, ŵ) ↦ m(ŵ)] )

We leave it to the reader to verify that the equality of these two expressions follows from the dinaturality equation (12) for θ. □

10.3 Main Result

We are now ready to state the main result of the paper, which follows from the previous discussion.

Theorem 10.9 (Full Completeness) Let M and M′ be formulas in multiplicative linear logic, interpreted as definable multivariant functors on RT VEC. Then the vector space of diadditive Z-uniform dinatural transformations Z−Dinat(M, M′) has as basis the denotations of cut-free proofs in the theory MLL + MIX.

A full completeness theorem establishes such a tight correspondence between syntax and semantics that the syntactic proof of compositionality of definable dinaturals can be lifted to any semantics for which such a theorem holds. Thus one can show:

Corollary 10.10 Uniform diadditive dinatural transformations compose. Thus we obtain an ∗-autonomous category by taking as objects formulas, interpreted as multivariant functors. Morphisms will be uniform diadditive dinatural transformations^{2}.

At this point, we mention an open question. We have been unable to exhibit a Z-uniform dinatural which is not diadditive. This leads us to ask: does Z-uniformity imply diadditivity?

11 Hopf Algebras

The representation theory of Hopf algebras provides a natural generalization of that of groups and may ultimately allow us to generalize the previous results to the noncommutative, braided and cyclic settings. We briefly review the basic theory before stating our conservativity result. For a more complete discussion, see [1] or [45].

11.1 Definition and Categorical Structure

Definition 11.1 A Hopf algebra is a vector space, H, equipped with an algebra structure, a compatible coalgebra structure and an antipode. These must satisfy equations as outlined in [45]. The following chart summarizes the necessary structure.

2In fact, we obtain an indexed ∗-autonomous category in the sense of [42].

Structure  k[G]
Algebra m: H ⊗ H → H m(g_{1} ⊗ g_{2}) = g_{1}g_{2}
η: k→H  η(1_{k}) = 1_{G}
Coalgebra Δ: H→H ⊗ H  Δ(g) = g ⊗ g
ϵ: H→k  ϵ(g) = 1_{k}
Antipode  S: H → H  S(g) = g^{−1}

One obtains a Hopf algebra from a group G by taking the vector space generated by the elements of the group. The previous chart also illustrates this associated Hopf structure. Many other examples are discussed in [45] and [1].

We now discuss the representation theory of Hopf algebras. In the following definition V can either be a vector space, an object of T VEC or RT VEC. In the latter cases, we topologize the Hopf algebra discretely, and use the appropriately topologized tensor product.

Definition 1 A (left) module over a cocommutative Hopf algebra H is a space V, together with a linear action map ρ : H ⊗ V → V satisfying the following two diagrams:

[figure: H ⊗ H ⊗ V; id ⊗ ρ; H ⊗ V; V; ρ; H ⊗ V]
[figure: ≅]
[figure: H ⊗ V; m ⊗ id; ρ; V; ρ; k ⊗ V; η ⊗ id]

The category of discrete H-modules and equivariant maps is denoted MOD(H). The category of linearly topologized H-modules is denoted T MOD(H).

The representations of a Hopf algebra associated to a group correspond precisely to representations of the group.

Proposition 11.2 MOD(H) and T MOD(H) are monoidal categories.

Proof. If U and V are modules, then U ⊗ V has a natural module structure given by:

[figure: H ⊗ U ⊗ V; Δ ⊗ id; H ⊗ H ⊗ U ⊗ V; c_{23}; H ⊗ U ⊗ H ⊗ V; ρ ⊗ ρ; U ⊗ V]

□

This module will be denoted as U ⊗H V or just U ⊗ V if there is no danger of confusion. A significant difference between groups and Hopf algebras is that the tensor in MOD(H) need not be symmetric:

Definition 11.3 H is said to be cocommutative if:

H  \overline{Δ^{}}H ⊗ H
[figure: Δ]
H ⊗ H^{^{}c_{12}}

Here c_{12} is the canonical symmetry. An easy calculation shows:

Lemma 11.4 If H is a cocommutative Hopf algebra, MOD(H) and T MOD(H) are symmetric monoidal categories.

The fact that MOD(H) need not be symmetric means that these categories are of great use in modeling variants of the traditional commutative linear logic. By altering the Hopf algebra, one may obtain models of noncommutative logic, braided logic or cyclic logic. Hopf algebras are viewed as a unifying structure for these different logics, and the structure of the logic you are modeling is reflected in the structure of the algebra. This is discussed in [10].

While MOD(H) and T MOD(H) may not be symmetric, they will always be closed. For the rest of the section, we will assume H is cocommutative, although the next result holds in a more general setting [10].

Theorem 11.5 Let H be a cocommutative Hopf algebra. MOD(H) and T MOD(H) are symmetric monoidal closed categories.

Proof. In the case of MOD(H) the internal HOM is given by the space of k-linear maps with action described as follows:

Let V and W be modules, f : V →W a k-linear map, and v ∈ V. Then define:

hf(v) = Σh_{1}f(S(h_{2})v)

where

Δ(h) = Σh_{1} ⊗ h_{2}

For T MOD(H), the internal HOM will be the space of k-linear continuous maps. □

Note that the action of the internal HOM is the obvious generalization of the contragredient representation of groups. It is easily seen that the work of Lefschetz and Barr on the structure of the category T VEC lifts to the category T MOD(H). In particular,

Theorem 11.6 If V ∈ T MOD(H), then μ : V →V^{⊥⊥} is a bijection. Let RT MOD(H) denote the full subcategory of T MOD(H) of objects for which μ is an isomorphism. Then RT MOD(H) is a ∗-autonomous category and a reflective subcategory of T MOD(H) via the functor (−)^{⊥⊥}. The forgetful functor from RT MOD(H) to RT VEC is a ∗-autonomous functor.

11.2 Conservativity Theorem

The following result is a corollary of the previous theorem and the full completeness theorem. It can be viewed as a conservativity result.

Theorem 11.7 A diadditive dinatural transformation between definable multivariate functors which is uniform with respect to the additive group of integers is uniform with respect to arbitrary cocommutative Hopf algebras.

Proof. This follows immediately from the fact that the forgetful functor preserves the ∗- autonomous structure. □

These results suggest that general Hopf algebras may be useful in deriving full completeness theorems for noncommutative logics, such as those studied in [4] and [48].

12 Conclusion

We now discuss possible extensions of this work.

While Theorem 11.7 is straightforward to prove, it is an extremely suggestive result. In [10], it is observed that Hopf algebras provide a unifying framework for modeling a number of different variants of linear logic. These different variants are obtained by modifying or eliminating the exchange rule. In this way, one obtains noncommutative (planar) linear logic, cyclic linear logic, and braided linear logic. By choosing an appropriate Hopf algebra, we are able to model all of these different variants. The Hopf algebra is used to control the degree of symmetry of the model. Thus the notion of uniformity may be used to derive full completeness theorems for these various fragments. In particular, there is one Hopf algebra, the shuffle algebra, described in [45] and [10], which we conjecture will provide a fully complete semantics for cyclic linear logic.

We also observe that since the category RT VEC is complete and cocomplete, it is possible to model second order quantification via the end interpretation of [5]. The extent to which full completeness holds for this fragment is worth exploring.

Finally, we point out that the notion of group action and invariant element recurs throughout mathematics. For example, the notion of a group acting on a graph has been studied extensively. By allowing a group to act on the underlying web of a coherence space, we are led to the notion of a G-coherence space. This structure may prove illuminating for obtaining full completeness for a larger fragment of linear logic.

References

[1] K. Abé, Hopf Algebras, Cambridge University Press, (1977).

[2] S. Abramsky, R. Jagadeesan, Games and Full Completeness for Multiplicative Linear Logic, J. Symbolic Logic, Vol. 59, No.2 (1994), pp. 543-574.

[3] S. Abramsky, R. Jagadeesan, P. Malacaria, Games and Full Abstraction for PCF, Parts I, II. Research Announcements (July, Sept. 1993), Imperial College, London.

[4] V.M. Abrusci, Phase Semantics and Sequent Calculus for Pure Noncommutative Classical Linear Propositional Logic, J. Symbolic Logic Vol. 56 (1991), pp. 1403-1456.

[5] E. Bainbridge, P. Freyd, A. Scedrov, P. Scott, Functorial Polymorphism, Theoretical Computer Science 70, (1990), pp. 1403-1456.

[6] M. Barr, Duality of Vector Spaces, Cahiers de Top. et Géom. Diff. 17, (1976), pp. 3-14.

[7] M. Barr, ∗-Autonomous Categories, Springer Lecture Notes in Mathematics 752, (1980).

[8] M. Barr, Separability of tensor in Chu categories of vector spaces, Appendix to [10].

[9] R. Blute, Linear Logic, Coherence and Dinaturality, Theoretical Computer Science 115, (1993), pp. 3-41.

[10] R. Blute, Hopf Algebras and Linear Logic, to appear: Mathematical Structures in Computer Science, (1995).

[11] R. Blute, Braided Proof Nets and Categories, in preparation, (1995)

[12] R. Blute, J.R.B. Cockett, R.A.G. Seely, T. Trimble, Natural Deduction and Coherence for Weakly Distributive Categories, to appear: J. Pure and Applied Algebra, (1995)

[13] J.R.B. Cockett, R.A.G. Seely, Weakly Distributive Categories, in: Applications Of Categories in Computer Science, London Mathematical Society Lecture Notes Series 177, (1992)

[14] V. Danos, L. Regnier, The Structure of Multiplicatives, Arch. Math. Logic 28, (1989), pp.181-203.

[15] A. Fleury, C. Rétoré, The MIX Rule, preprint, (1991)

[16] P. J. Freyd, E.P. Robinson, and G. Rosolini, Dinaturality for Free, in: Applications of Categories in Computer Science, ed. by M.P. Fourman, P. Johnstone, and A. M. Pitts, Cambridge University Press, (1992), pp.107-118.

[17] P. J. Freyd, E.P. Robinson, and G. Rosolini, Functorial Parametricity, Proc. of Logic in Computer Science 1992, I.E.E.E.

[18] W. Fulton, J. Harris, Representation Theory, Springer-Verlag Graduate Texts in Mathematics 129, (1991)

[19] J. Y. Girard, Linear Logic, Theoretical Computer Science 50, p. 1-102 (1987)

[20] J.Y. Girard, Y. Lafont, Linear Logic and Lazy Computation, in: Springer Lecture Notes in Computer Science 250, (1988)

[21] J.Y. Girard, Y. Lafont, P.Taylor, Proofs and Types, Cambridge Tracts in Theoretical Computer Science 7, (1989).

[22] J. Y. Girard, A. Scedrov, P. Scott, Normal Forms and Cut-free Proofs as Natural Transformations, in : Logic From Computer Science, Mathematical Science Research Institute Publications 21, (1991), pp. 217-241. (Also available by anonymous ftp from: theory.doc.ic.ac.uk, in: papers/Scott).

[23] V. Harnik, M. Makkai, Lambek’s Categorical Proof Theory and Läuchli’s Abstract Realizability, Journal of Symbolic Logic 57, (1992), pp. 200-230.

[24] J. Horvath, Topological Vector Spaces and Distributions, Addison-Wesley Series in Mathematics, (1966).

[25] P. Johnstone, Topos Theory, Academic Press, (1977).

[26] G.M. Kelly, M. La Plaza, Coherence for Compact Closed categories, J. Pure and Applied Algebra 19, (1980), p. 193-213.

[27] G.M. Kelly, S. Mac Lane, Coherence in Closed Categories, J. Pure and Applied Algebra 1, p. 97-140, (1971).

[28] J. Lambek, Bilinear Logic in Algebra and Linguistics, preprint, (1993).

[29] J. Lambek, P.J. Scott, Introduction to Higher Order Categorical Logic, Cambridge University Press, (1986).

[30] H. Läuchli, An Abstract Notion of Realizability for which Intuitionistic Predicate Calculus is Complete, Intuitionism and Proof Theory, North-Holland,(1970), pp. 227-234.

[31] S. Lefschetz, Algebraic Topology, American Mathematical Society Colloquium Publications 27, (1963).

[32] R. Loader, The Undecidability of λ-definability, manuscript, 1993. (available by anonymous ftp from theory.doc.ic.ac.uk, in: papers/Loader).

[33] R. Loader, Linear Logic, Totality and Full Completeness, Proc. Logic in Computer Science (LICS) 1994, IEEE Computer Science Press.

[34] R. Milner, Fully Abstract Models of Typed Lambda Calculi, Th. Computer Science, Vol.4, (1977), pp. 1-22.

[35] J.C. Mitchell, Type Systems for Programming Languages, in: Handbook of Theoretical Comp. Science, Elsevier Publishers, (1990).

[36] J. C. Mitchell and E. Moggi, Kripke-style models for typed lambda calculus. Annals Pure Appl. Logic,51, (1991), pp. 99-124.

[37] J.C. Mitchell, A. Scedrov, Notes on Sconing and Relators, in Computer Science Logic ’92, Springer Lecture Notes in Computer Science 702 pp. 352-378 (1993).

[38] J.C. Mitchell, P.J. Scott, Typed Lambda Models and Cartesian Closed Categories, in: Contemporary Mathematics Vol. 92, (1989), pp. 301-316.

[39] G.D. Plotkin, Lambda Definability in the Full Type Hierarchy, in: To H.B. Curry, Essays on Combinatory Logic, Lambda Calculus and Formalism, (1980), pp. 363-373.

[40] J. Reynolds, Types, Abstraction and Parametric Polymorphism, Information Processing ’83, North-Holland, (1983).

[41] H.H. Schaefer, Topological Vector Spaces, Springer Graduate Texts in Mathematics 3, (1970).

[42] R.A.G. Seely, Linear Logic, ∗-Autonomous Categories, and Cofree Coalgebras, Contemporary Mathematics 92, (1989), pp. 371-382.

[43] R. Statman, Logical Relations and the Typed Lambda Calculus, Information and Control 65, (1985), pp. 85-97.

[44] A. Stoughton, Mechanizing Logical Relations, Proc. Mathematical Foundations of Programming Semantics, Lecture Notes in Computer Science 802, Springer-Verlag (1994).

[45] M. Sweedler, Hopf Algebras, Benjamin Press, (1969).

[46] W.W. Tait, Intensional Interpretation of Functionals of Finite Type, Journal of Symbolic Logic 32, (1967), pp. 198-212.

[47] A. Troelstra, Lectures on Linear Logic, CSLI Publications (1991)

[48] D. Yetter, Quantales and (Noncommutative) Linear Logic, Journal of Symbolic Logic 55, (1990), pp. 41-64.