I think I basically have a nice syntactic proof that classical and…: jcreed

I think I basically have a nice syntactic proof that classical and constructive multimodal propositional logic are expressively equivalent. It's somewhat of an argument back in favor of Pfenning-Davies "context-obliterating" style of modality definition, as opposed to the labelled style, which, although I was able to find the proof earlier, is much more complicated. The thing that makes the new proof easy, unsurprisingly, is essentially focussing discipline again. The reason I went for labelled box before is that it was a nice negative connective, but Pfenning-Davies box still functions perfectly well attached to the left side of an arrow (much like the proof-irrelevant modality, linear bang, and like how tensor, oplus, etc. are "curryable-away" in the same position) so that's how the encoding works. Besides, classical logic is essentially a logic of all hypotheses (and a single invariant conclusion of falsehood), so it admits a straightforward box, because it's secretly a box on the left of an arrow no matter where you put it.

Party at

chrisamaphone's was awesome fun. I enjoyed having one of my favorite temporary-party-escape tactics be the purpose of the party. Max Kaufmann and

hvincent and her friend James (I think his name was?) are ridiculously good artists oh man. Got too tired to go to Mike Beattie's party afterward, which is sort of regrettable since I hardly ever get to hang out with those kids any more.

(no subject)

(no subject)

(no subject)

Error