October 31st, 2012

beartato phd

(no subject)

Some patches of sunlight today, but quite cold. The subway being down for the whole city is crazy. Traffic is just an unbelievable near-standstill everywhere I've been able to see. It's striking to see how essential public transportation is for this city, for better or worse. Once again I note how phenomenally, stupidly lucky I am in almost every aspect of my situation. Even unemployment feels like a benefit at this point. I don't have a job to get to or to stress out about on top of everything else. Actually, even if I did, I probably could have done it adequately from home.

I had some thoughts about mixing together the first-order aspects of my Intuitionistic Letcc paper with Frank with the Simpson-thesis-inspired soundness proof of labelled classical modal logic. I figure that, as long as first-order terms are also world-labelled, Barcan's formula should fail, and soundness should still hold. Trying to formalize the whole mess better and more incrementally than "you know, a big graph of worlds and stuff" is tricky though. I splatted down about five pages into the TeX buffer before running into some notation-management problems I don't know how to bail myself out of yet.