Is it possible to define a negation in intuitionistic linear logic, the way one does in intuitionistic logic, i.e. $A^{\bot} \equiv A \multimap \mathbf{0}$ (or, as it would be written in intuitionistic logic, $\neg A \equiv A \to \bot$)?

While I can prove, e.g. the theorem... $$A^{\bot\bot}\otimes B^{\bot\bot}\vdash(A\otimes B)^{\bot\bot}$$

...I cannot prove... $$(A\otimes B)^{\bot\bot}\vdash A^{\bot\bot}\otimes B^{\bot\bot}$$

...without copying the assumption $(A\otimes B)^{\bot\bot}$ to both subproofs $A^{\bot\bot}$ and $B^{\bot\bot}$. Even though I end up only using the $A$ and $B$ parts once, I still have to copy the assumption.

Edit: For completeness' sake, the system I'm using is the one introduced in Philip Wadler's, A Taste of Linear Logic.

Edit: Just to make sure, I checked, and $(A\otimes B)^{\bot\bot}\equiv A^{\bot\bot}\otimes B^{\bot\bot}$ is a theorem of linear logic under the axiomatisation on the Stanford Encyclopedia of Philosophy (as it should be).

Edit: Sequent Calculi for Intuitionistic Linear Logic with Strong Negation by Norihiro Kamide seems to be a relevant publication.

  • $\begingroup$ $\multimap$? I have not seen this befor. What does it do? $\endgroup$ – Conor O'Brien May 20 '15 at 11:19
  • $\begingroup$ @CᴏɴᴏʀO'Bʀɪᴇɴ Can't say exactly, but it stands for implication in a relevant logic (where for example $A \to (B \to A)$ is not valid) $\endgroup$ – Stefan Perko May 27 '15 at 16:27
  • $\begingroup$ It stands (in this case) for implication in linear logic. The idea is that you have to use every argument of the implication exactly once, meaning that the theorem mentioned by Stefan isn't valid, and neither is $A \to (A\wedge A)$. $\endgroup$ – wen May 27 '15 at 22:02

This is a late answer, but you made some good observations. Negation can be defined in intuitionistic linear logic, but it doesn't satisfy all of the properties of either classical linear negation or intuitionistic non-linear negation – that doesn't mean it's a bad definition! The definition you gave ($\neg A := A \multimap 0$) is fine, but an even better one is $$\neg A := A \multimap p$$ where $p$ is a fixed, atomic formula not appearing in $A$. (The main difference between these two definitions is that your definition validates ex falso quod libet (also called the principle of explosion) $A \otimes \neg A \vdash B$ for generic formulas $B$, while the other definition doesn't.) In any case, with either definition, one can prove double-negation introduction $$ A \vdash \neg\neg A $$ but not double-negation elimination (even though it is valid classically), and likewise one can prove the distributivity law $$ \neg \neg A \otimes \neg\neg B \vdash \neg\neg(A \otimes B) $$ but not the reverse entailment (even though it is valid intuitionistically). (There are actually two distinct, canonical ways of proving $\neg \neg A \otimes \neg\neg B \vdash \neg\neg(A \otimes B)$. Can you spot them?)

The fragment of intuitionistic linear logic consisting of just tensor ($\otimes$) and negation ($\neg$) has a surprisingly rich structure – Paul-André Melliès calls this fragment "tensorial logic" and has written a lot about it (e.g., see his paper with Nicolas Tabareau, Resource modalities in tensor logic). In particular, there is a good motivation for studying such a weak form of negation that comes from the theory of programming languages: $\neg A$ is precisely the type of linear continuations.

  • $\begingroup$ I'm not sure how your definition of $\neg$ would apply in the case $\neg\neg A$. I can get to $\neg(A\multimap p)$ easily, but to unfold the outer negation it looks like I would need to deviate either from your specification that $p$ is "fixed" or from the specification that it doesn't appear in the formula to be negated... $\endgroup$ – Henning Makholm Sep 23 '18 at 1:10

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.