Multiple Conclusion Linear Logic: Cut Elimination and More

Abstract

Full Intuitionistic Linear Logic (FILL) was first introduced by Hyland and de Paiva, and went against current beliefs that it was not possible to incorporate all of the linear connectives, e.g. tensor, par, and implication, into an intuitionistic linear logic. It was shown that their formalization of FILL did not enjoy cut-elimination by Bierman, but Bellin proposed a change to the definition of FILL in the hope to regain cut-elimination. In this note we adopt Bellin’s proposed change and give a direct proof of cut-elimination. Then we show that a categorical model of FILL in the basic dialectica category is also a LNL model of Benton and a full tensor model of Melliès’ and Tabareau’s tensorial logic. Lastly, we give a double-negation translation of linear logic into FILL that explicitly uses par in addition to tensor.

1 Introduction

A commonly held belief during the early history of linear logic was that the linear-connective par could not be incorporated into an intuitionistic linear logic. This belief was challenged when de Paiva gave a categorical understanding of Gödel’s Dialectica interpretation in terms of dialectica categories [8, 9].

Dialectica categories were initially believed to be models of intuitionistic logic, but they are actually models of intuitionistic linear logic, containing the linear connectives: tensor, implication, the additives, and the exponentials. Further work improved de Paiva’s models to capture both intuitionistic and classical linear logic. Armed with this semantic insight de Paiva gave the first formalization of Full Intuitionistic Linear Logic (FILL) [8]. FILL is a sequent calculus with multiple conclusions in addition to multiple hypotheses. Logics of this type go back to Gentzen’s work on the sequent calculus for classical logic LK and for intuitionistic logic LJ, and Maehara’s work on LJ’ [16, 24]. The sequents in these types of logics usually have the form $\varGamma \vdash \varDelta$ where $\varGamma$ and $\varDelta$ are multisets of formulas. Sequents such as these are read as “the conjunction of the formulas in $\varGamma$ imply the disjunction of the formulas in $\varDelta$”. For a brief, but more complete history of logics with multiple conclusions see the introduction to [11].

Gentzen showed that to obtain intuitionistic logic one could start with the logic LK and then place a cardinality restriction on the right-hand side of sequents, however, this is not the only means of enforcing intuitionism. Maehara showed that in the propositional case one could simply place the cardinality restriction on the premise of the implication right rule, and leave all of the other rules of LK unrestricted. This restriction is sometimes called the Dragalin restriction, as it appeared in his AMS textbook [12]. The classical implication right rule has the form:

By placing the Dragalin restriction on the previous rule we obtain:

de Paiva’s first formalization of FILL used the Dragalin restriction, see [8] p. 58, but Schellinx showed that this restriction has the unfortunate consequence of breaking cut-elimination [22].

Later, Hyland and de Paiva gave an alternative formalization of FILL with the intention of regaining cut-elimination [13]. This new formalization lifted the Dragalin restriction by decorating sequents with a term assignment. Hypotheses were assigned variables, and the conclusions were assigned terms. Then using these terms one can track the use of hypotheses throughout a derivation. They proposed a new implication right rule:

Intuitionism is enforced in this rule by requiring that the variable being discharged, x, is not free terms annotating other conclusions. Unfortunately, this formalization did not enjoy cut-elimination either.

Bierman was able to give a counterexample to cut-elimination [4]. As Bierman explains the problem was with the left rule for the multiplicative disjunction par. The original rule was as follows:

In this rule the pattern variables x and y are bound in each term of $\varDelta$ and $\varDelta '$ respectively. Notice that the variable z becomes free in every term in $\varDelta$ and $\varDelta '$. Bierman showed that this rule mixed with the restriction on implication right prevents the usual cut-elimination step that commutes cut with the left rule for par. The main idea behind the counterexample is that in the derivation before commuting the cut it is possible to discharge z using implication right, but after the cut is commuted past the left rule for par, the variable z becomes free in more than one conclusion, and thus, can no longer be discharged.

In the conclusion of Bierman’s note he gives an alternate left rule for par that he attributes to Bellin. This new left-rule is as follows:

In this rule and only let-bind z in t or $t'$ if $x \in FV(t)$ or $y \in FV(t')$. Otherwise the terms are left unaltered. Bellin showed that by adopting this rule cut-elimination can be proven by reduction to the cut-elimination procedure for proof nets for multiplicative linear logic with the mix rule [1]. However, this is an indirect proof that requires the adoption of proof nets.

