First Order Linear Logic

in

Symmetric Monoidal Closed Categories

Simon John Ambler

Doctor of Philosophy University of Edinburgh

Abstract

There has recently been considerable interest in the development of ‘logical frameworks’ which can represent many of the logics arising in computer science in a uniform way. Within the Edinburgh LF project, this concept is split into two components; the first being a general proof theoretic encoding of logics, and the second a uniform treatment of their model theory. This thesis forms a case study for the work on model theory.

The models of many first and higher order logics can be represented as fibred or indexed categories with certain extra structure, and this has been suggested as a general paradigm. The aim of the thesis is to test the strength and flexibility of this paradigm by studying the specific case of Girard’s linear logic. It should be noted that the exact form of this logic in the first order case is not entirely certain, and the system treated here is significantly different to that considered by Girard.

To secure a good class of models, we develop a carefully restricted form of first order intuitionistic linear logic, called L_{F OLL}, in which the linearity of the logic is also reflected at the level of types. That is, the terms of the logic are given by a linear type theory LTT corresponding to the algebraic idea of a symmetric monoidal closed category. The study of logic in such categories is motivated by two examples which are derived as linear analogues of presheaf topoi and Heyting valued sets respectively. We introduce the concept of a monoidal factorisation system over such categories to provide a basis for a theory of linear predicates. A monoidal factorisation system then gives rise to a structure preserving fibration between symmetric monoidal closed categories, which we term a linear doctrine. We provide a sequent calculus formulation of L_{F OLL} and show that it is both sound and complete with respect to a linear doctrine semantics.

Although the logic L_{F OLL} sits nicely within the fibred category framework, we note that it also displays some quite unexpected features which should be of interest in future work on both the categorical semantics of linear logic and model theory in the general case.

Acknowledgements

I would like to thank the following people for supervising this work at various stages : Eugenio Moggi, Bob Harper, Barry Jay, Mike Fourman, Gordon Plotkin, Rod Burstall, and John Power.

I would like to thank Martin Hyland, Paul Taylor, and Bob Harper for the specific encouragement they gave at crucial moments; Doug Gurr and Barry Jay for their useful comments on the first draft; John Power for his help at the end; and John Power, Doug Gurr, and Carolyn Brown for many interesting and stimulating discussions throughout.

I would like to acknowledge the financial support of the Science and Engineering Research Council and the University of Edinburgh.

The categorical diagrams were produced using Paul Taylor’s diagram macros.

Declaration

This thesis was composed by myself and the work reported in it is my own.

Simon J. Ambler

Table of Contents

1. Introduction 8

2. Linear Logic and Quantales 15

2.1 Intuitionistic Linear Logic . . . . . . . . . . . . . . . . . . . . . . . 17 2.1.1 Structural rules . . . . . . . . . . . . . . . . . . . . . . . . . 17 2.1.2 Logical rules . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 2.1.3 The Modality “Of Course” . . . . . . . . . . . . . . . . . . . 19 2.1.4 Consequence Algebras . . . . . . . . . . . . . . . . . . . . . 20

2.2 Quantales . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 2.2.1 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 2.2.2 Quotients and Nuclei . . . . . . . . . . . . . . . . . . . . . . 28 2.2.3 Resource Semantics . . . . . . . . . . . . . . . . . . . . . . . 30

3. Symmetric Monoidal Closed Categories 33

3.1 Symmetric Monoidal Closed Categories . . . . . . . . . . . . . . . . 35

3.1.1 Monoidal Functors . . . . . . . . . . . . . . . . . . . . . . . 38 3.2 Linear Type Theory . . . . . . . . . . . . . . . . . . . . . . . . . . 40

3.2.1 Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 3.2.2 Combinators . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 Table of Contents 5

3.2.3 Type Assignment and the Calculation of Subscripts . . . . . 41 3.2.4 Derived Combinators . . . . . . . . . . . . . . . . . . . . . . 44 3.2.5 Variables and Terms . . . . . . . . . . . . . . . . . . . . . . 44 3.2.6 Equations between terms . . . . . . . . . . . . . . . . . . . . 46 3.2.7 A Normal Form for Terms . . . . . . . . . . . . . . . . . . . 47

3.3 The Interpretation of LTT in C . . . . . . . . . . . . . . . . . . . . 49

3.3.1 The category T_{0} . . . . . . . . . . . . . . . . . . . . . . . . . 50 3.4 Equational Theories in LTT . . . . . . . . . . . . . . . . . . . . . . 54

3.4.1 Monoids . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 3.4.2 Enriched Categories . . . . . . . . . . . . . . . . . . . . . . 56 3.4.3 The Theory Associated with a Category . . . . . . . . . . . 57

4. Two Examples 61

4.1 Resource Semantics in a Presheaf Category . . . . . . . . . . . . . . 62 4.1.1 Presheaves and Kripke Models . . . . . . . . . . . . . . . . . 62 4.1.2 Ends and Kan extensions . . . . . . . . . . . . . . . . . . . . 63 4.1.3 Day’s Tensor Product . . . . . . . . . . . . . . . . . . . . . 65 4.1.4 Discussion of Resources . . . . . . . . . . . . . . . . . . . . . 67

4.2 Q-sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68 4.2.1 Functional Completeness . . . . . . . . . . . . . . . . . . . . 73 4.2.2 Tensor Product and Internal Hom . . . . . . . . . . . . . . . 76 4.2.3 Reflection Theorem . . . . . . . . . . . . . . . . . . . . . . . 79

5. Monoidal Factorisation Systems 83 5.1 Factorisation Systems . . . . . . . . . . . . . . . . . . . . . . . . . . 85 Table of Contents 6

5.1.1 Subobjects . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89 5.1.2 Direct and Inverse Images . . . . . . . . . . . . . . . . . . . 90

5.2 Monoidal Factorisations . . . . . . . . . . . . . . . . . . . . . . . . 91 5.3 Factorisation in Q-Set . . . . . . . . . . . . . . . . . . . . . . . . . 92 5.4 Non-fibrewise Operations . . . . . . . . . . . . . . . . . . . . . . . . 96

5.4.1 Fusion from Tensor Product . . . . . . . . . . . . . . . . . . 96 5.4.2 The Category Sqr (M) . . . . . . . . . . . . . . . . . . . . . 98 5.4.3 Linear Implication by Pullback . . . . . . . . . . . . . . . . 100

5.5 Algebraic Limitations . . . . . . . . . . . . . . . . . . . . . . . . . . 105 5.5.1 The Beck Chevalley Condition . . . . . . . . . . . . . . . . . 107

6. First Order Linear Logic 109 6.1 Formulae and Sequents . . . . . . . . . . . . . . . . . . . . . . . . . 112 6.2 Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113

6.2.1 Structural Rules . . . . . . . . . . . . . . . . . . . . . . . . . 113 6.2.2 Logical Rules . . . . . . . . . . . . . . . . . . . . . . . . . . 113

6.3 Properties of the Calculus L_{F OLL} . . . . . . . . . . . . . . . . . . . 116 6.3.1 Theorems and Derivations in L_{F OLL} . . . . . . . . . . . . . 117 6.3.2 Predicates on a Monoid . . . . . . . . . . . . . . . . . . . . 121 6.3.3 Girard’s Double Negation Closure . . . . . . . . . . . . . . . 123

7. Model Theory 125

7.1 Linear Doctrines . . . . . . . . . . . . . . . . . . . . . . . . . . . . 126 7.1.1 Fibrations . . . . . . . . . . . . . . . . . . . . . . . . . . . . 126 7.1.2 Linear Doctrines . . . . . . . . . . . . . . . . . . . . . . . . 130 Table of Contents 7

7.2 Soundness of the calculus L_{F OLL} . . . . . . . . . . . . . . . . . . . 132

7.2.1 Interpretation of formulae . . . . . . . . . . . . . . . . . . . 133 7.3 Completeness of L_{F OLL} . . . . . . . . . . . . . . . . . . . . . . . . . 139

7.3.1 The fibre category P_{0} and the functor z_{0} : P_{0} → T_{0} . . . . . 140 8. Conclusions and Further Work 144 Bibliography 150

Chapter 1

Introduction

Logic is a key tool in the theoretical analysis of computer science and the diversity of computational phenomena leads to a profusion of logical systems : first order, higher order, and equational logic are used in program specification; temporal, dynamic and modal action logics arise in the analysis of system behaviour; type theory and the λ-calculus form the basis of functional programming; and there are many other examples of importance.

Recently, there has been considerable interest in developing a ‘logical framework’ in which these logics can be represented in a uniform way. The Edinburgh LF [HHP87], Martin Löf type theory [ML84], and the Isabelle proof environment [Pau89] are examples of such a framework, which all classify logics according to their proof theory. This thesis forms part of a complementary line of research, being undertaken at Edinburgh, which aims to provide a uniform representation of logics through their model theory. Traditionally, the model theoretic approach to logic has been more popular, but there has been little work on general model theoretic frameworks for logic. The ‘abstract model theory’ of Barwise [Bar74] is limited to the theories of classical logic; whereas the ‘institutions’ of [BG84] give a uniform understanding of the relationship between theories and models in an arbitary logic, but no analysis of the structure of models. It is therefore not immediately clear what a model theoretic framework should be. As is often the case, category theory provides a convenient language in which to formulate the problem and evaluate ideas. There are numerous categorical studies of specific first and higher order logics in which the models are presented as fibred categories with certain extra structure depending on the logic [MR77,See83,HJP80,See87a]. It is reasonable to suppose that fibred categories could form the basis of a general framework, and this is the view adopted by the Edinburgh group. The aim of this thesis is to gain further insight by studying another specific example; one which is of natural interest in computer science, yet is problematic enough to pose a challenge to the fibred category paradigm.

Linear logic [Gir87a] is the weakest of the family of relevance logics and provides the most discerning analysis of entailment so far. Its simplicity and elegance make it a natural vehicle for research, and it seems clear that a logic with such good structural properties should have many applications. Furthermore, linear logic lies close to many of the concerns which are important in computer science. In particular, it can be used to describe the properties of systems which change as they are observed (the necessary algebraic semantics were originally proposed in the context of quantum mechanics), and thus some of the most successful applications so far have been in the theory of concurrency. Linear logic has been employed to capture both the compositional properties [Dam88,Dam90] and the evolutional properties [AV90] of processes in Milner’s CCS [Mil89]. It has also been used to describe the behaviour of Petri nets [Bro90].

Interest in linear logic has generated a number of new ideas in the theory of programming languages. Girard, Scedrov and Scott [GSS] give a type system based on bounded linear logic in which an algorithm is typable if and only if it is computable in polynomial time. Lafont [Laf88] defines the linear abstract machine, an execution mechanism for the proof terms of intuitionistic linear logic. This simple model of functional programming can operate without garbage collection because storage is handled explicitly at the level of types. Abramsky [Abr90] takes this further, proposing that the proof terms of second order classical linear logic could form the basis of a full polymorphic functional programming language in which execution is both concurrent and without garbage collection. There is also work on logic programming in linear logic [HP,HM91].

Girard [Gir87b] describes linear logic as a logic of action. Whereas classical and intuitionistic logic are concerned with stable truth, the nature of linear ‘facts’ is transient and depends upon the internal state of a dynamic system. This is illustrated by the simple example of buying a packet of cigarettes. Let ϕ, ψ, θ denote the following linear facts :

ϕ = to have $1
ψ = to have a packet of Camels
θ = to have a packet of Marlboro

A proof of the linear implication ϕ −∘ ψ is given by the action of spending $1 and buying a packet of Camels. Thus linear implication involves a principle of conservation of resource. There are two distinct forms of conjunction in linear logic. The meet (ψ ∧ θ) corresponds to the possibility of having a packet of one or other brand of cigarette, and the fusion (ψ ∘ θ) corresponds to actually having two packets. The difference between them is illustrated by the fact that ϕ −∘ (ψ ∧ θ) is provable, since given $1 we can buy either a packet of Camels or Marlboro, but ϕ −∘ (ψ ∘ θ) is not, since we cannot use $1 to buy two packets^{1}.

Given the shift of perspective between linear logic and its forbears, it is unclear to what extent the categorical ideas developed for classical and intuitionistic logic apply in the linear case. Makkai and Reyes [MR77] give a categorical account of models of first order theories in classical logic. In this approach, the types and functions of a logic are modelled by the objects and morphisms of a category C while the formulae are modelled by ‘subobjects’ in C. The subobjects of an object A form a partial order Sub(A) corresponding to the formulae ϕ with a free variable x of ‘type’ A. Pullback along a morphism f : A → B in C gives rise to a functor f^{∗} : Sub(B) → Sub(A). This models the operation of substitution which maps a formula ψ with free variable y of type B to the formula ψ[f(x)/y] with free variable x of type A. If f^{∗} has left and right adjoints then these can be interpreted as forms of existential and universal quantification respectively. This fundamental observation is due to Lawvere [Law69,Law70].

1The author is inclined to save his $’s and leave both packets on the shelf.

The subobjects as a whole form a fibred category with base C [Gra66] in which the fibre over an object A is Sub(A). The two main ingredients of categorical model theory are therefore a base category C which forms the theory of types and functions, and a fibred category of subobjects whose objects represent predicates over these types. Given a category C whose structure is sufficiently rich, we may adopt it as our ‘type theory’ and attempt a logical investigation of its subobjects. The logic thus obtained is the ‘internal logic’ of C. In order to carry out our programme, we need structured categories for which first order linear logic is the internal logic.

A version of first order linear logic appears in Seely’s paper [See87b]. He treats first order linear logic as propositional linear logic ‘indexed over’ a category C with finite limits. In that view, the connectives are taken as primitive and not related to any property of C. Consequently, the only real models of this kind are given by construction [See90]. If, however, first order linear logic is to arise naturally from the subobjects of a category C then there must be some structure on C which allows the connectives to be defined. Specifically, the fusion of predicates should arise from a tensor product on C and the linear implication from the corresponding internal hom. We therefore take the overall structure of C to be that of a symmetric monoidal closed category, and define a modified version of first order linear logic whose models are given by the subobject structure of such categories.

The importance of symmetric monoidal closed categories as type theories is already well established in the context of enriched category theory [Kel82]. Here an arbitary such category V takes the place of Set as the ambient universe. Jay [Jay89a,Jay90] has considered an internal language of types and functions for monoidal categories. This language can be used to simplify proofs in enriched category theory by allowing diagramatic arguments to be replaced by simple type theoretic ones. We shall use it as the type theoretic basis for our logic.

Many of the nice algebraic properties of the categories studied by Makkai and Reyes stem from the fact that there is a good interaction between limit and colimit structure. We cannot hope for such a good situation. In linear logic the failure of meet to distribute over join is precisely the failure of this kind of neat interaction.

The logic of symmetric monoidal closed categories has several disturbing features. We shall see that substitution fails to permute with the logical connectives. The logic that we develop is therefore equipped with explicit substitution operators. These act very much like the additive connectives and there are various distributive and half-distributive laws which hold.

This analysis tells us three things about general model theoretic frameworks for classifying logics. First, there is an advantage in considering fibrations over indexed categories: the definition of a linear doctrine refers to the closure of the category of predicates as a whole, and so could not have been so conveniently expressed in terms of indexed categories. Secondly, there is a need for categories with added structure specified in terms of functors, natural transformations, and coherences; rather than categories with structure specified only by universal properties such as cartesian closed categories or elementary topoi. Lastly, as the logical connectives are not preserved by substitution, one must allow the possibility of making substitution explicit.

Other work on linear logic has focussed on its elegant proof theory, as this provided the original motivation for the logic, and there has been considerable work on the categorical semantics of linear proofs [See87b,dP89,BG90]. That work is concerned with the idea that the propositions and proofs of a (constructive) logic can be modelled by the objects and arrows of a suitable category, and is motivated by the celebrated ‘Curry Howard isomorphism’ between the normal form proofs of intuitionistic logic and the free cartesian closed category generated by the atomic propositions [LS86, part I]. The ‘semantics of proofs’ given by such work are in contrast to the model theoretic semantics developed here.

In chapter 2, we recall the theory of propositional linear logic. An elementary algebraic semantics is given in terms of ‘consequence algebras’ which we define here. The second half of the chapter deals with the class of consequence algebras which are lattice theoretically complete. These are known in the literature as ‘commutative quantales with unity’. Examples are given and the important features of the theory of quantales are reviewed. Finally, we elucidate the notion of resource which is implicit in linear logic by developing an abstract resource semantics similar to the semi-lattice semantics for relevance logic.

In chapter 3, we introduce the concept of a symmetric monoidal closed category together with some standard examples. We use this to motivate our definition of the linear type theory LTT. This is based on Jay’s language for monoidal categories [Jay89a], and comprises a system of types, combinators, and terms with restrictions on the occurrence of variables. We define the interpretations of an equational theory in LTT, and show that there is an initial model of such theories.

In chapter 4, we give two examples of symmetric monoidal closed categories that arise naturally from a consideration of linear logic. These are linear analogues of presheaf topoi and Heyting valued sets respectively, both of which have been developed independently and with different motivation in the theory of enriched categories.

In chapter 5, we introduce the minimal structure required to derive first order linear logic in a symmetric monoidal closed category. Both of the examples of chapter 4 have such structure. We take the notion of subobject to be relative to a factorisation system (E, M) on C where M is a class of monomorphisms. We then define algebraic operations on these subobjects that correspond to the logical connectives. We assume that C is sufficiently complete and cocomplete that the M-subobjects of an object A form a lattice Sub_{M}(A). The additive connectives are interpreted by the lattice theoretic operations. The multiplicatives are defined in terms of the symmetric monoidal closed structure of C, so we restrict to categories in which the factorisation system (E, M) is monoidal, i.e. behaves well with respect to the tensor product. The multiplicatives are non-fibrewise operations, so rather than acting on a single fibre, they give families of maps

∘_{A,B} : Sub_{M}(A) × Sub_{M}(B) → Sub_{M}(A ⊗ B)
−∘_{A,B} : Sub_{M}(A) × Sub_{M}(B) → Sub_{M}([A, B])

In theorem 5.4.5 we show that, despite their non-fibrewise nature, fusion and linear implication are related by an adjunction generalising that of the propositional case. The situation described above is quite general so there are many examples. The category Ab of abelian groups demonstrates many of the pathologies that can occur, and motivates many of the design decisions made about the form of the logic L_{F OLL}.

In chapter 6, we give a sequent calculus presentation of the logic L_{F OLL} which is built over the type theory LTT. Formulae are constructed by applying linear predicates to the terms of LTT. Sequents Γ ⊢ ϕ(t) are subject to a variable balancing condition which says that every variable which appears has exactly one occurence on each side of the turnstile. The introduction rules for the logical connectives appear as decorated forms of the corresponding rules in the propositional logic. There are also rules for the substitution operators and existential quantification. Many of the rules have side conditions to prevent the arbitary permutation of substitution with the other operations. We give some examples of derivable sequents and present two small applications.

Finally in chapter 7, we present the model theory of L_{F OLL} in terms of fibred categories. We define a notion of linear doctrine which adequately captures the categorical properties of the M-subobjects of a monoidal factorisation system (E, M) in C, so that every category with such structure gives rise to a linear doctrine. We define an interpretation of the formulae and sequents of L_{F OLL} in a linear doctrine and prove that the rules of L_{F OLL} are sound with respect to such interpretations. We also prove a completeness result by constructing a linear doctrine from the syntax of L_{F OLL}.

We assume a knowledge of the basic definitions of category theory; such as category, functor, natural transformation, and adjunction ; all of which can be found in Mac Lane’s book [ML71]. Some knowledge of indexed categories and fibrations would also be useful; see [Gra66] or [Tay86]. Other concepts will be introduced, as necessary, in the main text.

Linear Logic and Quantales

Girard [Gir87a]  This thesis
times ⊗ fusion ∘
(non-commutative) &
with  &  meet  ∧
plus  ⊕  join  ∨
par  ‘&’ inverted par  ⊕
entails  −∘  entails  −∘

Linear logic was introduced by Girard [Gir87a]. It is essentially a logic derived from proof theoretic consideration of Gentzen’s sequent calculi LJ and LK [Gen69]. An interesting discussion of linear logic and the philosophical ideas that surround it can be found in the first paper of the “Geometry of Interaction” series [Gir87b]. Girard notes that both the undecidability and nonconstructive nature of the classical predicate calculus LK can be traced back to the structural rule of contraction.

(weakening) \frac{Γ_{1}, Γ_{2} ⊢ ψ}{Γ_{1}, ϕ, Γ_{2} ⊢ ψ}  (contraction) \frac{Γ_{1}, ϕ, ϕ, Γ_{2} ⊢ ψ}{Γ_{1}, ϕ, Γ_{2} ⊢ ψ}  (2.1)

It is therefore natural to consider logics without this rule, and this had already been suggested by Ono and Kormori [OK85].

Relevance logicians have considered logics without weakening. The effect of this restriction is to stop the introduction of spurious or non-causal dependencies between assumptions and conclusion. If a proposition appears as an assumption then it is essential in deducing the conclusion. There is a large family of relevance logics. These logics often accept contraction and the distributivity of meet over join. Urquhart [Urq84] has shown that this is sufficient to make even the propositional logic undecidable.

In linear logic, both weakening and contraction are abandoned. This means that it actually matters how many times a proposition is asserted. In this way, a linear implication is analogous to a chemical equation where the various proportions of the reactants matter. In fact, Girard gives the combustion of hydrogen as the following linear implication.

(H_{2} ∘ H_{2} ∘ O_{2}) −∘ (H_{2}O ∘ H_{2}O)  (2.2)

There is a conservation principle acting between the two sides of a linear implication, and we therefore say that linear logic is resource bounded.

Linear logic has a number of pleasant features. In the fragment without modal operators, it is both relevant and constructive, the predicate logic is decidable, and there is a cut elimination algorithm executable in linear time.

The logic presented in [Gir87a] is often called classical linear logic because it features an involutive ‘negation’ reminiscent of that of classical logic. This thesis is essentially concerned with the nonstandard conjunction ∘ and the problems that arise from it. It is therefore appropriate to work with intuitionistic linear logic.

In section 2.1, we define propositional intuitionistic linear logic together with an appropriate algebraic semantics given in terms of consequence algebras. We prove that the latter is sound and complete with respect to the former. In section 2.2, we define quantales as the consequence algebras which are lattice theoretically complete. We give some examples, and review their basic theory. We also define a resource semantics for propositional intuitionistic linear logic similar to the semilattice semantics for relevance logic given by Urqhart [Urq72].

2.1 Intuitionistic Linear Logic

Let A = {p_{1}, p_{2}, …, p_{n}, …} be a countably infinite list of atomic propositions. The set F of formulae ϕ of intuitionistic linear logic is given by the following BNF grammar.

ϕ ::= 0 | 1 | ⊤ | p_{n} | ϕ_{1} ∘ ϕ_{2} | ϕ_{1} −∘ ϕ_{2} | ϕ_{1} ∧ ϕ_{2} | ϕ_{1} ∨ ϕ_{2}  (2.3)

If Γ is a finite list of formulae, possibly empty, and ϕ is a single formula then Γ ⊢ ϕ is a sequent of intuitionistic linear logic. The valid sequents are those derived using the rules of inference given in the next two sections.

2.1.1 Structural rules

The following rules operate on the structure of derivations.

(ref)  \overline{ϕ ⊢ ϕ}
(ex)  \frac{Γ_{1}, ϕ, ψ, Γ_{2} ⊢ θ}{Γ_{1}, ψ, ϕ, Γ_{2} ⊢ θ}
(cut) \frac{Γ_{1}, ϕ ⊢ ψ  Γ_{2} ⊢ ϕ}{Γ_{1}, Γ_{2} ⊢ ψ}

The additional structural rules of weakening and contraction given in Gentzen’s sequent calculus LJ for intuitionistic logic [Gen69] are not allowed.

Avron [Avr87] states the three rules above as the definition of a ‘consequence relation’. This is a generalisation of the original definition given by Scott [Sco74] which included both weakening and contraction, but is still slightly too restrictive because there are logics without the exchange rule, eg. the non-commutative linear logic of Yetter [Yet90].

Note that the cut rule is slightly simplified in the presence of exchange because we can assume that the cut formula is adjacent to the turnstile. Similar simplifications occur in the logical rules below. In non-commutative linear logic, the order of the formulae is critical and the rules are more complex as a result.

2.1.2 Logical rules

The logical rules allow the introduction of constants and connectives in a sequent derivation. They are classified as either left or right rules, depending on which side of the turnstile the introduction occurs.

The constants and connectives of linear logic are divided into two classes which, on the basis of the coherence space semantics, Girard has named the multiplicatives and the additives. In relevance logic, these classes are termed intensional and extensional respectively.

Multiplicative Connectives

(1 l) \frac{Γ ⊢ ϕ}{Γ, 1 ⊢ ϕ}  (1 r) \overline{⊢ 1}
(∘l) \frac{Γ, ϕ, ψ ⊢ θ}{Γ, ϕ ∘ ψ ⊢ θ}  (∘r) \frac{Γ_{1} ⊢ ϕ  Γ_{2} ⊢ ψ}{Γ_{1}, Γ_{2} ⊢ ϕ ∘ ψ}
( −∘ l) \frac{Γ_{1} ⊢ ϕ Γ_{2}, ψ ⊢ θ}{Γ_{2}, ϕ −∘ ψ, Γ_{1} ⊢ θ}  ( −∘ r) \frac{Γ, ϕ ⊢ ψ}{Γ ⊢ ϕ −∘ ψ}

Additive Connectives

(0) \overline{Γ, 0 ⊢ ϕ}  (⊤) \overline{Γ ⊢ ⊤}

\begin{matrix}(∧l1) & \frac{Γ, ϕ ⊢ θ}{Γ, ϕ ∧ ψ ⊢ θ} \\ (∧l2) & \frac{Γ, ψ ⊢ θ}{Γ, ϕ ∧ ψ ⊢ θ} \end{matrix}  (∧r) \frac{Γ ⊢ ϕ Γ ⊢ ψ}{Γ ⊢ ϕ ∧ ψ}

(∨l) \frac{Γ, ϕ ⊢ θ Γ, ψ ⊢ θ}{Γ, ϕ ∨ ψ ⊢ θ}  \begin{matrix}(∨r1) & \frac{Γ ⊢ ϕ}{Γ ⊢ ϕ ∨ ψ} \\ (∨r2) & \frac{Γ ⊢ ψ}{Γ ⊢ ϕ ∨ ψ} \end{matrix}

The crucial difference between the multiplicatives and the additives lies in the way in which their introduction rules handle the side formulae or contexts. For example, in (∘r) the contexts Γ_{1} and Γ_{2} appearing in the premise are combined to give Γ_{1}, Γ_{2} in the conclusion, whereas in (∧r) the conclusion has the same context as the premises. These differences are not significant in intuitionistic logic because, in the presence of weakening and contraction, the two forms of conjunction are interderivable.

2.1.3 The Modality “Of Course”

Girard’s calculus also includes the modal operator “of course” which takes a formula ϕ to the modal formula !ϕ. The effect of ! is to reintroduce weakening and contraction in a controlled manner by restricting their use to modal formulae. It has the following sequent rules.

(!l) \frac{Γ, ϕ ⊢ ψ}{Γ,!ϕ ⊢ ψ}  (!r) \frac{!Γ ⊢ ψ}{!Γ ⊢!ψ}
(weakening) \frac{Γ ⊢ ψ}{Γ,!ϕ ⊢ ψ}  (contraction) \frac{Γ,!ϕ,!ϕ ⊢ ψ}{Γ,!ϕ ⊢ ψ}

where !Γ denotes a finite sequence of formulae of the form !ϕ_{1}, …,!ϕ_{n}.

The “of course” modality gives linear logic the expressive power of intuitionistic logic, since intuitionistic implication can be defined as ϕ ⊃ ψ =!ϕ −∘ ψ ^{1}. However, it is inessential to the main thrust of this thesis, so we exclude it from the basic logic.

2.1.4 Consequence Algebras

We define the notion of ‘consequence algebra’ and use it to give an algebraic semantics for the basic connectives of intuitionistic linear logic. This is similar to the Heyting algebra semantics for intuitionistic logic.

Definition 2.1.1 A consequence algebra is a structure ⟨L, ∨, 0, ∧, ⊤, ∘, 1, −∘ ⟩ where ⟨L, ∨, 0, ∧, ⊤⟩ is a lattice, ⟨L, ∘, 1⟩ is a commutative monoid, and −∘ is a binary operation on L; such that for all x, y, z ∈ L

y ≤ z ⇒ x ∘ y ≤ x ∘ z  (2.4)

and

x ∘ y ≤ z ⟺ x ≤ y −∘ z  (2.5)

In the terminology of [Bir48], the operation −∘ is called residuation and a consequence algebra is a residuated multiplicative lattice in which the multiplication is commutative and has a unit.

A Heyting algebra is a consequence algebra in which ∘ = ∧ and 1 = ⊤. Other examples include de Morgan monoids, and the rational numbers between 0 and 1 under multiplication. In the next section, we consider ‘quantales’ which are consequence algebras whose underlying lattice is complete.

1In [Gir87a], Girard gives a sound interpretation of intuitionistic logic in linear which is based on this translation.

Proposition 2.1.2 The following identities (inequalities) hold in any consequence algebra A.

(x ∘ y) −∘ z = x −∘ (y −∘ z)  (2.6)
x ∘ (y ∨ z) = (x ∘ y) ∨ (x ∘ z)  (2.7)
x −∘ (y ∧ z) = (x −∘ y) ∧ (x −∘ z)  (2.8)
(x ∨ y) −∘ z = (x −∘ z) ∧ (y −∘ z)  (2.9)
(x −∘ y) ∘ (y −∘ z) ≤ (x −∘ z)  (2.10)
(u −∘ v) ∘ (x −∘ y) ≤ (u ∘ x) −∘ (v ∘ y)  (2.11)

Proof. These all follow routinely from the definition. We take 2.9 as an illustration.

First, since fusion is order preserving

x ∘ [(x ∨ y) −∘ z] ≤ (x ∨ y) ∘ [(x ∨ y) −∘ z] ≤ z

where the second inequality follows immediately from 2.5. Thus (x ∨ y) −∘ z is less than or equal to x −∘ z and similarly less or equal to y −∘ z. It follows that

(x ∨ y) −∘ z ≤ (x −∘ z) ∧ (y −∘ z)

In the other direction, we have

(x −∘ z) ∧ (y −∘ z) ≤ x −∘ z

Using two applications of 2.5 together with the commutativity of fusion, we can swap the positions of x and (x −∘ z) ∧ (y −∘ z) and so obtain

x ≤ [(x −∘ z) ∧ (y −∘ z)] −∘ z

As the same argument applies to y, we deduce that

x ∨ y ≤ [(x −∘ z) ∧ (y −∘ z)] −∘ z

and hence that (x −∘ z) ∧ (y −∘ z) ≤ (x ∨ y) −∘ z as required. □

An interpretation of intuitionistic linear logic in a consequence algebra L is a function [[−]] : F → L which sends each of the logical constants and connectives to the corresponding algebraic operation on L. Thus [[1]] = 1, [[ϕ ∘ ψ]] = [[ϕ]] ∘ [[ψ]], [[ϕ ∧ ψ]] = [[ϕ]] ∧ [[ψ]], and so on. An interpretation [[−]] can be extended to a list of formulae by defining [[ ]] = 1 and [[Γ, ϕ]] = [[Γ]] ∘ [[ϕ]]. A sequent Γ ⊢ ϕ is true in the interpretation [[−]] : F → L if [[Γ]] ≤ [[ϕ]].

Theorem 2.1.3 Intuitionistic linear logic is sound and complete with respect to the consequence algebra semantics.

Proof. Soundness is straightforward. For completeness, we consider equivalence classes of formulae in the logic under the relation ≡ where ϕ ≡ ψ holds if both ϕ ⊢ ψ and ψ ⊢ ϕ are derivable sequents. These form a consequence algebra L and the function [[−]] : F → L which maps each formula to its equivalence class yields an interpretation of intuitionistic linear logic such that Γ ⊢ ϕ is derivable if and only if [[Γ]] ≤ [[ϕ]]. Thus, if Γ ⊢ ϕ is true in every interpretation then [[Γ]] ≤ [[ϕ]] holds in L and Γ ⊢ ϕ is derivable. □

2.2 Quantales

Recall [Joh82] that a locale is a complete lattice in which finite meets distribute over arbitrary joins. Locales provide an algebraic semantics for propositional intuitionistic logic, but also form the basis of the theory of sheaves and hence the algebraic treatment of higher order intuitionistic logic (see [FS79,LS86]).

Quantales are a generalisation of locales which were introduced by Mulvey [Mul86] in an attempt to provide a constructive formulation of the foundations of quantum mechanics. The idea was to represent the sequencing of time using a non-commutative version of conjunction. Mulvey defined a quantale to be a complete lattice with an associative binary operation & which distributes over suprema on both sides. The product p & q should be read as “p holds and then q holds”.

Subsequently, Borceux and Van Den Bossche [BVDB85] extended the proof of the Gelfand-Naimark representation theorem, that every C^{∗}-algebra is isomorphic to the object of complex numbers in a suitable topos, to the non-commutative case by using quantales. Here, the motivating example of a quantale is the lattice of closed right ideals of a non-commutative C^{∗}-algebra. This has the additional properties that multiplication is idempotent and the top element is a right unit.

