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.
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.
-
(no subject)
ICFP contest has got me feeling kind of down about programming. I really don't like the problem this year. I had my hopes up that since they had…
-
(no subject)
Man, can't people just sit still in a class for an hour? I remain mystified by people who continually, for the entire 80 minute duration of class,…
-
I was once your vassal / You were once my castle
OH EM FUCKING GEE. I finally figured out that yes, the periodic chirping noise coming from the basement is indeed because there's a battery in the…
- Post a new comment
- 1 comment
- Post a new comment
- 1 comment
