Focus

[simrob]

Used a not-terrifically-worded question on MathOverflow and the fact that I had two hours to kill as an excuse to finally write out the cut-and-identity-based proof of the completeness of (weak) focusing for the negative fragment, where you don't have to admit that it's only weak focusing. I wrote out all the details in the Weak Focusing for Ordered Linear Logic tech report, but that TR has way the hell too much other stuff going on.