Bunched Implications and Resource Semantics

Proof. Antecedents are congruence classes by definition 43.3; the first statement is equality of sequents. The second is the congruence clause in the same definition. No logical or structural rule is required. ◻

Proof. Apply W or C, respectively, at the displayed hole. Structural- congruence invariance permits reassociation and exchange inside the additive subtree before or after the application. Because the surrounding object is a one-hole bunch context, neither rule changes any multiplicative ancestor. ◻

Proof. Induct on $A$. Atoms use Id. The two units use their right and left rules: $$\frac{{ϵ}_{\mathrm{a}}⊢\mathrm{\top }}{\mathrm{\top }⊢\mathrm{\top }}\mathrm{Top}-\mathrm{L}\frac{{ϵ}_{\mathrm{m}}⊢\mathsf{I}}{\mathsf{I}⊢\mathsf{I}}\mathrm{I}-\mathrm{L}.$$ For conjunction and multiplicative conjunction, use the induction hypotheses in the corresponding right rule, then expose the two assumptions with the left rule: $$\frac{{\displaystyle \frac{\begin{array}{c}A⊢A\\ B⊢B\end{array}}{A;B⊢A\wedge B}}\mathrm{And}-\mathrm{R}}{A\wedge B⊢A\wedge B}\mathrm{And}-\mathrm{L},$$ $$\frac{{\displaystyle \frac{\begin{array}{c}A⊢A\\ B⊢B\end{array}}{A,B⊢A\ast B}}\mathrm{Star}-\mathrm{R}}{A\ast B⊢A\ast B}\mathrm{Star}-\mathrm{L}.$$ For disjunction, introduce the selected injection in each branch and eliminate the assumption: $$\frac{\begin{array}{c}{\displaystyle \frac{A⊢A}{A⊢A\vee B}}\mathrm{Or}-{\mathrm{R}}_1\\ {\displaystyle \frac{B⊢B}{B⊢A\vee B}}\mathrm{Or}-{\mathrm{R}}_2\end{array}}{A\vee B⊢A\vee B}\mathrm{Or}-\mathrm{L}.$$ For additive implication, Imp-L and the induction hypotheses give $A;(A\to B)⊢B$. Additive commutativity turns this into $(A\to B);A⊢B$, and Imp-R yields $A\to B⊢A\to B$. The wand case is the same calculation with comma: $$\frac{{\displaystyle \frac{\begin{array}{c}A⊢A\\ B⊢B\end{array}}{A,(A-\ast B)⊢B}}\mathrm{Wand}-\mathrm{L}}{A-\ast B⊢A-\ast B}\mathrm{Wand}-\mathrm{R},$$ where multiplicative commutativity rewrites $A,(A-\ast B)⊢B$ as $(A-\ast B),A⊢B$, the premise required by Wand-R. These cases exhaust the grammar. ◻

Proof. Induct on the rank $\rho (({\mathcal{D}}_i{)}_{i=1}^n,\mathcal{E};A)$ from definition 43.7. The proof is organized into identity, commuting, one-sided principal, structural, and two-sided principal cases. Antecedents are congruence classes, so no congruence inference must be commuted: every rule instance may first be reassociated and exchanged until its displayed subtree is visible.

Identity cases.

If $n=0$, return $\mathcal{E}$. If $\mathcal{E}$ is the atomic identity $p⊢p$, its only displayed occurrence is the antecedent $p=A$, and the required derivation is ${\mathcal{D}}_1$. If some ${\mathcal{D}}_i$ is the atomic identity $p⊢p$, remove hole $i$ from the family: replacing that occurrence by its antecedent changes no sequent. The third rank component strictly decreases unless this was the only hole, in which case return $\mathcal{E}$.

Commuting through the right derivation.

Suppose no selected occurrence is principal in the last rule $R$ of $\mathcal{E}$. Distribute the numbered holes among the premises, apply the induction hypothesis to every premise containing at least one hole, and reapply $R$. The cut formula is unchanged, but each recursive call uses a proper premise of $\mathcal{E}$, so the second rank component decreases. The nonstructural distribution is as follows.

Identity was handled above, while W and C are handled separately below. Rules Top-R and I-R have antecedent units and therefore contain no selected formula occurrence unless $n=0$, which is the first identity case. For example, in the repeated-derivation specialization, if holes are split between the two premises of Star-R, $$\frac{\begin{array}{c}\mathcal{D}:\mathrm{\Delta }⊢A\\ {\displaystyle \frac{\begin{array}{c}{\mathcal{E}}_1:{\mathcal{M}}_1[A^i]⊢C\\ {\mathcal{E}}_2:{\mathcal{M}}_2[A^j]⊢D\end{array}}{{\mathcal{M}}_1[A^i],{\mathcal{M}}_2[A^j]⊢C\ast D}}\mathrm{Star}-\mathrm{R}\end{array}}{{\mathcal{M}}_1[{\mathrm{\Delta }}^i],{\mathcal{M}}_2[{\mathrm{\Delta }}^j]⊢C\ast D}\mathrm{MCut}$$ reduces to Star-R applied to the two recursively normalized premises. For Or-L, apply the induction hypothesis to both branches and reapply the same Or-L; both calls have smaller right height.

Commuting through the left derivation.

Choose one index $i$ such that the last rule $R$ of ${\mathcal{D}}_i$ does not introduce the outer connective of $A$. Replace only member $i$ by each premise of $R$ whose succedent is $A$, recurse, retain any auxiliary premise with a different succedent, and reapply $R$ at hole $i$. The cut formula and right derivation are unchanged, while the sum of left heights strictly decreases. No logical right rule occurs in this case: every right rule of ${\mathsf{LBI}}_0$ introduces the outer connective of its succedent. The possible nonprincipal rules are therefore left rules, W, and C.

The premise distribution is exhaustive. A one-premise left or structural rule has one recursive premise. Suppose member $i$ ends in Or-L with premises ${\mathcal{D}}_i^L:\mathcal{K}[E]⊢A$ and ${\mathcal{D}}_i^R:\mathcal{K}[F]⊢A$, where $\mathcal{K}[-]$ is a one-hole bunch context and $E,F$ are the disjuncts. Apply the induction hypothesis once to the family with member $i$ replaced by ${\mathcal{D}}_i^L$, and once with it replaced by ${\mathcal{D}}_i^R$. Rule Or-L combines the resulting derivations at occurrence $i$. If another member later also ends in Or-L, the outer induction repeats this construction in each existing branch. Thus two such members generate all four mixed choices, and $n$ such members generate the required $2^n$ branches; the proof does not retain only the two homogeneous branches. For Imp-L and Wand-L, the argument premise proves the antecedent of the implication and is retained unchanged; only the continuation premise has succedent $A$ and is recursive. Thus no auxiliary premise is mistaken for a derivation of the cut formula.

As a representative one-premise commutation, suppose $\mathcal{D}$ ends in Star-L: $$\frac{{\mathcal{D}}_0:\mathcal{K}[C,D]⊢A}{\mathcal{K}[C\ast D]⊢A}\mathrm{Star}-\mathrm{L}.$$ Replace member $i$ by ${\mathcal{D}}_0$ and recurse, obtaining a right derivation with $\mathcal{K}[C,D]$ at hole $i$ and all other replacements unchanged. Reapply Star-L at that hole to obtain $\mathcal{K}[C\ast D]$. This is exactly the required replacement for member $i$.

Additive weakening and contraction.

These cases are separated because contraction changes the number of displayed occurrences. Suppose $\mathcal{E}$ ends in W. Put every selected occurrence in the old subtree into one induction-hypothesis call on the premise. In the same rule instance, replace every selected occurrence in the newly added bunch $\mathrm{\Sigma }$ directly by its corresponding ${\mathrm{\Delta }}_i$, then reapply W. Thus one family may mix old and newly weakened occurrences: the old subfamily is handled recursively and the new subfamily is filled without a recursive cut because it was not used by the premise.

Suppose $\mathcal{E}$ ends in $$\frac{\mathcal{C}[\mathrm{\Xi };\mathrm{\Xi }]⊢B}{\mathcal{C}[\mathrm{\Xi }]⊢B}\mathrm{C}.$$ Form one recursive family containing every selected occurrence outside $\mathrm{\Xi }$ once and, for every selected occurrence inside $\mathrm{\Xi }$, both displayed descendants with the same corresponding derivation ${\mathcal{D}}_i$. Apply the induction hypothesis once to that whole mixed family and reapply C. Hence a family may simultaneously contain outside holes and holes duplicated inside $\mathrm{\Xi }$; no uniform-location assumption is being made. The right premise height has strictly decreased. Duplication may increase the third rank component, which is irrelevant after the second component has decreased.

If a selected ${\mathcal{D}}_i$ ends in W or C, recurse with its premise in member $i$, then reapply the same structural rule at that hole. Again the sum of left heights decreases. The heterogeneous family statement keeps both copies in this single recursive call.

One-sided principal cases.

Assume occurrence $i$ is principal in the last left rule of $\mathcal{E}$, but the last rule of ${\mathcal{D}}_i$ is not the matching right rule. The last rule of ${\mathcal{D}}_i$ then carries its succedent through a left or structural inference. Commute the multicut above that inference as in the left-derivation paragraph and reapply it at hole $i$. The third rank component decreases. Dually, if ${\mathcal{D}}_i$ introduces $A$ but occurrence $i$ is not principal in the last rule of $\mathcal{E}$, commute the cut above that last rule, decreasing $h(\mathcal{E})$. Thus the left-principal/right-nonprincipal and right-principal/left-nonprincipal cases each decrease the corresponding derivation height.

Other numbered occurrences in a principal case.

Before reducing the principal occurrence, push the cut into every proper premise of the final left rule for all other numbered holes. Those recursive calls retain the cut formula $A$ but use a smaller right-derivation height. In Or-L, a surrounding hole is processed in both branch premises; in Imp-L and Wand-L, holes are sent to the argument premise when the occurrence lies in its antecedent bunch, and otherwise to the continuation premise. After these calls, every nonprincipal occurrence has been replaced by its corresponding ${\mathrm{\Delta }}_j$, while the one principal occurrence remains exposed as the immediate subformula bunch of the left rule. Apply the one-occurrence principal reduction for that connective; its recursive cuts use proper subformulas of $A$. Thus a principal step with any finite number of additional holes first decreases the second rank component and then the first; no unlisted family of mixed principal/nonprincipal occurrences remains.

Two-sided principal units.

For $A=\mathrm{\top }$, the left derivation ends in Top-R and has antecedent ${ϵ}_{\mathrm{a}}$; the right derivation ends in Top-L with premise $\mathcal{C}[{ϵ}_{\mathrm{a}}]⊢B$. Erase both rules and return that premise. The $A=\mathsf{I}$ case is identical with ${ϵ}_{\mathrm{m}}$, I-R, and I-L.

Two-sided principal conjunctions.

For $A=C\wedge D$, the principal fragment is $$\frac{\begin{array}{c}{\displaystyle \frac{\begin{array}{c}{\mathcal{D}}_1:\mathrm{\Gamma }⊢C\\ {\mathcal{D}}_2:\mathrm{\Theta }⊢D\end{array}}{\mathrm{\Gamma };\mathrm{\Theta }⊢C\wedge D}}\mathrm{And}-\mathrm{R}\\ {\displaystyle \frac{{\mathcal{E}}_0:\mathcal{C}[C;D]⊢B}{\mathcal{C}[C\wedge D]⊢B}}\mathrm{And}-\mathrm{L}\end{array}}{\mathcal{C}[\mathrm{\Gamma };\mathrm{\Theta }]⊢B}\mathrm{MCut}.$$ The principal reduction records its rule pair on the transformation arrow: $${\mathrm{mcut}}_{C\wedge D}(\mathcal{D},\mathcal{E})\stackrel{And-R/And-L}{⟼}{\mathrm{mcut}}_D({\mathcal{D}}_2,{\mathrm{mcut}}_C({\mathcal{D}}_1,{\mathcal{E}}_0)).$$ The first result has antecedent $\mathcal{C}[\mathrm{\Gamma };D]$; the second has $\mathcal{C}[\mathrm{\Gamma };\mathrm{\Theta }]$. Both new cut formulas are proper subformulas of $C\wedge D$. The $C\ast D$ reduction is the same tree with semicolons replaced by commas and And by Star; it yields $\mathcal{C}[\mathrm{\Gamma },\mathrm{\Theta }]⊢B$. Hence each recursive call has a strictly smaller first rank component.

Two-sided principal disjunction.

If $\mathcal{D}$ ends in Or-R${}_1$, retain the left premise of the final Or-L in $\mathcal{E}$ and cut ${\mathcal{D}}_0:\mathrm{\Gamma }⊢C$ into ${\mathcal{E}}_1:\mathcal{C}[C]⊢B$. The formula $C$ is smaller than $C\vee D$. The Or-R${}_2$ case uses the right branch and cuts on $D$. The unused branch disappears because the injection has already selected a summand.

Two-sided principal additive implication.

Let the cut formula be $C\to D$. The last rules have premises $${\mathcal{D}}_0:\mathrm{\Gamma };C⊢D,{\mathcal{E}}_1:\mathrm{\Theta }⊢C,{\mathcal{E}}_2:\mathcal{C}[D]⊢B.$$ First cut ${\mathcal{E}}_1$ for the displayed $C$ in ${\mathcal{D}}_0$, obtaining $\mathrm{\Gamma };\mathrm{\Theta }⊢D$. Then cut this result for $D$ in ${\mathcal{E}}_2$. The conclusion is $\mathcal{C}[\mathrm{\Gamma };\mathrm{\Theta }]⊢B$, which is congruent to the required replacement of $C\to D$ in $\mathcal{C}[\mathrm{\Theta };(C\to D)]$. The two new cut formulas are $C$ and $D$, both smaller than $C\to D$. The two gains are visible in the annotated reduction: $${\mathrm{mcut}}_{C\to D}(\mathcal{D},\mathcal{E})\stackrel{Imp-R/Imp-L}{⟼}{\mathrm{mcut}}_D({\mathrm{mcut}}_C({\mathcal{E}}_1,{\mathcal{D}}_0),{\mathcal{E}}_2).$$

Two-sided principal wand.

For $C-\ast D$, the premises are Cut ${\mathcal{E}}_1$ into ${\mathcal{D}}_0$, obtaining $\mathrm{\Gamma },\mathrm{\Theta }⊢D$, then cut that result into ${\mathcal{E}}_2$. The conclusion $\mathcal{C}[\mathrm{\Gamma },\mathrm{\Theta }]⊢B$ is congruent to the required replacement in $\mathcal{C}[\mathrm{\Theta },(C-\ast D)]$. Again both recursive formulas are proper subformulas. Equivalently, the proof transformation is $${\mathrm{mcut}}_{C-\ast D}(\mathcal{D},\mathcal{E})\stackrel{Wand-R/Wand-L}{⟼}{\mathrm{mcut}}_D({\mathrm{mcut}}_C({\mathcal{E}}_1,{\mathcal{D}}_0),{\mathcal{E}}_2).$$

Every case either decreases the right height, decreases the sum of left heights while preserving the first two components, or replaces the cut by cuts on proper subformulas. The lexicographic induction is therefore well founded. Its cases are identity; nonprincipal logical, weakening, and contraction rules; one-sided principal rules; and the two-sided principal connectives $\wedge ,\vee ,\to ,\ast ,-\ast ,\mathrm{\top },\mathsf{I}$. ◻

Proof. The first statement is theorem 43.10 with one hole. For the second, induct on the finite list of formula families. The empty list leaves the given cut-free derivation unchanged. For a head family, apply the one-formula multicut theorem at its numbered holes to obtain a cut-free derivation, then apply the induction hypothesis to the remaining families. Because every replacement targets numbered holes, no unmarked occurrence changes. ◻

