Jason (jcreed) wrote,

Have been getting some work done today and yesterday.

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.

  • (no subject)

    K got back tonight, pretty late in subjective time (3-4am or so, coming from europe) but all in one piece. None of her houseplants, which were…

  • (no subject)

    K is off tonight to Old Country for a couple weeks, to fulfill family-seeing obligations. Sad! Thankfully we still have internet and skype and…

  • (no subject)

    Finally home. This time instead of mysteriously attracting screaming babies I mysteriously attracted full grown adults biting their nails or maybe…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded