Occasional pockets of conversation with gradually revealed that I've been mistaken about something in the Ill-Fated resource semantics paper for basically the last three years. It's a thing I like about math sometimes that when you're wrong, you're just flat out wrong and there's no quibbling about it. It ideally provides a nice boot in the butt to get you moving on to something else, although I have to admit it I still was on a bit of an emotional rollercoaster during thesis times as material alternately did and did not appear to work.

http://jcreed.org/math/modal-encoding/equational.html

The real scales-fall-from-eyes observation is that Nuel Belnap's "display property" seems to actually be really, really importantly involved in focusing working out right. I went back and looked at that silly little queue logic that I made up as a counterexample to make a point, and it turns out it focuses really badly! If you do it naively, the sequent p, ↓↑q |- p * q (where p and q are positive atoms) is not provable while p, q |- p * q plainly is. The only way I know how to recover is to bake shifts into some of the connectives: fuse must be of the form P * N, and blurs on its N argument, and right-arrow must be of the form N =>> N, and blurs on its left argument.

Relatedly, all the weird stuff in the shifty modalities like square, diamond, and circle is similarly "undisplayable", and so that's in a sense arguably why those connectives act like shifts.

Tags:
• #### (no subject)

Still kinda sick but maybe getting better. Really love these custom cast-plastic Settlers-of-Catan tiles: http://imgur.com/gallery/6hfG5

• #### (no subject)

Nice way of showing off easing functions: http://easings.net/

• #### (no subject)

over on twitter linked to this blogpost which has some thoughts about " Genius Loci". I found it notable initially because it…

• Post a new comment

#### Error

Anonymous comments are disabled in this journal

default userpic