ch:focusing-proof-search: ch:focusing-proof-search

Put $\mathrm{\Delta }=p\wedge q,r\wedge s$. The first schedule is $$\frac{{\displaystyle \frac{{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{{\displaystyle \frac{p\in \mathrm{\Delta },p}{\mathrm{\Delta },p⟹p}}\mathrm{U}-\mathrm{Init}}{\mathrm{\Delta }⟹p}}\mathrm{U}-\mathrm{AndL}1\\ {\displaystyle \frac{{\displaystyle \frac{r\in \mathrm{\Delta },r}{\mathrm{\Delta },r⟹r}}\mathrm{U}-\mathrm{Init}}{\mathrm{\Delta }⟹r}}\mathrm{U}-\mathrm{AndL}1\end{array}}{\mathrm{\Delta }⟹p\wedge r}}\mathrm{U}-\mathrm{AndR}}{p\wedge q⟹(r\wedge s)\to (p\wedge r)}}\mathrm{U}-\mathrm{ImpR}}{\cdot ⟹(p\wedge q)\to (r\wedge s)\to (p\wedge r)}\mathrm{U}-\mathrm{ImpR}.$$ The second schedule decomposes both left conjunctions before the right one: $$\frac{{\displaystyle \frac{{\displaystyle \frac{{\displaystyle \frac{{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{p\in \mathrm{\Delta },p,r}{\mathrm{\Delta },p,r⟹p}}\mathrm{U}-\mathrm{Init}\\ {\displaystyle \frac{r\in \mathrm{\Delta },p,r}{\mathrm{\Delta },p,r⟹r}}\mathrm{U}-\mathrm{Init}\end{array}}{\mathrm{\Delta },p,r⟹p\wedge r}}\mathrm{U}-\mathrm{AndR}}{\mathrm{\Delta },p⟹p\wedge r}}\mathrm{U}-\mathrm{AndL}1}{\mathrm{\Delta }⟹p\wedge r}}\mathrm{U}-\mathrm{AndL}1}{p\wedge q⟹(r\wedge s)\to (p\wedge r)}}\mathrm{U}-\mathrm{ImpR}}{\cdot ⟹(p\wedge q)\to (r\wedge s)\to (p\wedge r)}\mathrm{U}-\mathrm{ImpR}.$$ The first U-AndL1 commutes with U-AndR, as does the second; the two left decompositions also commute with each other. After those commuting conversions both trees have the same two initial leaves.

With positive atoms use $$(p^{+}\vee q^{+})\Rightarrow \uparrow (q^{+}\vee p^{+}).$$ With negative atoms use $$(\downarrow p^{-}\vee \downarrow q^{-})\Rightarrow \uparrow (\downarrow q^{-}\vee \downarrow p^{-}).$$ Erasure deletes each $\uparrow$ and $\downarrow$, sends both polarities of each atom to its unpolarized atom, sends $\Rightarrow$ to $\to$, and sends the positive disjunction to $\vee$. Both formulas therefore erase, component by component, to $(p\vee q)\to (q\vee p)$.

Read every rule bottom up. The positive inversion rules F-DownL, F-ZeroL, F-OrL, F-OnePosL, F-TensorL, and F-SuspendPos continue inversion or close its branch. The negative rules F-UpR, F-ImpR, F-OneNegR, F-WithR, and F-SuspendNeg do the same. Rules F-ReleaseR and F-FocusL start, respectively, a right and left focus from a stable inversion sequent.

The positive rules F-OrR1, F-OrR2, F-OnePosR, F-TensorR, and F-IdPos continue or close right focus. The negative rules F-ImpL, F-WithL1, F-WithL2, and F-IdNeg continue or close left focus. Rules F-DownR and F-UpL release right and left focus into inversion. The genuine connective choices are F-OrR1 versus F-OrR2, and F-WithL1 versus F-WithL2. Selecting which persistent negative hypothesis to focus on is a further proof-search choice, not a connective-rule alternative.

Write $G=(r^{+}\otimes s^{+})\Rightarrow \uparrow (p^{+}\otimes r^{+})$. Bottom-up, the complete forced prefix is where ${\mathrm{\Gamma }}_4=⟨p^{+}⟩,⟨q^{+}⟩,⟨r^{+}⟩,⟨s^{+}⟩$. Immediately before applying F-UpR bottom up the sequent is ${\mathrm{\Gamma }}_4;\cdot ⊢\uparrow (p^{+}\otimes r^{+})$; its premise is ${\mathrm{\Gamma }}_4;\cdot ⊢p^{+}\otimes r^{+}$. The remaining tree is $$\frac{{\displaystyle \frac{{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{\phantom{X}}{{\mathrm{\Gamma }}_4⊢[p^{+}]}}\mathrm{F}-\mathrm{IdPos}\\ {\displaystyle \frac{\phantom{X}}{{\mathrm{\Gamma }}_4⊢[r^{+}]}}\mathrm{F}-\mathrm{IdPos}\end{array}}{{\mathrm{\Gamma }}_4⊢[p^{+}\otimes r^{+}]}}\mathrm{F}-\mathrm{TensorR}}{{\mathrm{\Gamma }}_4;\cdot ⊢p^{+}\otimes r^{+}}}\mathrm{F}-\mathrm{ReleaseR}}{{\mathrm{\Gamma }}_4;\cdot ⊢\uparrow (p^{+}\otimes r^{+})}\mathrm{F}-\mathrm{UpR}.$$ Thus all four atoms are suspended before the sole right-focus phase begins.

Suppose the focused last rule is $$\frac{\begin{array}{c}{D}_P:\mathrm{\Gamma }⊢[P]\\ D_N:\mathrm{\Gamma };[N]⊢U\end{array}}{\mathrm{\Gamma };[P\Rightarrow N]⊢U}\mathrm{F}-\mathrm{ImpL}.$$ The two induction hypotheses, after inverting their final auxiliary rules, give $$E_P:{\mathrm{\Gamma }}^{\circ }⟹P^{\circ },E_N:{\mathrm{\Gamma }}^{\circ },N^{\circ }⟹U^{\circ }.$$ Weakening supplies $(P\Rightarrow N{)}^{\circ }$ in both contexts. Apply U-ImpL, contract its repeated principal formula, and then rebuild the auxiliary queue: $$\frac{{\displaystyle \frac{{\displaystyle \frac{\begin{array}{c}{\mathrm{\Gamma }}^{\circ },(P\Rightarrow N{)}^{\circ }⟹P^{\circ }\\ {\mathrm{\Gamma }}^{\circ },(P\Rightarrow N{)}^{\circ },N^{\circ }⟹U^{\circ }\end{array}}{{\mathrm{\Gamma }}^{\circ },(P\Rightarrow N{)}^{\circ }⟹U^{\circ }}}\mathrm{U}-\mathrm{ImpL}}{{\mathrm{\Gamma }}^{\circ },(P\Rightarrow N{)}^{\circ };\cdot ⟹U^{\circ }}}\mathrm{UQ}-\mathrm{Nil}}{{\mathrm{\Gamma }}^{\circ };(P\Rightarrow N{)}^{\circ }⟹U^{\circ }}\mathrm{UQ}-\mathrm{Cons}.$$ The upper two sequents are precisely the weakened forms of $E_P$ and $E_N$. This is part 3 of the de-focalization conclusion.

The principal pair is $$\frac{D:\mathrm{\Gamma };P⊢N}{\mathrm{\Gamma };\cdot ⊢P\Rightarrow N}\mathrm{F}-\mathrm{ImpR}\frac{\begin{array}{c}{E}_P:\mathrm{\Gamma }⊢[P]\\ E_N:\mathrm{\Gamma };[N]⊢U\end{array}}{\mathrm{\Gamma };[P\Rightarrow N]⊢U}\mathrm{F}-\mathrm{ImpL}.$$ Cut 1 on the immediate subformula $P$ gives $$\frac{\begin{array}{c}{E}_P:\mathrm{\Gamma }⊢[P]\\ D:\mathrm{\Gamma };P⊢N\end{array}}{\mathrm{\Gamma };\cdot ⊢N}\mathrm{Cut}-1.$$ Cut 2 on the immediate subformula $N$ then gives $$\frac{\begin{array}{c}\mathrm{\Gamma };\cdot ⊢N\\ E_N:\mathrm{\Gamma };[N]⊢U\end{array}}{\mathrm{\Gamma };\cdot ⊢U}\mathrm{Cut}-2.$$ Both calls have smaller cut formula than $P\Rightarrow N$, so the first component of the lexicographic measure decreases; no comparison of derivation heights is needed.

Let $D:\mathrm{\Gamma },⟨P\otimes Q⟩;\mathrm{\Omega }⊢U$. Weaken to $D^{\prime }$ in ${\mathrm{\Gamma }}^{\prime }=\mathrm{\Gamma },⟨P\otimes Q⟩,⟨P⟩,⟨Q⟩$. In ${\mathrm{\Gamma }}^{\prime }$, form $$\frac{\begin{array}{c}{\displaystyle \frac{\phantom{X}}{{\mathrm{\Gamma }}^{\prime }⊢[P]}}\mathrm{F}-\mathrm{IdPos}\\ {\displaystyle \frac{\phantom{X}}{{\mathrm{\Gamma }}^{\prime }⊢[Q]}}\mathrm{F}-\mathrm{IdPos}\end{array}}{{\mathrm{\Gamma }}^{\prime }⊢[P\otimes Q]}\mathrm{F}-\mathrm{TensorR}.$$ Apply SubstPos to this derivation and $D^{\prime }$, eliminating the compound suspension. The result is $$\mathrm{\Gamma },⟨P⟩,⟨Q⟩;\mathrm{\Omega }⊢U.$$ The induction hypothesis for $Q$ gives $\mathrm{\Gamma },⟨P⟩;Q,\mathrm{\Omega }⊢U$; the induction hypothesis for $P$ gives $\mathrm{\Gamma };P,Q,\mathrm{\Omega }⊢U$. Finally $$\frac{\mathrm{\Gamma };P,Q,\mathrm{\Omega }⊢U}{\mathrm{\Gamma };P\otimes Q,\mathrm{\Omega }⊢U}\mathrm{F}-\mathrm{TensorL}.$$ Both induction calls are on immediate subformulas, and focal substitution is uniform in the compound $P\otimes Q$.

For a positive conclusion, let the two induction hypotheses be $D_P:\mathrm{\Gamma };\cdot ⊢P$ and $D_Q:\mathrm{\Gamma };\cdot ⊢Q$. Put $H=\uparrow P$. Under $H,⟨P⟩,⟨Q⟩$, two F-IdPos rules, F-TensorR, and F-ReleaseR build the stable tensor. Positive expansion at $P$, F-UpL, and F-FocusL remove $⟨P⟩$. Expansion at $Q$ gives an inversion premise. Cut 4 with the weakened $D_Q$ removes it; F-UpR on $D_P$ and cut 3 remove $H$. The conclusion is $\mathrm{\Gamma };\cdot ⊢P\otimes Q$. The phase-changing rules are F-ReleaseR, F-UpL, F-FocusL, and F-UpR.

For the negative polarization, the induction hypotheses are $$D_N:\mathrm{\Gamma };\cdot ⊢\downarrow N,D_M:\mathrm{\Gamma };\cdot ⊢\downarrow M.$$ Rules F-IdNeg, F-FocusL, and F-DownL derive $\mathrm{\Gamma };\downarrow N⊢⟨N⟩$. Cut 4 with $D_N$ therefore gives $\mathrm{\Gamma };\cdot ⊢⟨N⟩$, and negative identity expansion $E_6(N)$ gives $\mathrm{\Gamma };\cdot ⊢N$. Repeating those named steps for $D_M$ gives $\mathrm{\Gamma };\cdot ⊢M$. Apply F-WithR, then Here F-DownR releases the right focus top down and F-ReleaseR starts it bottom up.

In the $p^{+}$-branch, the candidates can first enter in this order: The rule codes are F-IdPos, F-OrR2, F-ReleaseR, F-UpR, and F-SuspendPos. In the $q^{+}$-branch replace $p^{+}$ by $q^{+}$ and use F-OrR1; the remaining four rule kinds are unchanged. Once both fifth-stage candidates are present, F-OrL adds the disjunctive-queue conclusion and F-ImpR adds the original sequent.

A depth-first procedure may select the same persistent implication again after a downshift returns to the same stable goal. Formula size has then not decreased. Saturation has only one table entry for that candidate. Repeating the selection creates no new entry, so a finite table cannot follow the cycle forever.