Proof. Induct on the derivation. The induction hypothesis gives a cut-free derivation for each premise. If the last rule belongs to ${\mathsf{LBI}}_0$, reapply it. If the last rule is $$\frac{\begin{array}{c}\mathrm{\Delta }⊢A\\ \mathcal{C}[A]⊢B\end{array}}{\mathcal{C}[\mathrm{\Delta }]⊢B},$$ corollary 43.11 gives a cut-free derivation of the conclusion. ◻

Proof. The two right-rule implications are Frumin’s Lemma 3.2. The four left-rule implications are his Lemma 3.4, and the final collapse equivalence is his Corollary 3.5 [Fru22]. Each invertibility proof is an induction on derivation height. The principal case removes the displayed introduction; every other last rule is re-applied to the induction hypothesis. Atomic identity in definition 43.5 is essential: an unrestricted identity axiom would obstruct the compound left cases. From left to right, the final equivalence uses their invertibility; from right to left, it is an induction on $\mathrm{\Gamma }$ using the four left rules. Thus no cut theorem is imported through this lemma. ◻

Proof. Write $X=\bigcap _{i\in I}⟨A_i⟩$. Membership of $\mathrm{\Gamma }$ means $\mathrm{\Gamma }{⊢}_{\mathrm{cf}}{A}_i$ for every $i$. Rule W gives $\mathrm{\Gamma };\mathrm{\Delta }{⊢}_{\mathrm{cf}}{A}_i$, and C sends $\mathrm{\Gamma };\mathrm{\Gamma }{⊢}_{\mathrm{cf}}{A}_i$ to $\mathrm{\Gamma }{⊢}_{\mathrm{cf}}{A}_i$. The last equivalence follows pointwise from lemma 43.15, instantiated with the empty one-hole context. No cut is used. ◻

Proof. Write $Y=\bigcap _{j\in J}⟨B_j⟩$. The multiplicative residual has the principal-set presentation $$\mathsf{MRes}(X,Y)=\bigcap _{(\mathrm{\Delta },j)\in X\times J}⟨\mathsf{form}(\mathrm{\Delta })-\ast B_j⟩.$$ For left-to-right inclusion, membership gives $\mathrm{\Gamma },\mathrm{\Delta }{⊢}_{\mathrm{cf}}{B}_j$; use lemma 43.15 to replace $\mathrm{\Delta }$ by $\mathsf{form}(\mathrm{\Delta })$, then apply Wand-R. For right-to-left inclusion, use the right invertibility and collapse clauses of that lemma in the reverse order. This proves equality and hence closedness. Replacing comma and Wand-R with semicolon and Imp-R gives $\mathsf{ARes}(X,Y)$.

The multiplicative adjunction now unfolds: $Z\bullet X\subseteq Y$ iff $Z\subseteq \mathsf{MRes}(X,Y)$. The additive adjunction needs the structural laws. Suppose $Z\cap X\subseteq Y$ and $\mathrm{\Gamma }\in Z$. For every $\mathrm{\Delta }\in X$, weakening and additive commutativity give $\mathrm{\Gamma };\mathrm{\Delta }\in Z\cap X$, hence $\mathrm{\Gamma };\mathrm{\Delta }\in Y$; therefore $\mathrm{\Gamma }\in \mathsf{ARes}(X,Y)$. Conversely, if $Z\subseteq \mathsf{ARes}(X,Y)$ and $\mathrm{\Gamma }\in Z\cap X$, then $\mathrm{\Gamma };\mathrm{\Gamma }\in Y$, so contraction gives $\mathrm{\Gamma }\in Y$. These are exactly parts 1 and 2 of lemma 43.17. Thus $$Z\cap X\subseteq Y⟺Z\subseteq \mathsf{ARes}(X,Y).$$ The closure adjunction (43.4) permits closing the left-hand multiplicative product without changing its equivalence. ◻

Proof. Arbitrary intersections make ${\mathcal{U}}_{\mathrm{BI}}$ a complete meet-semilattice; closing unions supplies joins and the displayed bottom. The additive implication is the right adjoint proved in lemma 43.18, so the additive structure is a bounded Heyting algebra.

