Unit-free multiplicative proof nets

The exact signature of chapter 40 is classical one-sided, unit-free multiplicative linear logic. Its formulas and involutive linear negation are $$A,B::=p\mid p^{⟂}\mid A\otimes B\mid A\mathrm{\wp }B,A^{⟂⟂}=A,$$ $$(A\otimes B{)}^{⟂}=A^{⟂}\mathrm{\wp }{B}^{⟂},(A\mathrm{\wp }B{)}^{⟂}=A^{⟂}\otimes B^{⟂}.$$ Sequents are finite multisets. The complete sequent calculus used in the chapter is

$⊢p,p^{⟂}$

$⊢\mathrm{\Gamma },A,B$

$⊢\mathrm{\Gamma },A\mathrm{\wp }B$

$⊢\mathrm{\Gamma },A$$⊢B,\mathrm{\Delta }$

$⊢\mathrm{\Gamma },A\otimes B,\mathrm{\Delta }$

$⊢\mathrm{\Gamma },A$$⊢A^{⟂},\mathrm{\Delta }$

$⊢\mathrm{\Gamma },\mathrm{\Delta }$

The cut-free fragment omits only Cut. There is no unit, additive, exponential, box, quantifier, mix rule, noncommutative order, or generalized identity rule.

A cut-free proof structure on a nonempty sequent is its disjoint formula syntax forest together with a perfect matching of literal leaves, each edge joining one occurrence of $p$ to one occurrence of $p^{⟂}$ with the same name. Formula occurrences, not merely their labels, are vertices. Tensor and par roots have the two indicated premise occurrences; syntax-forest roots are conclusions. Translation of a cut-free derivation is generated by the following three graph operations:

1. Ax creates two literal vertices and their axiom edge;

2. Par adds one par root above two selected conclusions of one net;

3. Tensor takes the disjoint union of two premise nets and adds one tensor root above one selected conclusion from each.

For every par root, a switching retains exactly one of its two premise edges. The associated undirected correction graph retains every axiom edge, both premise edges of every tensor, and the selected edge of every par; it retains all formula vertices. A proof structure is Danos–Regnier correct, and hence a proof net, exactly when every correction graph is connected and acyclic. With cuts, a degree-two cut vertex joins dual conclusion occurrences by two incident cut edges, removes them from the external conclusions, and retains both edges in every switching.

The two and only two local cut contractions of this signature are the multiplicative contraction Mult-Cut, $$\mathrm{cut}(A\otimes B,A^{⟂}\mathrm{\wp }{B}^{⟂})⟶\mathrm{cut}(A,A^{⟂}),\mathrm{cut}(B,B^{⟂})$$ and the atomic splice Atomic-Cut, $$x{-}_{\mathrm{ax}}p{-}_{\mathrm{cut}}{p}^{⟂}{-}_{\mathrm{ax}}y⟶x{-}_{\mathrm{ax}}y,$$ with the dual orientation included. Reduction is compatible with the surrounding occurrence graph. The termination measure is $$(\sum _{c\text{ cut}}|A_c|,\mathrm{\#}\{c\mid c\text{ is atomic}\}),|p|=|p^{⟂}|=0,|A\star B|=1+|A|+|B|$$ in lexicographic order, for $\star \in \{\otimes ,\mathrm{\wp }\}$.

The direct checker fixes an order on the $k$ par roots, enumerates $\{0,1{\}}^k$, and runs parent-recording undirected depth-first search on each correction graph. It rejects on a nonparent edge to an already visited vertex or on an unvisited vertex after search; it accepts only after all bit vectors pass. This is the literal $O(2^{k}n)$-time, $O(n+k)$-space enumerator of definition 40.18, proposition 40.19, not the linear sequential-unification algorithm imported separately in theorem 40.20.