Jason (jcreed) wrote,
Jason
jcreed
I remembered at José's talk last monday Frank mentioning that classical logic and the lax modality don't tend to play well with one another. I noticed that if you just turn the double-negate-everything crank on the lax Circle, what pops out is very similar to the proof-irrelevance modality; I suppose this is because not-not is a monad itself, and the usual moral is "proof irrelevance is two monads". There are some classical degeneracies associated with being able to promote way more often than you might expect, since you can contract stuff apart on the right and use the promotional effect of a circle over and over again as soon as you ever get just one, but perhaps things would be less trivial in classical linear logic.

It also suggests (and I'm surprised I didn't think of it before) that perhaps there ought to be a constructive dual to the proof irrelevant modality --- not the "intentisonal" dual to the concept of proof irrelevance in the sense of Pfenning '01, but something that has the same demote/promote sort of protocol, but on opposite sides of the turnstile.

But it would be rather degenerate for the same reason as the classical (nonlinear) dual would be, so maybe it makes more sense linearly, too...
Tags: classical, lax, logic
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    switch
    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    Help
  • 0 comments