Contributions. In this paper our main contribution is to give a direct proof of cut-elimination for FILL with Bellin’s proposed par-left rule (Sect. 3). A direct proof accomplishes two goals: the first is to complete the picture of FILL Hyland and de Paiva started, and the second is to view a direct proof of cut-elimination as a means of checking the correctness of the formulation of FILL given here. The latter point is important for future work. Following the proof of cut-elimination we show that the categorical model of FILL called $\mathsf {Dial_2}(\mathsf {Sets})$, the basic dialectica category, is also a linear/non-linear model of Benton (Sect. 4) and a full tensor model of Melliès’ and Tabareau’s tensor logic (Sect. 5). Finally, we give a double-negation translation of multi-conclusion classical linear logic into FILL (Sect. 5.1). Due to the complexities of working in $\mathsf {Dial_2}(\mathsf {Sets})$ we have formalized all of the constructions and proofs used in Sects. 4 and 5 – although our formal verification does not include the double-negation translation in Sect. 5.1 – in the Agda proof assistant¹.

Related Work. The first formalization of FILL with cut-elimination was due to Braüner and de Paiva [5]. Their formalization can be seen as a linear version of LK with a sophisticated meta-level dependency tracking system. A proof of a FILL sequent in their formalization amounts to a classical derivation, $\pi$, invariant in what they call the FILL property:

• The hypothesis discharged by an application of the implication right rule in $\pi$ is a dependency of the conclusion of the implication being introduced.

They were able to show that their formalization is sound, complete, and enjoys cut-elimination. In favor of the term assignment formalization given here over Braüner and de Paiva’s formalization we can say that the dependency tracking system complicates both the definition of the logic and its use. However, one might conjecture that their system is more fundamental and hence more generalizable. It might be possible to prove cut-elimination of the term assignment formalization of FILL relative to Braüner and de Paiva’s dependency tracking system by erasing the terms on conclusions and then tracking which variable is free in which conclusion. However, as we stated above a direct proof is more desirable than a relative one.

de Paiva and Pereira used annotations on the sequents of LK to arrive at full intuitionistic logic (FIL) with multiple conclusion that enjoys cut-elimination [11]. They annotate hypothesis with natural number indices, and conclusions with finite sets of indices. The sets of indices on conclusions correspond to the collection of the hypotheses that the conclusion depends on. Then they have a similar property to that of Braüner and de Paiva’s formalization. In fact, the dependency tracking system is very similar to this formalization, but the dependency tracking has been collapsed into the object language instead of being at the meta-level.

Clouston et al. give both a deep inference calculus and a display calculus for FILL that admits cut-elimination [6]. Both of these systems are refinements of a larger one called bi-intuitionistic linear logic (BiLL). This logic contains every logical connective of FILL with the addition of the exclusion (or subtraction) connective. This connective can be defined categorically as the left-adjoint to par. Thus, exclusion is the dual to implication. A positive aspect to this work is that the resulting systems are annotation free, but at a price of complexity. Deep inference and display calculi are harder to understand, and their system requires FILL to be defined as a refinement of a system with additional connectives. We show in this paper that such a refinement is unnecessary. In addition, a term assignment system is closer to traditional logic than deep inference and display calculi, and it is closer, through the lens of the Curry-Howard-Lambek correspondence, to a type theoretic understanding of FILL.

2 Full Intuitionistic Linear Logic (FILL)

In this section we give a brief description of FILL. We first give the syntax of formulas, patterns, terms, and contexts. Following the syntax we define several meta-functions that will be used when defining the inference rules of the logic.

Definition 1

The syntax for FILL is as follows:

The formulas of FILL are standard, but we denote the unit of tensor as $\top$ and the unit of par as $\perp$. Patterns are used to distinguish between the various let-expressions for tensor, par, and their units. There are three different let-expressions:

In addition, each of these will have their own equational rules, see Fig. 2. The role each term plays in the overall logic will become clear after we introduce the inference rules.

