Jason (jcreed) wrote,
Jason
jcreed

wjl and I had an edifying conversation about linear logic.

So, like, I took for granted that classical linear logic is not conservative over intuitionistic linear logic, but unlike the classical logic vs. intuitionistic logic case, where there are some standard shibboleth propositions that distinguish them (double negation elimination, excluded middle, peirce's formula) I couldn't think of any off the top of my head.

If your notion of "intuitionistic linear logic" is the one from Frank/Kaustuv/Evan's JILL paper, then you at least get ⊥, and you can take the linear double negation elimination formula ((A -o ⊥) -o ⊥) -o A, which is not provable in JILL, but provable in CLL.

But suppose you disallow mentioning bottom: then what's a simple nice formula that's provable in CLL but not ILL? We puzzled over it for a bit, and only came up with the somewhat clunky formula
(A0 & B0)0 -o (A00 ⊕ B00)
(where A0 is an abbreviation for A -o 0, and A00 associates like (A -o 0) -o 0)

Can one do any better?
Tags: linear logic, zerp
Subscribe

  • (no subject)

    Some further progress cleaning up the https://xkcd.com/1360/ -esque augean stables that is my hard drive. Tomato chicken I made a couple days ago…

  • (no subject)

    Did some personal archaeology. Helped a little with laundry. Threw some chicken, onions, tomato, stock, peppers in the slow cooker and hopefully…

  • (no subject)

    Dinner with akiva and dannel at nuevo portal in carroll gardens. Ate a pile of chicken stew and rice and beans and maduros, good times. I do miss…

  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 13 comments

  • (no subject)

    Some further progress cleaning up the https://xkcd.com/1360/ -esque augean stables that is my hard drive. Tomato chicken I made a couple days ago…

  • (no subject)

    Did some personal archaeology. Helped a little with laundry. Threw some chicken, onions, tomato, stock, peppers in the slow cooker and hopefully…

  • (no subject)

    Dinner with akiva and dannel at nuevo portal in carroll gardens. Ate a pile of chicken stew and rice and beans and maduros, good times. I do miss…