ch:bunched-implications: ch:bunched-implications

(a) holds by additive exchange in the two children: $$(A;B),(C;D)\equiv (B;A),(D;C).$$

(b) does not hold. It is interchange between a multiplicative root with additive children and an additive root with multiplicative children.

(c) holds: $$A,(B,{ϵ}_{\mathrm{m}})\equiv A,B\equiv B,A.$$ The first step is the multiplicative unit law and the second is multiplicative exchange.

(d) does not hold. The displayed semicolon has additive unit ${ϵ}_{\mathrm{a}}$, not ${ϵ}_{\mathrm{m}}$; the equation would identify the units or add a new additive unit law.

(e) holds inside every bunch context: $$(A;B);C\equiv A;(B;C)\equiv A;(C;B),$$ and congruence lifts this chain through $\mathcal{C}[-]$.

The first derivation is $$\frac{\begin{array}{c}{\displaystyle \frac{P⊢P}{P;S⊢P}}\mathrm{W}\\ {\displaystyle \frac{Q⊢Q}{Q;T⊢Q}}\mathrm{W}\end{array}}{(P;S),(Q;T)⊢P\ast Q}\mathrm{Star}-\mathrm{R}.$$ Each weakening lies inside one child of the final comma.

For the second sequent, split the inner multiplicative subtree and then use the additive right rule: $$\frac{\begin{array}{c}P⊢P\\ {\displaystyle \frac{\begin{array}{c}Q⊢Q\\ R⊢R\end{array}}{Q,R⊢Q\ast R}}\mathrm{Star}-\mathrm{R}\end{array}}{P;(Q,R)⊢P\wedge (Q\ast R)}\mathrm{And}-\mathrm{R}.$$

For the final sequent, contraction is the final load-bearing step in the left premise of Star-R: $$\frac{\begin{array}{c}{\displaystyle \frac{{\displaystyle \frac{\begin{array}{c}P⊢P\\ P⊢P\end{array}}{P;P⊢P\wedge P}}\mathrm{And}-\mathrm{R}}{P⊢P\wedge P}}\mathrm{C}\\ Q⊢Q\end{array}}{P,Q⊢(P\wedge P)\ast Q}\mathrm{Star}-\mathrm{R}.$$ No weakening back to $P;P$ is permitted or needed.

(a) follows by additive weakening at the outer semicolon: $$\frac{Q,R⊢Q\ast R}{(Q,R);P⊢Q\ast R}\mathrm{W},$$ followed by additive exchange.

(b) does not follow: it requires multiplicative weakening to add $Q$ below a comma. (c) does not follow: it requires multiplicative contraction to replace two comma-separated copies by one. (d) is structural congruence, using exchange separately inside the two additive children.

(e) requires the forbidden interchange transformation. The source bunch $(A;B),(C;D)$ supports the displayed succedent by one comma split, with $A;B$ proving $A\wedge B$ and $C;D$ proving $C\wedge D$. The proposed bunch $(A,C);(B,D)$ instead represents $(A\ast C)\wedge (B\ast D)$: its two additive conjuncts may use two different resource decompositions. Deriving $(A\wedge B)\ast (C\wedge D)$ would require one shared decomposition whose left world forces both $A,B$ and whose right world forces both $C,D$. The ${\mathbb{Z}}_3$ calculation in proposition 43.30 shows that such a shared split need not exist.

First derive identity for $P\vee Q$: $$\frac{\begin{array}{c}{\displaystyle \frac{P⊢P}{P⊢P\vee Q}}\mathrm{Or}-{\mathrm{R}}_1\\ {\displaystyle \frac{Q⊢Q}{Q⊢P\vee Q}}\mathrm{Or}-{\mathrm{R}}_2\end{array}}{P\vee Q⊢P\vee Q}\mathrm{Or}-\mathrm{L}.$$ With $R⊢R$, rule Imp-L gives $(P\vee Q);((P\vee Q)\to R)⊢R$. Additive exchange puts the function first, and Imp-R yields identity for $(P\vee Q)\to R$.

For the wand, the induction hypotheses give $$\frac{{\displaystyle \frac{\begin{array}{c}P⊢P\\ Q⊢Q\end{array}}{P,Q⊢P\ast Q}}\mathrm{Star}-\mathrm{R}}{P\ast Q⊢P\ast Q}\mathrm{Star}-\mathrm{L}$$ and $$\frac{{\displaystyle \frac{\begin{array}{c}R⊢R\\ S⊢S\end{array}}{R;S⊢R\wedge S}}\mathrm{And}-\mathrm{R}}{R\wedge S⊢R\wedge S}\mathrm{And}-\mathrm{L}.$$ Apply Wand-L to these identities, use multiplicative exchange, and apply Wand-R. This derives identity for $(P\ast Q)-\ast (R\wedge S)$.

Finally derive the separate identities for $\mathrm{\top }$ and $\mathsf{I}$ with their left and right unit rules. Rule Star-R gives $\mathrm{\top },\mathsf{I}⊢\mathrm{\top }\ast \mathsf{I}$, and Star-L gives $\mathrm{\top }\ast \mathsf{I}⊢\mathrm{\top }\ast \mathsf{I}$. No equation identifies the two units.

For the star case, the unreduced cut is $$\frac{\begin{array}{c}{\displaystyle \frac{\begin{array}{c}P⊢P\\ Q⊢Q\end{array}}{P,Q⊢P\ast Q}}\mathrm{Star}-\mathrm{R}\\ {\displaystyle \frac{P,Q,R⊢(P\ast Q)\ast R}{P\ast Q,R⊢(P\ast Q)\ast R}}\mathrm{Star}-\mathrm{L}\end{array}}{P,Q,R⊢(P\ast Q)\ast R}\mathrm{Cut}.$$ Reduce it to a cut on $P$, followed by a cut on $Q$, in the premise $P,Q,R⊢(P\ast Q)\ast R$. Both are identity cuts and erase. Their formulas have sizes $|P|$ and $|Q|$, strictly below $|P\ast Q|$.

For the wand case, let $${\mathcal{D}}_0:(P-\ast Q),P⊢Q$$ be the premise of the identity expansion of the wand. The continuation $Q;T⊢Q\wedge Q$ is obtained from two weakened derivations $Q;T⊢Q$, followed by And-R, which produces $(Q;T);(Q;T)⊢Q\wedge Q$, and one C.

Cut $S⊢P$ into ${\mathcal{D}}_0$, obtaining $(P-\ast Q),S⊢Q$. Cut this result into the continuation on $Q$, obtaining $$((P-\ast Q),S);T⊢Q\wedge Q.$$ Multiplicative exchange gives the antecedent obtained by replacing the cut formula in $(S,(P-\ast Q));T$. The recursive cut formulas are $P$ and $Q$, both proper subformulas of the wand.

Construct the two additive premises $$\frac{{\displaystyle \frac{{\displaystyle \frac{\begin{array}{c}P⊢P\\ P⊢P\end{array}}{P;P⊢P\wedge P}}\mathrm{And}-\mathrm{R}}{P⊢P\wedge P}}\mathrm{C}}{P;S⊢P\wedge P}\mathrm{W}$$ and, symmetrically, $Q;T⊢Q\wedge Q$. Rule Star-R gives $$(P;S),(Q;T)⊢(P\wedge P)\ast (Q\wedge Q).$$ Apply And-L to package $P;S$ and $Q;T$, then apply Wand-R and Imp-R. This yields the required closed formula.

Changing the outer comma to a semicolon invalidates two distinct steps. Star-R must combine its premise antecedents with a comma, and Wand-R must discharge a comma-separated argument. The intervening And-L rules remain locally well formed because each packages one additive subtree.

Write $\mathsf{Force}(A)$ for the worlds forcing $A$. From the atomic valuation, $$\mathsf{Force}(P\wedge Z)=\{2\}.$$ For $P\ast Z$, the right witness must be $2$, and composing it with either world forcing $P$ gives $2$; only target world $2$ admits that split. Thus $\mathsf{Force}(P\ast Z)=\{2\}$.

Worlds $0$ and $1$ have the accessible counterexample $1⊩P$, $1⊮Z$, while world $2$ has none. Hence $$\mathsf{Force}(P\to Z)=\{2\}.$$ For the wand, test resources $1,2$. At world $0$, $0\circ 1=1⊮Z$; at worlds $1,2$, composition with either test resource is $2$. Therefore $$\mathsf{Force}(P-\ast Z)=\{1,2\}.$$

The only world forcing $P\ast Q$ is $2$, which also forces $Z$. Thus $\mathsf{Force}((P\ast Q)\to Z)=\{0,1,2\}$. The inner wand $Q-\ast Z$ has forcing set $\{1,2\}$; composing any world with either test resource forcing $P$ lands in that set. Consequently $$\mathsf{Force}(P-\ast (Q-\ast Z))=\{0,1,2\}.$$

The opening bunch is forced only at $2$, using the split $1\circ 1=2$. For the mixed formula, let an accessible $n$ force $P\wedge S$ and let $x$ force $Q\wedge T$. The same pair witnesses $n\circ x⊩P\ast Q$. Hence every world forces $\mathsf{Mix}(P,S,Q,T)$.

For $(P\wedge Q)\to P\ast Q$, take equality-preordered ${\mathbb{Z}}_2$ and put $V(P)=V(Q)=\{1\}$. At world $1$, the antecedent is true. The only pair forcing both atoms is $1,1$, whose sum is $0$, so the star is false at $1$.

For $(P-\ast Q)\to (P\to Q)$, use $M_2$ with $V(P)=\{1,2\}$ and $V(Q)=\{2\}$. At world $1$, composition with every resource forcing $P$ yields $2$, so the wand holds. But the accessible world $1$ itself forces $P$ and not $Q$, so the additive implication fails there. The outer implication is therefore false at world $1$.

For $\mathrm{\top }\to \mathsf{I}$, return to equality-preordered ${\mathbb{Z}}_2$. Every world forces $\mathrm{\top }$, while $\mathsf{I}$ is forced only at the unit world $0$. World $1$ refutes the implication. These examples include a nontrivial preorder and an equality preorder on a finite group, as required.

For Imp-L, prove the needed pointwise hole implication. If a world $u$ forces $\mathrm{\Delta };(A\to B)$, then it forces $\mathrm{\Delta }$ and $A\to B$. The first premise induction hypothesis gives $u⊩A$. Instantiate the implication clause at the reflexive extension $u⪰u$ to obtain $u⊩B$. Thus $$u⊩\mathrm{\Delta };(A\to B)⟹u⊩B$$ for every $u$. Context monotonicity lifts this implication through $\mathcal{C}[-]$, and the continuation induction hypothesis yields the succedent. No additional persistence step is needed in this case; the order appears only in the reflexive implication test.

For Wand-L, if $u$ forces $\mathrm{\Delta },(A-\ast B)$, choose $x,y$ with $x\circ y⪯u$, $x⊩\mathrm{\Delta }$, and $y⊩A-\ast B$. The first induction hypothesis gives $x⊩A$. The wand clause and commutativity give $x\circ y⊩B$; persistence along $x\circ y⪯u$ gives $u⊩B$. This is the sole persistence use. Context monotonicity and the continuation premise finish the case.

If multiplicative weakening were sound, $P⊢P$ would give $P,Q⊢P$. Rule Star-L would give $P\ast Q⊢P$, and Imp-R would close $P\ast Q\to P$. This contradicts the ${\mathbb{Z}}_2$ countermodel of proposition 43.30.

For the forward additive-implication case, assume $A⊢B\to C$, $[A]⪯[D]$, and $[D]⊩B$. Thus $D⊢A$ and, by induction, $D⊢B$. Cut $D⊢A$ into the first derivation. Rule Imp-L with $D⊢B$ and identity on $C$, followed by a cut of the resulting $D⊢B\to C$, gives $D;D⊢C$. Contract to $D⊢C$, and apply induction.

Conversely, assume $[A]⊩B\to C$ and put $D=A\wedge B$. The two projections give $D⊢A$ and $D⊢B$, hence $[A]⪯[D]$ and $[D]⊩B$. The semantic hypothesis and induction yield $A\wedge B⊢C$. Cut in $A;B⊢A\wedge B$ and apply Imp-R.

For the forward wand case, assume $A⊢B-\ast C$ and $[X]⊩B$. Induction gives $X⊢B$. Rule Wand-L with identity on $C$, followed by a cut of the assumed wand derivation and multiplicative exchange, gives $A,X⊢C$. The bunch/formula lemma gives $A\ast X⊢C$, so $[A\ast X]⊩C$.

Conversely, assume $[A]⊩B-\ast C$ and test world $[B]$. Identity and induction give $[B]⊩B$; hence $[A\ast B]⊩C$, so $A\ast B⊢C$. The bunch/formula lemma yields $A,B⊢C$, and Wand-R finishes.

At $[P\vee Q]$, identity derives $P\vee Q$, but neither disjunct is derivable separately. The ordinary equivalence-class world therefore fails the semantic disjunction clause. Repair would require enough prime bunches, a prime-extension construction compatible with the preorder and comma, a well-defined resource composition, an upward-closed canonical valuation, and a truth lemma proving that a forced disjunction selects a disjunct. The packaged article states that extension but delegates its construction to the absent monograph; the source statement alone proves none of these obligations inside the book.

Delete only the matching unit from each maximal node, flatten only children with the same constructor, sort the normalized children, and retain every alternation boundary. The first pair normalizes on both sides to $(A;B),(C,D)$, up to the chosen sorting order, so it is congruent. The second pair has different roots after normalization: additive for $(A,B);(C,D)$, multiplicative for $(A;C),(B;D)$; it is not congruent. The third pair normalizes on both sides to $A;B;C$, so it is congruent.

The algorithm recursively normalizes children, replaces each maximal semicolon or comma node by the sorted multiset of normalized children of that same kind, and deletes only its matching unit. Equality of the resulting finite trees is decidable. Induction on bunches shows that every ACU generator preserves the normal form. Conversely, equal normal forms determine a chain of exchanges, reassociations, and matching-unit deletions inside each retained node; congruence rebuilds those chains through the alternation tree.

For Imp-R/Imp-L, take $${\mathcal{D}}_0:\mathrm{\Gamma };C⊢D,{\mathcal{E}}_1:\mathrm{\Theta }⊢C,{\mathcal{E}}_2:\mathcal{K}[D]⊢B.$$ The unreduced cut inserts $\mathcal{D}:\mathrm{\Gamma }⊢C\to D$ into the conclusion $\mathcal{K}[\mathrm{\Theta };(C\to D)]⊢B$. Its reduction is $${\mathrm{cut}}_D({\mathrm{cut}}_C({\mathcal{E}}_1,{\mathcal{D}}_0),{\mathcal{E}}_2):\mathcal{K}[\mathrm{\Gamma };\mathrm{\Theta }]⊢B.$$ Additive associativity and exchange identify this with the antecedent obtained by replacing the displayed implication occurrence. The new cut formulas $C,D$ are proper subformulas.

For Wand-R/Wand-L, replace semicolons by commas in the data and conclusion. The same two cuts yield $\mathcal{K}[\mathrm{\Gamma },\mathrm{\Theta }]⊢B$, and multiplicative associativity and exchange supply the final congruence.

If the final right rule contracts $\mathcal{C}[\mathrm{\Xi };\mathrm{\Xi }]$ to $\mathcal{C}[\mathrm{\Xi }]$, every selected occurrence inside $\mathrm{\Xi }$ has two displayed descendants in the premise. Put both descendants, with the same corresponding left derivation, into one heterogeneous multicut. Put any selected occurrence outside $\mathrm{\Xi }$ into that same family once. The recursive right derivation is the contraction premise, so its height is smaller even though duplication may increase the sum of left heights. Two uncontrolled sequential cuts do not expose this lexicographic decrease.

The upward-closed subsets of are $$\varnothing ,\{2\},\{1,2\},\{0,1,2\}.$$ Thus two atoms have sixteen ordered valuation pairs. For every pair, $P\ast Q\to P\wedge Q$ is valid. A witness $x\circ y⪯n$ for the star satisfies $x⪯x\circ y⪯n$ and $y⪯x\circ y⪯n$ in truncated addition. Upward closure therefore gives $n⊩P\wedge Q$.

Every valuation consequently makes this particular frame behave as though multiplicative weakening were available: its order satisfies $x⪯x\circ y$ and $y⪯x\circ y$ for all $x,y$. This is a frame property, not a theorem over all resource frames. The equality-preordered ${\mathbb{Z}}_2$ fails those inequalities and refutes multiplicative weakening.

The universally valid direction is $$(A\wedge B)\ast (C\wedge D)⟶(A\ast C)\wedge (B\ast D).$$ If $m$ forces the antecedent, choose $x,y$ with $x\circ y⪯m$, $x⊩A\wedge B$, and $y⊩C\wedge D$. The same pair witnesses both stars in the conclusion.

The converse fails in equality-preordered ${\mathbb{Z}}_3$. Put $V(A)=V(C)=\{0\}$, $V(B)=\{1\}$, and $V(D)=\{2\}$. At world $0$, $A\ast C$ is witnessed by $0+0$, while $B\ast D$ is witnessed by $1+2$. No world forces $A\wedge B$ or $C\wedge D$, so their star is false.

The invalid converse corresponds to the replacement $$(A,C);(B,D)⟼(A;B),(C;D).$$ Two independently chosen splits would have to become one shared split. The valid direction merely reuses one already supplied split in two additive conjuncts and is not a bunch-congruence equation.

The audited language is $$p,\mathrm{\top },\mathsf{I},\wedge ,\vee ,\to ,\ast ,-\ast ,$$ with no additive falsity. Frames are preordered commutative monoids with monotone composition. Atomic valuations are upward closed in the chapter’s orientation. Forcing uses the ordinary intuitionistic clauses, unit condition $e⪯m$, decomposition for $\ast$, and universal composition for the wand. Lemma 43.40 converts these clauses to the paper’s downwards-closed convention.

Proposition 7 in §3.5, printed p. 12, proves the easy theorem for formulas without additive falsity or disjunction. The following paragraph states full falsity-free completeness and attributes its prime-bunch construction to Pym’s monograph. Section 5.2, printed pp. 28–30, sketches a related prime-evaluation invariant but does not supply the delegated construction. Proposition 6 gives the counterexample showing why additive falsity cannot be restored over elementary total monoids.

Promotion of convention 43.41 would require the absent prime-extension theorem with all its hypotheses, closure of the prime worlds under the resource operation, a proof that the induced preorder and operation form the selected model class, the canonical valuation and its closure proof, the complete truth lemma including disjunction, and exact transport through lemma 43.39, lemma 43.40, lemma 43.34. None of those obligations is discharged merely by citing the source statement; the full reverse implication therefore remains outside the book’s theorem ledger.