10
$\begingroup$

This question is about Girard's system LU, presented in his paper On the unity of logic. Girard starts by giving a "modal" sequent calculus with two zones of both hypotheses and consequents, $\Gamma;\Gamma'\vdash \Delta';\Delta$, of which $\Gamma'$ and $\Delta'$ are treated classically (with contraction and weakening) and $\Gamma$ and $\Delta$ are treated linearly (without contraction and weakening). He gives rules in this calculus for the usual connectives $\otimes,\oplus,\&,⅋,\neg,\multimap,!,?,\bigwedge,\bigvee$ of classical linear logic, and explains how the result is bi-interpretable with ordinary classical linear logic. At this point it seems clear that he has just given a different presentation of the "same" classical linear logic.

Then he introduces new "chimeric" connectives $\wedge,\vee,\Rightarrow,\supset,\forall,\exists$. It appears as though each of these connectives is defined in terms of the linear ones, although not by a uniform definition but rather by a case analysis on whether the input formulas are "positive, negative, or neutral". For instance, $A\wedge B$ is $A\otimes B$ if $A$ and $B$ are both positive, but it is $A\& B$ if $A$ and $B$ are both negative, while if $A$ is positive and $B$ is negative then $A\wedge B$ is $A\otimes !B$, and so on. He gives explicit rules for these new connectives as well, but a brief perusal of these rules suggests to me that they are derived from the definitions of the new connectives in terms of the linear ones. Finally he considers several fragments of the resulting system that embed classical and intuitionistic nonlinear logics: classical logic uses $\wedge,\vee,\neg,\Rightarrow,\forall,\exists$ while intuitionistic logic uses $\wedge,\vee,\supset,\bigvee,\exists$.

It seems to me, therefore that LU is just a rephrasing of linear logic together with new embeddings of classical and intuitionistic logic into it that are defined by case analysis on the polarity of formulas rather than "uniformly" as the more common embeddings are. (This "just" is not meant to be disparaging; I find LU very interesting, I'm just trying to understand it better.) But Girard doesn't seem to view it this way; and moreover in Vauzeilles's proof of cut-elimination for LU it takes $3\frac12$ extra pages to extend the result to the chimeric connectives, which doesn't seem like it would be the case if they were simply defined in terms of the linear ones. So I must be missing something; what is it?

$\endgroup$
  • 1
    $\begingroup$ When did you turn into a logician? $\endgroup$ – Andrej Bauer Aug 7 '17 at 21:30
  • 2
    $\begingroup$ I am not familiar with the cut elimination proof, but one reason to deal with the chimeric connectives as a separate case is to make sure that cut elimination can be performed without "unfolding" them and destroying the structure of the proof tree anymore than necessary. I.e., perhaps we want the chimeric connectives to "survive" cut elimination. $\endgroup$ – Andrej Bauer Aug 7 '17 at 21:32
  • 1
    $\begingroup$ @AndrejBauer That makes some sense, I didn't think of that. (My transformation into a part-time logician has been happening gradually over the past 5 years; didn't you notice?) $\endgroup$ – Mike Shulman Aug 8 '17 at 0:56
  • $\begingroup$ Now that you mention it, the sickness has been consuming you for a while indeed. $\endgroup$ – Andrej Bauer Aug 8 '17 at 8:23
5
$\begingroup$

Sorry if my answer comes so late, maybe you already figured it out by yourself in the meantime, I hope this helps anyway.

