May 10th, 2013

beartato phd

(no subject)

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.