Jason (jcreed) wrote,

Ok I think I have a satisfying-to-me* explanation of all the stuff in frank's modal logic "weather report" now. They key points are:

  • Box is still straightforwardly "for all future worlds".
  • Upshift is still frame-parameterized double-negation,
    ↑P @ w = ∀φ.(P @ w → #(φ, w)) → #(φ, w)

    This is what achieves the "tethering" effect of Pfenning Davies.
  • Diamond is a variant of this:
    ◇P @ w = ∀φ.w ≥ φ → (∀v ≥ w. P @ v → #(φ,v)) → #(φ, w)

*i.e., fiddly-token-passing-translation-compatible

The tricksy thing I am doing is assuming there is an inclusion from frames (e.g. the φ that is quantified over) into Kripke worlds (e.g. the v, w) so that I can compare them in that w ≥ φ there.

The punchline is that I should be able to vary the axiomatization of ≥ from no axioms to just refl to just trans to refl and trans, and I think I get out weather-report K, T, K4, and S4, respectively.
Tags: logic, math, modal logic

  • (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