These very strong assumptions allow a large part of the theory of locales to be lifted to a non-commutative setting, and Borceux and Van Den Bossche have exploited this in a series of papers. In [BVDB85], they define quantum spaces, a variant of topological spaces in which the intersection of open sets is replaced by a noncommutative multiplication, and demonstrate a duality between the category of ‘sober’ quantum spaces and quantales ‘with enough points’. In [BVDB86] they give a notion of ‘quantic sheaf ’.

Joyal and Tierney initiated the study of commutative quantales in [JT84]. They observed that many interesting properties of locales can be studied in the more general setting of ‘commutative monoids in the category of complete semilattices’ (commutative quantales with unity). There is a strong parallel between such monoids and rings. In particular, Joyal and Tierney show that commutative quantales have a theory of ‘modules’ similar to that for rings.

Mulvey’s formulation of quantales does not require & to have a unit. From a logical point of view this is an omission, because the unit determines which elements of the quantale are considered to represent ‘truths’. An element a of Q is said to be valid or designated if 1 ≤ a .

The assumption of idempotency is also undesirable from our point of view because it includes the logical principle of contraction. We shall concentrate on commutative non-idempotent quantales and refer to [Yet90] for an account of the quantale semantics of non-commutative linear logic.

Definition 2.2.1 A commutative quantale with unity is a structure ⟨Q, ≤, ∘, 1, 0, ⊤⟩ where ⟨Q, ≤, 0, ⊤⟩ is a complete lattice, ⟨Q, ∘, 1⟩ is a commutative monoid and ∘ distributes over suprema, ie.

a ∘ ( ⋁_{i∈S} b_{i}) = ⋁_{i∈S}(a ∘ b_{i})  (2.12)

The multiplication ∘ is called fusion in the tradition of relevance logic. Notation 2.2.2 Henceforth, ‘quantale’ will mean ‘commutative quantale with unity’.

A quantale homomorphism is a function f : Q → Q′ which preserves 1, ∘ and suprema. Let CQuant denote the category of quantales and quantale homomorphisms.

We note that a quantale Q is necessarily a consequence algebra via :

a −∘ b = ⋁{x|x ∘ a ≤ b}  (2.13)

In categorical terms, the functor (−) ∘ b from Q to Q preserves colimits and so, since the solution set condition is trivial for partial orders, has a right adjoint b −∘ (−).

Conversely, if Q is consequence algebra whose underlying lattice is complete then Q is a quantale, because the existence of a right adjoint b −∘ (−) ensures that the functor (−) ∘ b preserves colimits.

2.2.1 Examples

We know that every locale is a quantale with the multiplication given by binary meet. There are, however, many other forms of quantale. The examples in this section have been chosen to demonstrate their wide diversity and some of the possible pathologies.

Power Set of a Monoid

Let ⟨M, ·, e⟩ be a commutative monoid. The complete lattice ⟨℘(M), ⊆⟩ forms a quantale P(M) with X ∘Y = XY = {xy|x ∈ X, y ∈ Y } and 1 = {e}. The residual X −∘ Y = {z ∈ Q|∀x ∈ X . xz ∈ Y } is denoted X\Y.

In fact P(M) is the free quantale on the monoid M.

3-Valued Logic

The behaviour of fusion on the elements 0 ≤ 1 ≤ ⊤ is determined by the definitions: x ∘ 0 = 0 since 0 is the sup of the empty set, ⊤ is idempotent since ⊤ = ⊤ ∘ 1 ≤ ⊤ ∘ ⊤, and x ∘ 1 = x since 1 is the unit for ∘.

\begin{matrix}∘ & 0 & 1 & ⊤ \\ 0 & 0 & 0 & 0 \\ 1 & 0 & 1 & ⊤ \\ ⊤ & 0 & ⊤ & ⊤ \end{matrix}  \begin{matrix}−∘ & 0 & 1 & ⊤ \\ 0 & ⊤ & ⊤ & ⊤ \\ 1 & 0 & 1 & ⊤ \\ ⊤ & 0 & 0 & ⊤ \end{matrix}  (2.14)

The quantale consisting of the three elements 0 ≤ 1 ≤ ⊤ with the induced multiplication has been used by Routley and Meyer as the basis of their three valued relevance logic (see [AB75]). We denote it RM3.

Additive Subgroups of a Commutative Ring

The subgroups of a group ordered by inclusion form a complete lattice with ⋀_{γ∈I} X_{γ} = ∩_{γ∈I}X_{γ} and ⋁_{γ∈I} X_{γ} = {Σ_{1≤i≤n}x_{i}|x_{i} ∈ ∪_{γ∈I}X_{γ}}. Let ⟨R, +, 0, ×, 1⟩ be a commutative ring, and consider subgroups of ⟨R, +, 0⟩. We can define a multiplication of subgroups as follows.

X ∘ Y = {Σ_{1≤i≤n}(x_{i} × y_{i})|x_{i} ∈ X, y_{i} ∈ Y }  (2.15)

The subgroup generated by {1} is a unit for this multiplication (its elements are known as the integers of R). As ∘ is clearly monotone we need only check that X ∘ ⋁_{γ∈I} Y_{i} ≤ ⋁_{γ∈I}(X ∘ Y_{i}).

Suppose that z ∈ X ∘ ⋁_{γ∈I} Y_{i}, then z is a finite sum of terms x × Σ_{1≤j≤m}y_{j} where x ∈ X and y ∈ ∪_{γ∈I}Y_{γ}. By distributivity, this is just a finite sum of terms x × y where y ∈ Y_{γ} ie. an element of ⋁_{γ∈I}(X ∘ Y_{i}).

Similarly, the ideals of R form a quantale Idl(R).

Flat Quantales

Let ⟨M, ·, e⟩ be a commutative monoid, and let L be the complete lattice whose underlying set is M ∪ {0, ⊤} and whose order is defined as

x ≤ y ⟺ x = y or x = 0 or y = ⊤  (2.16)

We can extend the multiplication on M to produce a monotone operation on L as follows.