The intuitionistic derivation is $$\frac{\begin{array}{c}{\displaystyle \frac{\phantom{X}}{⟨p^{+}⟩⊢[p^{+}]}}\mathrm{F}-\mathrm{IdPos}\\ {\displaystyle \frac{\phantom{X}}{⟨p^{+}⟩⊢[p^{+}]}}\mathrm{F}-\mathrm{IdPos}\end{array}}{⟨p^{+}⟩⊢[p^{+}\otimes p^{+}]}\mathrm{F}-\mathrm{TensorR}.$$ The same persistent context is present in both premises. A linear tensor rule would require a disjoint split ${\mathrm{\Delta }}_1\uplus {\mathrm{\Delta }}_2=\{⟨p^{+}⟩\}$. Exactly one side can contain the unique resource. The other side would have to derive $p^{+}$ in right focus from the empty resource context, but the only atomic right-focus rule is identity and its membership premise fails. Inversion on the proposed linear tensor rule therefore proves underivability.

For queued conjunction, induction on $\mathrm{\Psi }$ moves its head past $A,B$, uses the induction hypothesis, exchanges it back, and rebuilds UQ-Cons. At $\mathrm{\Psi }=\cdot$, weaken by $A\wedge B$, apply U-AndL2 and U-AndL1, and use UQ-Nil. The disjunction proof performs the same induction in both premises and uses U-OrL at the empty queue. The falsehood proof has no premises and uses U-BotL at the empty queue.

The simultaneous de-focalization induction then has the following complete rule-family map. Positive right focus erases to the matching ordinary right rule; F-DownR erases its shift and F-IdPos becomes U-Init. Positive inversion uses the three queued lemmas for zero, disjunction, and tensor; downshift only moves a formula and positive unit uses weakening. Negative inversion maps implication, with, and unit to U-ImpR, U-AndR, and U-TopR; upshift erases. Positive suspension is one UQ-Cons; negative suspension erases identically. F-ReleaseR preserves the right-focus induction hypothesis. F-FocusL inverts UQ-Cons and UQ-Nil, contracts the selected hypothesis, and restores UQ-Nil. F-UpL erases its shift; F-ImpL is the displayed construction in exercise 39.5; the two with projections use the matching ordinary conjunction-left rule. Finally, at F-IdNeg, suspension-normality forces $N=p^{-}$. The erased branch is $$\frac{{\displaystyle \frac{{\displaystyle \frac{p\in {\mathrm{\Gamma }}^{\circ },p}{{\mathrm{\Gamma }}^{\circ },p⟹p}}\mathrm{U}-\mathrm{Init}}{{\mathrm{\Gamma }}^{\circ },p;\cdot ⟹p}}\mathrm{UQ}-\mathrm{Nil}}{{\mathrm{\Gamma }}^{\circ };p⟹p}\mathrm{UQ}-\mathrm{Cons}.$$ These entries account for every primitive focused rule and prove all three clauses simultaneously.

For positive disjunction, start with $D:\mathrm{\Gamma },⟨P\vee Q⟩;\mathrm{\Omega }⊢U$. In the first branch weaken by $⟨P⟩$, use F-IdPos and F-OrR1 to build $[P\vee Q]$, and apply SubstPos to $D$. Expand the smaller $P$. The second branch uses F-OrR2 and expands the smaller $Q$. Rule F-OrL joins the results. Positive unit builds $[{\mathbf{1}}^{+}]$ by F-OnePosR, substitutes it for the compound suspension, and applies F-OnePosL; it has no induction hypothesis.

For $\downarrow N$, weaken by the persistent $N$. Focus on that hypothesis, apply F-IdNeg, and expand the smaller $N$; F-DownR supplies $[\downarrow N]$. Positive focal substitution removes $⟨\downarrow N⟩$, and F-DownL moves $N$ back from the queue. For $\uparrow P$, build the left focus $[\uparrow P]$, apply F-UpL, expand the smaller $P$, use negative focal substitution on $⟨\uparrow P⟩$, and finish with F-UpR.

Negative unit is F-OneNegR; the suspended premise is unused by weakening. For , use F-WithL1 followed by F-IdNeg to obtain $⟨N⟩$ from a focus on the compound, and similarly use F-WithL2 for $⟨M⟩$. Substitute the suspended compound into each projection, expand the smaller $N$ and $M$, and join them by F-WithR. Thus every induction hypothesis is on an immediate subformula; atoms are exactly F-SuspendPos and F-SuspendNeg.