Polarization, Focusing, and Proof Search

Proof. Fix one of the five rules and induct on the given derivation of its conclusion. If the last rule introduces the connective being inverted, its immediate premise or premises are the required sequents; set weakening restores any repeated assumption. Otherwise apply the induction hypothesis to every premise of the last rule and reapply that rule. For example, to invert U-AndR over a final U-OrL deriving $\mathrm{\Gamma },A\vee B⟹C\wedge D$, apply the induction hypothesis to both U-OrL premises to derive $C$ and $D$ from each of $\mathrm{\Gamma },A$ and $\mathrm{\Gamma },B$; rebuild U-OrL once for $C$ and once for $D$, then apply U-AndR. The other nonprincipal rule pairs use the same premise-by-premise commutation. An initial or nullary last rule closes because its triggering atom or $\mathrm{\perp }$ remains a member after the required set extension. These cases cover every last rule of definition 39.1.

For U-AndL1 and U-AndL2, invertibility is the direct weakening fact: a derivation from $\mathrm{\Gamma },A\wedge B$ remains a derivation after adding $A$ or $B$. This unfocused invertibility does not determine the focused phase of a polarization; negative -left retains a genuine choice between its projections. ◻

Proof. Inspect the rules and induct on derivation height. The only rule that adds a positive suspension to the persistent context is F-SuspendPos; it adds exactly $⟨p^{+}⟩$. A suspension exposed by F-IdNeg is already in its conclusion, so normality forces its formula to be the atom $p^{-}$. Every other rule preserves existing suspensions and introduces none. ◻

Proof. Induct on the focused derivation, enlarging $\mathrm{\Gamma }$ uniformly in every premise. Membership premises remain true. In F-FocusL, retain the same selected negative hypothesis; in F-IdPos, retain the same suspended member. Every other rule reapplies directly to the induction hypotheses. ◻

Proof. All three clauses use induction on $\mathrm{\Psi }$. We write the conjunction case because it contains the entire mechanism. If $\mathrm{\Psi }=D,{\mathrm{\Psi }}^{\prime }$, invert UQ-Cons, apply the induction hypothesis at the finite-set context $\mathrm{\Gamma },D$, and rebuild UQ-Cons. If $\mathrm{\Psi }=\cdot$, inversion gives $\mathrm{\Gamma },A,B⟹C$. Weaken by $A\wedge B$, apply U-AndL2 and then U-AndL1, and finish with UQ-Nil.

For disjunction, apply the two induction hypotheses at $\mathrm{\Gamma },D$ and rebuild UQ-Cons. At the empty list, weaken both ordinary premises by $A\vee B$, apply U-OrL, and use UQ-Nil. For falsehood, recurse down a nonempty list; at the empty list use U-BotL followed by UQ-Nil. Thus every positive-left rule is available underneath the whole queue. ◻

Proof. Induct simultaneously on the three displayed derivations. When an induction hypothesis for a right-focus premise ends in UQ-Nil, invert that auxiliary rule, apply the corresponding ordinary right rule, and restore UQ-Nil.

For F-TensorR, for example, the two inversions give ${\mathrm{\Gamma }}^{\circ }⟹P^{\circ }$ and ${\mathrm{\Gamma }}^{\circ }⟹Q^{\circ }$. Rule U-AndR gives ${\mathrm{\Gamma }}^{\circ }⟹P^{\circ }\wedge Q^{\circ }$, and UQ-Nil $${\mathrm{\Gamma }}^{\circ };\cdot ⟹P^{\circ }\wedge Q^{\circ }.$$ For F-OrR1 and F-OrR2, apply the corresponding ordinary disjunction rule to derive ${\mathrm{\Gamma }}^{\circ }⟹P^{\circ }\vee Q^{\circ }$. For positive unit, U-TopR derives ${\mathrm{\Gamma }}^{\circ }⟹\mathrm{\top }$. F-DownR changes no erased formula. Suspension-normality makes the F-IdPos formula an atom. Since $⟨p^{+}⟩\in \mathrm{\Gamma }$, its erasure belongs to ${\mathrm{\Gamma }}^{\circ }$, and the erased derivation is exactly $$\frac{{\displaystyle \frac{p\in {\mathrm{\Gamma }}^{\circ }}{{\mathrm{\Gamma }}^{\circ }⟹p}}\mathrm{U}-\mathrm{Init}}{{\mathrm{\Gamma }}^{\circ };\cdot ⟹p}\mathrm{UQ}-\mathrm{Nil}.$$

For positive inversion, F-DownL merely moves the same erased formula from the queue to the persistent context, and F-OnePosL erases by weakening. The zero, disjunction, and tensor cases use the three clauses of lemma 39.12. In the tensor case the induction hypothesis is $${\mathrm{\Gamma }}^{\circ };P^{\circ },Q^{\circ },{\mathrm{\Omega }}^{\circ }⟹U^{\circ };$$ clause 1 turns it into ${\mathrm{\Gamma }}^{\circ };P^{\circ }\wedge Q^{\circ },{\mathrm{\Omega }}^{\circ }⟹U^{\circ }$, exactly the erased conclusion.

For negative inversion, F-ImpR becomes U-ImpR, F-WithR becomes U-AndR, negative unit becomes U-TopR, and F-UpR forgets the shift. In F-SuspendNeg, the premise and conclusion have the same erasure. The positive suspension rule instead changes the queue. Its induction hypothesis is $${\mathrm{\Gamma }}^{\circ },p;{\mathrm{\Omega }}^{\circ }⟹U^{\circ }.$$ One use of UQ-Cons gives precisely ${\mathrm{\Gamma }}^{\circ };p,{\mathrm{\Omega }}^{\circ }⟹U^{\circ }$, the erased conclusion of F-SuspendPos.

It remains to check the two choices of focus. For F-ReleaseR, the right-focus induction hypothesis already is ${\mathrm{\Gamma }}^{\circ };\cdot ⟹P^{\circ }$, which is the erased conclusion. Suppose F-FocusL selected the persistent hypothesis $N$. Part 3 of the induction hypothesis gives $${\mathrm{\Gamma }}^{\circ },N^{\circ };N^{\circ }⟹U^{\circ }.$$ Invert UQ-Cons and then UQ-Nil; contract the duplicate $N^{\circ }$; and reapply UQ-Nil. The result is ${\mathrm{\Gamma }}^{\circ },N^{\circ };\cdot ⟹U^{\circ }$, exactly the erased focus conclusion.

For F-UpL, the premise and conclusion erase identically. For F-WithL1 and F-WithL2, invert the leading UQ-Cons and UQ-Nil in the induction hypothesis. Weaken the resulting ordinary sequent by $N^{\circ }\wedge M^{\circ }$, apply respectively U-AndL1 or U-AndL2, and restore UQ-Nil and UQ-Cons. In F-ImpL, the first induction hypothesis yields ${\mathrm{\Gamma }}^{\circ }⟹P^{\circ }$. Inverting the leading auxiliary rule in the second yields ${\mathrm{\Gamma }}^{\circ },N^{\circ }⟹U^{\circ }$. Put $H=(P\Rightarrow N{)}^{\circ }$. Weaken both ordinary sequents by $H$, apply U-ImpL, and contract its repeated principal formula. Then UQ-Nil followed by UQ-Cons moves $H$ from the ordinary context into the one-formula auxiliary queue, producing ${\mathrm{\Gamma }}^{\circ };H⟹U^{\circ }$. This is the erased conclusion; no premise that $H$ was already stored is needed.

Finally, suspension-normality forces the suspended conclusion of F-IdNeg to be atomic, so put $N=p^{-}$. Its erasure is the explicit tree $$\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}.$$ Thus negative identity needs queued membership rather than ordinary context membership. The inversion, right-focus, left-focus, release, suspension, and identity cases of definition 39.8 have each been translated. ◻