At this point we introduce some syntax and meta-level functions that will be used in the definition of the inference rules for FILL. Left contexts are multisets of formulas each labeled with a variable, and right contexts are multisets of formulas each labeled with a term. We will often write $\varDelta _{{\mathrm {1}}} \mid \varDelta _{{\mathrm {2}}}$ as syntactic sugar for $\varDelta _{{\mathrm {1}}} , \varDelta _{{\mathrm {2}}}$. The former should be read as “$\varDelta _{{\mathrm {1}}}$ or $\varDelta _{{\mathrm {2}}}$.” We denote the usual capture-avoiding substitution by $[ t / x ] t'$, and its straightforward extension to right contexts as $[ t / x ] \varDelta$. Similarly, we find it convenient to be able to do this style of extension for the let-binding as well.

Definition 2

We extend let-binding terms to right contexts as follows:

Lastly, we denote the usual function that computes the set of free variables in a term by $\mathsf {FV}( t )$, and its straightforward extension to right contexts as $\mathsf {FV}(\varDelta )$.

Fig. 1.

Inference rules for FILL

The inference rules for FILL are defined in Fig. 1. The $\textsc {Parl}$ rule depends on the function $\mathsf {{\text {let-pat}} }\, z \, p \, \varDelta$ which we define next.

Definition 3

The function $\mathsf {{\text {let-pat}} }\, z \, p \, t$ is defined as follows:

It is straightforward to extend the previous definition to right-contexts, and we denote this extension by $\mathsf {{\text {let-pat}} }\, z \, p \, \varDelta$.

The motivation behind this function is that it only binds the pattern variables in and if and only if those pattern variables are free in the body of the let. This overcomes the counterexample given by Bierman in [4].

The terms of FILL are equipped with an equivalence relation defined in Fig. 2. There are a number of $\alpha$, $\beta$, and $\eta$ like rules as well as several rules we call naturality rules. These rules are similar to the rules presented in [13].

Fig. 2.

Equivalence on terms

3 Cut-Elimination

FILL can be viewed from two different angles: i. as an intuitionistic linear logic with par, or ii. as a restricted form of classical linear logic. Thus, to prove cut-elimination of FILL one only needs to start with the cut-elimination procedure for intuitionistic linear logic, and then dualize all of the steps in the procedure for tensor and its unit to obtain the steps for par and its unit. Similarly, one could just as easily start with the cut-elimination procedure for classical linear logic, and then apply the restriction on the implication right rule producing a cut-elimination procedure for FILL.

The major difference between proving cut-elimination of FILL from classical or intuitionistic linear logic is that we must prove an invariant across each step in the procedure. The invariant is that if a derivation $\pi$ is transformed into a derivation $\pi '$, then the terms in the conclusion of the final rule applied in $\pi$ must be transformable, when the equivalences defined in Fig. 2 are taken as left-to-right rewrite rules, into the terms in the conclusion of the final rule applied in $\pi '$.

We finally arrive at cut-elimination.

Theorem 1

If $\varGamma \vdash t_{{\mathrm {1}}} : A_{{\mathrm {1}}} , \, ... \, , t_{ i } : A_{ i }$ steps to $\varGamma \vdash t'_{{\mathrm {1}}} : A_{{\mathrm {1}}} , \, ... \, , t'_{ i } : A_{ i }$ using the cut-elimination procedure, then $t_{ j } = t'_{ j }$ for $1 \le j \le i$.

Proof

The cut-elimination procedure given here is the standard cut-elimination procedure for classical linear logic except the cases involving the implication right rule have the FILL restriction. The structure of our procedure follows the structure of the procedure found in [17]. Throughout this proof we treat the equivalences defined in Fig. 2 as left-to-right rewrite rules. For the entire proof see the companion report [14].

Corollary 1

(Cut-Elimination). Cut-elimination holds for FILL.

4 Full LNL Models

One of the difficult questions considering the categorical models of linear logic was how to model Girard’s exponential, !, which is read “of course”. The ! modality can be used to translate intuitionistic logic into intuitionistic linear logic, and so the correct categorical interpretation of ! should involve a relationship between a cartesian closed category, and the model of intuitionistic linear logic.

de Paiva gave some of the first categorical models of both classical and intuitionistic linear logic in her thesis [8]. She showed that a particular dialectica category called $\mathsf {Dial_2}(\mathsf {Sets})$ is a model of FILL where ! is interpreted as a comonad which produces natural comonoids, see page 76 of [8].

Definition 4

The category $\mathsf {Dial_2}(\mathsf {Sets})$ consists of

