3
$\begingroup$

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.

$\endgroup$
3
$\begingroup$

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.

$\endgroup$

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.