Jason (jcreed) wrote,

Sudden cold weather with snow today in the north east. Huddled indoors and ate food and dicked around with programming stuff. K came over in the afternoon and we slapped together some tasty baked pasta with sausage/peppers/onions/cheese.

I'm frustrated that I'm able (I think, unless I made a mistake) to see by individual proofs that
classical Pfenning-Davies K = classical Simpson K
classical Pfenning-Davies T = classical Simpson T
classical Pfenning-Davies K4 = classical Simpson K4
classical Pfenning-Davies S4 = classical Simpson S4
but that each proof relies on individual insights about world graphs and expressions involving boxes and so on. I have a strong gut feeling that there's got to be a more systematic proof, but I can't find one, and I've currently run out of leads.

An intuition for why the proof is hard to systematize is that it's really close to false. If you make things intuitionistic, it's false. (see Rob's counterexample from the other day) If you add a first-order quantifier (at least if you do it the obvious way: see Barcan's formula) it's false. If you make things linear, it's false. (For □A & □B ⊢ □(A & B) holds in simpson but not pfenning-davies).

It leads me to suspect that the whole thing should hinge on the ambipolarity of nonlinear conjunction: because we're in a propositional, classical, nonlinear setting, it's kind of the only connective around, besides □, and the negation that's baked into the classical setting.

(Q: "What the heck do you mean by Pfenning-Davies K, T, K4?"
A: Well, the systematic way of determining what Pfenning-Davies X is from a set of axioms X about a Kripke-ish world accessibility relation is the paper I'm currently working with Sean on writing up. Specifically, however, S4 is actual Pfenning-Davies as it exists, K4 is what you get if you throw out the copy rule, T is what you get if the box-right rule erases all true hypotheses and also turns all valid hypothesis into merely true, and K is what you get if you do both of these things)
Tags: math, modal logic, programming, weather

  • (no subject)

    Remember that series of photographs of what the world eats? I was reminded of it by " Where children sleep" in that both are really powerful…

  • (no subject)

    Some random pictures from recently. A handmade book _tove showed me how to make. There was a bit of fiasco for a while where the…

  • (no subject)

    Tom7 "friending" me on Flickr reminded me that I had a Flickr account! So put up a couple more pictures. You can see them here. My favorite one is…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded