Jason (jcreed) wrote,
Jason
jcreed

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
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 0 comments