![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
simrobUsed 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.