• objects that are triples, $A = (U,X,\alpha )$, where U and X are sets, and $\alpha \subseteq U \times X$ is a relation, and

• maps that are pairs $(f,F) : (U,X,\alpha ) \rightarrow (V,Y,\beta )$ where $f : U \rightarrow V$ and $F : Y \rightarrow X$ such that

  • For any $u \in U$ and $y \in Y$, $\alpha (u,F(y))$ implies $\beta (f(u),y)$.

Suppose $A = (U,X,\alpha )$, $B = (V,Y,\beta )$, and $C = (W,Z,\gamma )$. Then identities are given by $(\mathsf {id}_U,\mathsf {id}_X) : A \rightarrow A$. The composition of the maps $(f,F) : A \rightarrow B$ and $(g, G) : B \rightarrow C$ is defined as $(f;g,G;F) : A \rightarrow C$.

In her thesis de Paiva defines a particular class of dialectica categories called GC over a base category C, see page 41 of [8]. The category $\mathsf {Dial_2}(\mathsf {Sets})$ defined above can be seen as an instantiation of GC by setting C to be the category $\mathsf {Sets}$ of sets and functions between them. This model is a non-trivial model (all four units of the multiplicative and additive disjunction are different objects in the category), and does not model classical logic; see [8] page 58.

Seely gave a different, syntactic categorical model that confirmed that the of-course exponential should be modeled by a comonad [23]. However, Seely’s model turned out to be unsound, as pointed out by Bierman [3]. This then prompted Bierman, Hyland, de Paiva, and Benton to define another categorical model called linear categories (Definition 5) that are sound, and also model ! using a monoidal comonad [3].

Definition 5

A linear category, $\mathcal {L}$, consists of:

• A symmetric monoidal closed category $\mathcal {L}$,

• A symmetric monoidal comonad $(!, \epsilon , \delta , m_{A,B}, m_I)$ such that

  • For every free !-coalgebra $(!A,\delta _A)$ there are two distinguished monoidal natural transformations $e_A : !A \rightarrow I$ and $d_A : !A \rightarrow !A \otimes !A$ which form a commutative comonoid and are coalgebra morphisms.

  • If $f : (!A,\delta _A) \rightarrow (!B,\delta _B)$ is a coalgebra morphism between free coalgebras, then it is also a comonoid morphism.

This definition is the one given by Bierman in his thesis, see [3] for full definitions.

Intuitionistic logic can be interpreted in a linear category as a full subcategory of the category of !-coalgebras for the comonad, see proposition 17 of [3].

Benton gave a more balanced view of linear categories called LNL models.

Definition 6

A linear/non-linear model (LNL model) consists of

• a cartesian closed category $(\mathcal {C}, 1, \times , \Rightarrow )$,

• a SMCC $(\mathcal {L},I,\otimes ,\multimap )$, and

• a pair of symmetric monoidal functors $(G,n) : \mathcal {L} \rightarrow \mathcal {C}$ and $(F,m) : \mathcal {C} \rightarrow \mathcal {L}$ between them that form a symmetric monoidal adjunction with $F \dashv G$.

See Benton, [2], for the definitions of symmetric monoidal functors and adjunctions.

A non-trivial consequence of the definition of a LNL model is that the ! modality can indeed be interpreted as a monoidal comonad. Suppose $(\mathcal {L}, \mathcal {C},F,G)$ is a LNL model. Then the comonad is given by $(\mathop {!}, \epsilon : \mathop {!} \rightarrow \mathsf {Id}, \delta : \mathop {!} \rightarrow \mathop {!!})$ where $! = FG$, $\epsilon$ is the counit of the adjunction and $\delta$ is the natural transformation $\delta _A = F(\eta _{G(A)})$, see page 15 of [2]. We recall the following result from Benton [2]:

Theorem 2

(LNL Models and Linear Categories)

• i. (Sect. 2.2.1 of [2]) Every LNL model is a linear category.

• ii. (Sect. 2.2.2 of [2]) Every linear category is a LNL model.

Proof

The proof of part i. is a matter of checking that each part of the definition of a linear category can be constructed using the definition of a LNL model. See lemmata 3–7 of [2].

