On the Canonicity of Linear Logic Connectives

Posted on by Olivier Laurent

Connectives of linear logic are sometimes classified as canonical or not. This refers to the possibility (or not) to characterise a connective (up to logical equivalence) by means of its introduction rules. The standard claim is that all linear-logic connectives, but the exponential ones, are canonical.

We want to stress that this claim strongly depends, not only on linear logic itself, but on the way rules are constructed. This means in particular that canonicity is not an intrinsic property of connectives but depends on how they are presented: canonicity is not canonical…

Canonicity of Linear Connectives in the Literature

Linear logic [1] is known to be a logic with a lot of connectives. Propositional linear connectives are classified into three families: multiplicative (\otimes, \parr, \multimap, 1, \bot), additive (\with, \oplus, \top, 0) and exponential ({\oc}, {\wn}) connectives. The exponential ones are often presented as less canonical (discussion and formal definition provided later) than the others. One can find various comments in the linear logic literature going in that direction.

Here are some of them:

As is well known, the sequent calculus rules for the exponentials, unlike those for the other connectives, do not imply their uniqueness modulo linear equivalence: if we introduce a unary connective {\oc}', with the same rules as the exponential {\oc}, then neither \oc A\multimap \oc' A or \oc' A \multimap \oc A are derivable.DJS93, page 128

Girard has pointed out that the exponential connectives or modalities, {\oc} and {\wn}, unlike the other connectives, are not determined by the axioms of linear logic. More precisely, if one added to linear logic a second pair of modalities, say {\oc}' and {\wn}', subject to the same rules of inference as the original pair, then one could not deduce that the new modalities are equivalent to the old.Bla95, page 80

Even if we fix the inference rules for the exponentials, as in standard linear logic, the rules do not describe unique exponentials. If one gives a red tensor and a blue tensor the same inference rules, then one can prove that these two tensors are, in fact, equivalent. All of linear logic connectives except the exponentials yield similar theorems.BM07, page 93

More precisely, if we add to the language of linear logic two more operators, {\oc}' and {\wn}', and postulate of them the same rules as for {\oc} and {\wn}, we cannot prove that \oc A \multimapboth \oc' A and \wn A \multimapboth \wn' A. In contrast, if we introduce {\with}', {\bot}', etc, we can prove that the new operators are equivalent to the old ones.nLab wiki, linear logic

One interesting aspect of the exponentials is that they are not canonical: if we introduce copies of the exponentials, say {\oc}', {\wn}' satisfying the same respective laws as {\oc}, {\wn}, we cannot prove that necessarily {\oc} = {\oc}' and {\wn} = {\wn}' on this basis alone (see Section 6.1 of [2]). This is in stark contrast with the multiplicative and additive connectives, which are indeed canonical in this way.this blog
Show more
Show less

They are mostly correct because they (sometimes implicitly) rely on Girard’s sequent calculus rules for linear logic. Nevertheless such statements often lead to a common belief that this (non-) canonicity properties are an intrinsic property of linear logic connectives. We will discuss what happens with different presentations of the logic leading to the conclusion that canonicity depends on the presentation, not only on the logic itself.

Defining Canonicity of Connectives

Following the quotations above, here is a proposal definition for canonicity of connectives:

Definition. (Canonical Connective) A connective \star is canonical if, whenever we consider two copies \textcolor{red}{\star} and \textcolor{blue}{\star} with the same rules as \star, we can prove \textcolor{red}{\star} and \textcolor{blue}{\star} to be logically equivalent.

It is important to notice that, by relying on what are the rules, this notion has no reason to be invariant when moving from a proof calculus to another.

We will focus on intuitionistic linear Logic [3] restricted to the connectives {\otimes}, 1, {\multimap}, {\with}, \top, {\oc} as it is sufficient for our discussion and slightly simpler for the presentation of some systems. Things are very similar in classical linear logic.

Traditional Sequents

We consider here Girard-Lafont’s sequent calculus [3] for intuitionistic linear logic based on sequents \Gamma \vdash A with \Gamma a list of formulas and A a formula.

    \begin{gather*}\inferrule*[rightstyle=\sf,right=ax]{~}{A \vdash A} \qquad\qquad \inferrule*[rightstyle=\sf,right=cut]{\Gamma \vdash A \\ \Delta, A \vdash C}{\Gamma, \Delta \vdash C}\qquad\qquad \inferrule*[rightstyle=\sf,right=ex]{\Gamma, A, B, \Delta \vdash C}{\Gamma, B, A, \Delta \vdash C} \\ \inferrule*[rightstyle=\sf,right=$\otimes$\textsc{r}]{\Gamma \vdash A \\ \Delta \vdash B}{\Gamma, \Delta \vdash A \otimes B} \qquad\qquad \inferrule*[rightstyle=\sf,right=$\otimes$\textsc{l}]{\Gamma, A, B \vdash C}{\Gamma, A \otimes B \vdash C} \qquad\qquad \inferrule*[rightstyle=\sf,right=$1$\textsc{r}]{~}{{} \vdash 1} \qquad\qquad \inferrule*[rightstyle=\sf,right=$1$\textsc{l}]{\Gamma \vdash C}{\Gamma, 1 \vdash C} \\ \inferrule*[rightstyle=\sf,right=$\multimap$\textsc{r}]{\Gamma, A \vdash B}{\Gamma \vdash A \multimap B} \qquad\qquad \inferrule*[rightstyle=\sf,right=$\multimap$\textsc{l}]{\Gamma \vdash A \\ \Delta, B \vdash C}{\Gamma, \Delta, A \multimap B \vdash C} \\ \inferrule*[rightstyle=\sf,right=$\with$\textsc{r}]{\Gamma \vdash A \\ \Gamma \vdash B}{\Gamma \vdash A \with B} \qquad\quad \inferrule*[rightstyle=\sf,right=$\with_1$\textsc{l}]{\Gamma, A \vdash C}{\Gamma, A \with B \vdash C} \qquad \inferrule*[rightstyle=\sf,right=$\with_2$\textsc{l}]{\Gamma, B \vdash C}{\Gamma, A \with B \vdash C} \qquad\quad \inferrule*[rightstyle=\sf,right=$\top$\textsc{r}]{~}{\Gamma \vdash \top} \\ \inferrule*[rightstyle=\sf,right=$\oc$\textsc{r}]{\oc\Gamma \vdash A}{\oc\Gamma \vdash \oc A} \qquad\qquad \inferrule*[rightstyle=\sf,right=$\oc$\textsc{l}]{\Gamma, A \vdash C}{\Gamma, \oc A \vdash C} \qquad\qquad \inferrule*[rightstyle=\sf,right=$\oc c$]{\Gamma, \oc A, \oc A \vdash C}{\Gamma, \oc A \vdash C} \qquad\qquad \inferrule*[rightstyle=\sf,right=$\oc w$]{\Gamma \vdash C}{\Gamma, \oc A \vdash C} \end{gather*}

Show more
Show less