x ∘ y = \{ \begin{matrix}x · y & if x, y ∈ M \\ 0 & if x = 0 or y = 0 \\ ⊤ & otherwise \end{matrix}  (2.17)

Now, suppose that ⟨M, ·, e⟩ is a commutative cancellation monoid. That is, for all x, y ∈ M there is at most one z ∈ M such that xz = y. We can define linear implication as follows.

x −∘ y = \{ \begin{matrix}⊤ & if x = 0 or y = ⊤ \\ z & if x, y ∈ M and x · z = y \\ 0 & otherwise \end{matrix}  (2.18)

It is easy to check that x −∘ (−) is right adjoint to (−) ∘ x, from which it follows that ⟨M ∪ {0, ⊤}, ∘, e, ≤⟩ is a quantale. We call it the flat quantale on M and denote it F(M). The three element quantale RM3 is the flat quantale on the trivial monoid.

Recall that an element of a quantale is said to be designated if it is greater than or equal to the unit, and that the designated elements are intended to represent linear ‘truths’. It is interesting to note that if G is a non-trivial abelian group then for any element a ≠ e we have that aa^{−1} = e is a designated element of F(G) despite the fact that neither a nor a^{−1} is designated. In terms of linear logic, we have a conjunction which is valid as a whole without either of its conjuncts being valid.

Ordinal examples

An ordinal is a set whose elements are well ordered by membership. For any ordinal α let O_{α} be the set α + 1 = α ∪ {α} with the opposite of the membership order. This is a complete lattice with the supremum of S ⊆ O_{α} given by the least element of S with respect to the order of α + 1. Fusion is based on ordinal addition.

β ∘ γ = min{β + γ, α}  (2.19)

The distributivity is derived from the well-ordering of α + 1 as follows.

β ∘ ⋁_{i∈I} γ_{i} = min{β + min_{i∈I}(γ_{i}), α}  (2.20)
= min{min_{i∈I}(β + γ_{i}), α}  (2.21)
= min_{i∈I}(min{β + γ_{i}, α})  (2.22)
= ⋁_{i∈I}(β ∘ γ_{i})  (2.23)

In general, there is very little we can say about the relationship between fusion and meet. The ordinal examples illustrate the fact that fusion might not distribute over infs of chains. For example, consider the descending chain 1 ≥ 2 ≥ … ≥ n ≥ … in O_{2ω}. We have ⋀_{n∈ω} 1 ∘ n = ω but 1 ∘ ⋀_{n∈ω} n = ω + 1.

Reals with ∞

Let [0, ∞] be the ordered set of non-negative reals together with a maximum element ∞ and let [0, ∞]^{op} be the same set with the opposite order. Addition is extended to ∞ by defining x + ∞ = ∞ for all x. Every subset of [0, ∞] has an infimum by the elementary properties of the reals, so [0, ∞]^{op} is a complete lattice. Furthermore it is residuated

x + y ≥ z ⟺ x ≥ y ˙−z  (2.24)

where ˙− denotes truncated subtraction given by :

a ˙−b = \{ \begin{matrix}a − b & if b ≤ a \\ 0 & otherwise \end{matrix}  (2.25)

Thus ℜ = ⟨[0, ∞]^{op}, +, 0⟩ is a quantale. Note that the function x ↦ 2^{−x} is an isomorphism of quantales between ℜ and ⟨[0, 1], ≤, ×, 1⟩.

2.2.2 Quotients and Nuclei

In this section, we review some basic results in the theory of quantales.

Recall [Bir48] that a closure (resp. co-closure) operation on a complete lattice L is an order preserving function c : L → L which is increasing (resp. decreasing) and idempotent. That is, x ≤ c(x) (resp. c(x) ≤ x) and c(c(x)) = c(x). We say that an element x of L is c-closed if c(x) = x, or equivalently if x lies in the image of c.

Definitions 2.2.3

1. A quantic nucleus on a quantale Q is a closure operation j : Q → Q such

that for all x, y ∈ Q

j(x) ∘ j(y) ≤ j(x ∘ y)  (2.26)

2. A quantic conucleus on Q is a co-closure operation h : Q → Q such that for all x, y ∈ Q

1 ≤ h(1)  (2.27)
h(x) ∘ h(y) ≤ h(x ∘ y)  (2.28)

In the terminology of the next chapter, quantales are a particular form of symmetric monoidal category and the conditions 2.26, 2.27 and 2.28 say that nuclei and conuclei are monoidal functors. Of course, the condition on a nucleus j which corresponds to 2.27 is already given by the fact that j is increasing.

The following result gives an easy way to identify quantic nuclei.

Lemma 2.2.4 [NR88] A function j : Q → Q is a quantic nucleus if and only if x −∘ j(y) = j(x) −∘ j(y) for all x, y ∈ Q.

Quantic nuclei are important in that they give a way of constructing new quantales from old.

Lemma 2.2.5 [NR88] The image Q_{j} of a quantic nucleus j : Q → Q forms a quantale with 1′ = j(1), x ∘′ y = j(x ∘ y), and ⋁′_{i∈I} x_{i} = j(⋁_{i∈I} x_{i}).

The meet of a family of j-closed elements in Q is again j-closed, so infima in Q_{j} coincide with those of Q. This is also true for linear implications.

Clearly, we can regard a quantic nucleus j : Q → Q as a surjective map of quantales from Q to Q_{j}. Moreover, every surjective map of quantales e : Q → Q′ is isomorphic to one produced in this way. Since e preserves suprema it has a right adjoint e′ : Q′ → Q defined by

e′(y) = ⋁{x|e(x) = y}  (2.29)

Let j : Q → Q be the composite e′e. It is not difficult to show that j is a quantic nucleus and that e factors through j : Q → Q_{j} by an isomorphism Q_{j} ≅ Q′.

Thus, the image Q_{j} of a quantic nucleus j is called a quantic quotient. The following lemma allows us to readily identify such quotients.

Lemma 2.2.6 [NR88] A subset S of the quantale Q is a quantic quotient if and only if S is closed under ⋀ and x −∘ s ∈ S whenever x ∈ Q and s ∈ S.

We note from [Ros90] that every quantale can be presented as the quotient of the free quantale over a monoid M. Consider Q as a monoid and let j : P(Q) → P(Q) be the function which maps a subset S of Q to the set of elements below ⋁(S). Then j is a quantic nucleus and Q ≅ P(Q)_{j}.

By the subset ordering on quotients, the quantic nuclei on Q form a complete lattice N(Q). This is isomorphic to the lattice of congruence relations on Q. It follows from the above that every quantale has a presentation in terms of generators and relations (see [Vic89]).

Examples 2.2.7

1. For any p ∈ Q, t_{p} = p −∘ (p ∘ (−)) : Q → Q is a quantic nucleus.

2. p∘(−) : Q → Q is a quantic nucleus if and only if p is an idempotent greater than 1. This is true if and only if p ∘ (−) = t_{p}. In particular, ⊤ ∘ (−) is a quantic nucleus.

3. u_{p} = p −∘ (−) : Q → Q is a quantic nucleus if and only if p is an idempotent less than 1. This is true if and only if p −∘ (−) = t_{p}.

4. c_{p} = p ∨ (−) is a quantic nucleus if and only if p ∘ ⊤ ≤ p.

Proposition 2.2.8 Let Q be a commutative quantale and b be any element of Q. Then j(−) = ((−) −∘ b) −∘ b is a quantic nucleus. Furthermore, b is j-closed and the operation (−) −∘ b is an involution on Q_{j}.

Applying this construction to the free quantale on a commutative monoid, we obtain Girard’s phase semantics for classical linear logic. We define a Girard quantale to be a quantale Q with an element ⊥ such that the operation (−)^{⊥} defined by x^{⊥} = x −∘ ⊥ is an involution. A simple example is given by RM3 with ⊥ = 1.

We turn our attention briefly to conuclei.

Lemma 2.2.9 Let h : Q → Q be a quantic conucleus. The image Q_{h} of h is a subquantale of Q. That is, Q_{h} contains the unit and is closed under ∘ and ⋁.

The modal operator !(−) can be interpreted as a conucleus. As !-closed formulae are required to satisfy weakening and contraction, !ϕ must be interpreted by an idempotent element less than 1. The set of such elements form a locale, in fact the largest localic subquantale of Q. We take the interpretation of !(−) to be the corresponding conucleus.

2.2.3 Resource Semantics

In this section, we aim to elucidate the conservation principles which are implicit in linear logic by developing a semantics based on an abstract notion of resource. These ideas will be used later on in the construction of the presheaf example of chapter 4. The resource semantics is similar in style to the semantics for relevance logic proposed by Urquhart [Urq72], Routley and Meyer [RM72], and Fine [Fin74]; an account of which can be found in [Dun86]. Similar ideas have been used by Dam [Dam88,Dam90] to analyse the compositional properties of processes in Milner’s CCS.

The minimum requirement of an abstract notion of resource is that there is an operation which combines resources. We shall go further and require that resources form a commutative monoid. A linear proposition ϕ will be modelled by the set of resources sufficient to prove it. Thus interpreting linear propositions in the power set of a monoid M gives a simple resource semantics. It is helpful to think of M as the natural numbers ⟨N, +, 0, ≤⟩ and suppose that we are counting the number of computation steps in some process that will validate ϕ. Alternatively, if every element of M is idempotent then we can imagine that they are ‘pieces of information’ which might allow us to deduce ϕ, and this is Urquhart’s semi-lattice semantics [Urq72].

There may also be a partial order representing the idea that one resource is better than another, in the sense that it can prove more facts.

Definition 2.2.10 A resource model of propositional linear logic is a structure ⟨M, ·, e, ≤, ⊧⟩ where ⟨M, ·, e⟩ is a commutative monoid, ≤ is a partial order on M such that multiplication is monotone in both arguments, and ⊧ is a relation between elements of M and atomic propositions of intuitionistic linear logic which satisfies

x ≤ y and x ⊧ ϕ ⇒ y ⊧ ϕ  (2.30)

The relation ⊧ can be extended to all linear propositions as follows.

x ⊧ ϕ ∨ ψ ⟺ x ⊧ ϕ or x ⊧ ψ  (2.31)
x ⊧ ϕ ∧ ψ ⟺ x ⊧ ϕ and x ⊧ ψ  (2.32)
x ⊧ ϕ ∘ ψ ⟺ ∃y, z ∈ M (yz ≤ x and y ⊧ ϕ and z ⊧ ψ) (2.33)
x ⊧ ϕ −∘ ψ ⟺ ∀y ∈ M (y ⊧ ϕ ⇒ xy ⊧ ψ)  (2.34)
x ⊧ 1 ⟺ e ≤ x  (2.35)
x ⊧ ⊤ for all x ∈ M  (2.36)
x|̸= 0 for any x ∈ M  (2.37)

A sequent Γ ⊢ ϕ is valid in the model ⟨M, ·, e, ≤, ⊧⟩ if x ⊧ θ implies that x ⊧ ϕ, where θ is the fusion of formulae in Γ and is 1 when Γ is empty.

There is a straightforward connection between the resource semantics given above and the consequence algebra semantics. For any subset S of the monoid M let ↑ (S) denote the upward closure of S. As multiplication in M is monotone in both arguments, ↑: P(M) → P(M) is a quantic nucleus whose image P(M)_{↑} is the upwardly closed subsets of M. The resource semantics corresponds to an interpretation of linear propositions in the quantale P(M)_{↑} and hence propositional intuitionistic linear logic is sound with respect to this semantics.

The interpretation of the linear connectives given above captures the intention of the relational semantics of Routley and Meyer [RM72]. Their ternary relation R can be defined as

Rxyz ⟺ xy ≤ z  (2.38)

Note 2.2.11 Linear logic is not complete with respect to the resource semantics since the distributive law below is valid in all resource models but is not a derivable sequent of linear logic.

ϕ ∧ (ψ ∨ θ) ⊢ (ϕ ∧ ψ) ∨ (ϕ ∧ θ)  (2.39)

See [Rea88] for a discussion of linear logic with this additional rule.

Symmetric Monoidal Closed Categories

There is now a well established correspondence between type theories and classes of ‘category with structure’ [See84,See87a,HP88]. This is often expressed as an equivalence between a category of type theories and the corresponding category of categories. Two important examples, both contained in [LS86], are the correspondence between elementary topoi and higher order intuitionistic type theory, and that between cartesian closed categories and the simply typed λ-calculus.

Symmetric monoidal closed categories are a mild, but important, generalisation of cartesian closed categories, and it is therefore natural to seek a syntactic analogue of these categories. In this chapter, we present a form of linear type theory, denoted LTT, and we state and prove a correspondence between LTT and symmetric monoidal closed categories. The system LTT forms a type theoretic basis for the logic of chapter 6.

In section 3.1, we define symmetric monoidal closed categories and give some standard examples. In the next chapter, we study in detail two further examples which are, perhaps, more interesting because they are actually derived from a consideration of linear logic.

In section 3.2, we introduce the language of LTT which consists of types and terms with restrictions placed on the occurrence of variables. In contrast to the other examples mentioned above, symmetric monoidal closed categories have less structure than cartesian closed categories. We must therefore limit the expressiveness of the syntax to the fragment of equational reasoning that is valid in a symmetric monoidal closed category. In general, the tensor product of a symmetric monoidal closed category has no diagonal map, so we must restrict ourselves to terms in which there is no repetition of variables. We allow equational axioms between terms provided that the same variables occur on each side.

The definition of linear type theory is parametric in three arguments: a set B of basic types, a set F of function symbols, and a set E of equational axioms. We use LTT(B, F, E) to denote the language defined with parameters B, F and E.

In section 3.3, we define an interpretation of a linear type theory in a symmetric monoidal closed category C, and give a syntactic construction to show that for every theory LTT(B, F, E) there exists an ‘initial model’ T_{0}(B, F, E).

In section 3.4, we give examples of equational theories to illustrate the sort of equational reasoning that that is possible within a symmetric monoidal closed category. The first of these is a simple theory of monoids and monoid actions. The examples include quantales, which are monoids in the category CSLat of complete semilattices, and rings, which are monoids in Ab.

The idea that category theory itself can be internalised in a symmetric monoidal closed category is the foundation of enriched category theory [Kel82], and indeed ‘categories’ form the second of our examples.

Finally, we modify LTT so that it includes equations between types, and show that for any symmetric monoidal closed category C there exists a (modified) linear type theory whose initial model is C. This gives an equivalence between the category LTT of linear type theories and the category SMCC of symmetric monoidal closed categories.

3.1 Symmetric Monoidal Closed Categories

Definition 3.1.1 A monoidal category C = ⟨C, ⊗, I, a, l, r⟩ consists of a category C, a functor ⊗ : C × C → C, an object I of C, and natural isomorphisms

a_{X,Y,Z} : (X ⊗ Y) ⊗ Z → X ⊗ (Y ⊗ Z)  (3.1)
l_{X} : I ⊗ X → X  (3.2)
r_{X} : X ⊗ I → X  (3.3)

which satisfy the following coherence axioms.

[figure: ((W ⊗ X) ⊗ Y) ⊗ Z; \overline{a ⊗ 1}; (W ⊗ (X ⊗ Y)) ⊗ Z; a; (W ⊗ X) ⊗ (Y ⊗ Z); a; a; W ⊗ (X ⊗ (Y ⊗ Z)); 1 ⊗ a; W ⊗ ((X ⊗ Y) ⊗ Z)]  (3.4)

[figure: (X ⊗ I) ⊗ Y; \overline{a}; X ⊗ (I ⊗ Y); r ⊗ 1; 1 ⊗ l; X ⊗ Y]  (3.5)

These are called the pentagon and triangle laws respectively. A monoidal category is said to be strict if a, l, r are identities.

Definition 3.1.2 A symmetry for a monoidal category ⟨C, ⊗, I, a, l, r⟩ is a natural transformation c_{X,Y} : X ⊗ Y → Y ⊗ X satisfying the following coherence axioms.

[figure: (X ⊗ Y) ⊗ Z; \overline{a}; X ⊗ (Y ⊗ Z); \overline{c}; (Y ⊗ Z) ⊗ X; c ⊗ 1; a; (Y ⊗ X) ⊗ Z; \overline{a}; Y ⊗ (X ⊗ Z); \overline{1 ⊗ c}; Y ⊗ (Z ⊗ X)]  (3.6)

[figure: X ⊗ Y; I ⊗ X; \overline{c}; X ⊗ I; c; 1; l; r; Y ⊗ X; \overline{c}; X ⊗ Y; X]  (3.7)

A symmetric monoidal category is a monoidal category equipped with a symmetry.

If C is a category with finite products then C is a symmetric monoidal category with ⊗ given by the cartesian product, I the terminal object, and a, c, l given by appropriate combinations of pairing and projection.

Definition 3.1.3 A symmetric monoidal category C is closed if for each X ∈ Obj(C) the functor (−) ⊗ X has a specified right adjoint [X, −].

That is, there exist natural transformations

ε_{X,Y} : [X, Y] ⊗ X → Y
δ_{X,Y} : X → [Y, X ⊗ Y]

which satisfy the triangle identities for an adjunction :

1 = ε(δ ⊗ 1) : X ⊗ Y → [Y, X ⊗ Y] ⊗ Y → X ⊗ Y  (3.8)
1 = [1, ε]δ : [X, Y] → [X, [X, Y] ⊗ X] → [X, Y]  (3.9)

The notion of an adjunction has several equivalent formulations [ML71, page 81], and we can also usefully state the definition of closure in terms of a universal property :

Lemma 3.1.4 A symmetric monoidal category C is closed if for each X, Y ∈ Obj(C) there exists an object [X, Y] and an arrow ε_{X,Y} : [X, Y] ⊗ X → Y which is universal from (−) ⊗ X to Y. That is, whenever f : Z ⊗ X → Y is a morphism of C, there exists a unique map λ(f) : Z → [X, Y] such that ε_{X,Y} (λ(f) ⊗ 1_{X}) = f.

Remark 3.1.5 If C is a symmetric monoidal closed category then, by the parameter theorem for adjunctions [ML71, page 100], there is a unique way to ‘piece together’ the hom functors [X, −] to give a single functor [−, −] : C^{op} × C → C such that the isomorphism

C(Z ⊗ X, Y) ≅ C(Z, [X, Y])

is natural in X, Y and Z. Example 3.1.6 Perhaps the best known example of a symmetric monoidal closed category is the category Ab of abelian groups.

The tensor product of two abelian groups A and B is the abelian group generated by elements a ⊗ b with a ∈ A and b ∈ B subject to the relations

(a_{1} + a_{2}) ⊗ b = (a_{1} ⊗ b) + (a_{2} ⊗ b)  (3.10)
a ⊗ (b_{1} + b_{2}) = (a ⊗ b_{1}) + (a ⊗ b_{2})  (3.11)

The unit for ⊗ is given by Z, the group of integers under addition. The internal hom [A, B] is the set of all group homomorphisms from A to B with addition defined pointwise :

(f + g)(a) = f(a) + g(a)  (3.12)

and identity given by the trivial homomorphism mapping all of A to the zero in B.

In fact, the symmetric monoidal closed structure on Ab is a special case of that on the category R-Mod of modules over a ring R, since Ab is equivalent to Z-Mod where Z is the ring of integers. Examples 3.1.7

1. Every consequence algebra, and hence every quantale, is strict symmetric monoidal closed when viewed as a category.

2. A category C with finite products is said to be cartesian closed if it is closed with respect to ×. Examples of cartesian closed categories include Set, the category Poset of partial orders and order preserving maps, the category Cat of all small categories, the category CPO of partial orders with sups of ω-chains and Scott continuous maps between them [Sch86], Heyting algebras, and topoi.

3. The category of (generalised) metric spaces and distance decreasing maps (see section 4.2).

4. The category Set_{∗} of sets with a distinguished element ∗ and functions which preserve that element. The tensor product X ⊗ Y is the quotient of X × Y ∪ {∗} under the smallest equivalence relation containing the relations ⟨x, ∗⟩ ≡ ∗ ≡ ⟨∗, y⟩ for all x ∈ X and y ∈ Y. The unit I is the set {∗} and the internal hom [X, Y] is the function space Y^{X} with distinguished element given by the constant function mapping all of X to ∗.

3.1.1 Monoidal Functors

There is more than one interesting notion of map between symmetric monoidal closed categories C and D. The most obvious is to take a functor F : C → D which preserves all the structure on the nose. A more subtle notion is a functor which preserves the tensor product and unit up to a comparison. That is, F X ⊗ F Y and F (X⊗Y) are not necessarily equal, but there is a comparison map F (X)⊗F (Y) → F (X ⊗ Y) between them subject to certain coherence conditions. Quantic nuclei are an example of such a functor.

Definition 3.1.8 Let C, D be symmetric monoidal categories. A symmetric monoidal functor from C to D is a triple ⟨F, F̃, F^{0}⟩ where F : C → D is a functor, F^{0} is a morphism I → F (I) in D and F̃ is natural transformation with components F̃_{X,Y} : F (X) ⊗ F (Y) → F (X ⊗ Y). The following coherence axioms are required.

[figure: (F (X) ⊗ F (Y)) ⊗ F (Z); \overline{a}; F (X) ⊗ (F (Y) ⊗ F (Z)); F̃ ⊗ 1; 1 ⊗ F̃; F (X ⊗ Y) ⊗ F (Z)  F (X) ⊗ F (Y ⊗ Z); F̃; F̃; F ((X ⊗ Y) ⊗ Z); \overline{F (a)}; F (X ⊗ (Y ⊗ Z))]  (3.13)

[figure: I ⊗ F (X); \overline{l}; F (X); F^{0} ⊗ 1; F (l); F (I) ⊗ F (X); \overline{F̃}; F (X ⊗ I)]  (3.14)

[figure: F (X) ⊗ F (Y); \overline{c}; F (Y) ⊗ F (X); F̃; F̃; F (X ⊗ Y); \overline{F (c)}; F (Y ⊗ X)]  (3.15)

Remark 3.1.9 In the nonsymmetric case we would need to give a coherence condition for r, but here it follows from the conditions on l, c and the fact that r = lc.

Note that the existence of a comparison F̃ : F (X) ⊗ F (Y) → F (X ⊗ Y) automatically gives the following comparison for the internal hom.

F̂_{X,Y} = λ(F (ε)F̃) : F [X, Y] → [F (X), F (Y)]  (3.16)

The next definition gives some of the stronger notions of map between symmetric monoidal closed categories.

Definition 3.1.10 A symmetric monoidal functor ⟨F, F̃, F^{0}⟩ : C → D is said to be

1. strong if F^{0} and F̃ are natural isomorphisms,

2. strict if F^{0} and F̃ are identities,

3. strong closed if F^{0} and F̂ are natural isomorphisms,

4. strict closed if F^{0} and F̂ are identities.

Quantale homomorphisms are examples of strict monoidal functors, but are not necessarily strict closed. The linear doctrines defined in chapter 7 (definition 7.1.5) are strict monoidal strict closed.

3.2 Linear Type Theory

In this section, we use a language of combinators and types to give a syntactic presentation of symmetric monoidal closed categories. This is based on Jay’s language for monoidal categories [Jay89a,Jay90] but also bears some relation to the language of Lafont’s linear abstract machine [Laf88].

3.2.1 Types

Let B = {X, Y, Z, …} be a set of basic types. The set T of types is built inductively from basic types and the unit type I, by the application of the binary type constructors tensor product ⊗ and internal hom [−, −].

t ::= I | X | t_{1} ⊗ t_{2} | [t_{1}, t_{2}]  (3.17)

3.2.2 Combinators

The basic combinators are given below, together with their type.

Id_{A}  : A → A
assl_{A,B,C} : A ⊗ (B ⊗ C) → (A ⊗ B) ⊗ C
assr_{A,B,C} : (A ⊗ B) ⊗ C → A ⊗ (B ⊗ C)
swap_{A,B} : A ⊗ B → B ⊗ A
open_{A} : A → I ⊗ A
close_{A} : I ⊗ A → A
eval_{A,B} : [A, B] ⊗ A → B

(3.18)

In addition to the basic combinators above, we have a set F of function symbols. Each F ∈ F has a specified type F : A → B. General combinators are built inductively from the function symbols and basic combinators by the following three rules.

\frac{α : A → B  β : B → C}{β • α : A → C}  (3.19)

\frac{α : A → B  β : C → D}{α ⊗ β : A ⊗ C → B ⊗ D}  (3.20)

\frac{α : A ⊗ B → C}{Λ(α) : A → [B, C]}  (3.21)

In the tradition of the λ-calculus, we call Λ(α) the ‘currying of α’.

3.2.3 Type Assignment and the Calculation of Subscripts

The combinators given above are explicitly typed. In proposition 3.2.3, we show that the subscripts on the basic components of a combinator α are uniquely determined by its type, and so can be dropped whenever the type is clear from the context. To do this we briefly consider an extension of the system of types which includes type variables. The type expressions are given by the following BNF grammar

e ::= I | X | x | e_{1} ⊗ e_{2} | [e_{1}, e_{2}]

where x ranges over type variables. The basic combinator schemes are given by 3.18 where A, B, C are taken to range over type expressions. Function symbols are assumed to have a specified type U → V with no type variables. General combinator schemes are built up from basic schemes and function symbols using the rules 3.19 to 3.21.

In addition to the combinator schemes, we need to consider combinator expressions without subscripts. The untyped combinators are given by the following BNF grammar

c ::= Id | assl | assr | swap | open | close | eval
F | c_{1} • c_{2} | c_{1} ⊗ c_{2} | Λ(c)  (3.22)

If α is a combinator scheme then erase(α) denotes the untyped combinator derived from α by deleting the subscripts on basic components, eg.

erase(open_{[X,Y]} •Λ(eval_{X,Y} • eval_{X,[X,Y]⊗X})) =open •Λ(eval • eval)

Not all of the untyped combinators have a typed counterpart, swap •Λ(swap) for example. We say that an untyped combinator γ is stratified if there exists a combinator scheme α with erase(α) = γ.

We say that a combinator scheme α′ : A′ → B′ is a substitution instance of a scheme α : A → B if there exists a simultaneous substitution θ of type expressions for type variables which maps A to A′, B to B′ and α to α′. The following result says that if an untyped combinator γ is stratified then there exists a most general combinator scheme with erasure γ. This is similar to the principal types lemma found in [HS86].

Lemma 3.2.1 If an untyped combinator γ is stratified then there exists a combinator scheme β : C → D such that erase(β) = γ and, furthermore, whenever erase(β′) = γ then β′ is a substitution instance of β.

Proof. By induction on the structure of γ. Note that for any combinator scheme β : A → B with erase(β) = γ, the structure of the type derivation of β is exactly determined by the structure of γ.

The only difficult case is γ = γ_{1} • γ_{2}. By the induction hypothesis, there exist β_{1} : A → B and β_{2} : B′ → C which are the most general combinator schemes such that erase(β_{i}) = γ_{i} for i = 1, 2. We know that there exists a combinator scheme α such that erase(α) = γ, so by examination of the type derivation of α there is at least one substitution of type expressions for type variables which makes B and B′ equal. Thus, by the first order unification theorem (see [Rob79]), there exists a most general one θ. It is routine to verify that θ(β_{2}) • θ(β_{1}) : θ(A) → θ(B) is the most general combinator scheme with erase(β) = γ. □

Lemma 3.2.2 Let β : B → C be a combinator scheme. Then every type variable in the subscripts of β appears either in B or in C. ^{1}

Proof. By induction on the structure of the type derivation.

Again, the only difficult case is the composition rule 3.19. Suppose that β = β_{2} • β_{1} where β_{1} : B → D and β_{2} : D → C. We use the fact that the combinators of LTT correspond to the consequence relation of intuitionistic linear logic. For each type variable x let v_{x} be a mapping of type expressions into the quantale RM3 such that

v_{x}(A) = \{ \begin{matrix}⊤ & if A = x \\ v_{x}(A_{1}) ∘ v_{x}(A_{2}) & if A = A_{1} ⊗ A_{2} \\ v_{x}(A_{1}) −∘ v_{x}(A_{2}) & if A = [A_{1}, A_{2}] \\ 1 & otherwise \end{matrix}  (3.23)

Note that v_{x}(A) = 1 if and only if x does not occur in A. We can show inductively that if γ : G → H is a combinator scheme then v_{x}(G) ≤ v_{x}(H). For example, if γ is a function symbol then G and H contain no type variables, so v_{x}(G) = v_{x}(H) = 1.

If the type variable x does not appear in C or D above then

1 = v_{x}(B) ≤ v_{x}(D) ≤ v_{x}(C) = 1  (3.24)

so x does not occur in D either. □

Proposition 3.2.3 Let α, α′ be combinators with the same type. If erase(α) = erase(α′) then α = α′.

Proof.

Let β : B → C be the most general combinator with erase(β) = erase(α). It follows that both α, α′ are substitution instances of β. As every type variable occurring in the subscripts of β appears in B or C, it suffices to know the domain and codomain of α to calculate a substitution θ such that α = θβ. Hence α, α′ must be equal because they have the same domain and codomain. □

1This is related to a result by Kelly and Mac Lane [KML71] which says that the allowable natural transformations of a closed category have ‘graphs’ which do not contain any loops.

Proposition 3.2.3 shows that the subscripts on a combinator are uniquely determined by its type, and the proof of lemma 3.2.1 embodies an algorithm for calculating them. Thus, we shall omit the subscripts from combinators when the overall type is clear. However, there are important situations where this is not the case (see remark 6.3.3) and the subscripts must be retained.

3.2.4 Derived Combinators

The following combinators are important enough to merit names.

hold_{A,B}  = Λ(Id)
: A → [B, A ⊗ B]
inter_{A,B,C,D} = assr •((assl •(Id ⊗ swap)• assr)⊗ Id)• assl
: (A ⊗ B) ⊗ (C ⊗ D) → (A ⊗ C) ⊗ (B ⊗ D)
tensor_{A,B,C,D} = Λ((eval ⊗ eval)• inter)
: [A, C] ⊗ [B, D] → [A ⊗ B, C ⊗ D]
comp_{A,B,C}  = Λ(eval •(Id ⊗ eval)• assr)
: [B, C] ⊗ [A, B] → [A, C]
curry_{A,B,C}  = Λ(Λ(eval • assr))
: [A ⊗ B, C] → [A, [B, C]]

If α : A′ → A and β : B → B′ then we can define a combinator [α, β] : [A, B] → [A′, B′] which corresponds to the morphism part of the hom functor.

[α, β] = Λ(β• eval •(1 ⊗ α))  (3.25)

3.2.5 Variables and Terms

We assume that we have a countably infinite set var(A) = {a_{1}, a_{2}, …, a_{n}, …} of variables for each type A in T . The following rules generate a set of preterms for each type A.

1. () ∈ preterm(I).

2. If a ∈ var(A) then a ∈ preterm(A).

3. If s ∈ preterm(A) and t ∈ preterm(B) then (s, t) ∈ preterm(A ⊗ B).

4. If s ∈ preterm(A) and α : A → B then α(s) ∈ preterm(B)^{2}.

A preterm s is a term if no variable occurs more than once in s. Thus (F (x), eval (comp (f, g), y)) is a term but swap (x, x) is not. The set of terms of type A is denoted term(A).

We say that a term is basic if it contains no combinators. Thus basic terms are built from variables and round brackets only. A basic term (x, y) ∈ term(A ⊗ B) is essentially a variable of the tensor type. The reason for introducing single variables v ∈ var(A ⊗ B) is to give a clean definition of substitution.

If t is a preterm and v is a variable of the same type then for any preterm s we can define the preterm s[t/v], the result of substituting t for v in s as follows.

()[t/v] = ()  (3.26)
w[t/v] = \{ \begin{matrix}t & if v = w \\ w & otherwise \end{matrix}  (3.27)
(s_{1}, s_{2})[t/v] = (s_{1}[t/v], s_{2}[t/v])  (3.28)
α(s)[t/v] = α(s[t/v])  (3.29)

Lemma 3.2.4 If s, t are terms with no variables in common, and v is a variable with the same type as t, then s[t/v] is a term.

Proof. Easy induction on the structure of s. □

2If s = () or s = (t, u) then shall shall omit the brackets and write αs.

3.2.6 Equations between terms

Definition 3.2.5 An equivalence relation ≈ on terms is substitutive if it satisfies the following two conditions.

1. whenever t_{1}, t_{2} are terms with the same type as a variable v and s_{1}, s_{2} are terms whose variables do not appear in t_{1}, t_{2} then

s_{1} ≈ s_{2} and t_{1} ≈ t_{2} ⇒ s_{1}[t_{1}/v] ≈ s_{2}[t_{2}/v]  (3.30)

2. whenever x is a basic term with the same type as v, and none of the variables of x already appear in s_{1}, s_{2} then

s_{1}[x/v] ≈ s_{2}[x/v] ⇒ s_{1} ≈ s_{2}  (3.31)

This second condition will allow us to assume that variables of the tensor type are actually pairs.

Definition 3.2.6 An equivalence relation ≈ on terms is extensional if whenever f, g are terms of type [X, Y] and x is a basic term of type X then

eval_{X,Y} (f, x) ≈ eval_{X,Y} (g, x) ⇒ f ≈ g  (3.32)

Definition 3.2.7 Let E be a set of linear equational axioms, that is pairs ⟨s ≈ t⟩ of terms such that s, t have the same type and exactly the same variables. The relation ≈_{E} of term equality relative to E is defined to be the smallest substitutive and extensional equivalence relation ≈ including the equational axioms E and the equations 3.33 to 3.41 below.

Id_{A} (s) ≈ s  (3.33)
(γ • α)(s) ≈ γ(α(s))  (3.34)
α ⊗ β(s, t) ≈ (α(s), β(t))  (3.35)
assl_{A,B,C} (s, (t, u)) ≈ ((s, t), u)  (3.36)
assr_{A,B,C} ((s, t), u) ≈ (s, (t, u))  (3.37)
swap_{A,B} (s, t) ≈ (t, s)  (3.38)

open_{A} (s) ≈ ((), s)  (3.39)
close_{A} ((), s) ≈ s  (3.40)
eval_{B,C} (Λ(α)(s), t) ≈ α(s, t)  (3.41)

Definition 3.2.8 The language LTT(B, F, E) of linear type theory with a set B of basic types, F of function symbols and E of linear equational axioms consists of the set T of types generated from B together with, for each type A, the set term(A) of terms of type A built from variables and function symbols in F subject to the relation ≈_{E} of term equality defined above.

Notation 3.2.9 Henceforth, we shall omit the subscript E and write ≈ for term equality wherever this causes no confusion.

Lemma 3.2.10 If s ≈ t then s, t are terms of the same type with the same variables.

Proof. By induction on the number of steps required to derive s ≈ t. □

3.2.7 A Normal Form for Terms

In this section, we show that every term has a normal form consisting of a single combinator applied to a basic term. This means that we can separate the ‘function’ part of LTT from the ‘variable’ part, which is important for the interpretation of formulae given in section 7.2.

Definition 3.2.11 Let s be a term in LTT(B, F, E). We define an associated combinator, ac(s), and an associated basic term, abt(s), as follows.

ac(()) = Id_{I}  abt(()) = ()
ac(v_{A}) = Id_{A}  abt(v) = v
ac((s, t)) = ac(s) ⊗ ac(t)  abt((s, t)) = (abt(s), abt(t))
ac(α(s)) = α • ac(s)  abt(α(s)) = abt(s)

(3.42)

Lemma 3.2.12 If t is a term of type A and v ∈ var(A) then for all terms s

ac(s)(abt(s)[t/v]) ≈ s[t/v]  (3.43)

In particular, if v does not occur in s then s ≈ ac(s)(abt(s)).

Proof. Easy induction on the structure of s. □

Definition 3.2.13 A combinator is central if it is built entirely from instances of Id, assl, assr, open, close, swap by composition and tensor product.

Lemma 3.2.14 If x, y are two basic terms with the same variables then there exists a central combinator ξ such that ξ(x) ≈ y.

Proof. Given a list Φ = {A_{1}, A_{2}, …, A_{n}} of types, there are two canonical ways to form a tensor product of Φ :

L(Φ) = (… ((A_{1} ⊗ A_{2}) ⊗ A_{3}) ⊗ … ⊗ A_{n})
R(Φ) = (A_{1} ⊗ … ⊗ (A_{n−2} ⊗ (A_{n−1} ⊗ A_{n})) …)

Let A be any other product of the types A_{1}, A_{2}, …, A_{n} which retains their order. We give an inductive definition of central combinators left_{n}: A → L(Φ) and right_{n}: A → R(Φ) which map basic terms of type A with variables in A_{1}, A_{2}, …, A_{n} to their left and right associated forms. That is, left_{n} (x) ≈ x′ and right_{n} (x) ≈ x′′ where x′ and x′′ are basic terms of type L(Φ) and R(Φ) respectively.

If n = 1 then L(Φ) = R(Φ) = A so left_{1}=right_{1}=Id. For n ≥ 2, A = B_{1} ⊗ B_{2} where B_{1}, B_{2} are products of lists Φ_{1}, Φ_{2} of length n_{1}, n_{2} respectively. We define

left_{n} = assl^{n_{1}−1} • (left_{n_{1}} ⊗ right_{n_{2}})
right_{n} = assr^{n_{2}−1} • (left_{n_{1}} ⊗ right_{n_{2}})

Given the right associated product R(Φ) of a list Φ = {A_{1}, A_{2}, …, A_{n}}, we can define central combinators

pull_{i}: A_{1}⊗(… A_{i−1}⊗(A_{i}⊗(A_{i+1}⊗…)) …) → A_{i}⊗(A_{1}⊗(… A_{i−1}⊗(A_{i+1}⊗…) …) which move the ith term of an n-tuple to the first position.

pull_{1} = Id
pull_{i+1} = assr • swap • assl •(Id ⊗ pull_{i})

These can be combined to give combinators which perform any permutation of the terms.

Let x and y be basic terms with the same variables. We can apply right_{n} to obtain the right associated form of x, then use the appropriate combinations of the pull_{i} to obtain the right associated form of y, and finally apply the inverse of right_{n} to obtain y. □

3.3 The Interpretation of LTT in C

Let ⟨C, ⊗, I, [−, −], a, c, l, ε, λ⟩ be a symmetric monoidal closed category and let ı : B → Obj(C) be a function which maps each basic type to an object of C. We extend ı to all types as follows.

ı (I) = I
ı (A ⊗ B) = ı (A) ⊗ ı (B)
ı ([A, B]) = [ı (A), ı (B)]

Let ȷ be a mapping of the basic function symbols given by F to morphisms of C such that

γ : A → B  ⇒  ȷ (γ) : ı (A) → ı (B)  (3.44)

We extend the definition of ȷ inductively to all combinators in such a way that the functorial property 3.44 holds for an arbitrary γ. The basic combinators are mapped to components of the natural transformations a, l, c, ε as follows.

ȷ (Id_{A})  = 1_{ı (A)}
ȷ (assr_{A,B,C}) = a_{ı (A),ı (B),ı (C)}
ȷ (assl_{A,B,C}) = a_{ı (A),ı (B),ı (C)}^{−1}
ȷ (swap_{A,B}) = c_{ı (A),ı (B)}
ȷ (open_{A}) = l_{ı (A)}
ȷ (close_{A}) = l_{ı (A)}^{−1}
ȷ (eval_{A,B}) = ε_{ı (A),ı (B)}

(3.45)

If α : A → B and β : B → C are composable combinators then, using 3.44 as an induction hypothesis, ȷ (α) and ȷ (β) are composable morphisms of C, and we can define

ȷ (β • α) = ȷ (β)ȷ (α)  (3.46)

Similarly for the tensor product

ȷ (α ⊗ β) = ȷ (α) ⊗ ȷ (β)  (3.47)

Suppose that α : A ⊗ B → C. By the induction hypothesis ȷ (α) is a morphism from ı (A) ⊗ ı (B) to ı (C) in C. We define ȷ (Λ(α)) to be the transpose of ȷ (α) across the adjunction (−) ⊗ ı (B) ⊣ [ı (B), −], i.e.

ȷ (Λ(α)) = λ(ȷ (α))  (3.48)

Definition 3.3.1 Let ı : B → Obj(C) and ȷ : F → Mor(C) be functions such that 3.44 holds. We say that the pair ⟨ı, ȷ⟩ is an interpretation of LTT(B, F, E) if whenever x is a basic term and α(x) ≈ β(x) is derivable from the equational axioms E, then ȷ (α) = ȷ (β) in C.

3.3.1 The category T_{0}

We construct a symmetric monoidal closed category T_{0}(B, F, E) from the syntax of LTT(B, F, E), and show that there is an interpretation of LTT(B, F, E) in T_{0}(B, F, E) which is initial in the sense that every interpretation factors uniquely through it.

Let ≡ be the equivalence relation between combinators defined as follows.

α ≡ β ⟺ α(x) ≈ β(x)  (3.49)

where x is a basic term of type A. Note that by 3.30 and 3.31, this definition is independent of the choice of x.

Notation 3.3.2 We use [α] to denote the equivalence class of α under ≡.

Lemma 3.3.3 The following are derived rules for the equivalence of combinators.

\frac{α ≡ α′ : A → B  β ≡ β′ : B → C}{β • α ≡ β′ • α′ : A → C}  (3.50)

\frac{α ≡ α′ : A → B  β ≡ β′ : C → D}{α ⊗ β ≡ α′ ⊗ β′ : A ⊗ B → C ⊗ D}  (3.51)

\frac{α ≡ β : A ⊗ B → C}{Λ(α) ≡ Λ(β) : A → [B, C]}  (3.52)

Lemma 3.3.4 The following data define a category T_{0}(B, F, E) : the objects are the types of LTT(B, F, E) and morphisms from A to B are the equivalence classes of combinators α : A → B under ≡. Composition of equivalence classes [α] : A → B and [β] : B → C is given by [β • α] : A → C, and the identity on A is [Id_{A}].

Proof.

Composition is well defined by 3.50. To verify the axioms for a category we check the following equivalences

Id_{B} •α ≡ α ≡ α• Id_{A}  (3.53)
γ • (β • α) ≡ (γ • β) • α  (3.54)

and this is straightforward. □

Proposition 3.3.5 T_{0}(B, F, E) is a symmetric monoidal category.

Chapter 3. Symmetric Monoidal Closed Categories 52 Proof. We verify that T_{0}(B, F, E) has the required data. Tensor Product.

The tensor product on types gives rise to a functor ⊗ : T_{0} × T_{0} → T_{0} where [α] ⊗ [β] is [α ⊗ β]. This is well defined by 3.51. We need to check the following equivalences

Id_{A} ⊗ Id_{B} ≡ Id_{A⊗B}  (3.55)
(β ⊗ β′) • (α ⊗ α′) ≡ (β • α) ⊗ (β′ • α′)  (3.56)

but this is quite routine. We shall omit the details of this and of the similar calculations below. Natural Transformations.

We define

a_{A,B,C} = [assr_{A,B,C}] : (A ⊗ B) ⊗ C → A ⊗ (B ⊗ C)
a_{A,B,C}^{−1} = [assl_{A,B,C}] : A ⊗ (B ⊗ C) → (A ⊗ B) ⊗ C
l_{A} = [close_{A}] : I ⊗ A → A
l_{A}^{−1} = [open_{A}] : A → I ⊗ A
c_{A,B} = [swap_{A,B}] : A ⊗ B → B ⊗ A

To show that these define natural transformations we need to check the following equivalences.

assr •((α ⊗ β) ⊗ γ) ≡ (α ⊗ (β ⊗ γ))• assr  (3.57)
assl •(α ⊗ (β ⊗ γ)) ≡ ((α ⊗ β) ⊗ γ)• assl  (3.58)
open •α ≡ (Id_{I} ⊗α)• open  (3.59)
close •(Id_{I} ⊗α) ≡ α• close  (3.60)
swap •(α ⊗ β) ≡ (β ⊗ α)• swap  (3.61)

To show that a, l are isomorphisms we check that

assl • assr ≡ Id_{(A⊗B)⊗C}  (3.62)
assr • assl ≡ Id_{A⊗(B⊗C)}  (3.63)

open • close ≡ Id_{I⊗A}  (3.64)
close • open ≡ Id_{A}  (3.65)

Coherence.

The remaining equivalences to be verified come from the coherence axioms given in diagrams 3.4 to 3.7.

assr • assr ≡ (Id ⊗ assr)• assr •(assr ⊗ Id)  (3.66)
(Id ⊗ close)• assr ≡ (close • swap)⊗ Id  (3.67)
assr • swap • assr ≡ (Id ⊗ swap)• assr •(swap ⊗ Id)  (3.68)
swap • swap ≡ Id  (3.69)
□

To establish that T_{0}(B, F, E) is closed with respect to the tensor product, we need the following lemma.

Lemma 3.3.6 Let α : X ⊗ Y → Z and β : W → X. The following equivalences are derivable from the equations 3.33 to 3.41.

eval •(Λ(α)⊗ Id_{Y}) ≡ α  (3.70)
Λ(eval_{X,Y}) ≡ Id_{[X,Y]}  (3.71)
Λ(α • (β⊗ Id_{Y})) ≡ Λ(α) • β  (3.72)

The equivalences 3.70 and 3.71 correspond to the λ-calculus notions of betaequivalence and eta-equivalence.

Proposition 3.3.7 T_{0}(B, F, E) is a symmetric monoidal closed category.

Proof. It remains to show that T_{0}(B, F, E) is closed. Let ε_{A,B} = [eval_{A,B}] : [A, B] ⊗ A → B. We show that ε_{A,B} is universal from (−) ⊗ A to B and hence that T_{0} is closed. Let [α] : A ⊗ B → C, we need to show that there is a unique map [β] : A → [B, C] such that ε_{A,B}([β] ⊗ 1_{A}) = [α].

Using equivalence 3.70 from the lemma above, we see that [Λ(α)] satisfies the required condition. If [γ] is another such map then eval •(γ⊗ Id) ≡ α and so

Λ(α) ≡ Λ(eval •(γ⊗ Id)) by 3.52
≡ Λ(eval) • γ  by 3.72
≡ γ  by 3.71

The pair ⟨id, [−]⟩ is an interpretation of LTT(B, F, E) in T_{0}(B, F, E), trivially, and we have the following result. □

Proposition 3.3.8 The pair ⟨ı, ȷ⟩ is an interpretation of LTT if and only if there exists a strict monoidal strict closed functor I : T_{0} → C such that ı (A) = I(A) and ȷ (α) = I([α]). Moreover, I is the unique such.

3.4 Equational Theories in LTT

The restrictions on the occurence of variables limit the sort of equational theories which can be expressed in linear type theory. The theory of groups, for example, is excluded because the inverse law xx^{−1} = e requires the variable x to be duplicated on the left and thrown away on the right. Nevertheless, the following examples show that there are worthwhile algebraic theories which lie in this fragment of equational reasoning.

3.4.1 Monoids

Definition 3.4.1 A monoid in a monoidal category C consists of an object M of C together with morphisms μ : M ⊗ M → M and η : I → M such that the following diagrams commute.

[figure: (M ⊗ M) ⊗ M; \overline{a}; M ⊗ (M ⊗ M); \overline{1 ⊗ μ}; M ⊗ M; μ ⊗ 1; μ; M ⊗ M; \overline{μ}; M]  (3.73)

[figure: I ⊗ M; \overline{η ⊗ 1}; M ⊗ M; 1 ⊗ η; M ⊗ I; l; μ; r; M]  (3.74)

If C is symmetric then a monoid M in C is commutative if μc_{M,M} = μ.

If M is a monoid in C and X ∈ Obj(C) then a left action of M on X is a map ν : M ⊗ X → X such that the following diagram commutes.

[figure: (M ⊗ M) ⊗ X; \overline{a}; M ⊗ (M ⊗ X); \overline{1 ⊗ ν}; M ⊗ X; η ⊗ 1; I ⊗ X; μ ⊗ 1; ν; l; M ⊗ X; \overline{ν}; X]  (3.75)

Example 3.4.2

Monoidal Category C  Monoids in C
⟨Set, ×, 1⟩  Monoids
⟨Ab, ⊗, I⟩  Rings
⟨CSLat, ⊗, ℘(1)⟩  Quantales [JT84]
⟨Cat, ×, 1⟩  Strict Monoidal Categories
⟨C^{C}, ·, 1⟩  Monads

Thus, the analogy between rings and quantales, hinted at in chapter 2, is that they are both monoids in an appropriate monoidal category.

The theory of a monoid has the following presentation in LTT.

\begin{aligned}B & = & \{M\} \\ F & = & \{e : I → M , m : M ⊗ M → M\} \\ E & = & \{m(u, m(v, w)) ≈ m(m(u, v), w), \\ & & m(e(), u) ≈ u , m(u, e()) ≈ u\} \end{aligned}  (3.76)

The theory of a commutative monoid has the additional equation m(u, v) ≈ m(v, u).

Clearly, if ⟨ı, ȷ⟩ is an interpretation of this theory in a symmetric monoidal closed category C then ⟨ı (M), ȷ (m), ȷ (e)⟩ is a monoid in C.

The theory of a monoid with a left action on X is given by

\begin{aligned}B′ & = & B ∪ \{X\} \\ F′ & = & F ∪ \{h : M ⊗ X → X\} \\ E′ & = & E ∪ \{h(u, h(v, x)) ≈ h(m(u, v), x) , h(e(), x) ≈ x\} \end{aligned}  (3.77)

3.4.2 Enriched Categories

Recall that a monoid in Set is just a category with one object. Since the associativity and identity laws of a monoid are expressible in linear type theory, it is not suprising that this extends to the case of categories with more than one object.

The corresponding algebraic idea is that of a category enriched in V or ‘Vcategory’ where V is a symmetric monoidal closed category. Here, the ‘hom-sets’ in an ordinary category are replaced by ‘hom-objects’ taken from V. In contrast to the internal categories of a topos [Joh77], the objects of an enriched category are not internalised. Enriched categories were originally motivated by constructions found in representation theory, but, more recently, have been studied in computer science (eg. the O-categories of [SP82] and the quantaloids of [AV90] are categories enriched in cpo and CSLat respectively). We refer to [Kel82] for the basic definitions of enriched category theory, and state just the type theoretic version below.

The theory of a (small) enriched category with object set O is given by

\begin{aligned}B & = & \{A(X, Y)|X, Y ∈ O\} \\ F & = & \{m_{X,Y,Z} : A(Y, Z) ⊗ A(X, Y) → A(X, Z), \\ & & j_{X} : I → A(X, X)|X, Y, Z ∈ O\} \\ E & = & \{m_{W,Y,Z}(h, m_{W,X,Y} (g, f)) ≈ m_{W,X,Z}(m_{X,Y,Z}(h, g), f) \\ & & m_{X,Y,Y} (j_{Y} (), f) ≈ f \\ & & m_{X,X,Y} (f, j_{X}()) ≈ f\} \end{aligned}  (3.78)

3.4.3 The Theory Associated with a Category

In section 3.3.1, we saw that every linear type theory Θ = LTT(B, F, E) gives rise to a symmetric monoidal closed category T_{0}(B, F, E). In this section we consider how to generate a linear type theory from the objects and morphisms of a symmetric monoidal closed category C. In order to get a precise correspondance between the category and its type theory we extend the system of types and combinators given in sections 3.2.1 and 3.2.2 to include equations between types.

Let T be a set whose elements are pairs ⟨A, B⟩ where A, B are types. We define a relation ∼ of type equality relative to T. This is the smallest equivalence relation on types containing T and closed under the following two rules.

\frac{A ∼ A′  B ∼ B′}{(A ⊗ B) ∼ (A′ ⊗ B′)}  \frac{A ∼ A′  B ∼ B′}{[A, B] ∼ [A′, B′]}  (3.79)

We extend the typing of combinators by the following rule ^{3}.

\frac{A ∼ A′  α : A → B  B ∼ B′}{α : A′ → B′}  (3.80)

and similarly for terms

\frac{s ∈ term(A)  A ∼ A′}{s ∈ term(A′)}  (3.81)

Let LTT(B, T, F, E) denote linear type theory with the set T of type equations as a parameter and the additional rules given above.

Let ⟨C, ⊗, I, a, l, r⟩ be a symmetric monoidal closed category. We use C to define a linear type theory with equations between types as follows.

B = \{\overline{X}|X is an object of C\}
T = \{\overline{I} ∼ I , \overline{X} ⊗ \overline{Y} ∼ \overline{X ⊗ Y} , [\overline{X}, \overline{Y}] ∼ \overline{[X, Y]} | X, Y ∈ Obj(C)\}
F = \{\overline{f} : \overline{X} → \overline{Y} |f : X → Y is a morphism of C\}

3This, of course, invalidates the type assignment property given in proposition 3.2.3 because the type subscripts in α need no longer appear as part of the domain or codomain type.

The equational axioms are as follows, where x, y, z are basic terms of the appropriate type and α is any combinator.

\overline{1_{A}}(x) ≈ x
\overline{gf}(x) ≈ \overline{g}(\overline{f}(x))
\overline{f ⊗ g}(x, y) ≈ (\overline{f}(x), \overline{g}(y))
\overline{a_{A,B,C}}((x, y), z) ≈ (x, (y, z))
\overline{c_{A,B}}(x, y) ≈ (y, x)
\overline{l_{A}}((), x) ≈ x
\overline{ε_{B,C}}(Λ(α)(x), y) ≈ α(x, y)

We need to extend the definition of an interpretation ⟨ı, ȷ⟩ of LTT so that it respects type equality. That is, if A ∼ A′ is provable then ı (A) = ı (A′). The construction of T_{0} is also modified so that the objects are the equivalence classes of types under ∼. We denote the equivalence class of X under ∼ by [X].

Proposition 3.4.3 Let ı be the function which maps each basic type \overline{X} to the object X of C and ȷ be the function which maps each function symbol \overline{f} : \overline{X} → \overline{Y} to the morphism f : X → Y. Then ⟨ı, ȷ⟩ is an interpretation of LTT(B, T, F, E) in C and the functor I : T_{0} → C given by proposition 3.3.8 is an isomorphism of categories.

Proof. It is routine to verify that ⟨ı, ȷ⟩ is an interpretation.

We show that I has an inverse. Let H : C → T_{0} be the mapping X ↦ [\overline{X}] on objects and similarly f ↦ [\overline{f}] on morphisms. It is easy to verify that H is a functor and that IH = 1_{C}. To show that HI = 1_{T_{0}} we need to check that A ∼ \overline{ı (A)} for all types A and that α ≡ \overline{ȷ (α)} for all combinators α. This is done by structural induction. □

If Θ_{1} = LTT(B_{1}, T_{1}, F_{1}, E_{1}) and Θ_{2} = LTT(B_{2}, T_{2}, F_{2}, E_{2}) are linear type theories then a strict map from Θ_{1} to Θ_{2} is a pair ⟨F, G⟩ where F is a function mapping types of Θ_{1} to types of Θ_{2} such that

\begin{aligned}F (I) & = & I \\ F (A ⊗ B) & = & F (A) ⊗ F (B) \\ F ([A, B]) & = & [F (A), F (B)] \end{aligned}  (3.82)

and if A ∼ B then F (A) ∼ F (B), and G is a function which maps each combinator α : A → B of Θ_{1} to a combinator G(α) : F (A) → F (B) such that

G(Id_{A}) = Id_{F (A)}
G(α ⊗ β) = G(α) ⊗ G(β)
G(β • α) = G(β) • G(α)
G(assl_{A,B,C}) = assl_{F (A),F (B),F (C)}
G(assr_{A,B,C}) = assr_{F (A),F (B),F (C)}
G(open_{A}) = open_{F (A)}
⋮
G(Λ(α)) = Λ(G(α))

(3.83)

and if α ≈ β then G(α) ≈ G(β). Thus, a strict map between type theories is a straightforward translation of one language into another which preserves all the structure on the nose. We view strict maps to be equivalent if they agree modulo the equivalence relations determined by ∼ and ≈. Let LTT denote the category of linear type theories with type equality and equivalence classes of strict maps between them, and let SMCC denote the category of small symmetric monoidal closed categories and strict monoidal strict closed functors.

It is routine to verify that the construction of a linear type theory from a symmetric monoidal closed category gives rise to a functor U : SMCC → LTT. Moreover, it follows from proposition 3.3.8, with a mild addition to account for type equality, that U has a left adjoint F. Further, by proposition 3.4.3, it follows that the counit of the adjunction is an isomorphism, and hence SMCC is a full reflective subcategory of LTT. U is also essentially surjective and hence an equivalence of categories. This correspondence can be treated more naturally at the level of 2-categories in terms of a biequivalence. However, the details of this correspondence are delicate, and are inessential to the main development of the thesis. We therefore omit an exposition of this form and summarize as follows.

Chapter 3. Symmetric Monoidal Closed Categories 60 Theorem 3.4.4 The category LTT is equivalent to the category SMCC of small symmetric monoidal closed categories and strict monoidal strict closed functors.

Two Examples

The internal language of a topos is expressive enough to support a large fragment of mathematical reasoning. Lambek and Scott, for example, regard the free topos as “an acceptable universe of mathematics for the moderate intuitionist” [LS86, Preface]. We shall not be concerned with such foundational issues, but merely the question of how the underlying logic adopted changes the properties that one might expect from a ‘universe of sets’.

The study of linear logic is still in its infancy, and it may be some time before a definitive notion of ‘universe’ for linear logic emerges. In the meantime, we can provide evidence to support the belief that such a universe should be a symmetric monoidal closed category with some extra ‘logical’ structure.

In this chapter, we present two examples of categories which can have some claim to being categories of ‘sets under linear logic’. These both arise as linear analogues of constructions in the theory of topoi. The first is the category of presheaves over a small symmetric monoidal category ⟨C, ⊗, I⟩. We view symmetric monoidal categories as a natural generalisation of resource monoids, and use ideas taken from the resource semantics to motivate the definition of a resource bounded tensor product of presheaves. This is the content of section 4.1. The second example is a category of sets with ‘equality predicates’ valued in a quantale Q, as explained in section 4.2. We show that both of these categories have a symmetric monoidal closed structure. Later on, in chapter 5, we shall see that they also have sufficient logical structure to provide models for first order linear logic.

4.1 Resource Semantics in a Presheaf Category

4.1.1 Presheaves and Kripke Models

We compare the Kripke semantics of propositional intuitionistic logic (found in eg. [Fit69]) with the resource semantics of section 2.2.3. Kripke semantics are defined with respect to a partial order ⟨W, ≤⟩. The elements of W are called possible worlds or states of knowledge, and a comparison x ≤ y indicates that y is a better world than x in the sense that more truths are known there. As in resource semantics, atomic propositions are interpreted as upwardly closed subsets of ⟨W, ≤⟩, and this interpretation can be extended to all propositions by an inductive definition. A key difference between the Kripke semantics and the resource semantics is that, in the former, there is no notion of combining possible worlds. In particular, intuitionistic implication is defined only in terms of the partial order on W.

x ⊧ ϕ ⊃ ψ ⟺ ∀y ≥ x(y ⊧ ϕ ⇒ y ⊧ ψ)  (4.1)

Kripke semantics are easily extended from the propositional logic to intuitionistic set theory. If A is an intuitionistic set then for each possible world x there is an ordinary set A(x) which represents our knowledge of A at x. Knowledge of a set covers both the existence of elements and their equality. If x ≤ y then all the elements that exist in A at stage x must also exist at stage y so there is a comparison map A_{x,y} : A(x) → A(y). This map is not necessarily injective as elements considered distinct at stage x may become equated at y as a result of the greater knowledge available. Thus, an intuitionistic set corresponds to a functor A : W → Set.

Recall from section 2.2.3 that the idea of a computational resource can be modelled abstractly by a partially ordered monoid ⟨M, ·, e, ≤⟩. Multiplication represents the combination of resources and the order indicates where one resource is better than another. To adapt the above ideas in the case of the resource semantics, we imagine some process of calculating information about a set A which is bounded by a limitation of resource measured in M. It is helpful to consider the natural numbers ⟨N, +, 0, ≤⟩ and suppose that we are counting the number of computation steps, calls to a particular routine, or seconds elapsed in the computation. The set A(x) represents the totality of all the information about A that could be acquired by the expenditure of resource x. As in the intuitionistic case, information covers both the existence of elements and their equality. If x ≤ y in M then y is a better resource than x so a computation using y yields more information about A than one using x. Again, it follows that there should be a comparison map A_{x,y} : A(x) → A(y) and that a resource bounded set should correspond to a functor A : M → Set.

The crucial difference between the two approaches comes when we consider the product of ‘sets’. The cartesian product of functors A, B : M → Set is defined by

(A × B)(x) = A(x) × B(x)  (4.2)

This expression is natural enough in the Kripke semantics where x denotes a state of knowledge, but is more problematic in terms of resources. It says that to ascertain that ⟨a, b⟩ is an element of A × B, we are allowed to use x twice to separately ascertain that a is in A and b is in B. Thus, the cartesian product fails to conserve resources. We seek instead a tensor product A ⊗ B which respects resources by analogy to the interpretation of fusion in 2.2.10. For example, if resource is a measure of time given by the monoid ⟨N, +, 0, ≤⟩ then we anticipate that the tensor product will be such that (A ⊗ B)(n) is some suitable colimit of the sets A(m)×B(n−m). That is, the time taken to calculate that a pair ⟨a, b⟩ is an element of the tensor product A ⊗ B is the sum of the time taken to calculate that a is in A and that b is in B. In section 4.1.3, we develop a general form of ‘resource bounded product’, the next section introduces some of the categorical machinary that we shall need.

4.1.2 Ends and Kan extensions

Definition 4.1.1 Let F : A^{op} × A → B be a functor. A wedge w : x ¨→F is an object x of B together with a function assigning to each object A of A an arrow w_{A} : x → F (A, A) such that for every morphism f : A → B of A the following diagram commutes.

[figure: x; \overline{w_{A}}; F (A, A); w_{B}; F (1, f); F (B, B); \overline{F (f, 1)}; F (A, B)]  (4.3)

An end for F is a wedge v : e ¨→F which is universal amongst wedges into F, that is, whenever w : x ¨→F is a wedge there exists a unique morphism g : x → e with v_{A} = w_{A}g for all A. Coends are defined dually.

We use the ‘integral’ notation ∫_{A} F (A, A) and ∫^{A} F (A, A) for the end and coend of F respectively.

Definition 4.1.2 Let X , Y and A be categories and let F : X → A and K : X → Y be functors. A left Kan extension of F along K is a functor L : Y → A with natural transformation η : F ˙→LK which is universal as an arrow from F to A^{K} : A^{Y} → A^{X}. That is,

[figure: A; F; ⟹^{η}  L ⟹^{σ} M; X; \overline{K}; Y]  (4.4)

given any functor M : Y → A and natural transformation α : F ˙→KM there exists a unique natural transformation σ : L ˙→M such that α = (σK)η.

Dually, a right Kan extension of F along K is a functor R : Y → A and a natural transformation ϵ : RK ˙→F which is universal as an arrow from A^{K} : A^{Y} → A^{X} to F.

Let Lan_{K} F denote the left Kan extension of F along K and Ran_{K} denote the right. If every functor from X to A has a left Kan extension along K then A^{K} : A^{Y} → A^{X} has a left adjoint (and similarly for the right).

We refer to chapters IX and X of [ML71] for the properties of ends and Kan extensions. In particular, if X is small, Y is locally small and A is complete then the Kan extensions of F : X → A along K : X → Y exist and have the following expressions in terms of ends

(Lan_{K} F)Y = ∫ ^{X} Y(K(X), Y) · F (X)  (4.5)
(Ran_{K} F)Y = ∫_{X} F (X)^{Y(Y,K(X))}  (4.6)

(If S is a set then A^{S} and S · A denote the product and coproduct of S copies of A.)

Lemma 4.1.3 Let C be a small category and let F : C → Set be a functor then

F (C) ≅ ∫ ^{X} C(X, C) × F (X)  (4.7)
F (C) ≅ ∫_{X}[C(C, X), F (X)]  (4.8)

Proof. Immediate from the observation that Lan_{1} F ≅ F ≅Ran_{1} F. □

Let A be a small category, B be locally small and G, H : A → B be functors. Then the natural transformations from G to H form a set and this has the following end formulation

Nat (F, G) = ∫_{A}[F (A), G(A)]  (4.9)

Applying this above, 4.8 is recognisable as the Yoneda lemma [ML71, page 61].

4.1.3 Day’s Tensor Product

There is a natural generalisation of the Kripke semantics which is given by replacing the partially ordered set W with an arbitrary category, by convention C^{op}, so that intuitionistic sets become functors C^{op} → Set or presheaves. These form a topos and we refer to [LS86] for an account of the semantics of higher order intuitionistic logic in presheaf topoi.

The resource semantics can also be generalised from partial orders to categories. If C is a small symmetric monoidal category then we regard C as a category of resources. The objects of C are resources, the morphisms are comparisons or transformations of resource, and the tensor product of C is the operation of combining resources. This includes the partially ordered monoids of section 2.2.3 as a special case, and we keep these in mind while developing the general theory. A resource bounded set built over a symmetric monoidal category C is given by a presheaf A : C^{op} → Set. We show that there is a resource bounded product on the category Ĉ of presheaves over C analogous to the interpretation of fusion in 2.2.10, and that this gives rise to a symmetric monoidal closed structure.

Let Ĉ be the functor category [C^{op}, Set] and let Y : C → Ĉ be the Yoneda functor, defined on objects of C by Y (x) = C(−, x) with a corresponding action on morphisms. Recall [LS86] that the Yoneda functor is a full and faithful embedding. Our aim is to extend the monoidal structure of C to Ĉ.

[figure: C; \overline{Y}; Ĉ; ⊗  ˆ⊗; C × C; \overline{Y × Y}; Ĉ × Ĉ]  (4.10)

Let ˆ⊗ : Ĉ × Ĉ → Ĉ be the left Kan extension of the composite Y ⊗ along the embedding Y × Y. The fact that Y × Y is full and faithful ensures that the unit

η_{Y ⊗} : Y ⊗ → ˆ⊗(Y × Y)  (4.11)

is a natural isomorphism, so Y (x) ˆ⊗Y (y) ≅ Y (x ⊗ y) for all objects x, y in C.

We can use the coend formula for the left Kan extension to calculate ˆ⊗ explicitly for arbitrary presheaves A, B

A ˆ⊗B = (Lan_{Y ×Y} Y ⊗)(A, B)  (4.12)
= ∫ ^{(x,y)} Ĉ × Ĉ((Y x, Y y), (A, B)) · Y (x ⊗ y)  (4.13)
= ∫ ^{(x,y)}(A(x) × B(y)) · Y (x ⊗ y)  (4.14)

As limits and colimits are evaluated pointwise in Ĉ

A ˆ⊗B(u) = ∫ ^{(x,y)} C(u, x ⊗ y) × A(x) × B(y)  (4.15)

We show that (−) ˆ⊗B has a right adjoint in Ĉ. Consider the following sequence of isomorphisms in Set.

Ĉ(A ˆ⊗B, C) = ∫_{x}[A ˆ⊗B(x), C(x)]
= ∫_{x}[∫ ^{y,z} C(x, y ⊗ z) × A(y) × B(z) , C(x)]]
≅ ∫_{x,y,z}[C(x, y ⊗ z) × A(y) × B(z) , C(x)]
≅ ∫_{y,z}[A(y) × B(z) , ∫_{x}[C(x, y ⊗ z), C(x)]]  (4.16)

By the Yoneda lemma

Ĉ(A ˆ⊗B, C) ≅ ∫_{y,z}[A(y) × B(z), C(y ⊗ z)]
≅ ∫_{y}[A(y), ∫_{z}[B(z), C(y ⊗ z)]]
= Ĉ(A, [B, C])  (4.17)

where [B, C] is defined by

[B, C] = ∫_{z}[B(z), C(− ⊗ z)]  (4.18)

The isomorphism 4.17 is natural in A and C by the parameter theorem for ends [ML71, page 224], so [B, −] is a right adjoint for (−) ⊗ B.

It is a matter of routine calculation to show that the associativity, symmetry and unit for ⊗ induce corresponding structure for ˆ⊗. The coherence conditions also follow from the parameter theorem.

4.1.4 Discussion of Resources

The elements of A ⊗ B at stage u are, modulo an equivalence, triples

⟨f, a, b⟩ ∈ C(u, x ⊗ y) × A(x) × B(y)  (4.19)

The map f : u → x ⊗ y is a comparison between the resource u and the combined resource x⊗y. This can be interpreted as saying that u is at least as good as x⊗y. In the partial order case, this reduces to xy ≤ u. Thus if we can use resource x to show that a is an element of A and y to show that b is in B then u must be sufficient to show that ⟨a, b⟩ is an element of the product.

Note the correspondence between the definition of internal hom and the interpretation of linear implication in 2.2.10. We explain this in terms of resources as follows. If we can use resource x to show that b is an element of B and resource y to show f is a function from B to C then the combined resource x ⊗ y is sufficent to ascertain that f(b) is an element of C.

In the specific case that C^{op} is the natural numbers ⟨N, +, 0, ≤⟩, the tensor product A ˆ⊗B can be evaluated at stage n as the colimit of the following diagram in Set.

A(0) × B(n − 1)  ⋯  A(n − 1) × B(0)
[figure: ⋯]
A(0) × B(n)  A(1) × B(n − 1)  ⋯  A(n) × B(0)

This is easy enough to calculate if each of the comparison maps is a monomorphism, so the equality relations of A and B remain fixed as the measure of resource increases; but is much more difficult to calculate in general. It seems unlikely, given the complexity of its construction, that we will be able to analyse the properties of ˆ⊗ much beyond the observation that ⟨Ĉ, ˆ⊗, Y (I), [−, −]⟩ is symmetric monoidal closed. Fortunately, this suffices for our purposes because the extra properties required in chapter 5 to show that Ĉ is a model of first order linear logic follow from the fact that it is a topos.

4.2 Q-sets

An important example of a topos is given by the category Shv(Ω) of sheaves over a locale Ω. This is defined as the full subcategory of the presheaf category [Ω^{op}, Set] whose objects satisfy a certain gluing condition [Joh82, page 171]. It is certainly possible to study sheaves by working directly with this definition, but there is an alternative approach which is based on the use of sets with Ω-valued equality predicates. This was pioneered by Fourman and Scott [FS79] and independently by Higgs [Hig73,Hig84].

An Ω-set X is a pair ⟨|X|, =_{X}⟩ where |X| is a set and =_{X}: |X| × |X| → Ω is a function which is ‘symmetric’ and ‘transitive’ in the evident way. The reflexivity of equality is not taken as an axiom. Instead the value of (x =_{X} x) is taken to be the extent to which x exists. Thus, the logic of sheaves is a logic of both existence and equality. Higgs showed that the category Ω-Set, whose objects are Ω-sets and whose morphisms are ‘functional relations’, is equivalent to Shv(Ω).

There is some difficulty in developing a theory of sets with quantale valued equality relations due to the presence of the two conjunctions. In his thesis [Naw85], Nawaz developed a theory of sets with a Q-valued equality where Q is a non-commutative quantale in which ⊤ is a right unit and multiplication is idempotent. This work has been extended by Borceux and others [BCBSC89], but unfortunately rests heavily on the assumption of idempotence. More recently, Borceux has considered a category of Q-sets where Q is a commutative quantale in which multiplication is not necessarily idempotent but 1 = ⊤ [Bor90].

In this section, we present a theory of sets with a Q-valued equality where Q is any commutative quantale with unity. We adopt the axiom of reflexivity in order to study the notion of quantale valued equality without reference to existence. This allows us to draw on the ideas about metric spaces and enriched categories given by Lawvere in [Law73].

This influential paper has inspired a great deal of work on monoidal categories, bicategories and the categories enriched in these, and the constructions we shall use are special cases of the much more general ones appearing in the literature. In particular, the notion of a ‘functional relation’ given in definition 4.2.9 is closely related to the notion of a ‘map’ in a bicategory [CW87], and the associated idea of ‘functional completeness’ is related to the notion of ‘Cauchy completeness’ appearing in [Wal81,Wal82,Str81]. The importance of studying the more restricted version of these concepts is that we stay close to a logical intuition and obtain a simple category in which it is possible to test ideas about the categorical semantics of linear logic by explicit calculation. Definition 4.2.1 Let Q be a commutative quantale with unity. A Q-category X is a set |X| equipped with a function X(−, −) : |X| × |X| → Q which satisfies the axioms Q1 and Q2 below. A Q-category X is a Q-set if it satisfies the additional axiom Q3.

\begin{aligned}Q1 & 1 & ≤ & X(u, u) \\ Q2 & X(u, v) ∘ X(v, w) & ≤ & X(u, w) \\ Q3 & X(u, v) & ≤ & X(v, u) \end{aligned}

If X is a Q-set then the function X(−, −) : |X| × |X| → Q is said to be the equality or metric of X.

Remark 4.2.2 Recall that a quantale Q can be viewed as a symmetric monoidal closed category, in which case the notion of Q-category defined above coincides with that of a V-enriched category in the sense of [Kel82] (compare the inequalities above with the basic function symbols of section 3.4.2). Note that the coherence conditions are trivial in the case that V is a partial order.

In categorical terms, the last axiom states that X is a self dual category in the very strong sense that X = X^{op}, and in logical terms, it says that the equality on X is symmetric. Though formally less critical than the first two, it fits our logical intuition and greatly simplifies some of the definitions below.

As Q-sets are self dual Q-categories, one possible notion of map between them is that of Q-functor.

Definition 4.2.3 If X, Y are Q-categories then a Q-functor from X to Y is a function f : |X| → |Y | such that for all x, x′ ∈ |X|

X(x, x′) ≤ Y (f(x), f(x′))  (4.20)

Let Q-Cat denote the category of small Q-categories with Q-functors between them, and let Q-CatSD denote the full subcategory of whose objects are self dual.

Example 4.2.4 The motivating example of [Law73] is that of generalised metric spaces. Recall from section 2.2.1 that the reals [0, ∞] with the reverse of the usual order form a quantale ℜ in which fusion is given by addition and the unit is 0.

When Q = ℜ the axioms above become

\begin{aligned}X(u, u) & = & 0 \\ X(u, w) & ≤ & X(u, v) + X(v, w) \\ X(u, v) & = & X(v, u) \end{aligned}  (4.21)

ℜ-sets are therefore a generalisation of metric spaces which allow points with infinite distance between them and distinct points x, y with X(x, y) = 0. Lawvere goes further and drops symmetry as well. ℜ-functors are distance decreasing maps.

We say that a generalised metric space X is Cauchy complete if every Cauchy sequence {x_{i}} has a unique limit point in X ^{1}.

Example 4.2.5 [Bor90] Let R be a commutative ring with unity. If r ∈ R then the annihilator of r is the ideal Ann(r) = {x ∈ R|rx = 0}. The elements of R can be given the structure of an Idl(R)-set R by defining

R(r, s) = Ann(r − s)  (4.22)

If x ∈ Ann(r − s) and y ∈ Ann(s − t) then

xy(r − t) = xy(r − s) + xy(s − t) = 0  (4.23)

so Ann(r − s)Ann(s − t) ⊆ Ann(r − t). Q1 and Q3 are immediate.

Example 4.2.6 Any quantale Q itself forms a Q-set with the equality given by bi-implication.

It is well known [Kel82, page 65] that for a complete symmetric monoidal closed category V the category V-Cat of small V-categories is also complete symmetric monoidal closed. The tensor product and internal hom are given by

|X ⊗ Y | = |X| × |Y |
X ⊗ Y (⟨x, y⟩, ⟨x′, y′⟩) = X(x, x′) ⊗ Y (y, y′)
|[X, Y]| = {Q-functors from X to Y }
[X, Y](f, g) = ∫_{x} Y (f(x), g(x))

1For spaces in which X(x, y) = 0 ⇒ x = y the uniqueness is immediate

The unit I for the tensor product is defined by |I| = {∗} and I(∗, ∗) = I_{V} where I_{V} is the unit for the tensor product in V. Thus, in particular, Q-Cat is complete symmetric monoidal closed. Though, in this case, the definition of [X, Y] is simplified by the fact that the end reduces to a meet. The subcategory Q-CatSD is also symmetric monoidal closed because it contains I and is closed under the tensor and hom constructions.

Although Q-functors are a natural notion of map between Q-sets, they bear little resemblance to the ‘functional relations’ defined between Ω-sets. Thus, in the spirit of Ω-valued sets, we pursue a more general notion of map.

Definition 4.2.7 If X, Y are Q-sets then a Q-valued relation R : X ⇝ Y is a function R : |X| × |Y | → Q which satisfies

\begin{aligned}R1 & X(x′, x) ∘ R(x, y) & ≤ & R(x′, y) \\ R2 & R(x, y) ∘ Y (y, y′) & ≤ & R(x, y′) \end{aligned}

Given relations R : X ⇝ Y and S : Y ⇝ Z the composite SR is defined by

SR(x, z) = ⋁_{y} R(x, y) ∘ S(y, z)  (4.24)

If R is a relation from X to Y then R^{op} is the relation from Y to X defined by R^{op}(y, x) = R(x, y).

It is clear that composition of relations is associative, and that the identity relation on a Q-set X is the equality of X. Thus Q-sets and Q-valued relations between them form a category Q-Rel. In fact, Q-Rel forms a locally ordered category with the evident ordering on relations.

If Q = 2 then a Q-set is just a set with an equivalence relation, a Q-valued relation X ⇝ Y is a relation between equivalence classes of X and Y, and 4.24 is just the usual composition of relations. 2-Rel is therefore equivalent to the category Rel of sets and relations. An important observation on the locally ordered category Rel is that

Proposition 4.2.8 A function is a relation which is left adjoint to its own opposite.

That is, a relation F ⊆ X × Y is a function if and only if 1_{X} ≤ F^{op}F and F F^{op} ≤ 1_{Y}. We extend this idea to an arbitrary quantale Q.

Definition 4.2.9 A functional relation between Q-sets X and Y is a relation F : X ⇝ Y such that F ⊣ F^{op}, that is

\begin{aligned}F1 & F (x, y) ∘ F (x, y′) & ≤ & Y (y, y′) \\ F2 & X(x, x′) & ≤ & ⋁_{y} F (x, y) ∘ F (x′, y) \end{aligned}  (4.25)

The identity relation on X is clearly functional and the composite of functional relations is again functional because adjunctions compose. Thus, Q-sets and functional relations form a category which we denote Q-Set.

Remark 4.2.10 We can give the following readings to F1 and F2. F1 says that F is single-valued : “if F maps x to y and also maps x to y′ then y and y′ are equal” and F2 says that F is total : “if x = x′ then there exists a y such that F maps x to y and F maps x′ to y”

Taking x = x′ in F2, we obtain

X(x, x) ≤ ⋁_{y} F (x, y) ∘ F (x, y)  (4.26)

Note that the proposition “F maps x to y” is asserted precisely twice. This is in sharp contrast to the intuitionistic case, where it does not matter how many times a proposition is asserted and the axiom (x =_{X} x) ≤ ⋁_{y} F (x, y) suffices to express the totality of F.

4.2.1 Functional Completeness

A Q-functor f : X → Y induces a functional relation f̂: X → Y via

f̂(x, y) = Y (f(x), y)  (4.27)

This correspondence gives rise to a functor ˆ(−) : Q-CatSD → Q-Set whose object part is the identity.

Given that every functor induces a functional relation, it is interesting to ask when the converse holds.

Definition 4.2.11 A Q-set Y is functionally complete if for every functional relation F : X → Y there is a unique Q-functor f : X → Y such that F = f̂.

Lemma 4.2.12 A functional relation F : X → Y is induced by a Q-functor if and only if there exists a function f : |X| → |Y | such that 1 ≤ F (x, f(x)) for all x ∈ |X|.

Proof. Given such a function f, we have

X(x, y) ≤ X(x, y) ∘ F (x, f(x)) ∘ F (y, f(y))
≤ F (y, f(x)) ∘ F (y, f(y))
≤ Y (f(x), f(y))  (4.28)

so f is a Q-functor. Furthermore, by F1

F (x, y) ≤ F (x, f(x)) ∘ F (x, y) ≤ Y (f(x), y)  (4.29)

and by R2

Y (f(x), y) ≤ F (x, f(x)) ∘ Y (f(x), y) ≤ F (x, y)  (4.30)

so F = f̂. The converse is trivial. □

Proposition 4.2.13 [Law73] A metric space is functionally complete if and only if it is Cauchy complete.

Proof. First, suppose that Y is Cauchy complete and that F : X → Y is a functional relation. By F2

0 = inf {F (x, y)|y ∈ |Y |}  (4.31)

so we can choose a sequence y_{n} of points in |Y | such that F (x, y_{n}) ≤ 1/n. Such a sequence is Cauchy since, by F1,

Y (y_{n}, y_{m}) ≤ F (x, y_{n}) + F (x, y_{m}) ≤ 1/n + 1/m  (4.32)

and furthermore if {z_{n}} is any other choice of points satisfying the same condition then Y (y_{n}, z_{n}) ≤ 2/n so {y_{n}} and {z_{n}} are equivalent Cauchy sequences. Let f(x) be the unique limit of the sequence {y_{n}}. As F is a relation

F (x, f(x)) ≤ inf {F (x, y_{n}) + Y (y_{n}, f(x))} = 0  (4.33)

so by lemma 4.2.12 f is a distance decreasing map with f̂ = F. As Y is Cauchy complete, it has the property that Y (y, y′) = 0 ⇒ (y = y′). Hence the uniqueness of f follows from F1.

For the converse we note that every Cauchy sequence {y_{n}} in |Y | defines a functional relation F : I → Y via

F (∗, y) = lim_{n→∞}Y (y, y_{n})  (4.34)

If f : I → Y is a Q-functor satisfying F (∗, y) = Y (f(∗), y) then f(∗) is a limit for {y_{n}}. □ Remark 4.2.14 The observation that the Cauchy completeness of a metric space could be expressed in terms of ℜ-valued relations, led Lawvere to propose the following generalised definition of Cauchy completeness for categories enriched in a symmetric monoidal category V. A V-category Y is said to be Cauchy complete if every pair of V-valued relations or ‘bimodules’ F : X ⇝ Y and G : Y ⇝ X with F ⊣ G is induced by a unique functor f : X → Y. Restricted to Q-sets, this definition is slightly stronger than that of functional completeness because there is no requirement that G = F^{op}. The precise relationship between functional and Cauchy completeness is not yet clear. If Q is a locale or Q = ℜ then they coincide, but this will not be so in general. It may be possible to characterise the cases in which they do coincide by considering the modularity condition on allegories given by Freyd and Scedrov [FS90], but we shall not pursue this here. Instead, we continue with our study of functional completeness.

Proposition 4.2.15 Every quantale Q is functionally complete as a Q-set.

Proof. Suppose that F : X → Q is a functional relation, and let f : |X| → |Q| be the function

f(x) = ⋁_{q} F (x, q) ∘ q  (4.35)

Then for all p ∈ |Q|, we have F (x, p) ≤ p −∘ f(x) and F (x, y) ≤ f(x) −∘ p by the following.

F (x, p) ∘ f(x) = ⋁_{q} F (x, p) ∘ F (x, q) ∘ q
≤ ⋁_{q}(p ∘−∘ q) ∘ q
≤ p  (4.36)

Thus F (x, p) ≤ (p ∘−∘ f(x)) = Q(p, f(x)). It now follows that

1 ≤ X(x, x) ≤ ⋁_{q} F (x, q) ∘ F (x, q)
≤ ⋁_{q} F (x, q) ∘ Q(q, f(x))
≤ F (x, f(x))  (4.37)

so by lemma 4.2.12 f is a Q-functor and F = f̂. The uniqueness of f follows from F1 and the observation that in a quantale 1 ≤ (p ∘−∘ q) implies p = q. □

4.2.2 Tensor Product and Internal Hom

In the next two propositions, we show that the tensor product of Q-CatSD can be lifted to a tensor product on Q-Set, and that Q-Set is closed with respect to this product.

Proposition 4.2.16 Q-Set is a symmetric monoidal category.

Proof. As in Q-Cat, the tensor product of Q-sets X, Y has underlying set |X ⊗ Y | = |X| × |Y | and equality relation

X ⊗ Y (⟨x, y⟩, ⟨x′, y′⟩) = X(x, x′) ∘ Y (y, y′)  (4.38)

and the unit is the Q-set I with underlying set |I| = {∗} and equality I(∗, ∗) = 1. If F : X → Y and G : U → V are functional relations then F ⊗ G is defined by

F ⊗ G(⟨x, u⟩, ⟨y, v⟩) = F (x, y) ∘ G(u, v)  (4.39)

Let X, Y, Z be Q-sets. We define the functional relations

A_{X,Y,Z} : (X ⊗ Y) ⊗ Z → X ⊗ (Y ⊗ Z)
L_{X} : I ⊗ X → X
C_{X,Y} : X ⊗ Y → Y ⊗ X

to be those induced by the corresponding data in Q-CatSD :

A_{X,Y,Z}(⟨⟨x, y⟩, z⟩, ⟨x′, ⟨y′, z′⟩⟩) = X(x, x′) ∘ Y (y, y′) ∘ Z(z, z′) (4.40)
L_{X}(⟨∗, x⟩, x′) = X(x, x′)  (4.41)
C_{X,Y} (⟨x, y⟩, ⟨y′, x′⟩) = X(x, x′) ∘ Y (y, y′)  (4.42)

Clearly A, L, C are isomorphisms. Naturality and coherences follow from the properties of ∘. □

Proposition 4.2.17 Q-Set is a symmetric monoidal closed category.

Proof. The internal hom [X, Y] is defined as follows. The underlying set |[X, Y]| is the set of all functional relations from X to Y. The equality is given by

[X, Y](F, G) = ⋀_{x,y} F (x, y) ∘−∘ G(x, y)  (4.43)

It is routine to check that [X, Y] is a Q-set. It is immediate from this definition that

F (x, y) ∘ [X, Y](F, G) ≤ G(x, y)  (4.44)

for all x ∈ |X| and y ∈ |Y |. The evaluation map E : [X, Y] ⊗ X → Y is defined by

E(⟨F, x⟩, y) = F (x, y)  (4.45)

which clearly satisfies R2 and F1. The other two conditions hold as follows.

([X, Y] ⊗ X)(⟨F′, x′⟩, ⟨F, x⟩) ∘ E(⟨F, x⟩, y) = [X, Y](F′, F) ∘ X(x′, x) ∘ F (x, y)
≤ [X, Y](F′, F) ∘ F (x′, y)
≤ E(⟨F′, x′⟩, y)

([X, Y] ⊗ X)(⟨F, x⟩, ⟨F′, x′⟩) = [X, Y](F, F′) ∘ X(x, x′)
≤ ⋁_{y} [X, Y](F, F′) ∘ F′(x, y) ∘ F′(x′, y)
≤ ⋁_{y} E(⟨F, x⟩, y) ∘ E(⟨F′, x′⟩, y)

Thus E is a functional relation. We show that it is universal from (−) ⊗ X to Y. Let F : Z ⊗ X → Y be a functional relation. Let F_{z} be the relation defined by F_{z}(x, y) = F (⟨z, x⟩, y). It is clear that F_{z} is functional. Furthermore, the mapping z ↦ F_{z} is a Q-functor from Z to [X, Y].

Z(z, z′) ≤ ⋀_{x,y} F (⟨z, x⟩, y) ∘−∘ F (⟨z′, x⟩, y) = [X, Y](F_{z}, F_{z′})  (4.46)

The currying of F is the functional relation G induced by this functor, i.e.

G(z, H) = [X, Y](F_{z}, H)  (4.47)

We now show that E(G ⊗ 1_{X}) = F and moreover that G is the unique map with this property.

E(G ⊗ 1_{X})(⟨z, x⟩, y) = ⋁_{⟨H,u⟩} G(z, H) ∘ X(x, u) ∘ H(u, y)
= ⋁_{H} [X, Y](F_{z}, H) ∘ H(x, y)
= F_{z}(x, y)
= F (⟨z, x⟩, y)

For uniqueness, suppose that G′ : Z ⊗ X → Y is another functional relation satisfying E(G′ ⊗ 1_{X}) = F, i.e.

F (⟨z, x⟩, y) = ⋁_{H} G′(z, H) ∘ H(x, y)  (4.48)

It follows that for all H ∈ |[X, Y]|

G′(z, H) ≤ H(x, y) −∘ F (⟨z, x⟩, y)  (4.49)

and

G′(z, H) ∘ F (⟨z, x⟩, y) = ⋁_{H′} G′(z, H) ∘ G′(z, H′) ∘ H′(x, y)
≤ ⋁_{H′}[X, Y](H, H′) ∘ H′(x, y)
≤ H(x, y)  (4.50)

Combining 4.49 and 4.50 we have

G′(z, H) ≤ ⋀_{x,y} F (⟨z, x⟩, y) ∘−∘ H(x, y) = G(z, H)  (4.51)

To get the converse inequality we note that

1 ≤ Z(z, z) ≤ ⋁_{H} G′(z, H) ∘ G′(z, H)
≤ ⋁_{H} G′(z, H) ∘ G(z, H)
= ⋁_{H} G′(z, H) ∘ [X, Y](H, F_{z})
= G′(z, F_{z})  (4.52)

and hence

G(z, H) ≤ G′(z, F_{z}) ∘ G(z, H)
≤ G′(z, F_{z}) ∘ [X, Y](F_{z}, H)
≤ G′(z, H)  (4.53)

which concludes the proof. □

4.2.3 Reflection Theorem

In this section, we show that Q-Set is equivalent to a full reflective subcategory of Q-CatSD. In the case of metric spaces, this reflection is the familiar Cauchy completion. We use this result to construct limits in Q-Set.

Lemma 4.2.18 For all Q-sets X and Y, the internal hom [X, Y] is functionally complete.

Proof. Let F : Z → [X, Y] be a functional relation. Since Q-Set is symmetric monoidal closed, F is equal to the currying of G = E(F ⊗ 1_{X}) which is, by definition, induced by a Q-functor from Z to [X, Y].

Suppose that f, g : Z → [X, Y] are Q-functors such that f̂ = F = ĝ then

1 ≤ Z(z, z) ≤ ⋁_{H} F (z, H) ∘ F (z, H)
= ⋁_{H}[X, Y](f(z), H) ∘ [X, Y](g(z), H)
= [X, Y](f(z), g(z))  (4.54)

and hence f(z) = g(z) for all z ∈ |Z|. □

This lemma allows us to make the following series of observations.

Proposition 4.2.19 Let s be the function which maps each Q-set X to the internal hom [I, X] viewed as an object of Q-CatSD, and each functional relation F : X → Y to the unique Q-functor f : [I, X] → [I, Y] such that f̂ = [I, F]. The function s determines a full and faithful functor S : Q-Set → Q-CatSD.

Proof. The functoriality of S follows directly from that of ˆ(−) : Q-CatSD → Q-Set. We verify that S is full and faithful.

Let f be a Q-functor S(X) → S(Y). As Q-Set is a closed category, there is a natural isomorphism X ≅ [I, X]. Applying this to f̂: [I, X] → [I, Y], we find that there is a unique functional relation F : X → Y such that [I, F] = f̂ and hence S(F) = f. □

Theorem 4.2.20 The functor ˆ(−) : Q-CatSD → Q-Set is left adjoint to S exhibiting Q-Set as a reflective subcategory of Q-CatSD.

Proof. If X is a Q-set then S(X̂) = [I, X] is functionally complete so we can define a Q-functor η_{X} : X → S(X̂) to be the unique map in Q-CatSD such that η̂_{X} is the currying of the isomorphism LC : X ⊗ I → X in Q-Set. We show that η_{X} is universal as an arrow from X to S.

Let f : X → S(Y) be a morphism of Q-CatSD. Then f̂ factors uniquely through η̂_{X} : X → [I, X] since this is an isomorphism in Q-Set, and hence f factors uniquely through η_{X} by the functional completeness of S(Y) = [I, Y].

[figure: X  X; η_{X}; f; η̂_{X}; ≅; f̂; S(X̂); Y; [I, X]; Y]  (4.55)

Thus ˆ(−) is left adjoint to S, and it follows from the proposition above that S is equivalent to a reflective subcategory of Q-CatSD. □

Proposition 4.2.21 The adjunction ˆ(−) ⊣ S restricts to an equivalence between Q-Set and the full subcategory A of Q-CatSD whose objects are functionally complete.

Proof. It is clear that the adjunction can be restricted to the subcategory A because the image of S is contained in A. Furthermore, if X is functionally complete then the inverse to η̂_{X} : X → [I, X] in Q-Set yields an inverse to η_{X}, so every object in A is isomorphic to one in the image of S. As S is full and faithful, we conclude that it is an equivalence of categories. □

Corollary 4.2.22 Q-Set is complete and cocomplete.

Proof. If Q-CatSD is complete and cocomplete then so is Q-Set because Q-Set is equivalent to a full reflective subcategory of Q-CatSD. It is easy to show that Q-CatSD is closed under limits and colimits in Q-Cat and hence that the completeness and completeness of Q-CatSD follow from that of Q-Cat. □

We give an explicit descriptions of products and equalisers in Q-Set.

Products

Let {X_{i}}_{i∈S} be a family of Q-sets indexed by a set S. Then the product Π_{i∈S}X_{i} has underlying set Π_{i∈S}|X_{i}| and equality

Π_{i∈S}(⟨x_{i}⟩_{i∈S}, ⟨y_{i}⟩_{i∈S}) = ⋀_{i∈S} X_{i}(x_{i}, y_{i})  (4.56)

The projections P_{j} : Π_{i∈S}X_{i} → X_{j} are defined by

P_{j}(⟨x_{i}⟩_{i∈S}, x) = X_{j}(x_{j}, x)  (4.57)

Given a cone {F_{i} : Y → X_{i}}_{i∈S} of functional relations, the mediator F : Y → Π_{i∈S}X_{i} is defined by

F (y, ⟨x_{i}⟩_{i∈S}) = ⋀_{i∈S} F_{i}(y, x_{i})  (4.58)

Equalisers

Let F, G : X → Y be functional relations. Let |U| ⊆ |[I, X]| be the set of functional relations S : 1 → X such that F S = GS and let U be the equality inherited from [I, X]. Then the functional relation K : U → X defined by K(S, x) = S(∗, x) is an equaliser of F and G.

Monoidal Factorisation Systems

In this chapter, we investigate the minimal additional structure required to derive an internal logic from a symmetric monoidal closed category C. We indicate the form that such a logic should take and discuss some of the problems that arise.

The basic categorical structure required is that of a factorisation system on C, as defined in section 5.1. This gives two classes of morphisms in C, called E and M, which satisfy an orthogonality condition and have the property that every map f in C factors as an element of E followed by an element of M. An important example of such a factorisation system is given by the classes of epimorphisms and monomorphisms in a topos. Here, predicates over an object A are associated with monomorphisms with codomain A. We shall take the notion of predicate in the category C to be relative to a particular factorisation system (E, M) where M is a subclass of the monomorphisms. Provided that C is sufficiently complete and cocomplete, this allows us to define operations corresponding to the additive connectives, substitution and existential quantification.

The multiplicative connectives are defined in terms of the symmetric monoidal closed structure of C. It is therefore important that the factorisation behaves well with respect to the tensor product. In section 5.2, we define a monoidal factorisation system to be one in which E is closed under tensor product. This single condition is sufficient to prove that fusion is associative, and to allow the definition of linear implication. This is a mild condition, so there is a wide class of examples. In particular, in section 5.3, we show that Q-Set has a natural monoidal factorisation system.

The definition of the multiplicative connectives, given in section 5.4, is slightly unexpected. The form of first order linear logic given by Seely [See87b,See90] consists of an indexed category in which each fibre is a model of the propositional logic. The logical structure given by a monoidal factorisation system is somewhat different. The multiplicatives are non-fibrewise operations, eg. fusion maps a predicate over A and a predicate over B to a predicate over A ⊗ B. In the next chapter, we shall see that this corresponds to a restriction on the occurrence of variables in formulae similar to that encountered in linear type theory.

Although fusion and linear implication are not operations on a single fibre, they are still related by an adjunction. We define a category Sqr (M) whose objects are elements of M and prove, in theorem 5.4.5, that this is a symmetric monoidal closed category with tensor product and internal hom given by fusion and linear implication respectively.

There are various difficulties involved in developing a logic of symmetric monoidal closed categories, which we illustrate in the case of Abin section 5.5. The properties observed in Ab fundamentally shape the logic presented in chapter 6. In particular, the fact that pullback fails to preserve the logical operations on the nose necessitates the use of explicit substitution operators, and removes the possibility of including universal quantification. We also note that the evident generalisation of the Beck-Chevalley condition fails. These are not a defects of our system, but rather the inevitable consequence of studying linear logic in a categorical framework.

5.1 Factorisation Systems

We recall the definitions and basic facts about factorisation systems [FK72].

Let f and g be morphisms of a category C. We say that f is orthogonal to g, written f ↓ g, if whenever there exist maps u,v with vf = gu there is a unique diagonal fill-in w making both triangles below commute.

[figure: A; \overline{f}; B; u; w; v; C; \overline{g}; D]  (5.1)

Definition 5.1.1 A factorisation system for a category C is a pair (E, M), where E, M are classes of morphisms of C such that

1. Both E and M are closed under composition, and contain the isomorphisms.

2. Every morphism f of C has a factorisation f = me with e ∈ E and m ∈ M.

3. e ↓ m whenever e ∈ E and m ∈ M.

A factorisation system (E, M) is said to be proper if every element of E is an epimorphism and every element of M is a monomorphism.

Note 5.1.2 If hme = m′e′g with m, m′ ∈ M and e, e′ ∈ E, then since e ↓ m′ there is a unique k which makes the diagram below commute.

[figure: X; \overline{e}; Y; \overline{m}; Z; g; k; h; X′; \overline{e′}; Y′; \overline{m′}; Z′]  (5.2)

Taking g and h to be identities we see that the factorisation of a map f is unique up to isomorphism. Provided that there is a choice of factorisation for each f diagram 5.2 shows that factorisation determines a functor C^{·→·} → C^{·→·→·} which maps an arrow f in C to its image in M and co-image in E.

If F is a class of morphisms then we write F^{↓} for {g|f ↓ g for all f ∈ F} and F^{↑} for {g|g ↓ f for all f ∈ F}.

Lemma 5.1.3 [FK72] If (E, M) is a factorisation system for a category C then E = M^{↑} and M = E^{↓}.^{1}

Proof. From the definition of a factorisation system E ⊆ M^{↑} and M ⊆ E^{↓}. To show that M^{↑} ⊆ E, suppose g ∈ M^{↑} and let its factorisation be g = ip. Since p ↓ g, there is a unique diagonal map t which fills in the square below.

[figure: A; \overline{p}; C; 1; t; i; A; \overline{g}; B]  (5.3)

Let t = jq be the factorisation of t. By the uniqueness of the factorisation of j · qp = 1 = 1 · 1, we know that j is an isomorphism, and hence that t ∈ E. By the uniqueness of the factorisation 1 · i = gt = pt · i we have that pt is an isomorphism. Since tp = 1, it follows that (pt)^{−1}p is an inverse for t, and hence g = it^{−1} ∈ M. □

Definition 5.1.4 An epimorphism e in a category C is said to be extremal if whenever e = jt with j a monomorphism, then j is an isomorphism. Extremal monomorphisms are defined dually.

We write Epi for the class of epimorphisms in C and Epi^{†} for the class of extremal epimorphisms. Similarly, for monomorphisms we write Mon and Mon^{†}.

1In [FK72], classes of morphisms F, G such that F = G^{↑} and G = F^{↓} are said to form a pre-factorisation.

Proposition 5.1.5 If C has all finite limits and admits an intersection for every class of monomorphisms {m_{α} : X_{α} → A} then (Epi^{†}, Mon) is a proper factorisation system on C.

Proof. See [FK72] page 176. □

Thus, (Epi^{†}, Mon) is likely to be a proper factorisation system in any category with reasonable limit properties.

Examples 5.1.6

1. For any ring R, (Epi, Mon) is a factorisation system on the categories of R-modules. In particular this is true for the category of abelian groups (Z-modules) and vector spaces over a field F.

2. (Epi, Mon) is a factorisation system on any topos T (see [LS86]). When T = Set this factorisation restricts to the category Set_{∗} of pointed sets.

3. The category Cat of small categories has several factorisation systems, eg. (E_{i}, M_{i}) for i = 1, 2 where

E_{1} = {functors which are bijective on objects}
M_{1} = {fully faithful functors}
E_{2} = {initial functors}
M_{2} = {discrete op-fibrations}

The first of these is straightforward and details of the second can be found in [SW73].

We summarise some of the important properties of factorisation systems.

Lemma 5.1.7 If (E, M) is a factorisation system for C, then

1. E ∩ M is the class of isomorphisms in C.

2. M is closed under pullback.

3. If {p_{i} : X → Y_{i}}_{i∈S} is the limit of a diagram {m_{i} : Y_{i} → Z}_{i∈S} where each m_{i} is in M, then k = m_{i}p_{i} : X → Z is in M.

4. Let J be a category with terminal object t and F : J → C be a diagram such that every morphism in J is mapped to an element of M. If F has a limit then the projection lim F → F (t) is in M.

5. If i is a monomorphism, or i ∈ M, or every element of E is an epimorphism; then ij ∈ M implies j ∈ M.

6. If every element of E is an epimorphism then M contains all equalisers in C.

Proof. Easy consequences of lemma 5.1.3. Note that 3 is an immediate consequence of 4. □

If M is a class of monomorphisms then clause 3 means that M is closed under such intersections as exist. This is important for the interpretation of the additive conjunction. Similarly, clause 2 will be needed for the interpretation of substitution.

Definitions 5.1.8

1. Let A be an object of the category C. The slice category C/A is the category whose objects are morphisms with codomain A and whose morphisms f : g_{1} → g_{2} are commuting triangles g_{1} = g_{2}f.

2. Let F be any class of morphisms in a category C and A be an object of C. We define the relative slice category C/_{F}A to be the full subcategory of the slice category whose objects are the morphisms of F.

Note that if f : m_{1} → m_{2} in C/_{M}A then f is an element of M by lemma 5.1.7 (5).

Proposition 5.1.9

1. If C is complete (resp. finitely complete) then so is C/_{M}A.

2. If C has finite (resp. small) coproducts then so does C/_{M}A.

Proof. The first part is immediate from lemma 5.1.7. The second can be shown by verifying that the image factorisation of the morphism [m_{i}]_{i∈S} : Σ_{i∈S}X_{i} → A in C is a coproduct for the family {m_{i} : X_{i} → A}_{i∈S} of objects in C/_{M}A. □

5.1.1 Subobjects

If M ⊆ Mon then there is at most one map between any two objects of C/_{M}A. That is C/_{M}A is a preorder

m_{1} ≺ m_{2}  ⟺  m_{1} factors through m_{2}  (5.4)

We define the M-subobjects of A to be the equivalence classes of objects in C/_{M}A modulo ≺. Let Sub_{M}(A) denote the class of M-subobjects of A with the induced partial order ≤. We say that C is M-well powered if for each object A of C Sub_{M}(A) is a set.

Under reasonable assumptions, for example if C is finitely complete, M-well powered and has finite coproducts, Sub_{M}(A) is a lattice. If C is complete then Sub_{M}(A) is a complete lattice. The additive connectives of first order linear logic will be interpreted by the lattice operations in Sub_{M}(A).

Notation 5.1.10 For the rest of this chapter we deal with categories C with a specific factorisation system (E, M). It is convenient to redefine the notation on arrows relative to this. Let

[figure: X; \overline{e}; Y]

and

X ^{_{>} m} \overline{}Y

denote elements of E and M respectively. Note that, unless (E, M) is proper, these arrows are not necessarily epimorphic or monomorphic.

5.1.2 Direct and Inverse Images

Let C be a category with factorisation system (E, M) such that every map has a choice of factorisation, and suppose that f : A → B is a morphism of C. Then f induces a functor f_{∗} : C/_{M}A → C/_{M}B as follows. The direct image of m along f is defined to be the M part of the factorisation of fm.

[figure: X; \overline{e}; f_{∗}X; _{∨  ∨}; m; f_{∗}m; A; \overline{f}; B]  (5.5)

If there exist choices of pullback for elements of M along arbitrary maps in C then f also induces a functor f^{∗} : C/_{M}B → C/_{M}A. The inverse image f^{∗}k is the pullback of k along f. Note that f^{∗}k ∈ M by lemma 5.1.7 (2).

[figure: f^{∗}Y; Y; _{∨  ∨}; f^{∗}k; k; A; \overline{f}; B]  (5.6)

Proposition 5.1.11 The functors f_{∗} : C/_{M}A → C/_{M}B and f^{∗} : C/_{M}B → C/_{M}A are adjoint : f_{∗} ⊣ f^{∗}

The direct and inverse image constructions give rise to functors f_{∗} : Sub_{M}(A) → Sub_{M}(B) and f^{∗} : Sub_{M}(B) → Sub_{M}(A) on subobjects.

Example 5.1.12 Let f : A → B be a homomorphism of abelian groups and let X, Y be subgroups of A, B respectively. Then

b ∈ f_{∗}X ⟺ ∃x(f(x) = b and x ∈ X)  (5.7)
a ∈ f^{∗}Y ⟺ f(a) ∈ Y  (5.8)

These expressions are identical to the ones giving the direct and inverse images in Set. So, at least in these constructions, the logic of Ab agrees with the underlying logic in Set.

The expression for f_{∗}X makes it clear that we should regard the direct image as a form of existential quantification along the morphism f. The inverse image corresponds to substitution along f.

Note 5.1.13 By working exclusively with subobjects it is possible to avoid the assumption of specific choices of pullback and factorisation. However it is more convenient to continue working directly with the elements of M and assume that the appropriate choices exist.

Note 5.1.14 Although ultimately we are only interested in factorisation systems in which M ⊆ Mon, few of the results or constructions in this chapter rely on this assumption. We give proofs in general and note that these can often be simplified if M ⊆ Mon or E ⊆ Epi.

5.2 Monoidal Factorisations

Definition 5.2.1 Let (E, M) be a factorisation system on a symmetric monoidal category ⟨C, ⊗, I⟩. We say that (E, M) is a monoidal factorisation system if the class E is closed under the functor (−) ⊗ X for each object X of C, ie.

e ∈ E ⇒ e ⊗ 1_{X} ∈ E

or, equivalently, e_{1}, e_{2} ∈ E ⇒ e_{1} ⊗ e_{2} ∈ E.

Lemma 5.2.2 If C is a symmetric monoidal closed category with a factorisation system (E, M) then E is closed under (−) ⊗ X if and only if M is closed under [X, −].

Proof. To show that e ⊗ 1_{X} is in E, it suffices to show that it is orthogonal to every m ∈ M. Suppose there exist morphisms f and g such that the left hand square below commutes.

[figure: A ⊗ X; \overline{e ⊗ 1}; B ⊗ X; A; \overline{e}; B; g; h; λ(g); λ(h); C; \overline{m}; D; [X, C]; \overline{[1, m]}; [X, D]]  (5.9)

Then the righthand square also commutes because it is the transposition of the left across the adjunction (−) ⊗ X ⊣ [X, −]. As [1, m] is in M, there exists a diagonal fill-in for the right and hence, transposing back again, for the left. □

Let C be a symmetric monoidal closed category on which (Epi^{†}, Mon) is a factorisation system. Then [X, −] preserves monomorphisms because it is a right adjoint and Epi^{†} is closed under tensor by the above. Thus, by proposition 5.1.5, there are plenty of examples of monoidal factorisation systems.

Remark 5.2.3 It is tempting to strengthen definition 5.2.1 to require that both E and M are closed under tensor product. This holds for vector spaces and pointed sets, but fails in the important example of abelian groups.

Let i : Z → Q be the inclusion of the integers into the rationals. If a ∈ A satisfies na = 0 for a positive integer n then for any q ∈ Q

a ⊗ q = a ⊗ n(q/n) = na ⊗ (q/n) = 0 ⊗ (q/n) = 0  (5.10)

In particular if A is a torsion group then A ⊗ Q ≅ O. In this case 1_{A} ⊗ i cannot be a monomorphism since Z ⊗ A ≅ A.

5.3 Factorisation in Q-Set

There are two important subclasses of the morphisms in Q-Set. Let E denote the class of functional relations F : X → Y such that for all y, y′ ∈ |Y |

⋁_{x} F (x, y) ∘ F (x, y′) = Y (y, y′)  (5.11)

and let M denote those for which

X(x, x′) = ⋁_{y} F (x, y) ∘ F (x′, y)  (5.12)

for all x, x′ ∈ |X|. Note that by the axioms F1 and F2 both of these conditions already hold as an inequality left to right.

Theorem 5.3.1 (E, M) is a proper monoidal factorisation system on Q-Set.

Proof. First we note that every M ∈ M is a monomorphism. Suppose that M : X → Y is in M and F, G : U → X are functional relations such that MF = MG. Then

F (u, x) = ⋁_{x′} F (u, x′) ∘ X(x′, x)
= ⋁_{x′} F (u, x′) ∘ (⋁_{y} M(x′, y) ∘ M(x, y))
= ⋁_{y} MF (u, y) ∘ M(x, y)
= ⋁_{y} MG(u, y) ∘ M(x, y)
= G(u, x)

A similar calculation shows that every element of E is an epimorphism. From the elementary properties of fusion, both E and M are closed under tensor product.

To show that (E, M) is a factorisation system we first show that every map has an (E, M) factorisation. Let F : X → Y be a functional relation. We define a Q-set U with the same underlying set as X.

U(x, x′) = ⋁_{y} F (x, y) ∘ F (x′, y)  (5.13)

By F2 X(x, x′) ≤ U(x, x′) so the ‘equality’ on U is stronger than that on X. Reflexivity (Q1) is immediate and symmetry (Q3) follows from the commutativity of fusion. We check Q2

U(x, x′) ∘ U(x′, x′′) = ⋁_{y,y′} F (x, y) ∘ F (x′, y) ∘ F (x′, y′) ∘ F (x′′, y′)
≤ ⋁_{y,y′} F (x, y) ∘ Y (y, y′) ∘ F (x′′, y′)
= ⋁_{y} F (x, y) ∘ F (x′′, y) = U(x, x′′)  (5.14)

Let G : X → U and H : U → Y be defined by

G(x, u) = U(x, u)  (5.15)
H(u, y) = F (u, y)  (5.16)

It is easy to check that these are functional relations. We see that H ∈ M by replacing F with H in 5.13, and that G ∈ E by the following.

U(u, u′) = ⋁_{x} U(u, x) ∘ U(x, u′)
= ⋁_{x} G(x, u) ∘ G(x, u′)  (5.17)

The composite HG is equal to F.

HG(x, y) = ⋁_{u} G(x, u) ∘ H(u, y)
= ⋁_{u} U(x, u) ∘ F (u, y)
= F (x, y)  (5.18)

Thus we have shown that every map F factorises as a map in E followed by a map in M.

We now prove that maps in E are orthogonal to those in M and hence that (E, M) is a factorisation system. Let G ∈ E and H ∈ M and suppose that there exist functional relations F_{1} and F_{2} such that HF_{1} = F_{2}G. We need to show that there is a unique map K which makes both triangles in the diagram below commute.

[figure: U; \overline{G}; V; F_{1}; K; F_{2}; W; > H; X]  (5.19)

If such a map exists then it is certainly unique since G is epi. Take K to be H^{op}F_{2}. That is

K(v, w) = ⋁_{x} F_{2}(v, x) ∘ H(w, x)  (5.20)

This is the same as F_{1}G^{op} since

K(v, w) = ⋁_{x,v′} V (v, v′) ∘ F_{2}(v′, x) ∘ H(w, x)

= ⋁_{x,v′,u} G(u, v) ∘ G(u, v′) ∘ F_{2}(v′, x) ∘ H(w, x)
= ⋁_{x,u} G(u, v) ∘ F_{2}G(u, x) ∘ H(w, x)
= ⋁_{x,u} G(u, v) ∘ HF_{1}(u, x) ∘ H(w, x)
= ⋁_{u} G(u, v) ∘ F_{1}(u, w)  (5.21)

The last step is dual to the first two. We need to verify that K is a functional relation. It is not difficult to see that it satisfies R1 and R2. It satisfies F2 as follows

⋁_{w} K(v, w) ∘ K(v′, w) = ⋁_{w,u,u′} G(u, v) ∘ G(u′, v) ∘ F_{1}(u, w) ∘ F_{1}(u′, w)
≥ ⋁_{u,u′} G(u, v) ∘ G(u′, v′) ∘ U(u, u′)
= ⋁_{u} G(u, v) ∘ G(u, v′)
= V (v, v′)  (5.22)

and, by a similar argument, it satisfies F1. It remains to show that K makes diagram 5.19 commute.

KG(u, w) = ⋁_{v} G(u, v) ∘ K(v, w)
= ⋁_{v,x} G(u, v) ∘ F_{2}(v, x) ∘ H(w, x)
= ⋁_{w′,x} F_{1}(u, w′) ∘ H(w′, x) ∘ H(w, x)
= ⋁_{w′} F_{1}(u, w′) ∘ H(w′, w)
= F_{1}(u, w)  (5.23)

Thus KG = F_{1} and by a similar argument HK = F_{2}. □

Let M : X → Y be a morphism in M and suppose that Y is functionally complete so that M = m̂ for some Q-functor m : X → Y. Then

X(x, x′) = ⋁_{y} M(x, y) ∘ M(x′, y)
= ⋁_{y} Y (m(x), y) ∘ Y (m(x′), y)
= Y (m(x), m(x′))  (5.24)

Thus elements of M are essentially inclusions of a subspace where the subspace bears the induced equality. In general there may be monomorphisms in Q-Set which are not of this form.

Example 5.3.2 Let X be the unit circle with the metric d_{X} where d_{X}(x, x′) is the shortest distance between x and x′ along the perimeter of the circle, and let Y be the real plane with d_{Y} the Euclidean metric. The inclusion j : X ↪ Y is a monomorphism in the category of metric spaces and distance decreasing maps, so the induced functional relation J is mono in ℜ-Set because X and Y are complete metric spaces. However J ∉ M because d_{X}(x, x′) is strictly greater than d_{Y} (j(x), j(x′)) whenever x and x′ are distinct.

5.4 Non-fibrewise Operations

This section introduces the algebraic operations which will correspond to multiplicative connectives in first order linear logic.

5.4.1 Fusion from Tensor Product

There are two different ways to construct the cartesian product of objects m_{1} : X_{1} → A and m_{2} : X_{2} → A in the relative slice category C/_{M}A. The first is to take the pullback of m_{1} along m_{2} and obtain a map m_{1} ∧ m_{2} ∈ M into A by composition.

[figure: X_{1} ∧ X_{2}; \underline{>}; X_{1}; _{∨  ∨}; m_{1}; X_{2}; > m_{2}; A]  (5.25)

It is not difficult to check that this is isomorphic to the pullback of m_{1} ×m_{2} along the diagonal Δ_{A} : A → A × A.

[figure: X_{1} ∧ X_{2}; X_{1} × X_{2}; _{∨  ∨}; m_{1} ∧ m_{2}; m_{1} × m_{2}; A; \overline{Δ_{A}}; A × A]  (5.26)

This alternative view has the advantage of relating ∧ to the cartesian product ×.

Let C be a symmetric monoidal category with a monoidal factorisation system (E, M). We would like to obtain a second conjunction by replacing × with ⊗ in diagram 5.26. However, since the tensor product has no diagonal map, this cannot lead to a fibrewise operation. The best we can hope for is a binary operation which maps a pair of morphisms m_{1},m_{2} ∈ M with codomains A_{1}, A_{2} to a morphism m_{1} ∘ m_{2} in M with codomain A_{1} ⊗ A_{2}.

Recall from remark 5.2.3 that, in Ab, the tensor product of monomorphisms is not necessarily a monomorphism. Thus the fusion m_{1} ∘ m_{2} of maps m_{1} : X_{1} → A_{1} and m_{2} : X_{2} → A_{2} is defined to be the image of m_{1} ⊗ m_{2}.

[figure: X_{1} ⊗ X_{2}; X_{1} ∘ X_{2}; ∨; m_{1} ⊗ m_{2}; m_{1} ∘ m_{2}; A_{1} ⊗ A_{2}]  (5.27)

The domain of m_{1} ∘ m_{2} will be written X_{1} ∘ X_{2}, but it is important to remember that the meaning of this notation is relative to m_{1} and m_{2}.

Example 5.4.1 In Ab, the fusion of subgroups X_{1} ⊆ A_{1} and X_{2} ⊆ A_{2} is the subgroup of A_{1} ⊗ A_{2} generated by the elements x_{1} ⊗ x_{2} with x_{1} ∈ X_{1} , x_{2} ∈ X_{2}. We will see below that fusion is associative up to the associativity of ⊗. That is, there exists an isomorphism a′ making the following square commute.

[figure: (X_{1} ∘ X_{2}) ∘ X_{3}; \overline{≅ ; a′}; X_{1} ∘ (X_{2} ∘ X_{3}); ∨  ∨; (m_{1} ∘ m_{2}) ∘ m_{3}; m_{1} ∘ (m_{2} ∘ m_{3}); (A_{1} ⊗ A_{2}) ⊗ A_{3}; \overline{≅ ; a}; A_{1} ⊗ (A_{2} ⊗ A_{3})]  (5.28)

Similarly, ∘ is commutative up to the symmetry of ⊗ and 1Z : Z → Z is a unit for ∘ up to the natural isomorphism l_{A} : Z ⊗ A → A.

Given the non-fibrewise nature of fusion — even to express its associativity we need to compare subobjects in different fibres — it makes little sense to restrict our attention to a single fibre. Instead we consider the subobjects in C as a whole. Comparisons between different fibres consist of commuting squares and these define a category.

5.4.2 The Category Sqr (M)

Let Sqr (M) denote the full subcategory of the functor category C^{·→·} determined by the elements of M. That is an object of Sqr (M) is a morphism in M and a morphism from m_{1} to m_{2} is a pair of maps (g, h) forming a commutative square :

[figure: X_{1}; \overline{h}; X_{2}; m_{1}; m_{2}; A_{1}; \overline{g}; A_{2}]  (5.29)

If M ⊆ Mon and there is a morphism (g, h) : m_{1} → m_{2} in Sqr (M) then we say that m_{1} entails m_{2} along g (note that h is uniquely determined by g).

If C is a symmetric monoidal category with monoidal factorisation system (E, M) then fusion in C functorial. The fusion of maps (g_{1}, h_{1}) : m_{1} → n_{1} and (g_{2}, h_{2}) : m_{2} → n_{2} is given by the pair (g_{1} ⊗ g_{2}, h_{1} ∘ h_{2}) where h_{1} ∘ h_{2} is the unique map which makes the diagram below commute.

[figure: X_{1} ⊗ X_{2}; \overline{h_{1} ⊗ h_{2}}; Y_{1} ⊗ Y_{2}; X_{1} ∘ X_{2}; \overline{h_{1} ∘ h_{2}}; Y_{1} ∘ Y_{2}; _{∨  ∨}; m_{1} ∘ m_{2}; n_{1} ∘ n_{2}; A_{1} ⊗ A_{2}; \overline{g_{1} ⊗ g_{2}}; B_{1} ⊗ B_{2}]  (5.30)

Note that the symbol ‘∘’ has been overloaded again.

Lemma 5.4.2 ⟨Sqr (M) , ∘, 1_{I}⟩ is a symmetric monoidal category.

Proof. Let e_{1,2} and e_{2,3} be the E components of the factorisations used to construct X_{1} ∘ X_{2} and X_{2} ∘ X_{3}.

[figure: (X_{1} ⊗ X_{2}) ⊗ X_{3}; \overline{≅ ; a}; X_{1} ⊗ (X_{2} ⊗ X_{3}); e_{1,2} ⊗ 1; 1 ⊗ e_{2,3}; (X_{1} ∘ X_{2}) ⊗ X_{3}  X_{1} ⊗ (X_{2} ∘ X_{3}); (X_{1} ∘ X_{2}) ∘ X_{3}; ≅ ; a′; X_{1} ∘ (X_{2} ∘ X_{3}); ∨  ∨; (m_{1} ∘ m_{2}) ∘ m_{3}; m_{1} ∘ (m_{2} ∘ m_{3}); (A_{1} ⊗ A_{2}) ⊗ A_{3}; \overline{≅ ; a}; A_{1} ⊗ (A_{2} ⊗ A_{3})]  (5.31)

The exterior of diagram 5.31 represents two (E, M) factorisations of the same map. Thus there is a unique map a′ : (X_{1} ∘ X_{2}) ∘ X_{3} → X_{1} ∘ (X_{2} ∘ X_{3}) making the diagram commute. Moreover, a′ is an isomorphism.

The pair (a, a′) defines the associativity (m_{1} ∘ m_{2}) ∘ m_{3} ≅ m_{1} ∘ (m_{2} ∘ m_{3}) in Sqr (M) . Similar constructions give the symmetry and unit. The coherence conditions follow easily from those of C using the uniqueness properties of factorisations. □

The import of lemma 5.4.2 can be conveniently summed up in a slogan.

Slogan : The tensor product on C gives rise to a multiplicative structure on the category of subobjects as a whole rather than to the individual fibres.

5.4.3 Linear Implication by Pullback

Just as the fusion of two subobjects is a subobject of a tensor product, their linear implication is a subobject of an internal hom. Let m_{1}, m_{2} ∈ M then m_{1} −∘ m_{2} is defined by the following pullback diagram.

[figure: X_{1} −∘ X_{2}; \overline{ρ}; [X_{1}, X_{2}]; _{∨  ∨}; m_{1} −∘ m_{2}; [1, m_{2}]; [A_{1}, A_{2}]; \overline{[m_{1}, 1]}; [X_{1}, A_{2}]]  (5.32)

Note that [1, m_{2}] ∈ M because (E, M) is monoidal, and so m_{1} −∘ m_{2} ∈ M because M is closed under pullback.

It is natural to ask in what sense can m_{1} −∘ m_{2} be considered an ‘implication’. We shall see below that linear implication is related to fusion by an adjunction in much the same way as in the propositional case. The situation is slightly more complex because the various objects involved in the adjunction lie in different fibres. The meaning of m_{1} −∘ m_{2} is clarified by the following two examples.

Example 5.4.3 Let X_{1} ⊆ A_{1} and X_{2} ⊆ A_{2} be inclusions in Set. Then

f ∈ X_{1} −∘ X_{2}  iff  ∀a ∈ A_{1}(a ∈ X_{1} ⇒ f(a) ∈ X_{2})  (5.33)

That is, X_{1} −∘ X_{2} is the set of functions A_{1} → A_{2} which map elements of X_{1} to elements of X_{2}.

Example 5.4.4 Let X_{1} and X_{2} be subgroups of the abelian groups A_{1} and A_{2} respectively. Then X_{1} −∘ X_{2} is the subgroup of [A_{1}, A_{2}] consisting of all homorphisms which map X_{1} into X_{2}. An element of (X_{1} −∘ X_{2}) ∘ X_{1} is a finite sum Σ_{i}f_{i} ⊗ x_{i} where x_{i} ∈ X_{1} and the f_{i} are homorphisms from A_{1} to A_{2} mapping X_{1} into X_{2}. It follows that

ε(Σ_{i}f_{i} ⊗ x_{i}) = Σ_{i}f_{i}(x_{i})  (5.34)

is an element of X_{2} and hence that (X_{1} −∘ X_{2})∘X_{1} entails X_{2} along the evaluation map ε : [A_{1}, A_{2}] ⊗ A_{1} → A_{2}.

Theorem 5.4.5 Let C be a symmetric monoidal closed category with monoidal factorisation system (E, M) and suppose there exists a choice of pullback for each m ∈ M and f ∈ Mor(C). Then ⟨Sqr (M) , ∘, 1_{I}, −∘ ⟩ is symmetric monoidal closed.

Proof. From lemma 5.4.2 we know that ⟨Sqr (M) , ∘, 1_{I}⟩ is a symmetric monoidal category, it remains to show that it is closed. For m_{1}, m_{2} ∈ M we construct a morphism ε_{m_{1},m_{2}} : (m_{1} −∘ m_{2})∘m_{1} → m_{2} in Sqr (M) and show that it is universal from (−) ∘ m_{1} to m_{2}.

First, observe that the following three squares, the front faces of a cube, form a commutative diagram.

[figure: (X_{1} −∘ X_{2}) ⊗ X_{1}; \overline{ρ ⊗ 1}; [X_{1}, X_{2}] ⊗ X_{1}; ε_{X_{1},X_{2}}; (m_{1} −∘ m_{2}) ⊗ 1; [1, m_{2}] ⊗ 1; X_{2}; ∨; [A_{1}, A_{2}] ⊗ X_{1}; \overline{[m_{1}, 1] ⊗ 1}; [X_{1}, A_{2}] ⊗ X_{1}; m_{2}; 1 ⊗ m_{1}; ε_{X_{1},A_{2}}; [A_{1}, A_{2}] ⊗ A_{1}; \overline{ε_{A_{1},A_{2}}}; A_{2}]  (5.35)

The top left hand square is just the pullback 5.32 tensored with X_{1}. The commutativity of the other two squares follow from the fact that evaluation in C is dinatural in its first and third arguments and natural in its second. The evaluation map ε_{m_{1},m_{2}} is defined to be the pair (\underline{ε}, \overline{ε}) where \underline{ε} is the evaluation ε_{A_{1},A_{2}} : [A_{1}, A_{2}] ⊗ A_{1} → A_{2} in C and \overline{ε} is the unique map making the following diagram, the remaining faces of the cube, commute.

[figure: (X_{1} −∘ X_{2}) ⊗ X_{1}; \overline{ρ ⊗ 1}; [X_{1}, X_{2}] ⊗ X_{1}; ε_{X_{1},X_{2}}; (m_{1} −∘ m_{2}) ⊗ 1; [X_{1}, A_{2}] ∘ X_{1}; \overline{ε}; X_{2}; _{∨  ∨}; [A_{1}, A_{2}] ⊗ X_{1}; (m_{1} −∘ m_{2}) ∘ m_{1}; m_{2}; 1 ⊗ m_{1}; [A_{1}, A_{2}] ⊗ A_{1}; \overline{ε_{A_{1},A_{2}}}; A_{2}]  (5.36)

Let k : Y → B be a morphism in M and let α = (\underline{α}, \overline{α}) be a map k ∘ m_{1} → m_{2} in Sqr (M) . We need to show that there is a unique morphism σ : k → m_{1} −∘ m_{2} such that ε_{m_{1},m_{2}}(σ ∘ 1_{m_{1}}) = α.

[figure: k  k ∘ m_{1}; σ; (σ ∘ 1_{m_{1}}); α; m_{1} −∘ m_{2}; (m_{1} −∘ m_{2}) ∘ m_{1}; \overline{ε_{m_{1},m_{2}}}; m_{2}]  (5.37)

Remember that k ∘ m_{1} is the M part of the (E, M) factorisation of k ⊗ m and let e be the E part. We have the following commutative diagram in C.

[figure: Y ⊗ X_{1}; \overline{e}; Y ∘ X_{1}; \overline{\overline{α}}; X_{2}; _{∨  ∨}; k ⊗ 1; k ∘ m_{1}; m_{2}; B ⊗ X_{1}; \overline{1 ⊗ m_{1}}; B ⊗ A_{1}; \overline{\underline{α}}; A_{2}]  (5.38)

Transposing diagram 5.38 across the adjunction (−) ⊗ X_{1} ⊣ [X_{1}, −] gives

[figure: Y; \overline{λ(\overline{α}e)}; [X_{1}, X_{2}]; _{∨  ∨}; k; [1, m_{2}]; B; \overline{λ(\underline{α}(1 ⊗ m_{1}))}; [X_{1}, A_{2}]]  (5.39)

Recall from remark 3.1.5 that the isomorphism λ_{U,V,W} : C(U⊗V, W) ≅ C(U, [V, W]) is natural in V as well as in U, W. Therefore

λ(\underline{α}(1 ⊗ m_{1})) = [m_{1}, 1]λ(\underline{α})  (5.40)

and so the commutative square in diagram 5.39 forms the exterior of diagram 5.41.

[figure: \overline{λ(\overline{α}e)}; Y; \overline{σ}; X_{1} −∘ X_{2}; \overline{ρ}; [X_{1}, X_{2}]; _{∨  ∨  ∨}; k; m_{1} −∘ m_{2}; [1, m_{2}]; B; \overline{λ(\underline{α})}; [A_{1}, A_{2}]; \overline{[m_{1}, 1]}; [X_{1}, A_{2}]]  (5.41)

We define σ to be the pair (\underline{σ}, \overline{σ}) where \underline{σ} = λ(\underline{α}) and \overline{σ} is the unique mediator of the pullback in 5.41. It is clear that σ is a morphism of Sqr (M) , it remains to check that it satisfies the conditions required.

[figure: Y ⊗ X_{1}; \overline{\overline{σ} ⊗ 1}; (X_{1} −∘ X_{2}) ⊗ X_{1}; e; ε_{X_{1},X_{2}}(ρ ⊗ 1); Y ∘ X_{1}; \overline{\overline{σ} ∘ 1}; (X_{1} −∘ X_{2}) ∘ X_{1}; \overline{\overline{ε}}; X_{2}; _{∨  ∨  ∨}; k ∘ m_{1}; (m_{1} −∘ m_{2}) ∘ m_{1}; m_{2}; B ⊗ A_{1}; \overline{\underline{σ} ⊗ 1}; [A_{1}, A_{2}] ⊗ A_{1}; \overline{\underline{ε}}; A_{2}]  (5.42)

The composite ε_{m_{1},m_{2}}(σ ∘ 1) is given by the lower half of diagram 5.42. Note that this diagram commutes from the definitions of ε_{m_{1},m_{2}} and σ ∘ 1. The lower component of ε_{m_{1},m_{2}}(σ ∘ 1) is

\underline{ε}(\underline{σ} ⊗ 1) = ε_{A_{1},A_{2}}(λ(\underline{α}) ⊗ 1) = \underline{α}  (5.43)

It remains to show that the upper component \overline{ε}(\overline{σ} ∘ 1) is \overline{α}. From the definition of \overline{σ} we know that ρ\overline{σ} = λ(\overline{α}e). Hence

ε_{X_{1},X_{2}}(ρ ⊗ 1)(\overline{σ} ⊗ 1) = ε_{X_{1},X_{2}}(λ(\overline{α}e) ⊗ 1) = \overline{α}e  (5.44)

Also \underline{α}(k ∘ m_{1}) = m_{2}\overline{α} because (\underline{α}, \overline{α}) : k ∘ m_{1} → m_{2} is a morphism of Sqr (M) . These two equations are to enough to ensure that \overline{α} = \overline{ε}(\overline{σ} ∘ 1) because of the orthogonality between e and m_{2}.

Let τ = (\underline{τ}, \overline{τ}) be any morphism of Sqr (M) which satisfies ε_{m_{1},m_{2}}(τ ∘1_{m_{1}}) = α. The first component \underline{τ} satisfies ε_{A_{1},A_{2}}(\underline{τ} ⊗ 1) = \underline{α} and hence \underline{τ} = λ(\underline{α}) by the universal property of ε_{A_{1},A_{2}}.

The second component \overline{τ} satisfies \overline{ε}(\overline{τ} ∘ 1) = \overline{α}. Precomposing with e yields

ε_{X_{1},X_{2}}(ρ\overline{τ} ⊗ 1) = \overline{ε}(\overline{τ} ∘ 1)e = \overline{α}e  (5.45)

Thus ρ\overline{τ} = λ(\overline{α}e) by the universal property of ε_{X_{1},X_{2}} and \overline{σ} = \overline{τ} by the uniqueness of the mediator in diagram 5.41. □

5.5 Algebraic Limitations

To explain the problems involved in developing a logic of symmetric monoidal closed categories it suffices to take Ab as an example. We have seen that (Epi, Mon) is a monoidal factorisation system on Ab, and so provides a model for the calculus L_{F OLL} of first order linear logic presented in the next chapter. We make a series of observations on the structure of Ab which shape the logic L_{F OLL}. These mostly amount to drawing distinctions between M-subobjects one might have thought equivalent. The logic must respect these distinctions and this necessitates the use of side conditions on the rules to carefully limit the derivations.

A key observation on the subobject structure of Ab is that Sub(G) is not necessarily distributive. For example, let U, V, W be the three distinct subgroups of order 2 in Z_{2} ⊕ Z_{2}.

[figure: Z_{2} ⊕ Z_{2}; m; U  V  W; O]  (5.46)

Then U ∧(V ∨W) = U strictly contains (U ∧V)∨(U ∧W) = O. This observation has led algebraists to the study of modular rather than distributive lattices (see [Bir48]). Recall from chapter 2 that the distributive law does not hold as a theorem of propositional linear logic.

Regarding Sub(U) as a sublattice of Sub(Z_{2} ⊕ Z_{2}) the operation U ∧ (−) is equivalent to m^{∗}. The nondistributivity of Sub(Z_{2} ⊕ Z_{2}) can therefore be restated as the fact that m^{∗} : Sub(Z_{2} ⊕ Z_{2}) → Sub(Z_{2}) fails to preserve suprema. In particular, the following inclusion is strict

m^{∗}V ∨ m^{∗}W ⊂ m^{∗}(V ∨ W)  (5.47)

This has two unpleasant consequences for our logic which might initially seem to be quite serious drawbacks. Firstly, it means that m^{∗} cannot have a right adjoint and so, in the internal logic of Ab and hence in our version of first order linear logic, there is no notion of universal quantification. Secondly, it means that substitution does not arbitrarily permute with logical connectives; in this case, it fails to permute with join. These problems are so closely related to linearity in the model that it would be impossible to correct them without making restrictions which are sufficient to rule out most of the natural examples. In the absence of a clear remedy, it seems more sensible to accept these features as part of the nonstandard flavour of the logic rather than attempting a cure.

Join is not the only connective which behaves badly with respect to substitution. One might expect to be able to exchange pullback and fusion as follows.

(f^{∗}X) ∘ Y = (f ⊗ 1)^{∗}(X ∘ Y)  (5.48)

where X, Y are subgroups of A, B and f is a group homorphism A′ → A. In general this only holds as an inclusion left to right.

Example 5.5.1 Let i : Z → Q be the inclusion of the integers into the rationals and consider the two subgroups O ↪ Q and Z_{p} ↪ Z_{p}. We note that the subgroup (i ⊗ 1_{Z_{p}})^{∗}(O ∘ Z_{p}) of Z ⊗ Z_{p} ≅ Z_{p} is actually the entire group, whereas i^{∗}O ⊗ Z_{p} is the trivial subgroup.

\{  [figure: O; O; _{∨  ∨}; Z; \overline{i}; Q] \} ⊗ Z_{p} ≅  [figure: O; O; _{∨  ∨}; Z_{p}; O]  (5.49)

Note 5.5.2 In Ab the pullback of the unique map O → H along f : G → H is the kernel of f. In logical terms, this means that substituting into the “false” predicate has a nontrivial content.

5.5.1 The Beck Chevalley Condition

Let ur = st be a commutative square in C and suppose that m is a morphism in M with the same codomain as r. Consider the following cube.

[figure: r^{∗}Y; e′; s^{∗}u_{∗}Y; _{∨  ∨}; s^{∗}u_{∗}m|; r^{∗}m; X; u_{∗}X; _{∨  ∨}; m; A; \overline{t}; B; u_{∗}m; r; s; C; \overline{u}; D]  (5.50)

The front face is the (E, M) factorisation defining u_{∗}m and the two sides are the pullbacks defining r^{∗}m and s^{∗}u_{∗}m respectively. As the left face is a pullback there is a unique map e′ : r^{∗}Y → s^{∗}u_{∗}Y making the top and back commute. It follows that t_{∗}r^{∗}m factors through s^{∗}u_{∗}m so there exists a map t_{∗}r^{∗}m → s^{∗}u_{∗}m in C/_{M}B.

We say that C satisfies the Beck Chevalley condition if this map is an isomorphism whenever the square ur = st is a pullback. As is well known, this holds precisely when E is closed under pullback.

If the base of 5.50 is a pullback then so is the top by elementary properties of pullback squares. E closed under pullback means that e′ ∈ E and hence the comparison t_{∗}r^{∗}m → s^{∗}u_{∗}m is an isomorphism by the uniqueness of factorisation. Conversely, suppose that the base of 5.50 is a pullback with u ∈ E. Take m to be the identity on C so that all the vertical maps are isomorphisms. By the Beck condition the image of t is iso and hence t ∈ E.

Let f : A → C and g : B → D and consider the following commuting square.

[figure: A ⊗ B; \overline{1_{A} ⊗ g}; A ⊗ D; f ⊗ 1_{B}; f ⊗ 1_{D}; C ⊗ B; \overline{1_{C} ⊗ g}; B ⊗ D]  (5.51)

In the particular case where ⊗ is actually the cartesian product then 5.51 is a pullback diagram, and provided that C satisfies the Beck condition then

∃_{f⊗1_{B}}(1_{A} ⊗ g)^{∗} = (1_{C} ⊗ g)^{∗}∃_{(f⊗1_{D})}  (5.52)

This would seem a desirable property since it states that substitution and existential quantification do not interfere when they act on different variables. However, it is too much to expect 5.52 to hold in general. Even if C satisfies the Beck condition, there is no reason why 5.51 should be a pullback. For example, let i : Z → Q be the inclusion of the integers in the rationals and let h : Z → Z_{p} be the quotient map with kernel pZ.

[figure: Z ⊗ Z; \overline{i ⊗ 1}; Q ⊗ Z; Z; \overline{i}; Q; 1 ⊗ h; 1 ⊗ h; h; Z ⊗ Z_{p}; \overline{i ⊗ 1}; Q ⊗ Z_{p}; Z_{p}; O]  (5.53)

We showed in 5.2.3 that Q ⊗ Z_{p} ≅ O. Thus the lefthand square is isomorphic to the right which is clearly not a pullback.

Consider the trivial subgroup of Z_{p}. Pulling back along h and then taking the image along i we obtain pZ as a subgroup of Q ; but taking the image and then pulling back we obtain the whole of Q.

First Order Linear Logic

In the previous chapter, we saw various algebraic operations which can be defined on the M-subobjects of a symmetric monoidal closed category C with monoidal factorisation system (E, M). These operations provide the connectives for the internal logic of C. We already know some of their algebraic properties: recall from lemma 5.4.2 that fusion is associative, and from theorem 5.4.5 that fusion and linear implication are related by an adjunction; but so far, we have only alluded to the form of logic which they define.

In this chapter, we give a syntactic account of the internal logic using a formal system L_{F OLL}. This is a first order extension of the sequent calculus presentation of propositional linear logic and is based on the type theory of chapter 3.

Recall from section 5.5, that some of the familiar principles of logic fail in the context of M-subobjects. Notably, the logical connectives do not necessarily commute with substitution. We shall see that others remain valid (eg. the distributive laws of section 6.3.1). The proposed sequent calculus is carefully formulated to allow only the valid inferences to be derived. Thus, the logic L_{F OLL} delimits the fragment of ordinary first order reasoning available in symmetric monoidal closed categories. This is achieved via restrictions on the occurrence of variables and also on the use of substitution operators. These restrictions appear quite natural in the sequent calculus presentation. For instance, the variable balancing property says that each variable which appears has exactly one occurrence on each side of the turnstile.

Each of the algebraic operations defined in chapter 5 gives rise to a corresponding logical operation on the predicates of L_{F OLL}. A formula in L_{F OLL} consists of a predicate applied to a term of LTT. For instance, if ϕ and ψ are predicates on terms of type A and B respectively then their fusion is a predicate on pairs of type A ⊗ B. We write (ϕ ∘ ψ)(s, t) rather than ϕ(s) ∘ ψ(t) to emphasise this. This choice is also important with respect to the relative order of binding between logical operations and substitution.

Since variables cannot be repeated in the terms of LTT, we cannot form the expression (ϕ ∘ ψ)(x, x). On the other hand the operations of meet and join are fibrewise. The repetition of variables in ϕ(x) ∧ ψ(x) is therefore harmless and we write (ϕ ∧ ψ)(x) to be clear.

Both fusion and meet can be read naturally as “and”: (ϕ ∘ ψ)(s, t) means that ϕ holds of s and ψ holds of t, whereas (ϕ ∧ ψ)(s) means that both ϕ and ψ hold of s. The fact that they apply to different arguments removes some of the confusion generated by having two forms of conjunction.

The meaning of the other connectives requires some explanation. Recall that the linear implication of two M-subobjects is a subobject of an internal hom. Thus, in the logic L_{F OLL}, if ϕ and ψ are predicates of type A and B respectively then the linear implication ϕ −∘ ψ is a predicate of the hom type [A, B]. Given a term f of type [A, B], we expect ϕ −∘ ψ to hold of f if whenever ϕ holds of a term s of type A then ψ holds of f evaluated at s. This form of implication is already quite familiar in computer science (eg. see [BJ90]). One can think of the linear implication ϕ −∘ ψ as a specification of the function term f. The predicates ϕ and ψ are the precondition and postcondition of the specification respectively, and a function f satisifies the specification if whenever its input satisfies the precondition then its output satisfies the postcondition. Note that if we were working in ordinary first order logic then this would be a compound statement involving both implication and universal quantification. The restrictions imposed by the structure of symmetric monoidal closed categories force us to accept the above operation as primitive.

The form of existential quantification presented in L_{F OLL} is quite standard in categorical logic. Recall that if m is an M-subobject of an object X and g : X → Y is a morphism of C then the direct image g^{∗}(m) is a subobject of Y. Correspondingly in the logic L_{F OLL}, if ϕ is a term of type A and α is a combinator of type A → B then ∃[α]ϕ is a predicate of type B. The intended meaning of ∃[α]ϕ(t) is that there exists an element x of type A such that α(x) = t and ϕ(x) holds. Again, this would be a compound statement in ordinary logic but here we are forced to take it as primitive.

The remaining operations are straightforward. The fibrewise join of M-subobjects correponds to a binary connective ∨ which can adequately read as “or”: ϕ∨ψ holds of s if either ϕ or ψ holds of s. The inverse image operations on M-subobjects correspond to substition operators in the logic. If ψ is a predicate of type B and α is a combinator of type A → B then α^{∗}ψ is a predicate of type A. Given a term s of type A, the meaning of α^{∗}ϕ(s) is the same as that of ϕ(α(s)).

Finally, the top and bottom elements of the subobject lattices Sub_{M}(X) give rise to constants T_{A} and F_{A} for each type A. These are units for the logical operations of meet and join. T_{I} is also a unit for fusion.

Recall from chapter 3 that the language of linear type theory has three parameters : a set B of basic types, a set F of function symbols, and a set E of equations. The language of first order linear logic is defined in terms of these parameters, but also has the additional parameter P which is a set of atomic predicates. We use L_{F OLL}(B, F, E, P) to denote the language of first order linear logic with parameters B, F, E and P.

In section 6.1 we define the formulae of first order linear logic; in section 6.2 we present the rules; and in section 6.3 we derive some basic theorems and properties of L_{F OLL}, and illustrate the use of the language by two examples arising from the subobjects of a monoid and Girard’s ‘double negation’ closure operation respectively.

6.1 Formulae and Sequents

Let P = {ϕ, ψ, θ, …} be a set of predicate symbols each of which has an associated type. We use the following rules to define a set pred(A), the predicates of type A, for each type A in LTT(B, F, E).

1. If ϕ is a predicate symbol of type A then ϕ ∈ pred(A).

2. If ϕ ∈ pred(A) and ψ ∈ pred(B) then ϕ ∘ ψ ∈ pred(A ⊗ B) and ϕ −∘ ψ ∈ pred([A, B]).

3. If ϕ and ψ are members of pred(A) then so are ϕ ∧ ψ and ϕ ∨ ψ.

4. If ϕ ∈ pred(B) and α is a combinator of type A → B then α^{∗}ϕ ∈ pred(A).

5. If ϕ ∈ pred(A) and α is a combinator of type A → B then ∃[α]ϕ ∈ pred(B).

6. T_{A} and F_{A} are members of pred(A), for all A.

A formula ϕ(s) of type A consists of a predicate ϕ of type A applied to a term s of type A.

A sequent is an expression

Γ ⊢ ϕ(s)

where ϕ(s) is a formula and Γ is a finite list of formulae. The formulae before the turnstile ⊢ are termed the antecedents and the single formula after the turnstile is the succedent.

A sequent Γ ⊢ ϕ(s) is said to be well formed if each variable which appears in Γ or ϕ(s) has exactly one occurrence on each side of the turnstile. This ‘variable balancing’ property is essential to the interpretation of sequents given in section 7.2.

A sequent Γ ⊢ ϕ(s) is said to be valid in L_{F OLL}(B, F, E, P) if it can be derived from the rules given in the following section.

6.2 Rules

As in the propositional case, the rules are divided into those which operate on the structure of derivation trees and those which introduce logical connectives.

6.2.1 Structural Rules

For each formula ϕ(s), we allow :

(Ref) \overline{ϕ(s) ⊢ ϕ(s)}

We also accept the structural rules of Exchange (on the left), and Cut :

(Ex)  \frac{Γ_{1}, ϕ(s), ψ(t), Γ_{2} ⊢ θ(u)}{Γ_{1}, ψ(t), ϕ(s), Γ_{2} ⊢ θ(u)}
(Cut) \frac{Γ_{1}, ϕ(s) ⊢ ψ(t)  Γ_{2} ⊢ ϕ(s)}{Γ_{1}, Γ_{2} ⊢ ψ(t)}

The structural rules of contraction and weakening would allow the formulae of a sequent to be duplicated and discarded respectively. They cannot be incorporated into L_{F OLL} without violating the restrictions on the occurrence of variables, and are therefore forbidden.

As in the propositional case, the presence of exchange simplifies many of the other rules.

6.2.2 Logical Rules

The logical rules are subject to two forms of restriction. Firstly, there are restrictions on the occurence of variables, which ensure that all the derivable sequents are well formed. Secondly, the introduction rules for connectives are often restricted to predicates on basic terms (that is, terms containing no combinators). This maintains an order between the introduction of connectives and the introduction of substitution operators, and so prevents the derivation of sequents in which these are permuted.

Notation 6.2.1 If e is either a term, a formula, or a list of formulae in the languange of L_{F OLL} then V (e) denotes the set of variables occuring in e.

True and False

(TR)  \overline{Γ ⊢ T_{X}(s)}  V (Γ) = V (s)
(TL)  \frac{Γ ⊢ ϕ(s)}{Γ, T_{I}() ⊢ ϕ(s)}
(T⊗) \frac{Γ, T_{X}(s), T_{Y} (t) ⊢ ϕ(u)}{Γ, T_{X⊗Y} (s, t) ⊢ ϕ(u)}

(F)

\overline{Γ, F_{X}(x) ⊢ ϕ(s)}

x is a basic term and V (Γ) ∪ V (x) = V (s).

Note that ⊢ T_{I}() is derivable as a special case of (TR).

Fusion

(∘R) \frac{Γ_{1} ⊢ ϕ(s)  Γ_{2} ⊢ ψ(t)}{Γ_{1}, Γ_{2} ⊢ (ϕ ∘ ψ)(s, t)} V (Γ_{1}) ∩ V (Γ_{2}) = ∅
(∘L) \frac{Γ_{1}, ϕ(x), ψ(y), Γ_{2} ⊢ θ(u)}{Γ_{1}, (ϕ ∘ ψ)(x, y), Γ_{2} ⊢ θ(u)} x, y are basic terms.

Linear Implication

( −∘ R)  \frac{Γ, ϕ(x) ⊢ ψ(eval_{X,Y} (f, x))}{Γ ⊢ (ϕ −∘ ψ)(f)}  x is a basic term.
( −∘ L) \frac{Γ_{1} ⊢ ϕ(s) Γ_{2}, ψ(eval_{X,Y} (f, s)) ⊢ θ(t)}{Γ_{2}, (ϕ −∘ ψ)(f), Γ_{1} ⊢ θ(t)}

Existential Quantification

(∃R)  \frac{Γ ⊢ ϕ(s)}{Γ ⊢ (∃[α]ϕ)(α(s))}

(∃L) \frac{Γ, ϕ(x) ⊢ ψ(s[α(x)/v])}{Γ, (∃[α]ϕ)(v) ⊢ ψ(s)} x is a basic term and v does

not occur in the premise.

Meet

(∧L1) \frac{Γ, ϕ(s) ⊢ θ(t)}{Γ, (ϕ ∧ ψ)(s) ⊢ θ(t)}  (∧L2) \frac{Γ, ψ(s) ⊢ θ(t)}{Γ, (ϕ ∧ ψ)(s) ⊢ θ(t)}

(∧R) \frac{Γ ⊢ ϕ(s)  Γ ⊢ ψ(s)}{Γ ⊢ (ϕ ∧ ψ)(s)}

Note that the rules for meet have no side conditions. This reflects the fact that meet behaves well with respect to substitution.

Join

(∨L) \frac{Γ, ϕ(x) ⊢ θ(t)  Γ, ψ(x) ⊢ θ(t)}{Γ, (ϕ ∨ ψ)(x) ⊢ θ(t)} x is a basic term.

(∨R1) \frac{Γ ⊢ ϕ(s)}{Γ ⊢ (ϕ ∨ ψ)(s)}  (∨R2) \frac{Γ ⊢ ψ(s)}{Γ ⊢ (ϕ ∨ ψ)(s)}

Substitution

(∗L) \frac{Γ, ϕ(α(s)) ⊢ ψ(t)}{Γ, α^{∗}ϕ(s) ⊢ ψ(t)}  (∗R) \frac{Γ ⊢ ϕ(α(s))}{Γ ⊢ α^{∗}ϕ(s)}

(≈ L) \frac{Γ, ϕ(s) ⊢ ψ(u)  s ≈ t}{Γ, ϕ(t) ⊢ ψ(u)}  (≈ R) \frac{Γ ⊢ ϕ(s)  s ≈ t}{Γ ⊢ ϕ(t)}

(Subst1) \frac{Γ, ϕ(s) ⊢ ψ(t)}{Γ, ϕ(s[u/v]) ⊢ ψ(t[u/v])} none of the variables of u

occur in the premise.

(Subst2) \frac{Γ, ϕ(s[x/v]) ⊢ ψ(t[x/v])}{Γ, ϕ(s) ⊢ ψ(t)} x is a basic term and

v does not occur in Γ.

6.3 Properties of the Calculus L_{F OLL}

The following lemma shows that our rules have the promised variable balancing property.

Lemma 6.3.1 Every derivable sequent of L_{F OLL} is well formed.

Proof. By induction on the structure of derivations. Clearly the conclusion ϕ(s) ⊢ ϕ(s) of the reflexive rule (Ref) is well formed because s contains no repeated variables. The other rules preserve this property.

For instance, consider ( −∘ L). The induction hypothesis states that

V (Γ_{1}) = V (ϕ(s))

and

V (Γ_{2}, ψ(eval (f, s))) = V (θ(t))

and furthermore that no variable is repeated in Γ_{1} or Γ_{2}, ψ(eval (f, s)). By the first of these equations, V ((ϕ −∘ ψ)(f), Γ_{1}) = V (f, s) = V (ψ(eval (f, s))) and hence by the second

V (Γ_{2}, (ϕ −∘ ψ)(f), Γ_{1}) = V (θ(t))

Now, since no variable is repeated in Γ_{2}, ψ(eval (f, s)), we must have V (Γ_{1}) ∩ V (Γ_{2}) = ∅ and hence no variable is repeated in Γ_{2}, (ϕ −∘ ψ)(f), Γ_{1}. □

Note 6.3.2 As a consequence of lemma 3.2.12, every formula ϕ(s) is provably equivalent to a predicate applied to a basic term :

ϕ(s) ⊣⊢ (ac(s)^{∗}ϕ)(abt(s))  (6.1)

Remark 6.3.3 As both variables and predicates have a specified type, it is often possible to determine both the domain and codomain of the combinators appearing in fomula ϕ(t), in which case we may omit the subscripts on their components. For example, this holds if ϕ(t) = α^{∗}ψ(s) or ϕ(t) = ∃[β]ψ(x) with ψ atomic and x basic. However, there are important situations where this is not the case, and the subscripts must be retained. For instance, if

ϕ(t) = (∃[eval_{X,Y}] eval_{X,Y}^{∗} ψ)(x)  (6.2)

then X cannot be deduced from the types of x and ψ alone.

6.3.1 Theorems and Derivations in L_{F OLL}

We define a preorder on predicates as follows. Let ϕ, ψ ∈ pred(A) then

ϕ ⊢ ψ ⟺ ϕ(x) ⊢ ψ(x) is a derivable sequent in L_{F OLL}  (6.3)

where x is a basic term of type A. The rules for substitution ensure that this definition is independent of the choice of x. The reflexivity and transitivity of ⊢ follow from (Ref) and (Cut) respectively.

Let ⊣⊢ denote the equivalence relation induced by ⊢, that is

ϕ ⊣⊢ ψ ⟺ ϕ ⊢ ψ and ψ ⊢ ϕ

Lemma 6.3.4 The logical operations ∘, ∨, ∧, α^{∗} and ∃[α] are monotone with respect to the preorder ⊢. Linear implication −∘ is anti-monotone in its first argument and monotone in its second.

It follows that the equivalence ⊣⊢ on predicates is a congruence relation with respect to the logical operations.

Lemma 6.3.5 Let ϕ and ψ be predicates of type A and B respectively, and let α, β be combinators of type A → B. Then

α ≡ β ⇒ ∃[α]ϕ ⊣⊢ ∃[β]ϕ′  (6.4)
α ≡ β ⇒ α^{∗}ψ ⊣⊢ β^{∗}ψ′  (6.5)

Many of the laws which hold in propositional linear logic have a counterpart in L_{F OLL}, although the interpretation here is slightly different. For example, the properties of fusion and the distributive laws given below are well known as valid sequents of the propositional logic, but here they refer to the typed predicates of L_{F OLL}. The derivations required are given by modifying the corresponding ones in the propositional calculus and we omit them here. There are some more substantial derivations to be found in the proof of first order specific properties, for example proposition 6.3.9.

Proposition 6.3.6 For all predicates ϕ, ψ and θ the following laws are derivable in L_{F OLL}.

T_{I} ∘ ϕ ⊣⊢ ϕ  (6.6)
ϕ ∘ ψ ⊣⊢ ψ ∘ ψ  (6.7)
ϕ ∘ (ψ ∘ θ) ⊣⊢ (ϕ ∘ ψ) ∘ θ  (6.8)

Proposition 6.3.7 Let ϕ be a predicate of type A and let ψ and θ be predicates of type B. The following laws are derivable in L_{F OLL}.

ϕ ∘ F_{B} ⊣⊢ F_{A⊗B}  (6.9)
ϕ ∘ (ψ ∨ θ) ⊣⊢ (ϕ ∘ ψ) ∨ (ϕ ∘ θ)  (6.10)
ϕ −∘ T_{B} ⊣⊢ T_{[A,B]}  (6.11)
ϕ −∘ (ψ ∧ θ) ⊣⊢ (ϕ −∘ ψ) ∧ (ϕ −∘ θ)  (6.12)
F_{B} −∘ ϕ ⊣⊢ T_{[B,A]}  (6.13)
(ψ ∨ θ) −∘ ϕ ⊣⊢ (ψ −∘ ϕ) ∧ (θ −∘ ϕ)  (6.14)

Proposition 6.3.8 Let ϕ and ψ be predicates of type B and let α and β be combinators of type A → B and B → C respectively. The following distributive laws are derivable in L_{F OLL}.

α^{∗}T_{B} ⊣⊢ T_{A}  (6.15)
α^{∗}(ϕ ∧ ψ) ⊣⊢ α^{∗}ϕ ∧ α^{∗}ψ  (6.16)
∃[β]F_{B} ⊣⊢ F_{C}  (6.17)
∃[β](ϕ ∨ ψ) ⊣⊢ ∃[β]ϕ ∨ ∃[β]ψ  (6.18)

The following ‘half-distributive’ laws are also valid.

α^{∗}ϕ ∨ α^{∗}ψ ⊢ α^{∗}(ϕ ∨ ψ)  (6.19)
∃[α](ϕ ∧ ψ) ⊢ ∃[α]ϕ ∧ ∃[α]ψ  (6.20)

Proposition 6.3.9 Let ϕ, ψ and θ be predicates of type A, B and C respectively, and let α be a combinator of type B → C. The following two distributive laws are derivable in L_{F OLL}.

ϕ ∘ ∃[α]ψ ⊣⊢ ∃[Id_{A} ⊗α](ϕ ∘ ψ)  (6.21)
ϕ −∘ α^{∗}θ ⊣⊢ Λ(α• eval)^{∗}(ϕ −∘ θ)  (6.22)

Proof. The following two derivations show that fusion distributes over existential quantification.

ψ(z) ⊢ ψ(z)  (∃R)
ϕ(x) ⊢ ϕ(x)  ψ(z) ⊢ (∃[α]ψ)(α(z)) (∘R)
ϕ(x), ψ(z) ⊢ (ϕ ∘ ∃[α]ψ)(x, α(z))  (∘L,≈R)
ϕ ∘ ψ(x, z) ⊢ (ϕ ∘ ∃[α]ψ)(Id_{A} ⊗α(x, z)) (∃L)
∃[Id_{A} ⊗α](ϕ ∘ ψ)(x, y) ⊢ (ϕ ∘ ∃[α]ψ)(x, y)

(6.23)

ϕ(x) ⊢ ϕ(x)  ψ(z) ⊢ ψ(z) (∘R)
ϕ(x), ψ(z) ⊢ ϕ ∘ ψ(x, z)  (∃R)
ϕ(x), ψ(z) ⊢ ∃[Id_{A} ⊗α](ϕ ∘ ψ)(Id_{A} ⊗α(x, z)) (≈R)
ϕ(x), ψ(z) ⊢ ∃[Id_{A} ⊗α](ϕ ∘ ψ)(x, α(z))  (∃L)
ϕ(x), ∃[α]ψ(y) ⊢ ∃[Id_{A} ⊗α](ϕ ∘ ψ)(x, y) (∘L)
(ϕ ∘ ∃[α]ψ)(x, y) ⊢ ∃[Id_{A} ⊗α](ϕ ∘ ψ)(x, y)

(6.24)

The next two derivations show that linear implication distributes over substitution.

θ(α(eval (f, x))) ⊢ θ(α(eval (f, x))) (∗L,≈R)
ϕ(x) ⊢ ϕ(x)  α^{∗}θ(eval (f, x)) ⊢ θ(α• eval (f, x)) ( −∘ L)
(ϕ −∘ α^{∗}θ)(f), ϕ(x) ⊢ θ(α• eval (f, x))  (≈R)
(ϕ −∘ α^{∗}θ)(f), ϕ(x) ⊢ θ(eval (Λ(α• eval)(f), x)) ( −∘ R)
(ϕ −∘ α^{∗}θ)(f) ⊢ (ϕ −∘ θ)(Λ(α• eval)(f))  (∗R)
(ϕ −∘ α^{∗}θ)(f) ⊢ Λ(α• eval)^{∗}(ϕ −∘ θ)(f)

(6.25)

θ(α(eval (f, x))) ⊢ θ(α(eval (f, x)))  (≈L)
ϕ(x) ⊢ ϕ(x)  θ(eval (Λ(α• eval)(f), x)) ⊢ θ(α(eval (f, x))) ( −∘ L)
ϕ −∘ θ(Λ(α• eval)(f)), ϕ(x) ⊢ θ(α(eval (f, x))) (∗R , −∘ R)
ϕ −∘ θ(Λ(α• eval)(f)) ⊢ (ϕ −∘ α^{∗}θ)(f)  (∗L)
Λ(α• eval)^{∗}(ϕ −∘ θ)(f) ⊢ (ϕ −∘ α^{∗}θ)(f)

(6.26) □

The next two propositions are a logical expression of the adjunctions relating fusion and linear implication (theorem 5.4.5), and substitution and existential quantification (proposition 5.1.11).

Proposition 6.3.10 Let ϕ and ψ be predicates of type A and B respectively, and let θ be a predicate of type A ⊗ B. Then

ϕ ∘ ψ ⊢ θ iff ∃[hold_{A,B}]ϕ ⊢ ψ −∘ θ  (6.27)
ϕ ⊢ ψ −∘ θ iff ϕ ∘ ψ ⊢eval^{∗} θ  (6.28)

Proposition 6.3.11 Let ϕ and ψ be predicates of type A and B respectively and let α be a combinator of type A → B. Then

∃[α]ϕ ⊢ ψ  iff  ϕ ⊢ α^{∗}ψ  (6.29)

Proposition 6.3.12 Let ϕ be a predicate of type B ⊗ C and let α and β be combinators of type A → B and C → D respectively. Then the following sequent is derivable in L_{F OLL}.

∃[Id_{A} ⊗β](α⊗ Id_{C})^{∗}ϕ ⊢ (α⊗ Id_{D})^{∗}∃[Id_{B} ⊗β]ϕ  (6.30)

The above law corresponds to the part of the modified Beck condition (5.52) which always holds. The converse is not derivable because the full condition does not hold in general.

6.3.2 Predicates on a Monoid

We now develop two small applications of the logic L_{F OLL}. These show how the logic can be used to calculate directly the order theoretic properties of Msubobjects, which would otherwise require a confusing diagram chase. In the next section, we shall consider how Girard’s double negation operator can be translated into the first order logic, but first we look at the properties of predicates over a commutative monoid.

Let (B, F, E) be the theory of a commutative monoid given in section 3.4.1. The comparisons m : M ⊗ M → M and Λ(m) : M → [M, M] allow us to define the following versions of fusion and linear implication for predicates over M.

1 = ∃[e] T_{I}  (6.31)
ϕ · ψ = ∃[m]ϕ ∘ ψ  (6.32)
ϕ ⊃ ψ = Λ(m)^{∗}(ϕ −∘ ψ)  (6.33)

Let C be the set of equivalence classes of pred(M) under ⊣⊢. By lemma 6.3.4, ⊣⊢ is a congruence with respect to the operations · and ⊃ so these give rise to operations ˆ· and ˆ⊃ on equivalence classes. Let ⟨C, ˆ∨, F̂_{M}, ˆ∧, T̂_{M},ˆ·, ˆ1, ˆ⊃⟩ denote the set C with the various induced operations.

Proposition 6.3.13 ⟨C, ˆ∨, F̂_{M}, ˆ∧, T̂_{M},ˆ·, ˆ1, ˆ⊃⟩ is a consequence algebra.

Proof. It is routine to verify that ⟨C, ˆ∨, F̂_{M}, ˆ∧, T̂_{M}⟩ is a lattice. The monotonicity of the multiplication · follows from lemma 6.3.4. We show that multiplication is associative as follows.

ϕ · (ψ · θ) = ∃[m](ϕ ∘ ∃[m](ψ ∘ θ))  (6.34)
⊣⊢ ∃[m]∃[Id ⊗m](ϕ ∘ (ψ ∘ θ))  (6.35)
⊣⊢ ∃[m • (Id ⊗m)]((ϕ ∘ ψ) ∘ θ)  (6.36)

There is a similar expression for (ϕ · ψ) · θ and this is equal to the above by the associativity of m.

The following derivations show that (ϕ ⊃ ψ) · ϕ ⊢ ψ and ϕ ⊢ ψ ⊃ (ϕ · ψ) respectively.

ψ(m(x, y)) ⊢ ψ(m(x, y))  (≈L)
ϕ(y) ⊢ ϕ(y)  ψ(eval (Λ(m)(x), y)) ⊢ ψ(m(x, y)) ( −∘ L)
ϕ −∘ ψ(Λ(m)(x)), ϕ(y) ⊢ ψ(m(x, y)) (∗L)
Λ(m)^{∗}(ϕ −∘ ψ)(x), ϕ(y) ⊢ ψ(m(x, y)) (∘L)
(Λ(m)^{∗}(ϕ −∘ ψ) ∘ ϕ)(x, y) ⊢ ψ(m(x, y)) (∃L)
∃[m](Λ(m)^{∗}(ϕ −∘ ψ) ∘ ϕ)(z) ⊢ ψ(z)

(6.37)

ϕ(x) ⊢ ϕ(x)  ψ(y) ⊢ ψ(y) (∘R)
ϕ(x), ψ(y) ⊢ ϕ ∘ ψ(x, y)  (∃R)
ϕ(x), ψ(y) ⊢ (∃[m]ϕ ∘ ψ)(m(x, y))  (≈R)
ϕ(x), ψ(y) ⊢ (∃[m]ϕ ∘ ψ)(eval (Λ(m)(x), y) ( −∘ R)
ϕ(x) ⊢ (ψ −∘ ∃[m]ϕ ∘ ψ)(Λ(m)(x))  (∗R)
ϕ(x) ⊢ Λ(m)^{∗}(ψ −∘ ∃[m]ϕ ∘ ψ)(x)

(6.38)

Thus, ˆ· and ˆ⊃ are related by the required adjunction. □

6.3.3 Girard’s Double Negation Closure

Let ⊥ be a fixed predicate of type Z, and for all ϕ ∈ pred(A) let ϕ^{⊥} denote the predicate ϕ −∘ ⊥ of type [A, Z]. Let at_{A,B}: A → [[A, B], B] be the derived combinator

at_{A,B}= Λ(eval_{A,B} • swap_{A,[A,B]})  (6.39)

which given a term s returns the function “evaluate at s”.

eval (at (s), f) \begin{matrix}≈ & eval (Λ(eval • swap)(s), f) \\ ≈ & (eval • swap)(s, f) \\ ≈ & eval (f, s) \end{matrix}  (6.40)

If ϕ is a predicate of type A then ϕ^{⊥⊥} ∈ pred([[A, Z], Z]), and hence ◇_{A}(ϕ) =at_{A,Z}^{∗} (ϕ^{⊥⊥}) is a predicate of type A. We show that ◇ is a closure operation on predicates over A.

ϕ(x) ⊢ ϕ(x)  ⊥(eval (f, x)) ⊢ ⊥(eval (f, x)) ( −∘ L)
ϕ(x), ϕ^{⊥}(f) ⊢ ⊥(eval (f, x)) (≈R)
ϕ(x), ϕ^{⊥}(f) ⊢ ⊥(eval (at (x), f)) ( −∘ R)
ϕ(x) ⊢ ϕ^{⊥⊥}(at (x))  (∗R)
ϕ(x) ⊢at^{∗} (ϕ^{⊥⊥})(x)

(6.41)

The idempotency of ◇_{A} is a consequence of the following.

ϕ^{⊥}(f), ϕ^{⊥⊥}(at (g)) ⊢ ⊥(eval (at (g), f)) (∗L,≈R)
ϕ^{⊥}(f), at^{∗} (ϕ^{⊥⊥})(g) ⊢ ⊥(eval (f, g)) ( −∘ R)
ϕ^{⊥}(f) ⊢ (at^{∗} (ϕ^{⊥⊥}))^{⊥}(f)  ( −∘ L)
ϕ^{⊥}(f), (at^{∗} ϕ^{⊥⊥})^{⊥⊥}(h) ⊢ ⊥(eval (h, f)) ( −∘ R)
(at^{∗} ϕ^{⊥⊥})^{⊥⊥}(h) ⊢ ϕ^{⊥⊥}(h)

(6.42)

Where the missing premise for the application of ( −∘ L) is supplied by the axiom ⊥(eval (h, f)) ⊢ ⊥(eval (h, f)).

For all ϕ ∈ pred(A) and ψ ∈ pred(B), the following relation holds.

◇_{A}ϕ ∘ ◇_{B}ψ ⊢ ◇_{A⊗B}(ϕ ∘ ψ)  (6.43)

The diamond operator is the first order analogue of the double negation nucleus given in proposition 2.2.8. Unfortunately, the presence of a combinator in the definition of ◇_{A} prevents us from constructing an involutive “negation” on the ◇_{A}-closed predicates.

Model Theory

In chapter 5, we developed the algebraic theory of M-subobjects in a symmetric monoidal closed category with a monoidal factorisation system (E, M). This provided the motivation for the logic L_{F OLL} presented in chapter 6, and remains the primary example of a model.

In the present chapter, we shall develop the model theory of L_{F OLL} in terms of linear doctrines. These are an axiomatisation of the subobject model viewed as a fibred category. We define interpretations of L_{F OLL} in a linear doctrine, and show that L_{F OLL} is both sound and complete with respect to this semantics. Choosing to work with fibrations rather than directly with the subobject semantics clarifies the statement and proof of these theorems. Furthermore, nothing is lost by taking this approach as there are translations back and forth between the two forms of model.

In section 7.1, we first give the definition of a fibration and some subsidiary definitions. We show how every factorisation system gives rise to a fibration. We then define the notion of a linear doctrine as a fibration with extra structure, and prove that our leading example of a monoidal factorisation yields a linear doctrine. Finally, we prove some elementary results about linear doctrines and give a construction on quantales as a further example.

In section 7.2, we define the interpretation of formulae of L_{F OLL} in a linear doctrine, and prove that linear doctrines are sound models of L_{F OLL}.

Finally, in section 7.3, we prove that linear doctrines form a complete class of models for L_{F OLL}, and further deduce that those linear doctrines which arise from monoidal factorisation systems also form a complete class of models.

7.1 Linear Doctrines

Before giving our presentation of linear doctrines, we recall some of the definitions and basic facts associated with the theory of fibred categories.

7.1.1 Fibrations

Fibrations [Gra66,B´85] give an abstract formulation of the notion of an ‘indexed family’. This extends the familiar notion of a family indexed by a set to include families indexed by the objects of an arbitrary base category B. Families of objects indexed by B and families of morphisms between them form a category F_{B}, the fibre over B. The fibres over different objects form part of a larger category F where the morphisms crossing between fibres involve re-indexing along a morphism of B. One consequence of the definition given below is that morphisms in F can always be separated into a vertical component, lying within a single fibre, followed by a cartesian component, corresponding to the re-indexing.

Definition 7.1.1 Let F and B be categories, z : F → B be a functor and f : U → V be a morphism in F. We say that f is cartesian with respect to z if for all g : W → V and for all γ : z(W) → z(U) such that z(g) = z(f)γ, there exists a unique map h : W → U in F such that fh = g and z(h) = γ.

[figure: W; h; g; U; \overline{f}; V; z(W); γ; z(g); z(U); \overline{z(f)}; z(V)]  (7.1)

If α is a morphism of B then f is cartesian over α if f is cartesian and z(f) = α. The functor z : F → B is a fibration if for each object X in F and for each morphism α : A → z(X) in B there exists a morphism f : U → X in F which is cartesian over α.

Dually, a functor z : F → B is an op-fibration if z^{op} : F^{op} → B^{op} is a fibration.

If z : F → B is a fibration or op-fibration and B is an object of B then F_{B} denotes the fibre over B, that is, the subcategory of F whose objects and morphisms are mapped to B and 1_{B} respectively.

Definition 7.1.2 A fibration z : F → B is cleaved if for each morphism α : A → B in B and each object p ∈ F_{B} there exists a choice of morphism ν_{α,p} : α^{∗}p → p which is cartesian over α. Such a choice is called a cleavage of z.

A fibration is split if it is cleaved and the choices of cartesian lifting cohere as follows. For all objects p of F such that z(p) = C, and for all morphisms α : A → B and β : B → C in T the following diagrams commute.

[figure: p; α^{∗}(β^{∗}p); \overline{ν_{α,β^{∗}p}}; β^{∗}p; _{∥  ∥}; ∥; 1_{p}; ∥; ν_{β,p}; 1_{C}^{∗}p; \overline{ν_{1_{C},p}}; p; (βα)^{∗}p; \overline{ν_{βα,p}}; p]  (7.2)

Example 7.1.3 Let (E, M) be a factorisation system on the category C and let cod : Sqr (M) → C be the functor which maps an object of Sqr (M) , that is a morphism m ∈ M, to its codomain in C and a morphism (f, g) : m_{1} → m_{2} of Sqr (M) to its first component. Then cod : Sqr (M) → C is an op-fibration. If pullbacks exist in C for every pair m ∈ M and f ∈ Mor(C) with a common codomain then cod : Sqr (M) → C is also a fibration. Furthermore if there exist choices of pullback and factorisation then these give rise to a cleavage and op-cleavage respectively.

There is a well known correspondence between split fibrations z : F → B and functors F : B^{op} → Cat, often known as ‘strict indexed categories’ [PS78]. Given a split fibration z : F → B, we define a functor F : B^{op} → Cat as follows. If B is an object of B then F (B) is the fibre over B, that is, the subcategory of F which maps to B under z. If α : U → V is an arrow of B then we can verify that the map p ↦ α^{∗}p extends to a functor F (f) : F (B) → F (A) by the universal properties of a fibration. The coherences of 7.2 ensure that F (1_{A}) = 1_{F (A)} and F (g)F (f) = F (gf) and hence that F forms a functor B^{op} → Cat.

Conversely, given a functor F : B^{op} → Cat, we can use the following construction, due to Grothendieck, to produce fibration z_{F} : F → B. The objects of F are pairs (B, X) where B is an object of B and X is an object of F (B). A morphism in F from (B, X) to (C, Y) is a pair (α, f) where α : B → C in B and f : X → F (α)(Y) in C(B). The composition of two such maps (α, f) : (B, X) → (C, Y) and (β, g) : (C, Y) → (D, Z) is given by (βα, F (α)(g)f) and the identity on (B, X) is (1_{B}, 1_{X}). It is routine to verify that this data defines a category and furthermore that the functor z_{F} : F → B which maps objects and morphisms of F to their first component is actually a split fibration.

There is a similar correspondence between cleaved fibrations and ‘pseudofunctors’ F : B^{op} → Cat, which preserve identities and composition up to coherent isomorphism. Despite these correspondences, fibrations have a certain conceptual advantage over indexed categories. See [B´85] for a philosophical discussion of fibrations and a critique of [PS78]. In our case, there are clear practical reasons for adopting the fibred category view; to formulate the definition of a linear doctrine we need to consider the category of predicates as a whole. We make no further mention of indexed categories except to note that the Grothendieck construction is implicit in the proof of the theorem 7.2.3 (the soundness of L_{F OLL}).

If z : F → B is a fibration then we say that a map f of F is vertical if z(f) is an isomorphism. We write Vert_{z} for the class of vertical maps, and Cart_{z} for the class of cartesian maps. Note that it is more usual to take the vertical maps to be those lying within a single fibre. We need to take the weaker definition in order to get the following result.

Lemma 7.1.4 If z : F → B is a fibration then (Vert, Cart) is a factorisation system on F.

Proof. Clearly, both Cart and Vert contain the isomorphisms and are closed under composition. If g : U → V is any morphism in F then we know that there exists a map f which is cartesian over z(g) and hence, by the universal property of f, a vertical map v such that z(v) = 1_{z(U)} and g factors as fv.

Now, let v ∈ Vert and f ∈ Cart, and suppose that we have a commuting square hv = fg.

[figure: U; \overline{v}; V; z(U); \overline{z(v) ; ≅}; z(V); g; σ; h; z(g); ρ; z(h); W; \overline{f}; X; z(W); \overline{z(f)}; z(X)]  (7.3)

Since z(v) is an isomorphism, there is a unique map ρ making both triangles of the righthand square commute. By the universal property of f applied to h, there exists a unique map σ : V → W such that z(σ) = ρ and h = fσ. Applying the same universal property to hv, we deduce that σv = g. Thus σ is the unique map making the lefthand square commute, since any other map σ′ with this property would necessarily satisfy z(σ′) = ρ. □

7.1.2 Linear Doctrines

The concept of a linear doctrine isolates the properties of the M-subobjects of a monoidal factorisation system (E, M) which are needed to prove the soundness and completeness of L_{F OLL}.

Definition 7.1.5 Let ⟨P, ∘, 1, −∘ ⟩ and ⟨T , ⊗, I, [−, −]⟩ be symmetric monoidal closed categories. A strict monoidal strict closed functor z : P → T is a linear doctrine if

1. z is both a fibration and an op-fibration,

2. for each object A of T , the fibre F_{A} has finite products and finite coproducts,

3. 1 is a terminal object in P_{I}, and whenever ⊤_{A} and ⊤_{B} are terminal in P_{A} and P_{B} respectively, then ⊤_{A} ∘ ⊤_{B} is terminal in P_{A⊗B}.

The key example of a linear doctrine is given by the codomain fibration cod : Sqr (M) → C of example 7.1.3 in the case that (E, M) is a monoidal factorisation.

Proposition 7.1.6 Let C be a symmetric monoidal closed category with finite coproducts and a monoidal factorisation system (E, M). Suppose that there exists a choice of pullback for every pair of maps m ∈ M and f ∈ Mor(C) with a common codomain and a choice of factorisation for every morphism of C. Then cod : Sqr (M) → C is a linear doctrine with cleavage and op-cleavage.

Proof. We know that cod : Sqr (M) → C is a fibration and op-fibration and that the choices of factorisation and pullback give rise to a cleavage and op-cleavage. Theorem 5.4.5 states that ⟨Sqr (M) , ∘, 1_{I}, −∘ ⟩ is symmetric monoidal closed and an examination of the data given reveals that the codomain components are given by the corresponding data in ⟨C, ⊗, I, [−, −]⟩ so cod is strict monoidal strict closed. The fibre over an object A of C is, of course, the relative slice category C/_{M}A and this has finite products and coproducts by lemma 5.1.9. Finally, a terminal object in the fibre over A is an isomorphism m : A′ ≅ A and these are preserved by fusion. □

Remark 7.1.7 There are two important special cases of a linear doctrine: where the fibres are preorders and partial orders respectively. If the factorisation system of the above proposition satisfies M ⊆ Mon then the fibres of cod : Sqr (M) → C are preordered. By taking an appropriate quotient of Sqr (M) , we can obtain a fibration z : F → C whose fibres are the M-subobject lattices of C, and hence partial orders. The interpretation of the logic L_{F OLL} given in the next section will be defined with respect to a linear doctrine whose fibres are partially ordered.

Proposition 7.1.6 shows that a monoidal factorisation system gives rise to a linear doctrine. In fact, there is a converse to this result.

Proposition 7.1.8 Let P = ⟨P, ∘, 1, −∘ ⟩ and T = ⟨T , ⊗, I, [−, −]⟩ be symmetric monoidal closed categories, and z : P → T be a linear doctrine. Then for all p ∈ Obj(P), OpCart_{z} is closed under (−)∘p and Cart_{z} is closed under p −∘ (−).

Proof. By the dual of lemma 7.1.4, (OpCart_{z}, Vert_{z}) is a factorisation system on P. We note that Vert_{z} is closed under p −∘ (−). If g : q_{1} → q_{2} is vertical then z(g) is an isomorphism and hence so is

z(p −∘ g) = [z(p), z(g)] : [z(p), z(q_{2})] → [z(p), z(q_{1})]  (7.4)

Thus, by lemma 5.2.2, OpCart_{z} is closed under (−) ∘ p.

The second part is just the dual of the first. □

Corollary 7.1.9 If z : P → T is a linear doctrine then (OpCart_{z}, Vert_{z}) is a monoidal factorisation system on P.

We turn briefly to the connection between linear doctrines and quantales. One way to view the predicates of L_{F OLL} is that they are much the same as the formulae of the propositional logic but ‘spread out’ over an underlying type theory. It seems that if we could collect together the predicates of different types then this should give a model of the propositional logic. We make this statement precise in terms of linear doctrines. Let z : P → T be a linear doctrine with T small, and suppose that the fibres of z are complete lattices. For each f : X → Y in T , the direct image functor f_{∗} : P_{X} → P_{Y} preserves suprema since it is left adjoint to f^{∗}. Thus, f_{∗} is a morphism of complete semilattices, and z defines a functor F : T → CSLat mapping objects to fibres and morphisms to direct image maps.

Proposition 7.1.10 The colimit of the diagram F : T → CSLat is a quantale.

Proof. Let Q be the colimit of F. For each pair of objects X, Y in T , fusion defines a bilinear map from P_{X} × P_{Y} to P_{X⊗Y} and hence a morphism ∘_{X,Y} : P_{X} ⊗ P_{Y} → P_{X⊗Y} of CSLat.

Let f : X → X′ and g : Y → Y′ be morphisms of T . As a result of lemma 7.1.8 the following diagram commutes.

[figure: P_{X} ⊗ P_{Y}; \overline{∘_{X,Y}}; P_{X⊗Y}; f_{∗} ⊗ g_{∗}; (f ⊗ g)_{∗}; P_{X′} ⊗ P_{Y′}; \overline{∘_{X′,Y′}}; P_{X′⊗Y′}]  (7.5)

Thus ∘_{X,Y} : P_{X} ⊗ P_{Y} → P_{X⊗Y} are the components of a natural transformation

⊗(F × F) →^{·} F.

Since CSLat is symmetric monoidal closed, ⊗ preserves colimits and so

Q ⊗ Q =colim (F)⊗ colim (F) ≅colim (⊗(F × F))  (7.6)

We define the multiplication m : Q ⊗ Q → Q to be the map between colimits induced by the natural transformation above. It is routine to verify that m is associative, commutative and has a unit. □

7.2 Soundness of the calculus L_{F OLL}

We give an interpretation of the sequents of L_{F OLL} in a linear doctrine z : P → T whose fibres are partial orders and prove that it is sound.

7.2.1 Interpretation of formulae

Let z : P → T be a linear doctrine, and let ⟨ı, ȷ⟩ be an interpretation of LTT in T . Let | − | be a mapping of atomic predicates to objects of P such that if ϕ is of type A then |ϕ| lies in the fibre P_{ı (A)}. We extend | − | to an interpretation of all predicates as follows.

\begin{aligned}|ϕ ∘ ψ| & = & |ϕ| ∘ |ψ| & |α^{∗}ϕ| & = & ȷ (α)^{∗}|ϕ| \\ |ϕ −∘ ψ| & = & |ϕ| −∘ |ψ| & |∃[α]ϕ| & = & ȷ (α)_{∗}|ϕ| \\ |ϕ ∧ ψ| & = & |ϕ| ∧ |ψ| & | T_{X} | & = & ⊤_{ı (X)} \\ |ϕ ∨ ψ| & = & |ϕ| ∨ |ψ| & | F_{X} | & = & 0_{ı (X)} \end{aligned}  (7.7)

Lemma 7.2.1 For all predicates ϕ ∈ pred(A), z(|ϕ|) = ı(A).

We can now give a function [[−]] from lists of formulae to objects of P. Let \overline{s} denote ȷ (ac(s)).

\begin{aligned}[[ ]] & = & 1 \\ [[ϕ(s)]] & = & \overline{s}^{∗}|ϕ| \\ [[Γ, ϕ(s)]] & = & [[Γ]] ∘ \overline{s}^{∗}|ϕ| \end{aligned}  (7.8)

We are not quite ready to state the soundness theorem. Although we can interpret the formulae on each side of the turnstile, these interpretations may lie in different fibres. To interpret a sequent Γ ⊢ ϕ(s) we need to define a comparison map z([[Γ]]) → z([[ϕ(s)]]). Firstly, we extend the concept of associated basic term to lists of formulae.

Abt() = ()
Abt(ϕ(s)) = abt(s)
Abt(Γ, ϕ(s)) = (Abt(Γ), abt(s))

(7.9)

If no variable occurs twice in the list γ then Abt(Γ) is a term. In particular, if Γ ⊢ ϕ(s) is a valid sequent then Abt(Γ) and Abt(ϕ(s)) are terms by the variable balancing property.

Lemma 7.2.2 If Γ is a list of formulae with Abt(Γ) ∈ term(A) then z([[Γ]]) = ı (A).

Theorem 7.2.3 Soundness of L_{F OLL}

Let z : P → T be a linear doctrine whose fibres are partial orders and let ⟨ı, ȷ, | − |⟩ be an interpretation of L_{F OLL}(B, F, E) in z. If Γ ⊢ ϕ(s) is derivable in L_{F OLL}(B, F, E) then there exists a morphism in P

g : [[Γ]] → [[ϕ(s)]]  (7.10)

and a central combinator ξ such that z(g) = ȷ (ξ) and ξ(Abt(Γ)) ≈ Abt(ϕ(s)).

Remark 7.2.4 The existence of g : [[Γ]] → [[ϕ(s)]] such that z(g) = ȷ (ξ) is equivalent to the inequality

[[Γ]] ≤ ȷ (ξ)^{∗}[[ϕ(s)]]  (7.11)

holding in the fibre P_{ı (A)} where A is the type of Abt(Γ).

Proof. The proof proceeds by induction on the structure of derivations. For each rule of L_{F OLL}, we show that theorem 7.2.3 holds of the conclusion if it holds of the premises. We present only the more difficult cases.

Fusion.

(∘R) \frac{Γ_{1} ⊢ ϕ(s) Γ_{2} ⊢ ψ(t)}{Γ_{1}, Γ_{2} ⊢ ϕ ∘ ψ(s, t)} provided that

V (Γ_{1}) ∩ V (Γ_{2}) = ∅.

Induction Hypothesis: There exist morphisms

g_{1} : [[Γ_{1}]] → \overline{s}^{∗}|ϕ| g_{2} : [[Γ_{2}]] → \overline{t}^{∗}|ψ|

and central combinators ξ_{1}, ξ_{2} such that ξ_{1}(Abt(Γ_{1})) ≈ abt(s), ξ_{2}(Abt(Γ_{2})) ≈ abt(t) and z(g_{i}) = ȷ (ξ_{i}) for i = 1, 2.

Abt(Γ_{1}, Γ_{2}) is the left associated form of (Abt(Γ_{1}), Abt(Γ_{2})). Following the proof of lemma 3.2.14, we can construct a central combinator, left such that left (Abt(Γ_{1}), Abt(Γ_{2})) ≈ Abt(Γ_{1}, Γ_{2}). There is a semantic counterpart to this construction which gives us a morphism h : [[Γ_{1}]] ∘ [[Γ_{2}]] → [[Γ_{1}, Γ_{2}]] in P with z(h) = ȷ (left).

Let ν_{1} : \overline{s}^{∗}|ϕ| → |ϕ| , ν_{2} : \overline{t}^{∗}|ψ| → |ψ| and ν : (\overline{s} ⊗ \overline{t})^{∗}|ϕ ∘ ψ| → |ϕ ∘ ψ| be cartesian over \overline{s}, \overline{t} and \overline{s} ⊗ \overline{t} respectively. Then

z((ν_{1} ∘ ν_{2})(g_{1} ∘ g_{2})) = \overline{s} ⊗ \overline{t} ȷ (ξ_{1} ⊗ ξ_{2})  (7.12)

By the universal property of ν, there is a unique map g : [[Γ_{1}, Γ_{2}]] → (\overline{s} ⊗ \overline{t})^{∗}|ϕ ∘ ψ| with z(g) = \overline{s} ⊗ \overline{t} making the diagram below commute.

[figure: [[Γ_{1}, Γ_{2}]]; ≅; [[Γ_{1}]] ∘ [[Γ_{2}]]; \overline{g_{1} ∘ g_{2}}; \overline{s}^{∗}|ϕ| ∘ \overline{t}^{∗}|ψ|; g; ν_{1} ∘ ν_{2}; (\overline{s} ⊗ \overline{t})^{∗}|ϕ ∘ ψ|; \overline{ν}; |ϕ ∘ ψ|]  (7.13)

The required map [[Γ_{1}, Γ_{2}]] → (\overline{s} ⊗ \overline{t})^{∗}|ϕ ∘ ψ| is thus the composition gh^{−1}. Note that z(gh^{−1}) = ȷ ((ξ_{1} ⊗ ξ_{2})• left^{−1}) where left^{−1} is the obvious ‘inverse’ of left.

(∘L) \frac{Γ_{1}, ϕ(x), ψ(y), Γ_{2} ⊢ θ(u)}{Γ_{1}, ϕ ∘ ψ(x, y), Γ_{2} ⊢ θ(u)}

The soundness of (∘L) follows from the observation that [[Γ_{1}, ϕ(x), ψ(y), Γ_{2}]] and [[Γ_{1}, ϕ ∘ ψ(x, y), Γ_{2}]] are just different products of the same finite set of objects in P.

Linear Implication.

( −∘ R) \frac{Γ, ϕ(x) ⊢ ψ(eval_{X,Y} (f, x))}{Γ ⊢ (ϕ −∘ ψ)(f)} x is a basic term.

Induction Hypothesis : There exists a map g : [[Γ]] ∘ |ϕ| → (ε(\overline{f} ⊗ 1))^{∗}|ψ| such that z(g) = ȷ (ξ) where ξ is a central combinator satisfying ξ(Abt(Γ), x) ≈ (abt(f), x).

Abt(Γ) and abt(f) are basic terms in the same variables so by lemma 3.2.14, there exists a central combinator ξ′ such that ξ′(Abt(Γ)) ≈ abt(f)). It follows that

ξ′⊗ Id (Abt(Γ), x) ≈ (abt(f), x) ≈ ξ(abt(f), x)  (7.14)

and hence ȷ (ξ′) ⊗ 1 = ȷ (ξ).

[figure: [[Γ]] ∘ |ϕ|; g; h; ε(\overline{f} ⊗ 1)^{∗}|ψ|; \overline{ν}; |ψ|; ı (A ⊗ B); \overline{ȷ (ξ)}; ı (A′ ⊗ B); \overline{ε(\overline{f} ⊗ 1)}; ı (C)]  (7.15)

Let h = νg where ν : ε(\overline{f} ⊗ 1)^{∗}|ψ| → |ψ| is cartesian and let

ȟ = [1, h]δ : [[Γ]] → |ϕ| −∘ |ψ| = |ϕ −∘ ψ|

Then

\begin{aligned}z(ȟ) & = & [1, z(h)]δ \\ & = & [1, ε(\overline{f} ⊗ 1)ȷ (ξ)]δ \\ & = & [1, ε(\overline{f}ȷ (ξ′) ⊗ 1)]δ \\ & = & \overline{f}ȷ (ξ′) \end{aligned}  (7.16)

[figure: [[Γ]]; g′; ȟ; \overline{f}^{∗}|ϕ −∘ ψ|; \overline{ν′}; |ϕ −∘ ψ|; ı (A); \overline{ȷ (ξ′)}; ı (A′); \overline{\overline{f}}; ı ([B, C])]  (7.17)

Thus ȟ factors as ȟ = ν′g′ where ν′ is cartesian over \overline{f} and z(g′) = ȷ (ξ′).

( −∘ L) \frac{Γ_{1} ⊢ ϕ(s) Γ_{2}, ψ(eval_{X,Y} (f, s)) ⊢ θ(t)}{Γ_{2}, (ϕ −∘ ψ)(f), Γ_{1} ⊢ θ(t)} provided that

V (Γ_{1}) ∩ V (Γ_{2}) = ∅.

Induction Hypothesis: There exist morphisms g_{1}, g_{2} in P

\begin{aligned}g_{1} & : & [[Γ_{1}]] → \overline{s}^{∗}|ϕ| \\ g_{2} & : & [[Γ_{2}]] ∘ (ε(\overline{f} ⊗ \overline{s}))^{∗}|ψ| → \overline{t}^{∗}|θ| \end{aligned}

and central combinators ξ_{1}, ξ_{2} such that

z(g_{1}) = ȷ (ξ_{1})  ξ_{1}(Abt(Γ_{1})) ≈ abt(s)
z(g_{2}) = ȷ (ξ_{2})  ξ_{2}(Abt(Γ_{1}), abt(f, s)) ≈ abt(t)

It is easy to check that ξ = ξ_{2}• assr •(Id ⊗ξ_{1}) satisfies

ξ((Abt(Γ_{2}), abt(f)), Abt(Γ_{1})) ≈ abt(t)  (7.18)

We shall define a morphism g as the composition of a series of arrows :

([[Γ_{2}]] ∘ \overline{f}^{∗}|ϕ −∘ ψ|) ∘ [[Γ_{1}]] ⟶^{h_{1}} [[Γ_{2}]] ∘ (\overline{f}^{∗}|ϕ −∘ ψ| ∘ \overline{s}^{∗}|ϕ|)
⟶^{h_{2}} [[Γ_{2}]] ∘ (ε(\overline{f} ⊗ \overline{s}))^{∗}|ψ|
⟶ \overline{t}^{∗}|θ|

Clearly, the last step is just g_{2}. We define h_{1} = a(1 ∘ g_{1}) and note that z(h_{1}) = ȷ (assr •(Id ⊗ξ_{1})).

Let ν_{1} : \overline{f}^{∗}|ϕ −∘ ψ| → |ϕ −∘ ψ| , ν_{2} : \overline{s}^{∗}|ϕ| → |ϕ| and ν : (ε(\overline{f} ⊗ \overline{s}))^{∗}|ψ| → |ψ| be cartesian over \overline{f}, \overline{s} and ε(\overline{f} ⊗ \overline{s}) respectively.

[figure: \overline{f}^{∗}|ϕ −∘ ψ| ∘ \overline{s}^{∗}|ϕ|; \overline{ν_{1} ∘ ν_{2}}; |ϕ −∘ ψ| ∘ |ϕ|; k; ε_{|ϕ|,|ψ|}; (ε(\overline{f} ⊗ \overline{s}))^{∗}|ψ|; \overline{ν}; |ψ|]  (7.19)

Since z(ε(ν_{1} ∘ ν_{2})) = ε(\overline{f} ⊗ \overline{s}), there is a unique map k with z(k) = 1 = ȷ (Id) making the above diagram commute. We now define h_{2} = 1 ∘ k and g = g_{2}h_{2}h_{1}. It is routine to verify that

z(g) = ȷ (ξ_{2}• assr •(Id ⊗ξ_{1}))  (7.20)

Existential Quantification.

(∃R) \frac{Γ ⊢ ϕ(s)}{Γ ⊢ (∃[α]ϕ)(α(s))}

Let g be a map [[Γ]] → \overline{s}^{∗}|ϕ| with z(g) = ȷ (ξ). From the adjunction ȷ (α)_{∗} ⊣ ȷ (α)^{∗}, we obtain a unique map

\overline{s}^{∗}|ϕ| → ȷ (α)^{∗}ȷ (α)_{∗}\overline{s}^{∗}|ϕ|  (7.21)

in the fibre P_{A} (where A is the type of abt(s)), and composing this with g gives the required map g′.

(∃L) \frac{Γ, ϕ(x) ⊢ ψ(s[α(x)/v])}{Γ, (∃[α]ϕ)(v) ⊢ ψ(s)} x is a basic term and v does

not occur in the premise.

Induction Hypothesis : There exists a map

g : [[Γ]] ∘ |ϕ| → \overline{s[α(x)/v]}^{∗}|ψ|

such that z(g) = ȷ (ξ) where ξ is a central combinator satisfying ξ(Abt(Γ), x) ≈ abt(s[α(x)/v]).

First, note that (Abt(Γ), v) and abt(s) are basic terms with the same variables, and hence there exists a central combinator ξ′ such that ξ(Abt(Γ), v) ≈ abt(s). Using the substitutivity of ≈

ξ(Abt(Γ), α(x)) ≈ abt(s)[α(x)/v]  (7.22)

Thus

(ac(s) • ξ′ • (Id ⊗α))(Abt(Γ), x) ≈ ac(s)(abt(s)[α(x)/v])
≈ s[α(x)/v]

(7.23)

By the induction hypothesis

(ac(s[α(x)/v]) • ξ)(Abt(Γ), x) ≈ ac(s[α(x)/v])(ξ(Abt(Γ), x))
≈ ac(s[α(x)/v])abt(s[α(x)/v])
≈ s[α(x)/v]

(7.24)

It follows from definition 3.3.1 that

ȷ (ac(s) • ξ′ • (Id ⊗α)) = ȷ (ac(s[α(x)/v]) • ξ)  (7.25)

The existence of g in the induction hypothesis is equivalent to the inequality

[[Γ]] ∘ |ϕ| ≤ ȷ (ξ)^{∗}\overline{s[α(x)/v]}^{∗}|ψ|  (7.26)

and hence by 7.25 to

[[Γ]] ∘ |ϕ| ≤ ȷ (Id ⊗α)^{∗}ȷ (ξ′)^{∗}\overline{s}^{∗}|ψ|  (7.27)

Transposing this inequality across the adjunction ȷ (Id ⊗α)_{∗} ⊣ ȷ (Id ⊗α)^{∗}

(1 ⊗ ȷ (α))^{∗}([[Γ]] ∘ |ϕ|) ≤ ȷ (ξ′)^{∗}\overline{s}^{∗}|ψ|  (7.28)

The result now follows from the fact that the op-cartesian maps in P are closed under fusion.

[[Γ]] ∘ ȷ (α)^{∗}|ϕ| ≤ ȷ (ξ′)^{∗}\overline{s}^{∗}|ψ|  (7.29)
□

7.3 Completeness of L_{F OLL}

Theorem 7.3.1 Let L_{F OLL}(B, F, E, P) be a theory of first order linear logic. Then there exists a linear doctrine z_{0} : P_{0} → T_{0} and an interpretation ⟨ı_{0}, ȷ_{0}, |−|_{0}⟩ of L_{F OLL}(B, F, E, P) in z_{0} such that whenever there exists a morphism

g : [[Γ]] → [[ϕ(s)]]  (7.30)

and a central combinator ξ such that z_{0}(g) = ȷ_{0}(ξ) and ξ(Abt(Γ)) ≈ Abt(ϕ(s)), then Γ ⊢ ϕ(s) is derivable in L_{F OLL}(B, F, E, P)

The proof of theorem 7.3.1 is the content of section 7.3.1.

Corollary 7.3.2 L_{F OLL} is complete with respect to the linear doctrine semantics.

Proof. If a sequent Γ ⊢ ϕ(s) is valid in every linear doctrine interpretation of L_{F OLL}(B, F, E, P) then it is valid for the interpretation ⟨ı_{0}, ȷ_{0}, | − |_{0}⟩ in z_{0} and hence is derivable in L_{F OLL}(B, F, E, P). □

Every monoidal factorisation system (E, M) on a symmetric monoidal closed category C gives rise to a linear doctrine. For completeness the apparent extra generality of linear doctrines is illusory because we have the following result.

Corollary 7.3.3 For every theory L_{F OLL}(B, F, E, P) of first order linear logic, there is a monoidal factorisation (E, M) on a symmetric monoidal closed category C such that the associated factorisation system satisfies the conditions of theorem 7.3.1.

Proof. Given z_{0} : P_{0} → T_{0} as in theorem 7.3.1, it follows from corollary 7.1.9 that (OpCart_{z_{0}}, Vert_{z_{0}}) is a monoidal factorisation system on P_{0}. Consider z′ : Sqr (∥_{z_{0}}) → P_{0} and define the interpretation ⟨ı′, ȷ′, | − |′⟩ by ı′(A) = T_{A}, ȷ′(α) = ⟨T_{A}, [α], T_{B}⟩ and |ϕ|′ is the unique map from |ϕ| to T_{A} in the fibre (P_{0})_{A}. □

7.3.1 The fibre category P_{0} and the functor z_{0} : P_{0} → T_{0}

Given L_{F OLL}(B, F, E, P) a theory of first order linear logic, define T_{0}(B, F, E) as in lemma 3.3.4. Given an object A of T_{0}, the objects of P_{0} in the fibre over A are equivalence classes of predicates with type A under the equivalence relation ⊣⊢ defined in section 6.3.1. Let [ϕ] denote the equivalence class of ϕ.

Let ϕ ∈ pred(A), ψ ∈ pred(B) and α be a combinator of type A → B in LTT(B, F, E). The triple ⟨[ϕ], [α], [ψ]⟩ is a morphism [ϕ] → [ψ] in P_{0} with z_{0}⟨[ϕ], [α], [ψ]⟩ = [α] provided that

ϕ ⊢ α^{∗}ψ  (7.31)

The identity on [ϕ] is the triple ⟨[ϕ], [Id_{A}], [ϕ]⟩ and composition is defined as follows.

⟨[ψ], [β], [θ]⟩ ⟨[ϕ], [α], [ψ]⟩ = ⟨[ϕ], [β • α], [θ]⟩  (7.32)

It is easy to check that this defines a morphism of P_{0}. That is

\frac{ϕ ⊢ α^{∗}ψ ψ ⊢ β^{∗}θ}{ϕ ⊢ (β • α)^{∗}θ}  (7.33)

Given that two morphisms of P_{0} have the same domain and codomain, their equality is determined by their middle components. Hence, composition is associative and z_{0} is a functor. Moreover, the commutativity of diagrams in P_{0} reduces to the commutativity of corresponding diagrams in T_{0}. Thus, we shall see that the equational axioms required to show that P_{0} is symmetric monoidal closed are essentially those already checked in section 3.3.1.

Where it is clear from the context, we shall drop the domain and codomain parts of a triple. Thus we write ⟨α⟩ : [ϕ] → [ψ] rather than ⟨[ϕ], [α], [ψ]⟩ : [ϕ] → [ψ].

Tensor Product

T_{0} is given the tensor product of proposition 3.3.5, and we define a tensor product on objects of P_{0} in the evident way : [ϕ] ∘ [ψ] = [ϕ ∘ ψ]. This is well defined by lemma 6.3.4, and z_{0} strictly preserves the tensor product.

Let ⟨α⟩ : [ϕ] → [ψ] and ⟨β⟩ : [ϕ′] → [ψ′]. The following derived rule for ⊢ shows that ⟨α ⊗ β⟩ : [ϕ ∘ ψ] → [ϕ′ ∘ ψ′] is a morphism of P_{0}.

\frac{ϕ ⊢ α^{∗}ψ ϕ′ ⊢ β^{∗}ψ′}{ϕ ∘ ψ ⊢ (α ⊗ β)^{∗}ϕ′ ∘ ψ′}  (7.34)

We therefore define ⟨α⟩ ∘ ⟨β⟩ to be ⟨α ⊗ β⟩ : [ϕ ∘ ψ] → [ϕ′ ∘ ψ′]. The functoriality of ∘ follows in the same way as the functoriality of ⊗ in T_{0} (see 3.53 and 3.54).

Natural Transformations

⟨assr_{X,Y,Z}⟩ : [(ϕ ∘ ψ) ∘ θ] → [ϕ ∘ (ψ ∘ θ)]
⟨assl_{X,Y,Z}⟩ : [ϕ ∘ (ψ ∘ θ)] → [(ϕ ∘ ψ) ∘ θ]
⟨close_{X}⟩ : [T_{I} ∘ ϕ] → [ϕ]
⟨open_{X}⟩ : [ϕ] → [T_{I} ∘ ϕ]
⟨swap_{X,Y} ⟩ : [ϕ ∘ ψ] → [ψ ∘ ϕ]

where X, Y, Z are the types of the predicates ϕ, ψ, θ respectively. Naturality follows from the base category, as do the coherence conditions.

Closure

By proposition 3.3.7, T_{0} is symmetric monoidal closed. We note that ⟨eval_{X,Y} ⟩ : [(ϕ −∘ ψ) ∘ ϕ] → [ψ] is a morphism of P_{0}, and show that it is universal from (−) ∘ [ϕ] to [ψ].

Let ⟨α⟩ : [θ ∘ ϕ] → [ψ] then

⋮
θ(x), ϕ(y) ⊢ θ ∘ ϕ(x, y)  θ ∘ ϕ(x, y) ⊢ ψ(α(x, y)) (Cut)
θ(x), ϕ(y) ⊢ ψ(α(x, y))  (≈R)
θ(x), ϕ(y) ⊢ ψ(eval (Λ(α)(x), y)) ( −∘ R)
θ(x) ⊢ ϕ −∘ ψ(Λ(α)(x))

(7.35)

It follows from the above derivation that ⟨Λ(α)⟩ : [θ] → [ϕ −∘ ψ] is a morphism of P_{0}. As in T_{0}, we have that ⟨Λ(α)⟩ is the unique map satisfying ⟨eval⟩(⟨Λ(α)⟩ ∘ 1_{[ϕ]}) = ⟨α⟩. Moreover, z_{0} is strict monoidal strict closed.

Note 7.3.4 The unit of the adjunction (−) ∘ [ϕ] ⊣ [ϕ] −∘ (−) is

⟨hold_{X}⟩ : [ϕ] → [ψ −∘ (ϕ ∘ ψ)]

Fibration/op-fibration

We have defined z_{0} : P_{0} → T_{0} be the functor which maps an object [ϕ] to the type of ϕ and a morphism ⟨α⟩ : [ϕ] → [ψ] to its middle component [α] : X → Y.

Let ψ ∈ pred(C) and [γ] : B → C in T_{0}. We show that ⟨γ⟩ : [γ^{∗}ψ] → [ψ] is cartesian over [γ].

Let ⟨α⟩ : [ϕ] → [ψ] and suppose that z_{0}(⟨α⟩) = [α] factors through [γ]. That is α ≡ γ • β for some β. Then

α^{∗}ψ ⊣⊢ (γ • β)^{∗}ψ ⊣⊢ β^{∗}(γ^{∗}ψ)  (7.36)

It follows that ϕ ⊢ β^{∗}(γ^{∗}ψ) and so ⟨β⟩ : [ϕ] → [γ^{∗}ψ] is a morphism in P_{0}. Clearly, ⟨β⟩ makes the following diagram commute

[figure: [ϕ]; ⟨β⟩; ⟨α⟩; [γ^{∗}ψ]; \overline{⟨γ⟩}; [ψ]]  (7.37)

and, like all maps in P_{0}, is uniquely determined by its domain, codomain, and image under z_{0}.

Let ϕ ∈ pred(B) and [β] : B → C in T_{0}. We show that ⟨β⟩ : [ϕ] → [∃[β]ϕ] is op-cartesian over [β].

Let ⟨α⟩ : [ϕ] → [ψ] and suppose that z_{0}(⟨α⟩) = [α] factors through [β]. That is α ≡ γ • β for some γ. Then α^{∗}ψ ⊣⊢ β^{∗}(γ^{∗}ψ) and hence ⟨γ⟩ : [∃[β]ϕ] → [ψ] is a morphism of P_{0} by the following derived rule for ⊢.

\frac{ϕ ⊢ β^{∗}(γ^{∗}ψ)}{∃[β]ϕ ⊢ γ^{∗}ψ}  (7.38)

Clearly, ⟨γ⟩ makes the following diagram commute.

[figure: [ψ]; ⟨α⟩; ⟨γ⟩; [ϕ]; \overline{⟨β⟩}; [∃[β]ϕ]]  (7.39)

Again the uniqueness property of [γ] is trivial.

Interpretation of L_{F OLL}(B, F, E, P) in z_{0} : P_{0} → T_{0}

The interpretation ⟨ı_{0}, ȷ_{0}, | − |_{0}⟩ is given by the identity on types, the function mapping a combinator to its equivalence class under ≈, and the function mapping a predicate to its equivalence class under ⊣⊢. It is immediate from the definitions that this interpretation satisfies the conditions of theorem 7.3.1.

Conclusions and Further Work

The work contained in this thesis represents a first attempt to apply the techniques developed in the categorical model theory of classical and intuitionistic logic to linear logic. The main body of the work is concerned with the derivation of a system L_{F OLL} of first order intuitionistic linear logic from its intended model theory. This forms part of a wider programme of research to develop a uniform model theoretic framework for the logics arising in computer science, and the main benefits of the work are to illuminate the issues and requirements of such a framework. Specifically, we have shown that the analysis of first order logics as fibred categories with added structure can be applied in the case of linear logic, though not without considerable care.

As we move away from classical logic to intuitionistic, relevance, or linear logic, many of the logical principles which were taken for granted no longer continue to hold. The interest and challenge of these weaker logics is to reformulate the standard concepts in such a way to recover as much of the logical intuition as possible. The work here shows the difficulty of correctly formulating a first order version of linear logic, even given a good understanding of the propositional logic. The easiest path would have been to follow Seely [See87b] and consider predicates to be families of propositions indexed over some category with finite limits. However, this leads to a theory whose only models are given by construction [See90], and so gives no insight into the meaning of the logical operations and connectives.

In contrast, the system of first order linear logic L_{F OLL} presented here has a simple and clear semantics, in terms of, say, the subgroups of abelian groups. The price to be paid for this simplicity is that the logic contains a number of compromises which perhaps detract from its aesthetic appeal. Some of these are inevitable consequences of the linearity constraints; for example the failure of pullback to preserve joins, the nonfibrewise nature of the multiplicative connectives, and the slightly strange presentation of existential quantification. The status of others is less clear cut. The failure of the modified Beck condition 5.52 is justified because it does not hold in Ab, but perhaps, if we were more discerning about our class of models, this is a property which could hold.

Clearly, we would like to go on to investigate categories with stronger logical properties, but it is important to resist the temptation to refine the class of models too early. The various features mentioned above might lead one to dismiss categories such as Ab as ‘nonlogical’. The main point of the work presented here is to proceed undeterred by these apparent failings and extract the logical content that still remains. The fact that we retain Ab as an example gives our logic an independent mathematical interest.

The suggested class of models, symmetric monoidal closed categories C with a monoidal factorisation system (E, M), is based on a simple condition which relates factorisation and tensor product, that E is closed under tensor product. This condition is the minimum requirement for the M-subobjects to form a model of linear logic, and is mild enough to retain a large number of interesting examples. Furthermore, it appears in practice in some of the more complex constructions in enriched category theory; for instance, as part of the definition of a ‘locally bounded’ symmetric monoidal closed category [Kel82, page 210]. This gives a hint of the implicit logical content of these constructions.

There is obviously more work to be done before we fully understand the role of linear logic as an internal logic of symmetric monoidal closed categories. The work done here is intended to provide a firm basis for further research. It identifies some of the important concepts and issues in the categorical study of linear logic, in particular the connection between linearity in the logic and linearity in the type theory. This is illustrated by the examples of chapter 4 where the linearity constraints of the logic are used to define a tensor product at the level of types.

More generally, this analysis tells us three things about general model theoretic frameworks for classifying logics. First, there is an advantage in considering fibrations over indexed categories; the definition of a linear doctrine refers to the closure of the category of predicates as a whole, and so could not have been so conveniently expressed in terms of indexed categories. Secondly, there is a need for categories with added structure specified in terms of functors, natural transformations, and coherences; rather than categories with structure specified only by universal properties. Lastly, as the logical connectives are not preserved by substitution, one must allow the possibility of making substitution explicit.

For future work, some of the algebraic ideas developed in chapters 5 and 7 seem worth pursuing; in particular, the theory of monoidal factorisations and linear doctrines. It may be possible to reformulate the definition of a linear doctrine as an indexed category rather than a fibration, although it would seem to be more difficult to state the closure condition on predicates in this setting. If C is a complete symmetric monoidal closed category with monoidal factorisation system (E, M) then we can show that Sub_{M} : C → CSLat is a monoidal functor with comparison maps

⊤_{I} : I → Sub_{M}(I)
∘_{A,B} : Sub_{M}(A) ⊗ Sub_{M}(B) → Sub_{M}(A ⊗ B)

where ⊤_{I} picks out the top element of Sub_{M}(I) and ∘_{A,B} is the fusion of subobjects. An important property of monoidal functors is that they preserve monoids. Thus, a monoid in C will be mapped to a monoid in CSLat. That is, the subobjects of a monoid M in C form a quantale, and hence a consequence algebra. This gives a simple algebraic proof of the observation proved syntactically in section 6.3.2.

There are several obvious questions to be answered about the logic L_{F OLL}. In the main these relate to the possible extensions. One possibility is to extend the logic to include an involutive negation similar to that of the classical propositional logic. However, from section 6.3.3, it seems clear that any category C providing a model for this would have to be ∗-autonomous to ensure that the double negation ϕ^{⊥⊥} of a subobject ϕ lies in the same fibre as ϕ. This would seem to greatly reduce the interest in such a negation, since there are fewer good examples of a ∗-autonomous category.

In a similar vein, one might consider trying to add a modal operator !(−) to reintroduce weakening and contraction, though it is far from clear how this can be done. The repetition of a formula ϕ(t) appearing in the premise of a contraction contains a duplication of the variables in t, and hence violates the variable balancing condition. To successfully incorporate the !(−) modality, we must devise a mechanism round this; either a more lenient set of restrictions, or a similar ‘modal’ operator at the level of types.

Jay [Jay89b] makes some interesting observations on natural numbers objects in symmetric monoidal closed categories. If N is a natural numbers object in V then we can define maps N → N ⊗ N and N → I by ‘recursion’. The effect of these maps is to duplicate and destroy variables respectively. Thus there may be some interest in adding recursive types to LTT.

An early version of LTT had cartesian products together with a much more complicated variable occurrence condition. These could be reintroduced together with coproducts. However, one should not speculate too deeply on the possible syntactic extensions, without a clearer analysis of the class of models it is intended to represent. The logic that we have produced so far is justified by its particularly wide class of models. We should not consider making unnatural restrictions on the models in order to accommodate the features which although present in the propositional logic, may be of less significance here.

Another aspect of the logic L_{F OLL} which perhaps deserves more attention is the associated proof theory. It is natural to ask whether there is a cut elimination theorem for proofs in L_{F OLL}. This has not been a concern in the work so far because we have been interested in the theories L_{F OLL}(B, F, E, P) where E is a nonempty set of linear equational axioms. In this case, there is no hope of a cut elimination theorem, and the consistency of the logic is established by appeal to existence of nontrivial models. However, if E = ∅ then the sequent calculus presentation of L_{F OLL} is just a decorated extension of that for the propositional calculus, and it seems likely that there is a cut elimination algorithm.

As remarked in the introduction to chapter 4, there is yet no notion of a universe for linear logic which compares with that of topos for intuitionistic logic. The two examples presented in chapter 4 represent the first steps towards an appropriate generalisation which would permit an analysis of higher order linear logic.

The presheaf example is perhaps the less promising of the two. It is difficult to work with, the tensor product is almost impossible to calculate in all but the most trivial cases, and [C^{op}, Set] has too many extra properties, derived from the fact that it is a topos, to give any clear guidance on the required categorical structure. Note that the presheaf model is a generalisation of the resource semantics of section 2.2.3 and, as such, inherits the distributivity of meet over join 2.39.

By comparison, it is quite easy to make explicit calculations in the category of Q-sets, and this seems the most promising area for further work. As Q itself is a Q-set it seems that there should be some form of higher order linear logic to be discovered. This should be analogous to the form of logic given by a topos, but may be significantly different in detail. For example, in metric spaces every subspace X ↪ Y induces a ‘classifying map’ χ_{X} : Y → ℜ which sends each point y ∈ |Y | to its distance from the subspace X. The subspace X is certainly a pullback of {0} along this map, but χ is not unique with this property. Johnstone has suggested that the category of metric spaces and distance decreasing maps should be an example of a ‘collapsed topos’ but the precise definition of this structure is not yet certain. It seems reasonable to suppose that further experimentation with Q-sets might suggest the requisite categorical axioms.

The theory of locale valued sets includes the concept of partial existence which we have avoided for simplicity. It should certainly be possible to reintroduce an existence predicate, though this must be done explicitly because the intuitionistic ‘trick’ of encoding existence into equality depends crucially upon the properties of the conjunction ∧. One possible idea is to take categories enriched in a suitable bicategory rather than in a quantale. Walters has already shown that sheaves on a Chapter 8. Conclusions and Further Work 149 locale can be viewed in this way [Wal81,Wal82], but it is not clear how to modify this work for a quantale.

Bibliography

[AB75] A.R. Anderson and N.D. Belnap. Entailment, volume 1. Princeton University Press, Princeton, N.J., 1975.

[Abr90] S. Abramsky. Computational interpretations of linear logic. Research Report DOC 90/20, Imperial College, London, October 1990.

[AV90] S. Abramsky and S. Vickers. Quantales, observational logic, and process semantics. Research Report DOC 90/1, Imperial College, London, January 1990.

[Avr87] A Avron. Simple consequence relations. Technical Report ECS-LFCS-87-30, Laboratory for the Foundations of Computer Science, Univ. of Edinburgh, June 1987.

[B´85] J. Bénabou. Fibred categories and the foundations of naive category theory. Journal of Symbolic Logic, 50, 1985.

[Bar74] J. Barwise. Axioms for abstract model theory. Annals of Mathematical Logic, 7, 1974.

[BCBSC89] U. Berni-Canani, F. Borceux, and R. Succi-Cruciani. A theory of quantal sets. J. Pure Appl. Algebra, 62:123–136, 1989.

[BG84] R. Burstall and J. Goguen. Introducing institutions. In Logics of Programs. Springer-Verlag, 1984.

[BG90] C.T. Brown and D.J. Gurr. A categorical linear framework for petri nets. In Proceedings of Logic in Computer Science, 1990.

[Bir48] G. Birkhoff. Lattice Theory, volume 25 of A.M.S Colloquium Publications. American Mathematical Society, 190 Hope St, Providence, Rhode Island, revised edition, 1948.

[BJ90] R.M. Burstall and McKinna J.H. Deliverables: an approach to program development in constructions. In G. Huet and G. Plotkin, editors, Proceedings of the First Annual Workshop on Logical Frameworks, Antibes, May 1990.

[Bor90] F. Borceux. Sheaf representation of rings demystified. In Proceedings Category Theory ’90, Como, July 1990. To appear.

[Bro90] C.T. Brown. Linear Logic and Petri Nets: Categories, Algebra and Proof. PhD thesis, Univ. of Edinburgh, 1990.

[BVDB85] F. Borceux and G. Van Den Bossche. An essay on non-commutative topology. Séminaire Mathématique 70, Univ. Catholique de Louvain, June 1985.

[BVDB86] F. Borceux and G. Van Den Bossche. Quantales and their sheaves. Order, 3:61–87, 1986.

[CW87] A. Carboni and R.F.C. Walters. Cartesian bicategories I. J. Pure Appl. Algebra, 49:11–32, 1987.

[Dam88] M. Dam. Relevance logic and concurrent composition. In Proceedings of Logic in Computer Science, pages 178–185, 1988.

[Dam90] M. Dam. Relevance Logic and Concurrent Composition. PhD thesis, Univ. of Edinburgh, September 1990.

[dP89] V.C.V. de Paiva. A dialectica-like model of linear logic. In Proceedings of Category Theory and Computer Science, pages 341–356, Manchester,UK, September 1989. Springer-Verlag.

[Dun86] J.M. Dunn. Relevance logic and entailment. In D. Gabbay and F. Guenther, editors, Handbook of Philosophical Logic Vol.3. D.Reidel, Dordrecht, 1986.

[Fin74] K. Fine. Models for entailment. Journal of Philosophical Logic, 3:347–372, 1974.

[Fit69] M.C. Fitting. Intuitionistic Logic, Model Theory and Forcing. Studies in Logic and the Foundations of Mathematics. North-Holland, 1969.

[FK72] P.J. Freyd and G.M. Kelly. Categories of continuous functors I. J. Pure Appl. Algebra, 2:169–191, 1972.

[FS79] M.P. Fourman and D.S. Scott. Sheaves and Logic, volume 753 of Lecture Notes in Mathematics, pages 302–401. Springer-Verlag, 1979.

[FS90] P.J. Freyd and A. Scedrov. Categories, Allegories, volume 39 of Mathematical Library. North-Holland, 1990.

[Gen69] G. Gentzen. Investigations into logical deduction. In M.E. Szabo, editor, The Collected Papers of Gerhard Gentzen, pages 68–131. North Holland, 1969.

[Gir87a] J.Y. Girard. Linear logic. Theoretical Computer Science, 50, 1987.

[Gir87b] J.Y. Girard. Towards a geometry of interaction. In Proceedings of the Congress in Categories and Computer Science, Boulder. Amer. Math. Soc., June 1987.

[Gra66] J.W. Gray. Fibred and cofibred categories. In Proceedings of the Conference on Categorical Algebra, La Jolla, 1965. Springer-Verlag, 1966.

[GSS] J.Y. Girard, A. Scedrov, and P.J. Scott. Bounded linear logic. manuscript.

[HHP87] R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. In Proc. 2nd LICS, Cornell, 1987.

[Hig73] D. Higgs. A category approach to boolean valued set theory. manuscript, 1973.

[Hig84] D. Higgs. Injectivity in the topos of complete Heyting valued sets. Canad. J. Math., 36:550–568, 1984.

[HJP80] J.M.E. Hyland, P.T. Johnstone, and A.M. Pitts. Tripos theory. Math. Proc. Camb. Phil. Soc., 88:205–232, 1980.

[HM91] J. S. Hodas and D. Miller. Logic programming in a fragment of intuitionistic linear logic. technical report ECS-LFCS-91-158, Laboratory for the Foundations of Computer Science, Edinburgh, May 1991. Extended Abstract.

[HP] J. Harland and D. Pym. The uniform proof-theoretic foundation of linear logic programming. To appear in Proc. ICLP 1991.

[HP88] J.M.E. Hyland and A.M. Pitts. The theory of constructions : Categorical semantics and topos-theoretic models. In Proceedings of the Conference on Categories in Computer Science and Logic. Contemporary Mathematics, A.M.S., 1988.

[HS86] J.R. Hindley and J.P. Seldin. Introduction to Combinators and λ-Calculus, volume 1 of London Mathematical Society Student Texts. Cambridge University Press, 1986.

[Jay89a] C.B. Jay. Languages for monoidal categories. J. Pure Appl. Algebra, 59(1):61–85, 1989.

[Jay89b] C.B. Jay. A note on natural numbers objects in monoidal categories. Studia Logica, XLVIII(3), 1989.

[Jay90] C.B. Jay. The structure of free closed categories. J. Pure Appl. Algebra, 66:271–285, 1990.

[Joh77] P.T. Johnstone. Topos Theory. L.M.S Monographs No.10. Academic Press, London, 1977.

[Joh82] P.T. Johnstone. Stone Spaces. Cambridge Studies in Advanced Mathematics 3. Cambridge University Press, 1982.

[JT84] A. Joyal and M. Tierney. An extension of the Galios theory of Grothendieck. Memoirs of the American Mathematical Society, 51(309), September 1984.

[Kel82] G.M. Kelly. Basic Concepts of Enriched Category Theory. London Mathematical Society Lecture Note Series 64. Cambridge University Press, 1982.

[KML71] G.M. Kelly and S. Mac Lane. Coherence in closed categories. J. Pure Appl. Algebra, 1(1):97–140, 1971.

[Laf88] Y. Lafont. Logiques,Categories & Machines : Implantation de Langages de Programmation guidée par la Logique Catégorique. PhD thesis, l’Universite Paris VII, January 1988.

[Law69] F.W. Lawvere. Adjointness in foundations. Dialectica, 23:281–296, 1969.

[Law70] F.W. Lawvere. Equality in hyperdoctrines and comprehension schema as an adjoint functor. In A. Heller, editor, Proc. New York Symposium on Applications of Categorical Logic, pages 1–14. Amer. Math. Soc., 1970.

[Law73] F.W. Lawvere. Metric spaces, generalized logic, and closed categories. Rend. del Sem. Mat. e Fis. di Milano, 43:135–166, 1973.

[LS86] J.L. Lambek and P.J. Scott. Introduction to Higher Order Categorical Logic. Cambridge Studies in Advanced Mathematics No.7. Cambridge University Press, 1986.

[Mil89] R. Milner. Communication and Concurrency. Prentice Hall, 1989.

[ML71] S. Mac Lane. Categories for the Working Mathematician. Graduate Texts in Mathematics 5. Springer-Verlag, 1971.

[ML84] P. Martin Löf. Intuitionistic Type Theory. Sudies in Proof Theory. Bibliopolis, Naples, 1984.

[MR77] M. Makkai and G.E. Reyes. First Order Categorical Logic : Model Theoretic Methods in the Theory of Topoi and Related Categories, volume 611 of LNM. Springer-Verlag, 1977.

[Mul86] C.J. Mulvey. “&”. Suppl. ai Rend. del Circ. Mat. di Palermo, Serie II, 12:99–104, 1986.

[Naw85] M. Nawaz. Quantales: Quantal Sets. PhD thesis, University of Sussex, 1985.

[NR88] S.B. Niefield and K.I. Rosenthal. Constructing locales from quantales. Math. Proc. Camb. Phil. Soc., 104, 1988.

[OK85] H. Ono and Y. Kormori. Logics without the contraction rule. Journal of Symbolic Logic, 50(1):169–201, 1985.

[Pau89] L.C. Paulson. The foundations of a generic theorem prover. Journal of Automated Reasoning, 5:363–397, 1989.

[PS78] R. Paré and D. Schumacher. Abstract families and the adjoint functor theorems. In P.T. Johnstone and R. Pare, editors, Indexed categories and their applications, pages 1–125. Springer-Verlag, 1978.

[Rea88] S. Read. Relevant Logic: a Philosophical Examination of Inference. O.U.P., 1988.

[RM72] R. Routley and R.K. Meyer. The semantics of entailment. J. of Philosophical Logic, 1:53–73 and 192–208, 1972.

[Rob79] J.A. Robinson. Logic : Form and Function. Edinburgh University Press, 1979.

[Ros90] K.I. Rosenthal. Quantales and their Applications. Longman Scientific & Technical, 1990.

[Sch86] D.A. Schmidt. Denotational Semantics : A Methodology for Language Development. Allyn and Bacon, 7 Wells Av., Newton, Massachusetts 02159, 1986.

[Sco74] D. Scott. Completeness and Axiomatizability in Many-valued Logic, volume XXV of Proceedings of Symposia in Pure Mathematics, pages 411–161. Amer. Math. Soc., Rhode Island, 1974.

[See83] R.A.G. Seely. Hyperdoctrines, natural deduction and the beck condition. Zeitschr. f. math. Logik u. Grundlagen der Math. Bd.29, 1983.

[See84] R.A.G Seely. Locally cartesian closed categories and type theory. Math. Proc. Camb. Phil. Soc., 95, 1984.

[See87a] R.A.G. Seely. Categorical semantics for higher order polymorphic lambda calculus. Journal of Symbolic Logic, 52:505–542, 1987.

[See87b] R.A.G. Seely. Linear logic,∗-autonomous categories and cofree algebras. In Proceedings of the Congress in Categories and Computer Science, Boulder. Amer. Math. Soc., June 1987.

[See90] R.A.G. Seely. Polymorphic linear logic and topos models. Manuscript, 1990.

[SP82] M.B. Smyth and G.D. Plokin. The category theoretic solution of recursive domain equations. SIAM Journal of Computing, 11(4), 1982.

[Str81] R. Street. Enriched categories and cohomology. Quaestiones Mathematicae, 6:265–283, 1981.

[SW73] R.H. Street and R.F.C. Walters. The comprehensive factorisation of a functor. Bull. Amer. Math. Soc., 79:936–941, 1973.

[Tay86] P. Taylor. Recursive Domains, Indexed Category Theory, and Polymorphism. PhD thesis, Imperial College, London, 1986.

[Urq72] A. Urquhart. Semantics for relevant logics. Journal of Symbolic Logic, 37:159–169, 1972.

[Urq84] A. Urquhart. The undecidability of entailment. Journal of Symbolic Logic, 49:1059–1073, 1984.

[Vic89] S. Vickers. Topology via Logic, volume 5 of Cambridge Tracts in Theoretical Computer Science. C.U.P., 1989.

[Wal81] R.F.C. Walters. Sheaves and Cauchy complete categories. Cahiers de Topologie et Géométrie Différentielle, XXII(3):283–286, 1981.

[Wal82] R.F.C. Walters. Sheaves on sites as cauchy-complete categories. J. Pure Appl. Algebra, 24:95–102, 1982.

[Yet90] D.N. Yetter. Quantales and (non-commutative) linear logic. Journal of Symbolic Logic, 55(1), 1990.