Jason (jcreed) wrote,

Couldn't help myself and noodled around with that encoding over lunch again. It's beginning to look like I can get Pfenning-Davies-style and Simpson-style modalities in the same logic, mediated by a "Simpsonly true" sort of, um, metamodality. Why have Pfenning-Davies be the default and Simpson guarded by a propositional operator and not the other way around, you ask? Because the main difference between how the two logics are encoded is whether a certain equality between worlds is checked (namely: are you trying to perform an "untethered" decomposition at a world that is not equal to the "current" world?) and it seems like it works out to tag the world with a bit of data that, when present, collapses that equality relation. And, being the good intuitionist that I am, it's easy to learn new equalities as intuitionism-time advances, and seems weird and wrong to forget them. So, passing under a modality should collapse more things, and become more licentious and Simpson-y.
Tags: logc, math, modal

  • (no subject)

    Something that's bugged me for a long time is this: How many paths, starting at the origin, taking N steps either up, down, left or right, end up at…

  • (no subject)

    Still sad that SAC seems to end up being as complicated as it is. Surely there's some deeper duality between…

  • (no subject)

    I had already been meaning to dig into JaneSt's "Incremental" library, which bills itself as a practical implementation (in ocaml) of the ideas in…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded