Bunched implications and resource semantics

The calculus ${\mathsf{LBI}}_0$ of chapter 43 is propositional intuitionistic BI without additive falsity. Its formulas contain atoms, $\mathrm{\top }$, $\mathsf{I}$, $\wedge$, $\vee$, $\to$, $\ast$, and $-\ast$. Antecedents are finite bunches with distinct additive and multiplicative constructors and units. Structural congruence is exactly the two separate commutative-monoid theories. Weakening and contraction occur only at a displayed semicolon. There is no distributivity, interchange, multiplicative weakening or contraction, unit identification, quantifier, modality, additive falsity, heap assertion, or program judgment.

Structural-congruence invariance is proposition 43.4, and the exact additive structural scope is proposition 43.6. Compound identity is theorem 43.8. The heterogeneous displayed multicut of theorem 43.10 has family ${\mathcal{D}}_i:{\mathrm{\Delta }}_i⊢A$, right derivation $\mathcal{E}:\mathcal{M}[A_1,\dots ,A_n]⊢B$, and rank $$(|A|,h(\mathcal{E}),\sum _{i=1}^{n}h({\mathcal{D}}_i)).$$ Its proof includes mixed old/new weakening occurrences, mixed outside/inside contraction occurrences, all $2^k$ branch combinations from $k$ selected Or-L members, and every two-sided principal connective. Displayed substitution and one-hole cut are corollary 43.11; cut elimination is theorem 43.13.

The syntax map is definition 43.14; principal cut-free theories, Moore closure, and the closed-set carrier are definition 43.16. Cut-free right and left invertibility is imported at the exact signature of Frumin Lemmas 3.2 and 3.4 and Corollary 3.5 in lemma 43.15. The two closed residuals and their distinct adjunctions are lemma 43.18; the universal algebra and Okada property are definition 43.19, proposition 43.20, lemma 43.21. Algebraic soundness imports Frumin Theorem 4.3 at theorem 43.23; reflection and semantic cut are theorem 43.22, corollary 43.24. The pinned Coq revision is 93aa9549cd122330d9cdb38900c69c21d2f5380a; its relevant identifiers are impl_r_inv, wand_r_inv, sep_l_inv, conj_l_inv, collapse_l_inv, seq_interp_sound, okada_property, C_interp_cf, and cut. These establish the universal algebra route, not resource-frame completeness.

A model is a preordered commutative monoid $(M,⪯,\circ ,e)$ with monotone composition and an upward-closed atomic valuation. Additive implication quantifies over accessible extensions; $\ast$ existentially splits resources; the wand universally composes with a separate resource. Bunch forcing is defined through the syntax map $\mathsf{form}$. No absorbing top resource or topological/sheaf structure belongs to the selected frame class.

Persistence is lemma 43.27; monotonicity under a bunch context is lemma 43.29; rule-by-rule soundness is theorem 43.31. The finite frames $M_2$, ${\mathbb{Z}}_2$, and ${\mathbb{Z}}_3$ calculate the connective distinctions and refute multiplicative weakening, contraction, interchange, and unit identification. The exact models are proposition 43.30; their nonadmissibility consequences are corollary 43.32. Atomic non-derivability is corollary 43.33.

The bunch/formula bridge is lemma 43.34. On the fragment also omitting $\vee$, formulas modulo $\simeq$ form the elementary term model of definition 43.35. Its frame laws are lemma 43.36, the truth lemma is theorem 43.37, and elementary completeness for that fragment is corollary 43.38. The same term model fails at disjunction because an arbitrary equivalence class need not select a disjunct.

The local ${\mathsf{LBI}}_0$/NBI bridge is lemma 43.39; the source’s HBI correspondence remains part of the external boundary. The upward/downward order convention is reconciled by lemma 43.40. Pym, O’Hearn, and Yang state full falsity-free elementary completeness after Proposition 7 in §3.5, printed p. 12, but delegate its prime-bunch construction to a monograph absent from the pinned package. Section 5.2, printed pp. 28–30, sketches a related invariant rather than supplying that proof. The chapter’s explicit boundary convention is therefore not a theorem proved or imported by this book. Proposition 6 on printed p. 12 blocks extension to additive falsity.

No heap carrier, allocation, mutation, command semantics, Hoare triple, locality theorem, frame rule, linked-structure proof, or heap-language safety result belongs to this signature. The heap model and program logic begin in chapter 44; no result from that chapter is used here.

The Kappa companion in artifacts/ch43-bi-resource-semantics/ checks a finite rule-tree fragment, separate ACU bunch equality, selected structural rejections, and finite-model forcing. Its three named mutations target multiplicative weakening, constructor identification/interchange, and the forcing clause for $\ast$. The artifact illustrates selected finite invariants only. It is not a proof of cut elimination, soundness, completeness, or decidability of full BI.