Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
How do I go about adding this discussion, please?
Do you mean how do you even begin to add? Or do you have questions about the details of editing? For the former, just go to the bottom of the page and click on ’edit’. There is general advice at HowTo. It’s good to give an idea of the changes back here.
By the way, thanks for the references on modal logic. One day I’ll get back to the subject.
Hi Valeria, and welcome!
I agree with what you say about linear logic, and you should always feel free to rewrite parts of any article so as to get closer to the truth. (Or, if you are not comfortable with Markdown+ITeX, feel free to ask questions or ask one of us to make changes.) Just to clarify, I don’t think anyone ’decided’ that Intuitionistic Linear Logic was somehow inferior to Classical Linear Logic; like most nLab articles, it’s simply at a rough or incomplete stage of development, written on a kind of as-needed basis, as opposed to an encyclopedia article. I think this is what sometimes confuses people.
As David says, the norm that regular contributors follow is, after making changes, to report that fact back here on the nForum, so that others know and can ask questions or make comments. Thanks for your interest!
I always felt that intuitionistic linear logic is sort of missing the point of linear logic. Classical logic is the logic of true/false facts, intuitionistic logic is the logic of verifiable truth (and therefore appropriate for mathematics overall), and (classical) linear logic is the logic of resource exchange. What is the intuitionistic fragment of linear logic the logic of?
However, this is probably my own prejudice, and I offer it only as an explanation for why the article is in the state that it is in. As you can see at the very bottom, it refers the reader to Wikipedia for ‘commonly studied fragments’. However, there’s no reason that we couldn’t cover such fragments in the nLab article and in particular no reason why we can’t cover ILL.
I have put a bit in the article about fragments. Feel free to write more.
“I always felt that intuitionistic linear logic is sort of missing the point of linear logic.” This seems predicated on the idea that a logic should have a philosophic point.
To me, the point could be constrained to mathematics: classical propositional logic is the logic of Boolean algebras; intuitionistic propositional logic is the logic of Heyting algebras and, in more categorified form where proofs are promoted over mere provability, cartesian closed categories. Continuing the last, multiplicative linear logic is the logic of -autonomous categories; multiplicative intuitionistic linear logic is the logic of symmetric monoidal closed categories. The technical advantages, or let’s say niceties, of these particular logics include the availability of a cut-elimination algorithm, and in the case of linear logics, a relatively clean graphical representation of “normal forms” of proofs.
In quasi-philosophic language, MILL maintains “conservation of resources” that is the hallmark of linear logic, but unlike MLL, there is a direction to the flow of information from hypotheses to conclusion. As a result, it is much easier to assign a functional term interpretation to proofs in MILL, whereas in MLL there is no canonical way to go about this (should a proof of be seen as a function , or as a function ?).
It’s worth mentioning that ordinary intuitionistic logic admits a translation into (what is called) classical linear logic. Thus, one might argue that “classical” linear logic already includes both ordinary classical logic and ordinary intuitionistic logic, making it redundant or unnecessary to consider a further “intuitionization” of linear logic. The point is, I guess, that the linear “negation” has a different meaning from the intuitionistic one, so that it can be involutive without contradicting an intuitionistic viewpoint. I learned this summer that the linear logic viewpoint gives a fairly compelling “explanation” of the difference between ordinary classical and intuitionistic logic: classical logic allows “backtracking” or “save-and-restore game playing”.
Personally, I think that what we call “intutionistic” linear logic is also interesting, due in large part to its connection with monoidal categories that Todd mentioned. However, I think it’s also true that the adjectives “intuitionistic” and “classical” applied to linear logic, while their formal meaning may be analogous to that of their applications to nonlinear logic, have rather different philosophical meanings. It might be better if we used different words altogether, such as “involutive linear logic” and “non-involutive linear logic”.
Thanks, Todd, that helps. (I already knew what Mike reports.)
Meanwhile, Valeria appears to have departed the discussion. I may get around to revising the entry, but it would be nice if people didn’t limit their involvement to a passing whinge. (Valeria, if you’re listening, then sorry, but that’s how it appears. It’s hard to know what you would find satisfactory.) It’s like people on the categories list complaining about a Wikipedia article – to what end?
Mike, my reading of MILL is that the connectives are and – no multiplicative and no multiplicative negation. So I’m not sure what it is that would be non-involutive. :-)
Still, MILL as a whole is non-involutive, as it has no involution (or more precisely no order-reversing involution).
Ah, okay. I was thinking of non-involutive as lack of a property, not lack of a structure. :-)
Yes, I guess you’re right.
Thanks Nikolaj, I’m glad you like it.
I was quite confused for a while about the use of “ex contradictione quodlibet” on page 5 to prove one “or” stronger, as you write, than the other. I then asked around on the web before I got back and on page 6 on the top and its footnote, where I saw this was actually about affine logic.
That’s what you get for knowing too much! (-:
The main point of that paper is the semantic construction on Heyting algebras, and its first-order extension, and it’s just a fact that what this yields is a model of affine logic (i.e. a semicartesian -autonomous category) rather than general linear logic. Indeed, as noted on p10, this construction also satisfies many other laws that don’t hold even in general affine logic. The intuitive motivation discussed in section 11 also, I believe, justifies adopting weakening, since the omission of unrestricted contraction is only a technical device to ensure that proofs by contradiction remain constructive, whereas weakening doesn’t affect this.
Regarding your second point, by “essentially the same thing” I meant “essentially the same thing in the logic we are talking about right now”: in classical/involutive linear (or affine) logic these two statements differ only by a De Morgan law.
1 to 13 of 13