As for the proof of part ii. Given a linear category we have a SMCC and so the difficulty of proving this result is constructing the CCC and the adjunction between both parts of the model. Suppose $\mathcal {L}$ is a linear category. Benton constructs the CCC out of the full subcategory of Eilenberg-Moore category $\mathcal {L}^!$ whose objects are exponentiable coalgebras denoted $\mathsf {Exp}(\mathcal {L}^!)$. He shows that this subcategory is cartesian closed, and contains the (co)Kleisli category, $\mathcal {L}_!$, Lemma 11 on page 23 of [2]. The required adjunction $F : \mathsf {Exp}(\mathcal {L}^!) \rightarrow L : G$ can be defined using the adjunct functors $F(A,h_A) = A$ and $G(A) = (!A,\delta _A)$, see lemmata 13–16 of [2].

Next we show that the category $\mathsf {Dial_2}(\mathsf {Sets})$ is a full version of a linear category. First, we extend the definitions of linear categories and LNL models to be equipped with the necessary categorical structure to model par and its unit.

Definition 7

A full linear category, $\mathcal {L}$, consists of a linear category $(\mathcal {L}, \top , \otimes , \multimap ,!A,e_A,d_A)$, a symmetric monoidal structure on L, , and distribution natural transformations and . The distributors must satisfy several coherence conditions which can all be found in [7].

Definition 8

A full linear/non-linear model (full LNL model) consists of a LNL model $(\mathcal {L}, \mathcal {C},F,G)$, and a symmetric monoidal structure on L, , as above.

First we show that $\mathsf {Dial_2}(\mathsf {Sets})$ is a full linear category, and then using the proof by Benton that linear categories are LNL models we obtain that $\mathsf {Dial_2}(\mathsf {Sets})$ is a full LNL model. In order for this to work we need to know that $\mathsf {Dial_2}(\mathsf {Sets})$ has a symmetric monoidal comonad $(!, \epsilon , \delta , m_{A,B}, m_I)$. At the time of de Paiva’s thesis it was not known that the comonad modeling the of-course exponential needed to be monoidal. We were able to show that the maps $m_{A,B}$ and $m_I$ exist in the more general setting of dialectica categories, and thus, these maps exist in $\mathsf {Dial_2}(\mathsf {Sets})$. Intuitively, given two objects $A = (X,U,\alpha )$ and $B = (V,Y,\beta )$ of $\mathsf {Dial_2}(\mathsf {Sets})$ the map $m_{A,B}$ is defined as the pair $(\mathsf {id}_{U \times V},F)$, where $F = (F_1,F_2)$, $F_1 : (U \times V) \Rightarrow (V \Rightarrow X)^* \rightarrow V \Rightarrow (U \Rightarrow X^*)$ and $F_2 : (U \times V) \Rightarrow (U \Rightarrow Y)^* \rightarrow U \Rightarrow (V \Rightarrow Y^*)$. The maps $F_1$ and $F_2$ build the sequence of all the results of applying each function in the input sequence to the input coordinate.

We can now show that the following holds.

Lemma 1

The category $\mathsf {Dial_2}(\mathsf {Sets})$ is a full linear category.

Proof

We only give a sketch of the proof here, but for the full details see that companion report [14]². First, we must show that $\mathsf {Dial_2}(\mathsf {Sets})$ is a linear category. The majority of the linear structure of $\mathsf {Dial_2}(\mathsf {Sets})$ is in de Paiva’s thesis [8]. We had to extend her definitions to show that the comonad $(!A,\delta ,\epsilon )$ is monoidal, however, this is straightforward.

After showing that $\mathsf {Dial_2}(\mathsf {Sets})$ is a linear category one must show that $\mathsf {Dial_2}(\mathsf {Sets})$ is a model of par and its unit. This easily follows from de Paiva’s thesis. The bifunctor which models par is given by de Paiva in Definition 10 on page 47 of [8].

Finally, $\mathsf {Dial_2}(\mathsf {Sets})$ must be distributive. The natural transformations $dist_1$ and $dist_2$ can be defined in terms of the maps and given on page 52 of [8]. Set $A' = \top$ in k and $C = \top$ in $k'$ to obtain $dist_1$ and $dist_2$ respectively. They can also be shown to satisfy the coherence conditions given in [7].

Corollary 2

The category $\mathsf {Dial_2}(\mathsf {Sets})$ is a full LNL model.

Proof

This follows directly from the previous lemma and Theorem 2 which shows that linear categories are LNL models.

The point of these calculations is to show that the several different axiomatizations available for models for linear logic are consistent and that a model proved sound and complete according to Seely’s definition (using the Seely isomorphisms $!(A \times B)\cong !A\otimes !B$ and $!1\cong \top$ but adding to it monoidicicty of the comonad) is indeed sound and complete as a LNL model too.

5 Tensorial Logic

Melliès and Tabareau introduced tensorial logic as a means of generalizing linear logic to a theory of tensor and a non-involutive negation called tensorial negation. That is, instead of an isomorphism $A = \lnot \lnot A$ we have only a natural transformation $A \rightarrow \lnot \lnot A$ [18]. Tensorial logic makes the claim that tensor and tensorial negation are more fundamental than tensor and negation defined via implication. This is at odds with FILL where implication is considered to be fundamental. In this section we show that multiplicative tensorial logic can be modeled by $\mathsf {Dial_2}(\mathsf {Sets})$ (Lemma 3) by showing that tensorial negation arises as a simple property of the implication in any SMCC (Lemma 2). While this is expected (after all negation being defined in terms of implication into absurdity is one of the staples of intuitionism) we think it bolsters our claim that linear implication is a fundamental connective that should not be redefined in terms of the multiplicative disjunction par. In any case, any model of FILL can be seen as a model of multiplicative tensorial logic.

A categorical model of tensorial logic is a symmetric monoidal category with a tensorial negation.

Definition 9

A tensorial negation on a symmetric monoidal category $(\mathcal {C},\otimes ,I)$ is defined as a functor $\lnot : \mathcal {C} \rightarrow \mathcal {C}^{\mathsf {op}}$ together with a family of bijections $\phi _{A,B,C} : \mathsf {Hom}_{\mathcal {C}}(A \otimes B,\lnot C) \cong \mathsf {Hom}_{\mathcal {C}}(A,\lnot (B \otimes C))$ natural in A, B, and C. Furthermore, the following diagram must commute:

The most basic form of tensorial logic is called multiplicative tensorial logic and only consists of tensor and a tensorial negation. The model of multiplicative tensorial logic is called a dialogue category.

Definition 10

A dialogue category is a symmetric monoidal category equipped with a tensorial negation.

At this point we show that tensorial negation arises as a simple property of implication, as is traditional.

Lemma 2

In any monoidal closed category, $\mathcal {C}$, there is a natural bijection $\phi _{A,B,C,D} : \mathsf {Hom}_{\mathcal {C}}(A \otimes B,C \multimap D) \cong \mathsf {Hom}_{\mathcal {C}}(A,(B \otimes C) \multimap D)$. Furthermore, the following diagram commutes:

Proof

Suppose $\mathcal {C}$ is a monoidal closed category. Then we can define $\phi (f : A \otimes B \rightarrow C \multimap D) = \mathsf {cur}(\alpha ^{-1} ; \mathsf {cur}^{-1}(f))$ and $\phi ^{-1}(g : A \rightarrow (B \otimes C) \multimap D) = \mathsf {cur}(\alpha ; \mathsf {cur}^{-1}(g))$. Clearly, these are mutual inverses, and hence, $\phi$ is a bijection. Naturality of $\phi$ easily follows. Lastly, the diagram given above also commutes. For the complete proof see the companion report [14].

Any model of FILL contains the unit of par, $\perp$, and thus, can be used to define the negation function $\lnot A := A \multimap \perp$. Now replacing D and E in the previous result with $\perp$ yields the definition of tensorial negation.

Lemma 3

$\mathsf {Dial_2}(\mathsf {Sets})$ is a model of multiplicative tensorial logic.

Proof

We have already shown $\mathsf {Dial_2}(\mathsf {Sets})$ to be a model of FILL, and thus, has a SMCC structure as well as the negation functor, and thus, by Lemma 2 has a tensorial negation³.

Extending a model of multiplicative tensorial logic with an exponential resource modality yields a model of full tensorial logic.

Definition 11

A resource modality on a symmetric monoidal category $(\mathcal {C}, \otimes , I)$ is an adjunction with a symmetric monoidal category $(\mathcal {M}, \otimes ', I')$:

A resource modality is called an exponential resource modality if $\mathcal {M}$ is cartesian where $\otimes '$ is the product and $I'$ is the terminal object.

