You Can Only Cross The Same River Once

The formula is strange. For example, here’s a small proof fragment, where is an arbitrary goal formula:

Is the in the right premise of the loli-left rule the same as the one we started with in the conclusion?

More on Focusing

Thinking a little bit more about my previous post about focusing:

• Does a greedy strategy work? Why or why not? Specifically, is it the case that the focused variant of a sequent that has the most premises in focus but is still sound and complete the one that reduces the proof space most effectively? (My guess is that it doesn’t work, but I’m not sure why.)
• What sequents are amenable to focusing? I’ve only really ever heard Linear Logic folks talking about it, but that may just be bias from its source in Andreoli’s work. It seems to me that it’s a general proof technique for any sequent calculus—is that true?

Comparing Focusing Strategies

Any unfocused sequent calculus can induce multiple viable focused calculi. Trivially, if you take one focused version you can leave off some of the focus in the conclusions. For example, the synchronous rule for tensor in focused linear logic is usually given as

but there’s nothing wrong, per se, with taking the rule to be

or the symmetric omission of focusing on the right premise, or even the degenerate