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)

I got off on the wrong foot with my proof attempt yesterday by stupidly thinking I could dodge diagonalization by computable approximation; I guess…

• #### (no subject)

Reading some about Ray Solomonoff I was reminded how funny universality of computation really is. WARNING WARNING PROBABLY NOT A VALID PROOF OF…

• #### (no subject)

A paper on describing circuits in an agda DSL: http://www.staff.science.uu.nl/~swier004/publications/2015-types-draft.pdf

• Post a new comment

#### Error

Anonymous comments are disabled in this journal

default userpic