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.