Bunched implications and resource semantics

The logical symbols in this table are owned by chapter 43. The later heap model prints its assertion connectives with the same glyphs, but separate macros preserve the change of operand sort.

symbol	meaning and scope	first
symbol	meaning and scope	first
$\mathrm{\Gamma };\mathrm{\Delta }$	additive bunch constructor; exchange, weakening, and contraction are available inside its subtree	chapter 43
$\mathrm{\Gamma },\mathrm{\Delta }$	multiplicative bunch constructor recording a resource split, without weakening or contraction	chapter 43
${ϵ}_{\mathrm{a}},{ϵ}_{\mathrm{m}}$	distinct additive and multiplicative bunch units	chapter 43
$\mathcal{C}[-]$	one-hole bunch context; replacement is written $\mathcal{C}[\mathrm{\Delta }]$	chapter 43
$\mathcal{M}[{-}_1,\dots ,{-}_n]$	numbered many-hole bunch context for heterogeneous displayed multicut	chapter 43
$\mathrm{\Gamma }\equiv \mathrm{\Delta }$	structural congruence: two separate ACU theories with no interchange	chapter 43
$\mathrm{\top },\mathsf{I}$	additive truth and multiplicative truth/unit formulas	chapter 43
$A\ast B$	BI multiplicative conjunction; forced by a resource decomposition	chapter 43
$A-\ast B$	BI multiplicative implication; tests composition with every resource forcing $A$	chapter 43
$(M,⪯,\circ ,e)$	preordered commutative resource monoid and its unit	chapter 43
$m⪰n$	reverse orientation of the BI accessibility preorder	chapter 43
$A\simeq B$	mutual derivability of formulas in the elementary BI term model	chapter 43
$m⊩A$	resource world $m$ forces a BI formula or the formula represented by a bunch	chapter 43
$\mathsf{form}(\mathrm{\Gamma })$	syntax-to-syntax formula represented by a bunch, not semantic interpretation brackets	chapter 43
$\mathrm{\Gamma }{⊢}_{\mathrm{cf}}A$	cut-free derivability; a reminder for the universal-algebra replay, extensionally the chapter’s $⊢$ relation	section 43.5
$⟨A⟩$	principal cut-free theory generated by formula $A$	definition 43.16
$\mathrm{cl}(X)$	Moore closure of a set of bunches	definition 43.16
${\mathcal{U}}_{\mathrm{BI}}$	universal BI algebra of Moore-closed bunch theories	definition 43.19
$X\bullet Y,1_{\bullet }$	raw comma product of bunch sets and its unit	section 43.5
$\mathsf{MRes}(X,Y),\mathsf{ARes}(X,Y)$	multiplicative and additive residual sets	lemma 43.18
$[[A{]]}_{\mathcal{B}}$	semantic interpretation of formula $A$ in explicitly named BI algebra $\mathcal{B}$	theorem 43.23
$\mathrm{\Gamma }{\vDash }_{\mathcal{F},V}A$	validity in one selected resource model; omitting the subscript quantifies over all such models	chapter 43