5
$\begingroup$

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.

$\endgroup$
  • 3
    $\begingroup$ Consider the sequent $\vdash p\otimes q, (p^\bot\mathrel{\wp} q^\bot)\otimes r, r^\bot$. You have three choices of focus but only one of them is correct: focusing on $r^\bot$ is obviously wrong, and decomposing $p\otimes q$ first leads you to a dead end (you need to send $(p^\bot\mathrel{\wp} q^\bot)\otimes r$ with $p$ or $q$, and in both cases you end up with an atom without matching dual). In particular, this an exemple (minimal, I guess) of two synchronous formulas that must be decomposed in a particular order. Does that answer your question? $\endgroup$ – Damiano Mazza Aug 9 '20 at 7:11
  • 2
    $\begingroup$ @DamianoMazza Yes, that's it! Thanks. I guess I got stuck because I didn't think of nesting an asynchronous formula like $p^\perp \wp q^\perp$ inside a $-\otimes r$ to make it synchronous. If you post that as an answer I'll accept it. $\endgroup$ – Mike Shulman Aug 9 '20 at 22:35
3
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Silly question, but does this ever happen in non-linear (classical) focused sequent calculus? $\endgroup$ – cody Aug 11 '20 at 14:02
  • 1
    $\begingroup$ Yes. The example I gave in fact is intuitionistic: it's the sequent $p\Rightarrow q, (p\Rightarrow q)\Rightarrow r\vdash r$, which is provable via the (linear) $\lambda$-term $z(\lambda x.yx)$. In a focused system for intuitionistic logic, you have the choice between focusing on one of the two formulas on the left of the sequent, and one choice leads to backtracking. $\endgroup$ – Damiano Mazza Aug 12 '20 at 8:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.