Proof. For SubstPos, induct on the second derivation. If it ends in F-IdPos using the distinguished suspension, return the first derivation. If it uses another suspension, rebuild F-IdPos. Every logical rule is rebuilt after applying the induction hypothesis to each premise. In the F-DownL case, set inclusion permits weakening by the persistent assumption introduced in its conclusion. For SubstNeg, induct on the first derivation. Its F-IdNeg endpoint returns the second derivation. If the first derivation ends in F-FocusL, write its premise as $\mathrm{\Gamma },M;[M]⊢⟨N⟩$. The induction hypothesis with the second substitution premise gives $\mathrm{\Gamma },M;[M]⊢U$; since a left-focus judgment requires stable $U$, reapplying F-FocusL derives $\mathrm{\Gamma },M;\cdot ⊢U$. Every other rule is rebuilt after applying the induction hypothesis to each premise. No connective case inspects $P$ or $N$; that uniformity is why compound suspensions were admitted in remark 39.11. ◻

Proof. Write $C_i(\mathcal{D},\mathcal{E})$ for the cut carrying that name with its two displayed input derivations. The four cuts are defined simultaneously. The naive rank $(|A|,h(\mathcal{D})+h(\mathcal{E}))$ fails on a phase commutation. When $C_4$ crosses F-ReleaseR, the recursive call is $$C_4(P;\mathcal{D},\mathsf{ReleaseR}(\mathcal{E}))\stackrel{F-ReleaseR}{{⇝}_0}{C}_1(P;\mathcal{D},\mathcal{E}).$$ The formula is still $P$, and exposing $\mathcal{E}$ need not reduce the sum of the two input heights after the reconstructed phase boundary. The missing descent is therefore the operation change . Order every call—including $C_1$ and $C_2$—by the lexicographic triple $$(|A|,i,h(\mathcal{D})+h(\mathcal{E})),$$ where $A$ is its cut formula and the operation order is and $h$ counts rule instances. Thus a recursive call may change derivations arbitrarily after the formula or operation component has decreased; when those two components are unchanged, it must use a strict premise and hence decrease the height sum. The recursive calls and their decreasing components are as follows.

Atomic principal cuts are exactly the positive and negative instances of the general focal-substitution lemma lemma 39.14; they are not additional base rules of the calculus. Positive zero has no right introduction, so its principal case is impossible.

Two principal reductions carry the mechanism used later. If a $C_1$ cut on $P\otimes Q$ meets F-TensorR and F-TensorL, its upper fragment is $$\frac{\begin{array}{c}{D}_P:\mathrm{\Gamma }⊢[P]\\ D_Q:\mathrm{\Gamma }⊢[Q]\end{array}}{\mathrm{\Gamma }⊢[P\otimes Q]}\mathrm{F}-\mathrm{TensorR}$$ and $$\frac{E:\mathrm{\Gamma };P,Q,\mathrm{\Omega }⊢U}{\mathrm{\Gamma };P\otimes Q,\mathrm{\Omega }⊢U}\mathrm{F}-\mathrm{TensorL}.$$ First apply $C_1(D_P,E)$, obtaining $\mathrm{\Gamma };Q,\mathrm{\Omega }⊢U$, and then apply $C_1$ with $D_Q$. Both calls cut immediate subformulas. The result is $\mathrm{\Gamma };\mathrm{\Omega }⊢U$.

For a $C_2$ cut on $P\Rightarrow N$, the two principal derivations end as $$\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}.$$ The smaller positive cut $C_1(E_P,D)$ yields $\mathrm{\Gamma };\cdot ⊢N$. The smaller negative cut with $E_N$ then yields $\mathrm{\Gamma };\cdot ⊢U$. The order matters: the antecedent cut produces the derivation used by the consequent cut.

