Proving Negation Identity in Intuitionistic Linear Logic

Question

In a Gentzen system (i.e. sequent calculus) for Intuitionistic Linear Logic (from now, ILL), given the usual rules for ILL ($\wedge L, \wedge R, \circ L, etc.$), I want to prove that the Identity $A \vdash A$ may be proved from the instances of identity using atomic propositions alone.

It follows a proof on the complexity of formulas. For $Conjunction$ we have:

$\quad A\vdash A \qquad B\vdash B $

$———————————— \; [\wedge L] $

$A\wedge B\vdash B\qquad A\wedge B\vdash B $

$ ———————————— \; [\wedge R] $

$ \qquad A\wedge B\vdash A\wedge B$

The rules for $Negation$ are the following two:

$ X \vdash A$

$ ———————————— \; [\neg L] $

$ X; \neg A \vdash $

$\;$

$ X; A \vdash $

$ ———————————— \; [\neg R] $

$ X \vdash \neg A $

So, my proof (and my problem) in this case is:

$\;$

$ A \vdash A$

$ ———————————— \; [\neg L] $

$ A; \neg A \vdash $

$ ———————————— \; [??] $

$\neg A; A \vdash $

$ ———————————— \; [\neg R] $

$ \neg A \vdash \neg A $

$\;$

Where I put the question marks is the line that I find problematic. Am I allowed to assume some sort of structural commutativity or exchange in ILL?

Thanks.

Answer 1

Linear logic does still have the exchange rule. Without the specific rules of your system, I can't tell you how this is manifest. It may simply have an Exchange rule, or it may implicitly support exchange by having the context be a finite multi-set. Exchange may also be a derived rule from some other collection of rules. However, unless you are working with a strange presentation, it's likely that the structural rules are kept separate from the rules for the connectives, so you probably don't need to involve the connectives to derive Exchange.