
[Nov. 11th, 201508:16 pm]
Jason

Wrote up that idea I had a few days ago. Turned out quite cute I think! I asked around and maybe it's not actually already a wellknown result. The standard phase semantics for inutitionistic linear logic seems to involve a closure operator standing in for the \bot\bot of classical phase semantics. So what focusing is doing is exactly splitting that closure operator (i.e. monad) into a galois connection (i.e. adjunction). It's nothing new to me that upshift and downshift are sorta adjoint somehow, but the phase semantics makes it really obvious  and I wasn't familiar until recently with the fact that there was a semantic appearance of the corresponding monad. (Because I have traditionally been super ignorant of anything to do with semantics)
But... viewed semantically, I like that focusing appears to simplify an existing mess, (or at least all of the mess is carefully tucked away in the shift operators) in contrast to the prooftheoretic case, where it makes the proof system a bit more messy (but in a way that has obvious benefits). If Andreoli hadn't figured it out from the angle of optimizing proof search, I feel like you'd still want to have invented focusing just to clean up the phase semantics.
Of course the really weird thing to me is that by doing semantics at all, I'm working in the ambiently classical world of set theory  and basically the identical set of "semantic" clauses give the same result of capturing ILL when I interpret them proof theoretically, i.e. in an ambiently intuitionistic world. My best guess is that the foralls in the definition of the shifts are hiding what's effectively a forall over kripke worlds. 

