I am currently going through some papers that use the "intuitionistic version" of Girard's Linear Logic. The problem is that I seem to find very little literature on it. There is a lot done on Linear Logic but I specifically wanted some introduction to its intuitionistic version (why did it come up, historical context, etc.). Any recommendations would be helpful!
$\begingroup$ $\endgroup$
4 
- $\begingroup$ Sílvia? xD${{}}$ $\endgroup$Git Gud– Git Gud2014-04-11 16:02:33 +00:00Commented Apr 11, 2014 at 16:02
- $\begingroup$ indeed! do i know you...? $\endgroup$essay– essay2014-04-11 19:00:11 +00:00Commented Apr 11, 2014 at 19:00
- $\begingroup$ Doesn't my nickname ring a bell? ^_^ Hint: I played chess today. $\endgroup$Git Gud– Git Gud2014-04-11 19:17:11 +00:00Commented Apr 11, 2014 at 19:17
- $\begingroup$ ha, i know who you are! (sorry about the delay. and about your chess game :P) but i am clueless about your nickname anyway... $\endgroup$essay– essay2014-04-17 13:04:39 +00:00Commented Apr 17, 2014 at 13:04
Add a comment |
2 Answers
$\begingroup$ $\endgroup$
See Jean-Yves Girard, Linear Logic (1987) and A.S.Troelstra, Lectures on Linear Logic (1992).
See also in SEP the entry on Linear Logic.
$\begingroup$ $\endgroup$
As I understand the article in the Stanford Encyclopedia of Philosophy, the link given in the answer of Mauro, the "intuitionistic" aspect is derived from a way of writing sequents. Intuitionistic logic was derived from classical logic (when using sequents) by limiting "conclusions" to one single conclusion per sequent.
Gentzen's sequent calculus proof system for intuitionistic logic was the result of restricting his sequent calculus for classical logic so that all sequents contained at most one formula on the right-hand side of sequents (Gentzen 1935). Such a single-conclusion restriction can also be explored in the context of linear logic
As a non-expert on that matter, this article confuses me at some points, especially the sentence which claims A⊕¬A would not be provable.
The paper "Around Classical and Intuitionistic Linear Logics" by Olivier Laurent is pretty clear about this distinction in the introduction.
Personally, I find it helpful here to directly see the difference. There is a helpful script "Introduction to Linear Logic" by Torben Braüner which lists the distinct sequent formalization on page 53 to 55.
Unsurprisingly, the Intuitionistic Linear Logic removes the involutive negation (a negation "which could undo itself"), i.e. A ≢ ¬¬A. From reading the paper it seems to me, the sense of negation or impossibility is fundamentally different and it is the only (or at least main) incompatibility.
By my understanding, the paper's introduction mentions Harold Schellinx to have found that formulas without combined use of implication ⊸ and 0 have a proof in intuitionistic linear logic when there is one in classic linear logic. It also mentions that intutionstic logic could be translated into classic linear logic from (A → B) to (!A ⊸ B).
