Jason (jcreed) wrote,

So this problem I've been hacking on lately is kind of the epitome of what I like about mathematics; that a thing can be proved in the literature one way, proved by a colleague another way, proved by yourself a third way, and yet there is still another significantly different proof idea that promises to explain still more interesting things about what's going on with the connection between letcc-like control flow on the one hand, and the gap between intuitionistic and classical logic on the other. And this is only one little corner of what seems to be going on with "labelled" presentations of judgmental logics; I think they may nicely subsume modal logics in the style of both Alex Simpson and Pfenning/Davies, the logic of bunched implications, and resource logics in the vein of linear logic (including affine and strict implication as special cases).

Anyway the "little corner" is Yet Another Proof that Gödel's modal interpretation of intuitionistic logic into classical logic is correct. This one works in three steps:

LMCSC → LND+letcc → LND → ND

  • LMCSC is the labelled multiple conclusion sequent calculus that embodies Gödel's translation.
  • LND+letcc is a labelled natural deduction system that has a letcc construct that is required to obey a certain label discipline: you are only allowed to throw data at world p to a continuation at world q if "q is an accessible world from p" ("q is in the future of p")
  • LND is the same labelled system only without letcc at all.
  • ND is ordinary natural deduction

LND → ND is the easiest part; the presence of labels in the rules can only make things harder to prove. If you erase all the labels in the rules in LND, you get the rules in ND.

LMCSC → LND+letcc is the next easiest. It's a routine exercise in programming classical reasoning with letcc. One caveat is that you can't pull quite all the same tricks that lambdacalculus can that essentially constitute Glivenko's theorem, and let you put only one letcc all the way on the outside. For some reason the label discipline prohibits those; I'm still not sure why. Anyway, it's not too bad.

LND+letcc → LND is the hard part: getting rid of all the letccs and throws. I think as of this afternoon, however that it might really work. Disjunction was my final worry. I've had everything worked out for every other basic connective (implication, conjunction, truth, and even falsehood) for a few days now, but disjunction is a total pain in the ass. If you have a lambda that has within its body a pile of nested case expressions, it looks like it may be necessary to commute up above the lambda those (and only those) case expressions that analyze an expression in which x does not occur free. Ugh ugh ugh.
Tags: math, work
  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded