Jason (jcreed) wrote,

Been thinking about encoding modal logic in resource semantics style since I talked to sean mclaughlin over the weekend about it. I sketched out some thoughts here. It's a translation that's meant to encode Pfenning-Davies in a sort-of-Kripke-ish-semantics way. I had an old version of this idea that did Pfenning-Davies with a linear target language, but sean's theorem prover is for plain ol' first-order logic. And I didn't want to just compose the Modal -> Linear translation with the Linear -> First-Order translation because it seemed to produce a mess.

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.
Tags: logic, math, modal

  • (no subject)

    Some further progress cleaning up the https://xkcd.com/1360/ -esque augean stables that is my hard drive. Tomato chicken I made a couple days ago…

  • (no subject)

    Did some personal archaeology. Helped a little with laundry. Threw some chicken, onions, tomato, stock, peppers in the slow cooker and hopefully…

  • (no subject)

    Dinner with akiva and dannel at nuevo portal in carroll gardens. Ate a pile of chicken stew and rice and beans and maduros, good times. I do miss…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded