Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorvaleriadepaiva
    • CommentTimeOct 22nd 2011
    hi,
    I take issue with the article on Linear Logic in the nLab. It says:

    (In this way, linear logic has a perfect de Morgan duality.) The logical rules for negation can then be proved.

    While this is true for *Classical* Linear Logic, for Intuitionistic Linear Logic things are very different and I feel that this whole 'dark side of the moon' is being thrown away for no good reason. There is no reason to decide that Classical Logic is better than Intuitionistic Logic and there is not reason to decide that Classical Linear Logic is better than Intuitionistic Linear Logic. the article should have a discussion of both realms. How do I go about adding this discussion, please?

    thanks
    Valeria
    • CommentRowNumber2.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 22nd 2011

    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.

    • CommentRowNumber3.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 22nd 2011

    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!

    • CommentRowNumber4.
    • CommentAuthorTobyBartels
    • CommentTimeOct 22nd 2011

    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.

    • CommentRowNumber5.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 23rd 2011

    “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 *\ast-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 ABA \wp B be seen as a function A BA^\perp \to B, or as a function B AB^\perp \to A?).

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeOct 23rd 2011

    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”.

    • CommentRowNumber7.
    • CommentAuthorTobyBartels
    • CommentTimeOct 24th 2011

    Thanks, Todd, that helps. (I already knew what Mike reports.)

    • CommentRowNumber8.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 25th 2011

    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 \otimes and \multimap – no multiplicative \bot and no multiplicative negation. So I’m not sure what it is that would be non-involutive. :-)

    • CommentRowNumber9.
    • CommentAuthorTobyBartels
    • CommentTimeOct 25th 2011

    Still, MILL as a whole is non-involutive, as it has no involution (or more precisely no order-reversing involution).

    • CommentRowNumber10.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 25th 2011

    Ah, okay. I was thinking of non-involutive as lack of a property, not lack of a structure. :-)

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeOct 26th 2011

    Yes, I guess you’re right.

    • CommentRowNumber12.
    • CommentAuthorNikolajK
    • CommentTimeApr 24th 2019
    • (edited Apr 24th 2019)
    Mike,
    I'm currently reading your [logic article](https://arxiv.org/abs/1805.07518)
    from last year on constructive mathematics - really thanks for writing it! And, more generally, a lot of your elaboratively minded texts.

    I'm not interested in "logics of resource" but am coming at this from a pure logic (should "A->(B->A)" be viewed as "entailment"?) as well as logic for math foundations (how far do we get constructively?) angle and for that I was previously reading into the [1000 page relevant logic treaty](https://www.amazon.com/Entailment-Vol-Logic-Relevance-Necessity/dp/0691071926/ref=sr_1_1?qid=1556098539&refinements=p_27%3AAlan+Ross+Anderson&s=books&sr=1-1&text=Alan+Ross+Anderson
    ).
    So I wonder if you could elaborate why you went the affine logic rule there? 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. Linear logic is commented on. Did you go for adopting weakening because the models you discuss are nicer with affine logic.

    A page later you also write that the (multiplicative) law of excluded middle” and law of non-contradiction are "essentially the same thing" but iirc even [minimal logic](https://en.wikipedia.org/wiki/Minimal_logic)
    (rejecting excluded middle and explosion), or at least many models of it, proves or demonstrate non-contradiction. The former just makes you weaker with regard to proving results, the latter protects you from your results being devalued.
    If you'd like to share, I'd like to hear your perspective on that.
    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeApr 24th 2019

    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 Chu(H,0)Chu(H,0) 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.