Does focused proof search ever have to backtrack across the choice of focus formula?

Question

There are a lot of different "focused" sequent calculi for lots of different logics, but my understanding is that many or most of them have the following flavor. First one divides the connectives into "left-asynchronous / positive" (e.g. $\vee$, $\oplus$, $\otimes$, $\exists$), whose left rules are invertible, and "right-asynchronous / negative" (e.g. $\wedge$, $\Rightarrow$, $\multimap$, $\forall$), whose right rules are invertible. Then the focused proof search (i.e. building a sequent calculus proof bottom-up) has two phases. First we apply all the asynchronous/invertible rules, in any order. Second, we focus on some formula and apply all of its synchronous rules, keeping focus on the formulas thereby generated and immediately applying any applicable asynchronous rules (or, equivalently, reverting to phase one in all generated subgoals), until we reach an atomic formula. At that point we can either finish the proof with an identity rule, or re-focus on a different formula.

At least some systems require the proof to finish as soon as the focus formula becomes atomic, which I believe means that if you chose the wrong formula to focus on in the first place you may have to backtrack. My question is rather about what happens if we allow the proof to re-focus on a different formula when it reaches an atomic one. In that case, is it possible to "choose the wrong formula" to focus on and have to backtrack? In other words, is it ever possible that there are synchronous formulas that must not be decomposed in a proof, or that must be decomposed in a particular order?

It's easy to come up with examples where you can get in trouble if you try to apply synchronous rules before asynchronous ones, e.g. $p\vee q \vdash q\vee p$. But the focused method requires all asynchronous rules to happen immediately, so this sort of problem doesn't arise.

Note also that there is another unrelated source of backtracking that this says nothing about, involved in individual synchronous rules. For instance, there are two $\& L$ rules that we have to choose between, and in a rule like $\otimes R$ we have to decide how to split the context between the two premises, and it's certainly always possible to make wrong choices there and have to backtrack. That's not what I'm asking about.

I've phrased this as a general question about all focused sequent calculi, but of course it's possible that the answer depends on the logic or on the details of the calculus. In that case I would be interested to know what properties of a logic or calculus lead to different behavior.

Answer 1

Yes, backtracking in focused proof search may be necessary due to a wrong choice of focus formula. Consider the provable sequent

$$\vdash p\otimes q, (p^\bot\mathrel{\wp} q^\bot)\otimes r, r^\bot.$$

Choosing to focus on $p\otimes q$ leads to a dead end, because however you "split" the context you end up with an atom ($p$ or $q$) without matching dual. So $(p^\bot\mathrel{\wp} q^\bot)\otimes r$ must be decomposed first.

---

A side remark, not directly related to the question but which gives some further context: the formula $p\otimes q$ above is known to proof net connoisseurs as a "non-splitting tensor". When showing that proof nets (in the sense of suitably labelled graphs satisfying certain connectivity and acyclicity conditions) correspond to sequent calculus proofs (the sequentialization theorem) one must at some point prove the non-trivial "splitting lemma": if the conclusions of a proof net come only from axiom or tensor nodes, then there is one such tensor node which is "splitting", in the sense that removing it decomposes the proof net into two connected components which are themselves proof nets (this allows sequentialization to be proved inductively). One of course may wonder whether all tensors are always splitting, and the above is the minimal counterexample.

In terms of proof nets, focusing strengthens the splitting lemma by adding that there always exists a "hereditarily splitting tensor", in the sense that there is a tensor node such that all tensor nodes directly above it have the splitting property.