The shift cases show how the four operations meet. In the downshift case, write the premises of the two last rules as $$D:\mathrm{\Gamma };\cdot ⊢N,E:\mathrm{\Gamma },N;\mathrm{\Omega }⊢U.$$ The displayed F-DownR/F-DownL cut $$\frac{D}{\mathrm{\Gamma }⊢[\downarrow N]}\mathrm{F}-\mathrm{DownR}\frac{E}{\mathrm{\Gamma };\downarrow N,\mathrm{\Omega }⊢U}\mathrm{F}-\mathrm{DownL}$$ therefore reduces exactly to $C_3(D,E):\mathrm{\Gamma };\mathrm{\Omega }⊢U$, whose cut formula is the proper subformula $N$. Dually, if $D:\mathrm{\Gamma };L⊢P$ and $E:\mathrm{\Gamma };P⊢U$, the F-UpR/F-UpL instance of $C_2$ reduces to $C_4(D,E):\mathrm{\Gamma };L⊢U$, cutting the proper subformula $P$. Disjunction chooses the branch selected by the right introduction; positive unit deletes the cut; negative conjunction keeps the selected projection; negative unit has no principal left case. These clauses account for every row of the table.

The outermost phases of $C_1$ and $C_2$ expose their cut formula, so they have no additional phase-commutative case. Their nonprincipal logical cases are the ordinary strict-premise commutations already covered by the table. For a commutative cut, rebuild the last rule that does not expose the cut formula and apply the same $C_i$ to each premise. The height component decreases. This statement includes every unary rule and both premises of F-OrL, F-TensorR, and F-WithR. There are two phase cases where height alone is not the reason. If the first derivation of $C_4$ ends in $$\frac{\mathrm{\Gamma }⊢[P]}{\mathrm{\Gamma };\cdot ⊢P}\mathrm{F}-\mathrm{ReleaseR},$$ invoke $C_1$ with the same second derivation; the operation component decreases from 4 to 1. If the second derivation of $C_3$ ends by selecting the distinguished $N$, its premise is $\mathrm{\Gamma },N;[N]⊢U$. First apply $C_3$ recursively to that strict premise, obtaining $\mathrm{\Gamma };[N]⊢U$; the height component decreases. Then invoke $C_2$ with this derived left-focus premise; the operation component decreases from 3 to 2. This preliminary $C_3$ substitution is essential: the raw premise still contains the distinguished persistent assumption and therefore is not an input to $C_2$. If F-FocusL selects another hypothesis, commute through the rule and use the height component. No rule family remains, so the simultaneous recursion is total. ◻

Proof. For identity expansion, induct on the displayed proposition. The atomic positive and negative cases are respectively F-SuspendPos and F-SuspendNeg. Positive zero uses F-ZeroL; positive unit uses F-OnePosL; disjunction expands both branches and applies F-OrL; downshift first expands the negative subformula and then applies F-DownL. Negative unit uses F-OneNegR; negative conjunction expands the two projections and joins them by F-WithR; and upshift uses positive expansion followed by F-UpR.

Here is the full tensor step. Given $D:\mathrm{\Gamma },⟨P\otimes Q⟩;\mathrm{\Omega }⊢U$, weaken it to $D^{\prime }$ with $⟨P⟩$ and $⟨Q⟩$. Put $${\mathrm{\Gamma }}^{\prime }=\mathrm{\Gamma },⟨P\otimes Q⟩,⟨P⟩,⟨Q⟩.$$ Then 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}.$$ Positive focal substitution removes the compound suspension from $D^{\prime }$. The induction hypothesis for $Q$, then the one for $P$, changes the queue to $P,Q,\mathrm{\Omega }$; F-TensorL gives the required conclusion. Every expansion call is on an immediate subformula.