A model of full tensorial logic is defined to be a model of multiplicative tensorial logic with an exponential resource modality. We now know that $\mathsf {Dial_2}(\mathsf {Sets})$ is a model of multiplicative tensorial logic. By constructing the co-Kleisli category which consists of the !-coalgebras as objects, and happens to be cartesian, we can show that $\mathsf {Dial_2}(\mathsf {Sets})$ is a model of full tensorial logic. The adjunction with the co-Kleisli category naturally arises from the proof that $\mathsf {Dial_2}(\mathsf {Sets})$ is a full LNL model (Corollary 2).

Lemma 4

The category $\mathsf {Dial_2}(\mathsf {Sets})$ is a model of full tensorial logic.

Proof

It suffices to show that there is an adjunction between $\mathsf {Dial_2}(\mathsf {Sets})$ and a cartesian category. Define the category $\mathsf {Dial_2}(\mathsf {Sets})_!$ as follows:

• Take as objects $(U , (U \Rightarrow X^*), \alpha _!)$ where U and X are sets, and $\alpha \subseteq U \times (U \Rightarrow X^*)$.

• Take as morphisms $(f , F) : (U , (U \Rightarrow X^*), \alpha _!) \rightarrow (V , (V \Rightarrow Y^*), \beta _!)$ where $f : U \rightarrow V$ and $F : (V \Rightarrow Y^*) \rightarrow (U \Rightarrow X^*)$ subject to the same condition on morphisms as $\mathsf {Dial_2}(\mathsf {Sets})$. Composition and identities are defined similarly to $\mathsf {Dial_2}(\mathsf {Sets})$.

Next we must show that $\mathsf {Dial_2}(\mathsf {Sets})_!$ is cartesian. Notice that $\mathsf {Dial_2}(\mathsf {Sets})_!$ is a subcategory of $\mathsf {Dial_2}(\mathsf {Sets})$, and there is a functor $J : \mathsf {Dial_2}(\mathsf {Sets})\rightarrow \mathsf {Dial_2}(\mathsf {Sets})_!$ which is defined equivalently to the endofunctor ! from the proof of Lemma 1. In fact, $\mathsf {Dial_2}(\mathsf {Sets})_!$ is the co-Kleisli category with objects free !-coalgebras and is cartesian closed [9]. However, we only need the fact that it is cartesian.

To show that $\mathsf {Dial_2}(\mathsf {Sets})_!$ is cartesian it suffices to show that J preserves the cartesian structure of $\mathsf {Dial_2}(\mathsf {Sets})$ – the proof that $\mathsf {Dial_2}(\mathsf {Sets})$ is cartesian can be found on page 48 of [8]. This follows by straightforward reasoning. For the complete proof see the companion report [14].

5.1 Double Negation Translation

In this section we show that we can use intuitionistic negation – which we showed was tensorial in the previous section – to define a negative translation of multi-conclusion linear logic (Fig. 3) into FILL where implication plays a central role. Melliès and Tabareau give a negative translation of the multiplicative fragment of linear logic into tensorial logic [19] using tensor as the main connective. For example, they define $( A \otimes B )^N = \lnot ( \lnot ( A )^N \otimes \lnot ( B )^N )$, and thus, they simulate par using tensor and negation. This definition would cause some syntactic issues with FILL, because the left-rule to par requires the let-pattern term defined in Definition 3, thus, encoding par in terms of tensor would require the let-pattern term to be used in the left-rule for tensor. While simulating par, using tensor and negation, can be seen as useful, in applications where only the tensor product can be actually calculated, in other applications we do have an extra bifunctor like par. This is true in the case of FILL, so we can modify Melliès and Tabareau’s translation into one that better fits the source logical system.

Fig. 3.

Multi-Conclusion Linear Logic

The following definition defines a translation of linear logic formulas into FILL formulas.

Definition 12

The following is the double-negation translation of linear logic into FILL:

The main point of the previous definition is that because FILL has intuitionistic versions of all of the operators of linear logic we can give a very natural translation that preserves these operators by double negating their arguments.

