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?