For the implication step, begin with $D:\mathrm{\Gamma };\cdot ⊢⟨P\Rightarrow N⟩$ and weaken by $⟨P⟩$. The derivation $$\frac{\begin{array}{c}{\displaystyle \frac{\phantom{X}}{\mathrm{\Gamma },⟨P⟩⊢[P]}}\mathrm{F}-\mathrm{IdPos}\\ {\displaystyle \frac{\phantom{X}}{\mathrm{\Gamma },⟨P⟩;[N]⊢⟨N⟩}}\mathrm{F}-\mathrm{IdNeg}\end{array}}{\mathrm{\Gamma },⟨P⟩;[P\Rightarrow N]⊢⟨N⟩}\mathrm{F}-\mathrm{ImpL}$$ is the required focused use of the implication. Negative focal substitution with the weakened $D$ produces $\mathrm{\Gamma },⟨P⟩;\cdot ⊢⟨N⟩$. Expand $N$, expand $P$ from suspension into the inversion queue, and finish with F-ImpR. This proves negative implication expansion without assuming either ordinary identity or focalization. The displayed cases plus the preceding connective clauses exhaust both grammars, completing the mutual proof. ◻

Proof. Induct on $P$ and $N$. Every case not beginning with two adjacent shifts chooses the formula itself. If $P=\downarrow \uparrow Q$, apply the positive induction hypothesis to obtain $Q_0$. From a derivation of $Q_0$, reconstruct $Q$, apply F-UpR, F-DownR, and F-ReleaseR; this derives $\downarrow \uparrow Q$. If $N=\uparrow \downarrow M$, reconstruct $M$ under the selected hypothesis, then apply F-DownL, F-UpL, and F-FocusL. Both recursive calls remove the outer adjacent pair before inspecting the remaining subformula, so the induction is structural. ◻

Proof. All constructions below use only the primitive focused rules, weakening and contraction of the persistent context, the four cuts of theorem 39.15, and the two expansions of theorem 39.16. In particular, no step converts an arbitrary stable derivation of $P$ into a right-focused derivation of $P$.

Right rules.

The positive-disjunction construction starts from $D_P:\mathrm{\Gamma };\cdot ⊢P$. In $\mathrm{\Gamma },⟨P⟩$, rules F-IdPos, F-OrR1, and F-ReleaseR derive $P\vee Q$. Operation $E_5(P)$ changes this derivation to $\mathrm{\Gamma };P⊢P\vee Q$, and $C_4(D_P,-)$ removes the queued $P$. The second injection uses F-OrR2 and $D_Q$.

For positive conjunction, let $$D_P:\mathrm{\Gamma };\cdot ⊢P,D_Q:\mathrm{\Gamma };\cdot ⊢Q,H=\uparrow P.$$ Put ${\mathrm{\Gamma }}^{\prime }=\mathrm{\Gamma },H,⟨P⟩,⟨Q⟩$. Two suspended identities, F-TensorR, and F-ReleaseR give $${\mathrm{\Gamma }}^{\prime };\cdot ⊢P\otimes Q.$$ Apply $E_5(P)$, then F-UpL and F-FocusL at $H$, to obtain $\mathrm{\Gamma },H,⟨Q⟩;\cdot ⊢P\otimes Q$. Next $E_5(Q)$ gives a $Q$-queue. Cut in the weakened $D_Q$ with $C_4$, derive $H$ from $D_P$ by F-UpR, and discharge $H$ with $C_3$. The resulting stable conclusion is $\mathrm{\Gamma };\cdot ⊢P\otimes Q$.

For negative conjunction, a stable premise $D_N:\mathrm{\Gamma };\cdot ⊢\downarrow N$ is converted to a native negative result without inversion of $D_N$. The rules F-IdNeg, F-FocusL, and F-DownL give $$\mathrm{\Gamma };\downarrow N⊢⟨N⟩.$$ Thus $C_4(D_N,-)$ derives $\mathrm{\Gamma };\cdot ⊢⟨N⟩$, and $E_6(N)$ derives $\mathrm{\Gamma };\cdot ⊢N$. Repeat this construction for $M$, apply F-WithR, then F-DownR and F-ReleaseR. This proves the stable rule with conclusion .