Assuming now we have two different copies of each connective, equivalences come from decorated axiom expansions:

    \begin{gather*}\inferrule*[rightstyle=\sf,right=$\textcolor{red}{\otimes}$\textsc{l}]{\inferrule*[right=$\textcolor{blue}{\otimes}$\textsc{r}]{\inferrule*[rightstyle=\sf,right=ax]{~}{A \vdash A} \\ \inferrule*[rightstyle=\sf,right=ax]{~}{B \vdash B}}{A, B \vdash A \mathbin{\textcolor{blue}{\otimes}} B}}{A \mathbin{\textcolor{red}{\otimes}} B \vdash A \mathbin{\textcolor{blue}{\otimes}} B} \quad \inferrule*[rightstyle=\sf,right=$\textcolor{red}{1}$\textsc{l}]{\inferrule*[right=$\textcolor{blue}{1}$\textsc{r}]{~}{{}\vdash \textcolor{blue}{1}}}{\textcolor{red}{1} \vdash \textcolor{blue}{1}} \qquad \inferrule*[rightstyle=\sf,right=$\textcolor{blue}{\multimap}$\textsc{r}]{\inferrule*[right=ex]{\inferrule*[right=$\textcolor{red}{\multimap}$\textsc{l}]{\inferrule*[rightstyle=\sf,right=ax]{~}{A \vdash A} \\ \inferrule*[rightstyle=\sf,right=ax]{~}{B \vdash B}}{A, A \mathbin{\textcolor{red}{\multimap}} B \vdash B}}{A \mathbin{\textcolor{red}{\multimap}} B, A \vdash B}}{A \mathbin{\textcolor{red}{\multimap}} B \vdash A \mathbin{\textcolor{blue}{\multimap}} B}\\ \inferrule*[right=$\textcolor{blue}{\with}$\textsc{r}]{\inferrule*[right=$\textcolor{red}{\with}_1$\textsc{l}]{\inferrule*[rightstyle=\sf,right=ax]{~}{A \vdash A}}{A \mathbin{\textcolor{red}{\with}} B \vdash A} \\ \inferrule*[right=$\textcolor{red}{\with}_2$\textsc{l}]{\inferrule*[rightstyle=\sf,right=ax]{~}{B \vdash B}}{A \mathbin{\textcolor{red}{\with}} B \vdash B}}{A \mathbin{\textcolor{red}{\with}} B \vdash A \mathbin{\textcolor{blue}{\with}} B} \qquad \inferrule*[rightstyle=\sf,right=$\textcolor{blue}{\top}$\textsc{r}]{~}{\textcolor{red}{\top} \vdash \textcolor{blue}{\top}}\end{gather*}

By also considering the dual proofs which swap red and blue, we get \textcolor{red}{\otimes} \dashv\vdash \textcolor{blue}{\otimes}, \textcolor{red}{\with} \dashv\vdash \textcolor{blue}{\with}, etc. So that multiplicative and additive connectives are proved to be canonical. However, because of the contextual constraint in the ({\oc}\textsc{r}) rule, it is not possible to prove \textcolor{red}{\oc} \dashv\vdash \textcolor{blue}{\oc}:

    \[\mprset{fraction={\cdot\cdots\cdot}}\inferrule*[rightstyle=\sf,right=$\textcolor{blue}{\oc}$\textsc{r}]{\mprset{fraction={---}}\inferrule*[rightstyle=\sf,right=$\textcolor{red}{\oc}$\textsc{l}]{\inferrule*[rightstyle=\sf,right=ax]{~}{A \vdash A}}{\mathord{\textcolor{red}{\oc}}A \vdash A}}{\mathord{\textcolor{red}{\oc}}A \vdash \mathord{\textcolor{blue}{\oc}}A}\]

since the dotted rule application is not valid as it violates the condition on the context required to contain formulas starting with \textcolor{blue}{\oc} only.

One can interpret the situation by saying that, in Girard-Lafont’s sequent calculus, the multiplicative connectives are canonical because there is a single (black) “,” representing them at the sequent level. Exponential connectives are not canonical because they rely on the contextual ({\oc}\textsc{r}) rule fixing the copy of {\oc} under consideration.

This means canonicity is partly driven by how connectives are dissolved into the sequent structure when reading rules bottom-up. From this remark, one can see that everything changes if we modify the structure of sequents as it happens with Andreoli’s dyadic sequents or with bunches.

Dyadic Sequents

In the context of proof-search, Andreoli [4] introduced alternative sequent calculi for linear logic. The status of canonical connectives happens to be different there. We consider only the dyadic case as it is sufficient for our purpose, and adapt it to intuitionistic linear logic. Dyadic intuitionistic sequents have the shape: \Gamma \mid \Delta \vdash A, with the property that such a sequent is provable if and only if \oc\Gamma, \Delta \vdash A is provable in Girard-Lafont’s system.

Let us focus on the exponential connectives. The dyadic axiom and exponential rules are:

    \[\inferrule*[rightstyle=\sf,right=ax]{~}{\Gamma \mid A \vdash A} \qquad\qquad \inferrule*[rightstyle=\sf,right=sel]{\Gamma, A \mid A, \Delta \vdash C}{\Gamma, A \mid \Delta \vdash C} \qquad\qquad \inferrule*[rightstyle=\sf,right=$\oc$\textsc{r}]{\Gamma \mid {} \vdash A}{\Gamma \mid {} \vdash \oc A} \qquad\qquad \inferrule*[rightstyle=\sf,right=$\oc$\textsc{l}]{\Gamma, A \mid \Delta \vdash C}{\Gamma \mid \oc A, \Delta \vdash C}\]

Now by considering two copies of {\oc}, we get:

    \[\inferrule*[rightstyle=\sf,right=$\textcolor{red}{\oc}$\textsc{l}]{\inferrule*[rightstyle=\sf,right=$\textcolor{blue}{\oc}$\textsc{r}]{\inferrule*[rightstyle=\sf,right=sel]{\inferrule*[rightstyle=\sf,right=ax]{~}{A \mid A \vdash A}}{A \mid {} \vdash A}}{A \mid {} \vdash \mathord{\textcolor{blue}{\oc}}A}}{{} \mid \mathord{\textcolor{red}{\oc}}A \vdash \mathord{\textcolor{blue}{\oc}}A}\]

so that \textcolor{red}{\oc} \dashv\vdash \textcolor{blue}{\oc}, i.e. the exponential connective {\oc} is canonical. The reason for that is that we have only one (black) “{\mid}” and the ({\oc}\textsc{r}) rule does not rely any more on the explicit mention of other occurrences of connectives in the context.

Bunched Sequents

Defining contexts in sequents as lists was imposing a single notion of “,”. If we follow the theory of bunched implication logic [5, 6], we can generalise lists to binary trees. We consider here the multiplicative fragment of bunched implication logic only.

A bunch is a binary tree with leaves which are either formulas or an empty bunch \{\}:

    \[ \Xi ::= A \mid \{\} \mid (\Xi, \Xi) \]

They are equipped with the congruence {\equiv} generated by the structure of a commutative monoid:

    \[(\Xi_1, (\Xi_2, \Xi_3)) \equiv ((\Xi_1, \Xi_2), \Xi_3) \qquad\qquad (\Xi, \{\}) \equiv \Xi \qquad\qquad (\Xi_1, \Xi_2) \equiv (\Xi_2, \Xi_1) \]

If \Theta is a bunch context (i.e. a bunch with a hole amongst its leaves), we use the notation \Theta[\Xi] for the bunch obtained by filing the hole of \Theta with the bunch \Xi. The relation \equiv being a congruence, we can deduce \Theta[\Xi_1] \equiv \Theta[\Xi_2] from \Xi_1 \equiv \Xi_2.

In this bunch-style presentation of intuitionistic linear logic, sequents have the shape \Xi \vdash A where \Xi is a bunch and A is a formula:

    \[ \inferrule*[rightstyle=\sf,right=$\otimes$\textsc{r}]{\Xi_1 \vdash A \\ \Xi_2 \vdash B}{(\Xi_1, \Xi_2) \vdash A \otimes B} \qquad\qquad \inferrule*[rightstyle=\sf,right=$\otimes$\textsc{l}]{\Theta[(A, B)] \vdash C}{\Theta[A \otimes B] \vdash C} \]

    \begin{gather*}\inferrule*[rightstyle=\sf,right=ax]{~}{A \vdash A} \qquad\qquad \inferrule*[rightstyle=\sf,right=cut]{\Xi \vdash A \\ \Theta[A] \vdash C}{\Theta[\Xi] \vdash C}\qquad\qquad \inferrule*[rightstyle=\sf,right=$\equiv$]{\Xi \vdash C \\ \Xi \equiv \Xi'}{\Xi' \vdash C} \\ \inferrule*[rightstyle=\sf,right=$1$\textsc{r}]{~}{\{\} \vdash 1} \qquad \inferrule*[rightstyle=\sf,right=$1$\textsc{l}]{\Theta[\{\}] \vdash C}{\Theta[1] \vdash C} \qquad\qquad \inferrule*[rightstyle=\sf,right=$\multimap$\textsc{r}]{(\Xi, A) \vdash B}{\Xi \vdash A \multimap B} \qquad \inferrule*[rightstyle=\sf,right=$\multimap$\textsc{l}]{\Xi \vdash A \\ \Theta[B] \vdash C}{\Theta[(\Xi, A \multimap B)] \vdash C} \end{gather*}