Comma makes $\bullet$ associative and commutative with unit $\{{ϵ}_{\mathrm{m}}\}$. The closure is strong: $$\mathrm{cl}(X)\bullet Y\subseteq \mathrm{cl}(X\bullet Y).$$ To prove the inclusion, test membership against an arbitrary principal set $⟨A⟩$ containing $X\bullet Y$; the residual description of lemma 43.18 turns this premise into a closed set containing $X$, hence one containing $\mathrm{cl}(X)$. The closure adjunction then lifts associativity, commutativity, and the unit to ${\ast }_{{\mathcal{U}}_{\mathrm{BI}}}$. The same lemma supplies its residual, proving the displayed BI adjunction. ◻

Proof. Induct on $A$. The atomic and unit cases are the definitions and their right rules. For $B\wedge C$, the induction hypotheses put the leaf bunches $B$ and $C$ in their interpretations. Additive weakening puts $B;C$ in both, using additive commutativity for the second one; the collapse clause of lemma 43.15 puts the leaf $B\wedge C$ in their intersection. Conversely, an element of that intersection derives both $B$ and $C$, so And-R followed by contraction derives $B\wedge C$.

For $B\ast C$, elements of the unclosed product have the form $\mathrm{\Gamma },\mathrm{\Delta }$ with derivations of $B$ and $C$. Rule Star-R derives $B\ast C$, and closure extends this inclusion. The formula bunch $B\ast C$ itself belongs after putting $B,C$ in the product and applying Star-L. The $\vee$ case uses the two right rules for inclusion and Or-L to place $B\vee C$ in the closed union. The implication and wand cases unfold the two residual descriptions, apply their right rules for the inclusion, and their left rules for membership of the formula bunch. These are all constructors of definition 43.1. ◻

Proof. By lemma 43.21, the formula bunch $\mathsf{form}(\mathrm{\Gamma })$ belongs to its interpretation. The assumed inclusion puts it in $[[A{]]}_{{\mathcal{U}}_{\mathrm{BI}}}$, and the other half of the Okada property gives $\mathsf{form}(\mathrm{\Gamma }){⊢}_{\mathrm{cf}}A$. Apply the cut-free bunch/formula equivalence of lemma 43.15. ◻

Proof. This is Frumin’s Theorem 4.3, seq_interp_sound [Fru22], restricted to the formula grammar of definition 43.1. Its proof is induction on the cut-free derivation. Additive weakening and contraction use monotonicity and idempotence of meet. The right implication rules use the two residual adjunctions, while their left rules use the corresponding counits and monotonicity. The unit and conjunction rules are their algebraic laws. Those cases cover every rule of definition 43.5; neither multicut nor cut elimination is an induction case. ◻

Proof. Theorem 43.23 applied to the two cut-free derivations gives $$[[\mathsf{form}(\mathrm{\Delta }){]]}_{{\mathcal{U}}_{\mathrm{BI}}}\subseteq [[A{]]}_{{\mathcal{U}}_{\mathrm{BI}}}\text{and}[[\mathsf{form}(\mathcal{C}[A]){]]}_{{\mathcal{U}}_{\mathrm{BI}}}\subseteq [[B{]]}_{{\mathcal{U}}_{\mathrm{BI}}}.$$ Induction on the one-hole bunch context, using monotonicity of meet and multiplicative product, replaces the occurrence of $[[A{]]}_{{\mathcal{U}}_{\mathrm{BI}}}$ by the smaller $[[\mathsf{form}(\mathrm{\Delta }){]]}_{{\mathcal{U}}_{\mathrm{BI}}}$. Hence $$[[\mathsf{form}(\mathcal{C}[\mathrm{\Delta }]){]]}_{{\mathcal{U}}_{\mathrm{BI}}}\subseteq [[B{]]}_{{\mathcal{U}}_{\mathrm{BI}}}.$$ Reflection, theorem 43.22, yields the cut-free conclusion. Thus this corollary re-derives the one-hole case of corollary 43.11 by a semantic engine. ◻