Is Girard's LU just an embedding of classical and intuitionistic logic into linear logic?

Question

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?

Answer 1

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!).