appendix sectionrules

Bunched implications and resource semantics

The chapter calculus is the additive-falsity-free propositional system ${LBI}_{0}$ . Its formulas and bunches are $\begin{aligned} A, B & ::= p ∣ ⊤ ∣ I ∣ A \land B ∣ A \lor B ∣ A \to B ∣ A * B ∣ A - * B, \\ Γ, Δ & ::= A ∣ ϵ_{a} ∣ ϵ_{m} ∣ Γ; Δ ∣ Γ, Δ . \end{aligned}$ A one-hole bunch context is $C [-] ::= [-] ∣ C [-]; Γ ∣ Γ; C [-] ∣ C [-], Γ ∣ Γ, C [-] .$ A finite many-hole context $M [-_{1}, \dots, -_{n}]$ contains each numbered hole exactly once. Structural congruence is the least congruence generated by the two separate commutative-monoid theories $\begin{array}{rclrcl} (Γ; Δ); Θ & \equiv & Γ; (Δ; Θ), & Γ; Δ & \equiv & Δ; Γ, \\ Γ; ϵ_{a} & \equiv & Γ, & (Γ, Δ), Θ & \equiv & Γ, (Δ, Θ), \\ Γ, Δ & \equiv & Δ, Γ, & Γ, ϵ_{m} & \equiv & Γ . \end{array}$ There is no equation between the two units, no distributivity or interchange, and no multiplicative weakening or contraction. Antecedents are read modulo this congruence.

The complete rule sheet is

p ⊢ p

C [Δ] ⊢ A

C [Δ; Σ] ⊢ A

C [Δ; Δ] ⊢ A

C [Δ] ⊢ A

ϵ_{a} ⊢ ⊤

Top-R

C [ϵ_{a}] ⊢ A

C [⊤] ⊢ A

Top-L

ϵ_{m} ⊢ I

I-R

C [ϵ_{m}] ⊢ A

C [I] ⊢ A

I-L

Γ ⊢ A

Δ ⊢ B

Γ; Δ ⊢ A \land B

And-R

C [A; B] ⊢ D

C [A \land B] ⊢ D

And-L

Γ ⊢ A

Γ ⊢ A \lor B

Or-R_1

Γ ⊢ B

Γ ⊢ A \lor B

Or-R_2

C [A] ⊢ D

C [B] ⊢ D

C [A \lor B] ⊢ D

Or-L

Γ; A ⊢ B

Γ ⊢ A \to B

Imp-R

Δ ⊢ A

C [B] ⊢ D

C [Δ; (A \to B)] ⊢ D

Imp-L

Γ ⊢ A

Δ ⊢ B

Γ, Δ ⊢ A * B

Star-R

C [A, B] ⊢ D

C [A * B] ⊢ D

Star-L

Γ, A ⊢ B

Γ ⊢ A - * B

Wand-R

Δ ⊢ A

C [B] ⊢ D

C [Δ, (A - * B)] ⊢ D

Wand-L

In Or-L, both premises contain the same one-hole context. Every hole in all rules occurs exactly once. The language is propositional, so there is no freshness or eigenvariable side condition.

Identity for every formula and cut are admissible, not primitive. Their reference forms are

A ⊢ A

Δ ⊢ A

C [A] ⊢ B

C [Δ] ⊢ B

Cut

The heterogeneous displayed multicut is

D_{i} : Δ_{i} ⊢ A (1 \leq i \leq n)

E : M [A_{1}, \dots, A_{n}] ⊢ B

M [Δ_{1}, \dots, Δ_{n}] ⊢ B

MCut

Each $A_{i}$ is a numbered occurrence of the same cut formula $A$ , while the antecedents $Δ_{i}$ and derivations $D_{i}$ may differ. Its lexicographic induction rank is $(| A |, h (E), \sum_{i = 1}^{n} h (D_{i})) .$ The separate right-height component is essential: contraction may duplicate selected occurrences and thereby increase the final sum only after $h (E)$ has decreased.

The reduction ledger is:

case	replacement and strict decrease
identity and zero holes	return the matching left derivation, remove an atomic identity member, or return the right derivation when $n = 0$
right commutation	distribute all numbered holes among the proper premises and reapply the final rule; every recursive call has smaller right height
left commutation	replace one member by each premise whose succedent is $A$ , retain auxiliary premises, and reapply the final left rule; the sum of left heights decreases
repeated Or-L	recurse into both branches for each selected member; $k$ such members generate all $2^{k}$ mixed branch choices, not only two homogeneous branches
additive weakening	recurse once for every old or surrounding occurrence, fill selected occurrences in the newly added $Σ$ directly by their own $Δ_{i}$ , and reapply one W; one family may mix both kinds
additive contraction	place every outside occurrence once and both descendants of each occurrence inside the contracted subtree into one heterogeneous family, using the same $D_{i}$ for both descendants; recurse once and reapply C
one-sided principal	commute above the nonprincipal side, decreasing the corresponding derivation-height component
other selected holes	first replace every nonprincipal occurrence in the proper premises, decreasing right height, then reduce the exposed principal occurrence on a proper subformula
$⊤$ , $I$	erase the matching right and left unit rules
$C \land D$ , $C * D$	cut first on $C$ and then on $D$ , rebuilding the corresponding additive or multiplicative bunch; formula size decreases
$C \lor D$	retain the branch selected by the final injection and cut on that proper subformula
$C \to D$ , $C - * D$	cut the left-rule argument into the right-rule premise on $C$ , then cut the result into the continuation on $D$ ; use semicolon for implication and comma for wand

The two principal implication reductions are, respectively, $\begin{matrix} D_{0} : Γ; C ⊢ D, E_{1} : Θ ⊢ C, E_{2} : C [D] ⊢ B \\ ⟼ {cut}_{D} ({cut}_{C} (E_{1}, D_{0}), E_{2}) : C [Γ; Θ] ⊢ B, \end{matrix}$ and $\begin{matrix} D_{0} : Γ, C ⊢ D, E_{1} : Θ ⊢ C, E_{2} : C [D] ⊢ B \\ ⟼ {cut}_{D} ({cut}_{C} (E_{1}, D_{0}), E_{2}) : C [Γ, Θ] ⊢ B . \end{matrix}$ In both cases the new cut formulas $C$ and $D$ are proper subformulas. Together with the ledger, these are the complete cases used by theorem 43.10, theorem 43.13.

The independent semantic replay uses $\begin{aligned} ⟨ A ⟩ & = {Γ ∣ Γ ⊢_{cf} A}, \\ cl (X) & = ⋂ {⟨ A ⟩ ∣ X \subseteq ⟨ A ⟩}, \\ MRes (X, Y) & = {Γ ∣ \forall Δ \in X . Γ, Δ \in Y}, \\ ARes (X, Y) & = {Γ ∣ \forall Δ \in X . Γ; Δ \in Y} . \end{aligned}$ Closed sets form $U_{BI}$ . Intersection is additive meet, closed union is join, closed comma-product is multiplicative product, and the two displayed residuals are their right adjoints. The imported invertibilities are lemma 43.15; algebraic soundness and reflection are theorem 43.23, theorem 43.22. Their composition is the semantic cut certificate corollary 43.24; it is independent of the displayed-multicut proof above.