
[Nov. 7th, 201210:01 pm]
Jason

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 PfenningDavies K = classical Simpson K classical PfenningDavies T = classical Simpson T classical PfenningDavies K4 = classical Simpson K4 classical PfenningDavies 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 firstorder 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 pfenningdavies).
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 PfenningDavies K, T, K4?" A: Well, the systematic way of determining what PfenningDavies X is from a set of axioms X about a Kripkeish world accessibility relation is the paper I'm currently working with Sean on writing up. Specifically, however, S4 is actual PfenningDavies as it exists, K4 is what you get if you throw out the copy rule, T is what you get if the boxright 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) 