Show more
Show less

Assume now, we consider two copies of {\otimes}, but also two associated copies of “,” (and \{\}) in the construction of bunches:

    \[ \Xi ::= A \mid \textcolor{blue}{\{\}} \mid \textcolor{blue}{(}\Xi\textcolor{blue}{,} \Xi\textcolor{blue}{)} \mid \textcolor{red}{\{\}} \mid \textcolor{red}{(}\Xi\textcolor{red}{,} \Xi\textcolor{red}{)} \]

then it is not possible any more to prove \textcolor{red}{\otimes} \vdash \textcolor{blue}{\otimes}:

    \[ \inferrule*[rightstyle=\sf,right=$\textcolor{red}{\otimes}$\textsc{l}]{\mprset{fraction={\cdot\cdots\cdot}}\inferrule*[right=$\textcolor{blue}{\otimes}$\textsc{r}]{\mprset{fraction={---}}\inferrule*[rightstyle=\sf,right=ax]{~}{A \vdash A} \\ \mprset{fraction={---}}\inferrule*[rightstyle=\sf,right=ax]{~}{B \vdash B}}{\textcolor{red}{(}A\textcolor{red}{,} B\textcolor{red}{)} \vdash A \mathbin{\textcolor{blue}{\otimes}} B}}{A \mathbin{\textcolor{red}{\otimes}} B \vdash A \mathbin{\textcolor{blue}{\otimes}} B} \]

since the dotted rule application is not valid as it violates the condition on the context required to be of the shape \textcolor{blue}{(}\Xi_1\textcolor{blue}{,} \Xi_2\textcolor{blue}{)}.

The situation is similar in, for example, calculus of structure presentations of linear logic [7].

Concluding with some Semantics

Moving to more semantic arguments, it is often used in the literature that, in a given denotational model of the multiplicative-additive fragment of linear logic, it may be possible to define multiple interpretations of the exponential connectives. This is in particular the case in coherent spaces [1] which have both a set-based exponential construction (the finitary one) and a multiset-based exponential construction (the free one). This is arguing for the non-canonicity of exponential connectives.

But already at the level of the multiplicative structure, there is no uniqueness. Given a category, there may be multiple monoidal or even *-autonomous structures on it.

The situation is however different for the additive connectives which correspond to product/co-product constructions thus, because they satisfy a universal property, are unique up to unique isomorphism.

Navigating through various ways of presenting the connectives of linear logic, we have seen that only the additive connectives really appear to be canonical by remaining canonical even when the rules are presented differently.

If rules are fixed, that is for a given presentation of the logic, more connectives may become canonical. This is what happens in Girard’s sequent calculus for classical linear logic and for Girard-Lafont’s sequent calculus for intuitionistic linear logic. Together with the additive connectives, the multiplicative ones become canonical in this particular system, while exponential connectives are not.

To sum up, if canonicity is considered globally with respect to the logic (i.e. independently from its presentations), only the additive connective should really be considered canonical. In the more local framework of a fixed particular proof system, more connectives may appear canonical (as it is the case for the multiplicative ones in the standard sequent calculus).

References

[1] [doi] J. Girard, “Linear logic,” Theoretical Computer Science, vol. 50, p. 1–102, 1987.
[Bibtex]
@Article{ll,
author = {Jean-Yves Girard},
title = {Linear logic},
journal = {Theoretical Computer Science},
volume = {50},
pages = {1--102},
year = {1987},
doi = {10.1016/0304-3975(87)90045-4}
}
[2] R. Di Cosmo and D. Miller, “Linear Logic,” in The Stanford Encyclopedia of Philosophy, E. N. Zalta and U. Nodelman, Eds., Metaphysics Research Lab, Stanford University, 2023.
[Bibtex]
@InCollection{llstanford,
author = {Di Cosmo, Roberto and Dale Miller},
title = {Linear Logic},
booktitle = {The {Stanford} Encyclopedia of Philosophy},
editor = {Edward N. Zalta and Uri Nodelman},
publisher = {Metaphysics Research Lab, Stanford University},
year = {2023},
url = {https://plato.stanford.edu/entries/logic-linear/}
}
[3] [doi] J. Girard and Y. Lafont, “Linear Logic and Lazy Computation,” in Proceedings of the International Joint Conference on Theory and Practice of Software Development (TAPSOFT’87), 1987, p. 52–66.
[Bibtex]
@InProceedings{lllazy,
author = {Jean-Yves Girard and Yves Lafont},
title = {Linear Logic and Lazy Computation},
booktitle = {Proceedings of the International Joint Conference on Theory and Practice of Software Development (TAPSOFT'87)},
editor = {Hartmut Ehrig and Robert Kowalski and Giorgio Levi and Ugo Montanari},
series = {Lecture Notes in Computer Science},
volume = {250},
pages = {52--66},
publisher = {Springer},
year = {1987},
doi = {10.1007/BFb0014972}
}
[4] [doi] J. Andreoli, “Logic Programming with Focusing Proofs in Linear Logic,” Journal of Logic and Computation, vol. 2, iss. 3, p. 297–347, 1992.
[Bibtex]
@Article{focusing,
author = {Jean-Marc Andreoli},
title = {Logic Programming with Focusing Proofs in Linear Logic},
journal = {Journal of Logic and Computation},
volume = {2},
number = {3},
pages = {297--347},
year = {1992},
doi = {10.1093/logcom/2.3.297}
}
[5] [doi] P. O’Hearn and D. Pym, “The Logic of Bunched Implications,” Bulletin of Symbolic Logic, vol. 5, iss. 2, p. 215–244, 1999.
[Bibtex]
@Article{bi,
author = {Peter O'Hearn and David Pym},
title = {The Logic of Bunched Implications},
journal = {Bulletin of Symbolic Logic},
volume = {5},
number = {2},
pages = {215--244},
month = jun,
year = {1999},
doi = {10.2307/421090}
}
[6] [doi] D. Pym, “Propositional BI as a Sequent Calculus,” in The Semantics and Proof Theory of the Logic of Bunched Implications, Springer, 2002, vol. 26, p. 89–95.
[Bibtex]
@InBook{lbi,
author = {David Pym},
title = {Propositional BI as a Sequent Calculus},
booktitle = {The Semantics and Proof Theory of the Logic of Bunched Implications},
series = {Applied Logic Series},
volume = {26},
publisher = {Springer},
pages = {89--95},
year = {2002},
doi = {10.1007/978-94-017-0091-7_6}
}
[7] [doi] L. Straßburger, “MELL in the Calculus of Structures,” Theoretical Computer Science, vol. 309, iss. 1–3, p. 213–285, 2003.
[Bibtex]
@Article{mellcos,
author = {Lutz Stra{\ss}burger},
title = {{MELL} in the Calculus of Structures},
journal = {Theoretical Computer Science},
volume = {309},
number = {1--3},
pages = {213--285},
year = {2003},
doi = {10.1016/S0304-3975(03)00240-8}
}

6 thoughts on “On the Canonicity of Linear Logic Connectives”

  1. Interesting. Maybe this is what you are hinting at in the final two paragraphs, but I feel that canonicity (of a particular connective) is given with respect to other connectives (or other structure present in sequents). Like if you have blue and blue* linear implication, formulated with respect to blue bunches, presumably they are equivalent (adjoints are unique up to unique iso).

    Reply

    1. Dear Sam, thanks for your feedback.
      Indeed, my point is that canonicity should better be considered with respect to some given context/constraints which may sometimes be “hidden” in the structure of sequents.
      The categorical analysis for example helps being more explicit on what is fixed or not. In this approach, the additive connectives are canonical without any particular hypothesis. Fixing the tensor product decides for the tensor unit and the linear implication as you mention. Once the multiplicative structure is fixed, the free ! (if it exists) is imposed, but distinct non-free ones can still be considered.

      Reply

      1. Thanks for the interesting post, to piggy back off Sam’s question, I wonder if the following makes sense:
        – Structurally, the bare minimum to interpret the Girard-Lafont sequent calculus seems to be a multicategory. I don’t know, but assume, the structure needed to interpret the additive and multiplicative structure in a multicategory can be characterised by universal properties of multicategories. The exponentials are not characterised by a universal property even in this setting so they are not canonical.
        – For Andreoli’s dyadic sequents, we need more than a multicategory since we have two contexts. So then we ask for some multicategory with extra structure, where now exponentials can be characterised by a universal property (ideally in a more interesting way than imposing the ! as structure of course).
        – For bunched sequents the bare minimum is then some alternative to a multicategory where now not even the multiplicative structure can be characterised by a universal property?
        Does this sound sensible, I would be interested in what might be some sufficiently general semantic setting to consider these and possibly more systems. This is quite far from my expertise, maybe there is already something of this flavour in the literature?

        Reply

        1. Hello Bruno, what you say makes sense to me, while moving a bit out of my expertise as well.
          Could it be that a framework for interpreting these intuitionistic sequent calculi would be generalised multicategories w.r.t some cartesian monad B on Set?
          In the case of traditional intuitionistic sequents, one could use `List’ for B and get multicategories as you suggest.
          In the case of bunched sequents, while I was playing with different notions of bunches, one should first fix one. Then in the single-colour case above, for example, B could be `Binary Trees’.
          In the case of dyadic sequents, things would probably be a bit more involved to deal with the context constraint on the (!R) rule.

          Reply

  2. It is great to see this point made so clearly: canonicity is framework-dependent.  

    In proof theory, establishing a canonical treatment of a logic or a specific logical feature is a central concern. Olivier’s note illustrates how the design of a proof system directly influences the study of that concern.

    However, from the perspective of applying proof theory to the specification of computation, non-canonical features are a bonanza, particularly when the underlying framework offers deep meta-theoretic results, such as cut-elimination and focusing theorems. When we fix our framework to be Gentzen’s sequent calculus, at least two logical features are notably non-canonical:

    1. First-order quantification: The domain of quantification is not fixed canonically. Consequently, first-order logic can be multisorted and applied across diverse domains, including lists, trees, and numbers.

    2. Linear logic exponentials: Because the exponentials are not canonical, subexponentials arise as one natural manifestation of this flexibility.

    If we shift the framework to the Andreoli-style focusing enhancement of sequent calculus, we find that the assignment of polarity to atomic formulas and certain logical connectives is not established canonically by that framework.

    These three features—first-order quantification, subexponentials, and polarity assignment—are available within sequent calculi that possess strong meta-theoretic properties. Such frameworks are highly appealing for writing computational specifications, since each non-canonical feature introduces a new dimension to the role logic plays in specifying computation. For instance, varying polarizations allows one to toggle a proof’s behavior between forward and backward chaining, or between call-by-name and call-by-value evaluation strategies.

    Vivek Nigam’s 2007 PhD thesis, “Exploiting non-canonicity in the sequent calculus” (https://theses.hal.science/pastel-00005487/), developed this theme extensively within proof-search-style logical specifications of computations.

    Reply

Leave a Reply

Your email address will not be published. Required fields are marked *