I think the main misunderstanding is that the "non-chimeric" fragment of $\mathbf{LU}$ is almost a different presentation of linear logic, but not quite (of course it does not help that Girard calls this the linear fragment of $\mathbf{LU}$...). There is a subtle discrepancy given by the presence of polarities: in $\mathbf{LU}$, structural rules on the right (resp. on the left) are allowed for every negative (resp. positive) formula, including the atoms. This is justified by the fact (which Girard mentions in passing at some point) that structural rules (on the right) are derivable in "usual" linear logic for negative formulas, which are those defined by $$M,N ::= \bot \mathrel{|} \top \mathrel{|} M\& N \mathrel{|} M⅋N \mathrel{|} \forall x.N \mathrel{|} ?A,$$ where $A$ is an arbitrary formula. The generalized promotion rule $$\frac{\vdash\mathcal N,A}{\vdash\mathcal N,!A}.$$ is also derivable when $\mathcal N$ is composed of negative formulas only. There are now two observations to make:

  • the negative formulas defined above do not contain atoms, so $\mathbf{LU}$ goes slightly beyond linear logic in that respect. Indeed, "usual" linear logic really corresponds to the linear fragment of $\mathbf{LU}$ restricted to neutral atoms. Unfortunately, Girard fails to mention this subtlety.

  • The structural rules and "promotion-with-negative-context" rule are derivable, but not cut-free derivable. This means that the obvious way of embedding the linear fragment of $\mathbf{LU}$ in "usual" linear logic (mapping each negative (resp. positive) atom $X$ to $?X$ (resp. $!X$)) is not "computationally transparent".

The second observation justifies the need to make sure that cut-elimination holds in $\mathbf{LU}$ as a logical system of its own (this had essentially already been pointed out by Andrej in his comment). That being done, one may study computationally meaningful embeddings of classical or intuitionistic logic in $\mathbf{LU}$, which turn out to be slightly more efficient than the ones directly in linear logic (there are less !'s and ?'s to take care of, because of the more liberal structural rules).

Such embeddings were studied more thoroughly by Olivier Laurent in his Ph.D. thesis. In particular, he defined polarized linear logic ($\mathbf{LLP}$), which is essentially the linear fragment of $\mathbf{LU}$ without neutral atoms (and, therefore, without neutral formulas in general), and showed how the $\lambda\mu$-calculus (Parigot's calculus for classical logic) may be nicely translated in it. You may look on his web page for more. Laurent's simplified system is what has been used in practice, so $\mathbf{LU}$ kind of fell into oblivion (in fact, "On the unity of logic" is one of the rare papers by Girard on linear logic which I had never read!).

$\endgroup$
  • 1
    $\begingroup$ Thanks, this is helpful! I will check out Laurent's thesis. I think Girard does mention the restriction to neutral atoms though, in the third paragraph of section 4: "This calculus is equivalent to the usual linear logic; more precisely we can translate the usual linear logic into this new system by declaring all atomic propositions to be neutral." $\endgroup$ – Mike Shulman Aug 20 '17 at 4:45
  • $\begingroup$ Ah, it had escaped me! Well, I guess that to make things completely clear, it wouldn't have hurt to add that the equivalence he is alluding to is not "computationally transparent" (the reverse translation maps cut-free LU proofs to LL proofs with cuts). To get a truly equivalent refurmulation of usual linear logic, one must restrict the linear fragment of LU to neutral atoms and forbid the "permeability rules" allowing a negative (resp. positive) formula on the right (resp. left) to pass the semicolon without "paying the price" of having a ? (resp. !) added to it. $\endgroup$ – Damiano Mazza Aug 20 '17 at 6:15
  • $\begingroup$ Right; so the overall answer, putting your points together with Andrej's, is that in terms of provability and denotation (hopefully I'm using the right words here) it's true that LU is a reformulation of classical linear logic and the chimeric connectives are defined in terms of the linear ones, but the computational / operational behavior of LU is different, which matters in particular when talking about cut-elimination theorems. $\endgroup$ – Mike Shulman Aug 20 '17 at 21:54
  • $\begingroup$ Yes! In fact, when Girard says "[t]his calculus is equivalent to the usual linear logic", he is implicitly talking about provability ($\Gamma\vdash\Delta$ is provable in LL iff $\Gamma;\vdash;\Delta$ is provable in the linear fragment of LU) and denotation (the two proofs have the same semantics in coherence spaces). And yes, I realize I forgot to mention in my answer that your understanding of chimeric connectives is absolutely correct, they are defined in terms of the linear ones, but they live in a calculus which, operationally, is not quite the same as linear logic. $\endgroup$ – Damiano Mazza Aug 21 '17 at 6:26

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.