At this point we need to extend the translation of linear logic formulas to sequents. However, we must be careful, because in FILL implication has the FILL restriction, and thus, if we choose the wrong translation then we will run into problems trying to satisfy the FILL condition. The method we employ here is to first translate a linear logic sequent into a single-sided sequent, and then translate that to FILL using the well-known translation. That is, it is easy to see that any linear logic sequent $A_{{\mathrm {1}}} , \, ... \, , A_{ i } \vdash B_{{\mathrm {1}}} , \, ... \, , B_{ j }$ is logically equivalent to the sequent $\cdot \vdash A_{{\mathrm {1}}} ^{\perp } , \, ... \, , A_{ i } ^{\perp } , B_{{\mathrm {1}}} , \, ... \, , B_{ j }$. Then we translate the latter into FILL as $x_{{\mathrm {1}}} : \lnot ( ( A_{{\mathrm {1}}} ^{\perp } )^N ) , \, ... \, , x_{ i } : \lnot ( ( A_{ i } ^{\perp } )^N ) , y_{{\mathrm {1}}} : \lnot ( ( B_{{\mathrm {1}}} )^N ) , \, ... \, , y_{ j } : \lnot ( ( B_{ j } )^N ) \vdash \cdot$ for any free variables $x_{{\mathrm {1}}} ,\ldots , x_{ i }$ and $y_{{\mathrm {1}}} ,\ldots , y_{ j }$, but this is equivalent to $x_{{\mathrm {1}}} : \lnot \lnot ( ( A_{{\mathrm {1}}} )^N ) , \, ... \, , x_{ i } : \lnot \lnot ( ( A_{ i } )^N ) , y_{{\mathrm {1}}} : \lnot ( ( B_{{\mathrm {1}}} )^N ) , \, ... \, , y_{ j } : \lnot ( ( B_{ j } )^N ) \vdash \cdot$. The reader may realize that this is indeed the translation of single-sided classical linear logic into single-conclusion intuitionistic linear logic. This translation also has the benefit that we do not have to worry about mentioning terms in the statement of the result.

Lemma 5

(Negative Translation). If $A_{{\mathrm {1}}} , \, ... \, , A_{ i } \vdash B_{{\mathrm {1}}} , \, ... \, , B_{ j }$ is derivable, then for any unique fresh variables $x_{{\mathrm {1}}} ,\ldots , x_{ i }$, and $y_{{\mathrm {1}}} ,\ldots , y_{ j }$, the sequent $x_{{\mathrm {1}}} : \lnot \lnot ( ( A_{{\mathrm {1}}} )^N ) , \, ... \, , x_{ i } : \lnot \lnot ( ( A_{ i } )^N ) , y_{{\mathrm {1}}} : \lnot ( ( B_{{\mathrm {1}}} )^N ) , \, ... \, , y_{ j } : \lnot ( ( B_{ j } )^N ) \vdash \cdot$ is derivable.

Proof

This can be shown by induction on the assumed sequent. For the complete proof see the companion report [14].

6 Conclusion and Future Work

We first recalled the definition of full intuitionistic linear logic using the left rule for par proposed by Bellin in Sect. 2, but using only proof-theoretic methods, no proof nets. We then directly proved cut-elimination for FILL in Sect. 3 by adapting the well-known cut-elimination procedure for classical linear logic to FILL.

In Sect. 4 we showed that the category $\mathsf {Dial_2}(\mathsf {Sets})$, a model of FILL, is a full LNL model by showing that it is a full linear category, and then replaying the proof that linear categories are LNL models by Benton. Then in Sect. 5 we showed that $\mathsf {Dial_2}(\mathsf {Sets})$ is a model of full tensorial logic. The point of this exercise in categorical logic is to show that, despite linear logicians infatuation with linear negation, there is value in keeping all your connectives independent of each other. Only making them definable in terms of others, for specific applications.

Games, especially programming language games are the main motivation for Tensorial Logic and have been one of the sources of intuitions in linear logic all along. Since we are interested in the applications of tensorial logic to concurrency, we would like to see if our slightly more general framework can be applied to this task, just as well as tensorial logic.

Independently of the envisaged applications to programming, we are also interested in developing a “man in the street” game-like explanation for the finer-grained connectives of FILL, especially for par, the multiplicative disjunction. The second author has talked about games for FILL in the style of Lorenzen [10], building up on the work of Rahman [15, 21]. Rahman showed that Lorenzen games could be defined for classical linear logic [20] and was able to define a sound and complete semantics in Lorenzen games for classical linear logic. While Rahman does mention that one could adopt a particular structural rule that enforces intuitionism, we have not seen a complete proof of soundness and completeness for this semantics. We plan to show that by adopting this rule we actually obtain a sound and complete semantics in Lorenzen games for FILL.