# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorMike Shulman
• CommentTimeJun 8th 2017
• (edited Jun 8th 2017)

The cut rule for linear logic used to be stated as

If $\Gamma \vdash A$ and $A \vdash \Delta$, then $\Gamma \vdash \Delta$.

I don’t think this is general enough, so I corrected it to

If $\Gamma \vdash A, \Phi$ and $\Psi,A \vdash \Delta$, then $\Psi,\Gamma \vdash \Delta,\Phi$.

• CommentRowNumber2.
• CommentAuthorTodd_Trimble
• CommentTimeJun 8th 2017

No objection, but I guess it would depend on the precise rules. In MLL which has duals, if we have rules which allow us to derive

$\frac{\Gamma \vdash \Sigma,\Phi}{\Gamma, \Phi^\ast \vdash \Sigma}, \qquad \frac{\Psi, \Sigma \vdash \Delta}{\Psi \vdash \Delta, \Sigma^\ast}$

where $\Phi^\ast$ is the list of duals of formulas of $\Phi$, and $A^{\ast\ast} = A$, I thought we would be able to derive your more general cut rule from the more specific cut rule:

$\array{ \arrayopts{\rowlines{solid}} \Gamma \vdash A, \Phi\;\;\;\;\;\;\;\;\; \Psi, A \vdash \Delta \\ \Gamma, \Phi^\ast \vdash A \;\;\;\;\;\;\;\;\; A \vdash \Psi^\ast, \Delta \\ \Gamma, \Phi^\ast \vdash \Psi^\ast, \Delta \\ \Psi, \Gamma \vdash \Delta, \Phi }$
• CommentRowNumber3.
• CommentAuthorMike Shulman
• CommentTimeJun 8th 2017

Yes, you’re right. But I think it’s better to formulate the rule in a way that remains correct in fragments without involutive negation.

• CommentRowNumber4.
• CommentAuthorTodd_Trimble
• CommentTimeJun 8th 2017

Understood (and agreed); I was just explaining the likely reason the original form was the way it was (I’m guessing I wrote that).

• CommentRowNumber5.
• CommentAuthorTobyBartels
• CommentTimeSep 10th 2018

Confirm that the game semantics presented here is the same as Blass's. (I still haven't actually read Blass 1992, yet, but I read a 1994 paper by Blass that summarizes the 1992 semantics.)

• CommentRowNumber6.
• CommentTimeMar 23rd 2019

Added differential linear logic to variants, included a reference to the paper introducing differential categories.

1. Link to game semantics article

Ammar Husain

2. Copycat example.

Ammar Husain

3. Caires, Pfenning

Ammar Husain

• CommentRowNumber10.
• CommentAuthorMike Shulman
• CommentTimeNov 12th 2019

• CommentRowNumber11.
• CommentTimeFeb 15th 2020

• CommentRowNumber12.
• CommentAuthorTobyBartels
• CommentTimeFeb 17th 2020

Mention Mike's antithesis interpretation.

• CommentRowNumber13.
• CommentAuthorMike Shulman
• CommentTimeMar 12th 2020

Thanks for adding that, Toby! I added a redirect for “antithesis interpretation” to this page, since you created a link to that from join. We could eventually have a separate page about it, but for now this is the best target of such a link.