The idea behind the new translation is you can squeeze the thing that holds the Kripke world into an atomic proposition h(...) that you keep in the conclusion. Having used the conclusion for that, where does the object-language conclusion go? Well, you stash it in the context, like in the resource semantics paper. How do you keep it from getting pathologically duplicated? You mark it with a frame variable φ, and shove that into a different argument of the h(...), and insist they line up everwhere they need to. Finally, there's a third argument of the h(...) that is some trick apparently required to model Pfenning-Davies diamond correctly. I don't know how to give an intuition for it. It just seems to be the thing that works.
The idea behind the new translation is you can squeeze the thing that holds the Kripke world into an atomic proposition h(...) that you keep in the conclusion. Having used the conclusion for that, where does the object-language conclusion go? Well, you stash it in the context, like in the resource semantics paper. How do you keep it from getting pathologically duplicated? You mark it with a frame variable φ, and shove that into a different argument of the h(...), and insist they line up everwhere they need to. Finally, there's a third argument of the h(...) that is some trick apparently required to model Pfenning-Davies diamond correctly. I don't know how to give an intuition for it. It just seems to be the thing that works.
-
(no subject)
Saw Mike Birbiglia's "Thank God for Jokes" with K in a little theater on bleeker. Funny show. I highly recommend his show "My girlfriend's boyfriend"…
-
(no subject)
Oh jeez Boulet, this is what you casually slap together for a 24-hour comic? Come on, now, you're just showing off. (But seriously it is so cute)
-
(no subject)
Second city yesterday was really funny. We got shoved in a front-row seat and picked on to provide detailed improv prompts for a big log improv…
- Post a new comment
- 0 comments
- Post a new comment
- 0 comments
