Apart from that, I've been trying to cook up some notes on this infinite-sequence-of-increasingly-powerful-boxes modal logic idea. Here's the intuitionistic sequent calculus
but don't believe the beginnings of the cut elimination proof. It takes a slightly more delicate case analysis than the usual structural cut elimination proof, but I think I got it all worked out on the whiteboard. The statement of the proof is at least the right level of generalization of the induction hypothesis.
Anyway if you're still reading this far I imagine you can picture what the classical version has to look like: just add deltas on the right everywhere, except not on the premise of the box-right rule, because going to an n-possible world where A is false forces you to discard all merely contingently known falsehoods.
The punchline is supposed to be that a dead simple recursive translation of propositions can carry the classical calculus into the intuitionistic calculus, and vice versa. Well, not the same translation, but the important thing is that it exists. From C into I, double-negate every subformula. From I to C, box_1 every subformula, and change every box_n you find into box_(n+1).
Actually I was hoping to pull further tricks so that there would actually be "classically true" and "intuitionistically true" modalities C and I, but now I'm not so sure how that would work. I'd have to make some decision as to whether ICA and CIA would be equivalent to A, and my intuition pump has run dry.
Also of course I have the suspicion that at least some of this is already done and dead and buried. Certainly I've seen Kripke structures defined with multiple accessibility relations, haven't I? I don't know if things like this subsume what I'm trying to do.