The implication-right case is the shift-sensitive one. Suppose $$D:\mathrm{\Gamma },\uparrow P;\cdot ⊢\downarrow N.$$ Abbreviate $$H=\uparrow P,G=\downarrow N,K=(\downarrow H)\Rightarrow (\uparrow G).$$ Applying F-UpR, F-DownL, and F-ImpR to $D$ gives $$\begin{array}{}\text{(}1\text{)}& J:\mathrm{\Gamma };\cdot ⊢K.\end{array}$$ It remains to build the desired implication under the bridge hypothesis $K$. Put $\mathrm{\Delta }=\mathrm{\Gamma },K,⟨P⟩$. From the suspended $P$, rules F-IdPos, F-ReleaseR, F-UpR, and F-DownR derive $$\begin{array}{}\text{(}2\text{)}& \mathrm{\Delta }⊢[\downarrow H].\end{array}$$ Independently, F-IdNeg, F-FocusL, F-DownL, and F-UpL derive $$\begin{array}{}\text{(}3\text{)}& \mathrm{\Delta };[\uparrow G]⊢⟨N⟩.\end{array}$$ Use F-ImpL on (2) and (3), select $K$ with F-FocusL, and apply $E_6(N)$: $$\begin{array}{}\text{(}4\text{)}& \mathrm{\Delta };\cdot ⊢N.\end{array}$$ Operation $E_5(P)$ changes (4) into $\mathrm{\Gamma },K;P⊢N$. Now F-ImpR, F-DownR, and F-ReleaseR give $$\begin{array}{}\text{(}5\text{)}& I:\mathrm{\Gamma },K;\cdot ⊢\downarrow (P\Rightarrow N).\end{array}$$ Finally $C_3(J,I)$ removes $K$. Every endpoint in this chain is a well-formed focused judgment; in particular, the given premise and the conclusion are stable.

The positive and negative unit conclusions use F-OnePosR and F-OneNegR; the negative unit is then enclosed by F-DownR and F-ReleaseR.

Left rules.

For disjunction, write $$H=\uparrow (P\vee Q),P^{\prime }=\downarrow \uparrow P.$$ In $\mathrm{\Gamma },H,⟨P⟩$, suspended identity followed by F-UpR, F-DownR, and F-ReleaseR derives $P^{\prime }$. Operation $E_5(P)$ therefore gives $$J_P:\mathrm{\Gamma },H;P⊢P^{\prime }.$$ Weaken $D_P:\mathrm{\Gamma },\uparrow P;\cdot ⊢U$ by $H$, and use F-DownL to derive $\mathrm{\Gamma },H;P^{\prime }⊢U$. Operation $C_4(J_P,-)$ gives the $P$-branch $\mathrm{\Gamma },H;P⊢U$. Replacing $P$ by $Q$ gives the other branch. Apply F-OrL, F-UpL, and F-FocusL to obtain $\mathrm{\Gamma },H;\cdot ⊢U$.

For positive conjunction left, put $$H=\uparrow (P\otimes Q),R=(\downarrow \uparrow P)\otimes (\downarrow \uparrow Q).$$ In $\mathrm{\Gamma },H,⟨P⟩,⟨Q⟩$, build a right focus on $R$ from the two suspended identities, using the shift rules on each component. Release that focus, then apply $E_5(Q)$ and $E_5(P)$. The result is $$J:\mathrm{\Gamma },H;P,Q⊢R.$$ From $D:\mathrm{\Gamma },\uparrow P,\uparrow Q;\cdot ⊢U$, weakening by $H$, two uses of F-DownL, and F-TensorL derive $$E:\mathrm{\Gamma },H;R⊢U.$$ Now apply $C_4(J,E)$, then F-TensorL, F-UpL, and F-FocusL. The result is $$\mathrm{\Gamma },H;\cdot ⊢U.$$

For the first negative-conjunction projection, put . Under $H$, rules F-IdNeg, F-WithL1, and F-FocusL, followed by $E_6(N)$, derive $$J_N:\mathrm{\Gamma },H;\cdot ⊢N.$$ Weaken $D_N:\mathrm{\Gamma },N;\cdot ⊢U$ by $H$ and apply $C_3(J_N,D_N)$. For the second projection, exchange F-WithL1 for F-WithL2 and $N$ for $M$ throughout.

For implication left, put $H=P\Rightarrow N$. Under $\mathrm{\Gamma },H,⟨P⟩$, rules F-IdPos, F-IdNeg, F-ImpL, and F-FocusL derive $⟨N⟩$. Apply $E_6(N)$, enclose the result in $\downarrow N$, and use $E_5(P)$ to obtain $$E:\mathrm{\Gamma },H;P⊢\downarrow N.$$ Cut the weakened $D_P:\mathrm{\Gamma };\cdot ⊢P$ into $E$ with $C_4$. Weaken $D_U:\mathrm{\Gamma },N;\cdot ⊢U$ by $H$, apply F-DownL, and use $C_4$ once more. The result is $\mathrm{\Gamma },H;\cdot ⊢U$.

Finally, F-ZeroL, F-UpL, and F-FocusL give falsehood left. Positive atomic identity is F-IdPos followed by F-ReleaseR; a shifted positive hypothesis is selected with F-FocusL, decomposed by F-UpL, and suspended by F-SuspendPos. Negative atomic identity is F-FocusL over F-IdNeg; a downshifted conclusion continues with F-SuspendNeg, F-DownR, and F-ReleaseR. These cases exhaust definition 39.1; lemma 39.17 restores any removed adjacent shifts. ◻

Proof. Induct on the given unfocused derivation. For every noninitial last rule, apply the induction hypothesis to its one or two premises using the stable polarizations fixed by the immediate subformulas of the principal formula. Thus a positive premise appears as a stable positive succedent or an upshifted persistent hypothesis, and a negative premise appears as a downshifted succedent or a native persistent hypothesis. These are exactly the endpoints stated in lemma 39.18. Apply the matching clause of lemma 39.18. This treats separately the right rule families for truth, disjunction, conjunction, and implication, and the left rule families for falsehood, disjunction, both conjunction projections, and implication.

If the last rule is U-Init, suspension-normality leaves four base shapes before adjacent shifts are restored. They are The first is F-IdPos followed by F-ReleaseR. For the second, select $\uparrow p^{+}$, apply F-UpL, suspend the queued atom, and use the first derivation. The third is F-FocusL over F-IdNeg. The fourth continues the third with F-SuspendNeg, F-DownR, and F-ReleaseR. These are exactly the two atom polarities and the two possible suspension locations. Identity expansion handles a compound suspension used internally, and lemma 39.17 restores any alternating outer shifts.

Every recursive appeal is on an immediate premise derivation. Because the polarization cases add rules only after those appeals return, derivation height strictly decreases and the induction is well founded. ◻

Proof. Choose recursively an all-negative polarization $N(C)$ of each ordinary formula $C$, and put $P(C)=\downarrow N(C)$. Polarize every member of $\mathrm{\Gamma }$ by $N(-)$, the cut occurrence in the second premise by $N(A)$, and the two premise conclusions by $P(A)$ and $P(B)$, respectively. Focalize derivations of $\mathrm{\Gamma }⟹A$ and $\mathrm{\Gamma },A⟹B$, obtaining $$D:{\mathrm{\Gamma }}^N;\cdot ⊢\downarrow N(A),E:{\mathrm{\Gamma }}^N,N(A);\cdot ⊢P(B).$$ Apply F-DownL to $E$, giving ${\mathrm{\Gamma }}^N;\downarrow N(A)⊢P(B)$. Cut $D$ into this derivation with $C_4$ of theorem 39.15, then de-focalize the resulting ${\mathrm{\Gamma }}^N;\cdot ⊢P(B)$. This yields $\mathrm{\Gamma }⟹B$.

The cut-free rules of definition 39.1 introduce in a premise only an immediate subformula of the principal conclusion formula (while retaining that principal formula on the left), so induction on a cut-free derivation gives the subformula property. No rule can be last in a derivation of the empty-context sequent $\cdot ⟹\mathrm{\perp }$. ◻