Proof Nets, Correctness Criteria, and Cut Elimination

Proof. Induct on $A$. The literal cases are Ax, up to the implicit exchange of the multiset. Suppose first that $A=B\otimes C$. The induction hypotheses end in $⊢B,B^{⟂}$ and $⊢C,C^{⟂}$. Apply Tensor to the occurrences $B,C$, then Par to their two duals: $$\frac{{\displaystyle \frac{\begin{array}{c}⊢B,B^{⟂}\\ ⊢C,C^{⟂}\end{array}}{⊢B\otimes C,B^{⟂},C^{⟂}}}\mathrm{Tensor}}{⊢B\otimes C,B^{⟂}\mathrm{\wp }{C}^{⟂}}\mathrm{Par}.$$ If $A=B\mathrm{\wp }C$, apply the same two induction hypotheses, first Tensor to $B^{⟂},C^{⟂}$, then Par to $B,C$. The conclusion is $⊢B\mathrm{\wp }C,B^{⟂}\otimes C^{⟂}$, as required. ◻

Proof. An axiom structure is one edge joining two vertices, hence a tree.

For Par, fix a switching of the conclusion. Its restriction to the premise is a switching of the premise net, hence a tree. The new par vertex is attached to that tree by exactly the one selected edge. Attaching one new leaf preserves connectedness and acyclicity.

For Tensor, fix switchings of the two premise nets. Their correction graphs are disjoint trees. The new tensor vertex is joined by one edge to a conclusion in each tree. The two edges and new vertex connect the trees, and they cannot create a cycle because there was no path between the disjoint premises. The result is again a tree. ◻

Proof. Induct on $\mathrm{\Pi }$. The three possible last rules are precisely the three cases of lemma 40.8. ◻

Proof. Unions and intersections of substructures preserve downward formula closure and axiom closure. Every switching of every substructure is acyclic, because a cycle would also be a cycle in an extension of that switching to $N$. Thus only connectedness needs attention.

For the first clause, a switching of $S\cup T$ restricts to trees on $S$ and $T$. Their nonempty intersection connects those two trees. For two vertices in $S\cap T$, the path between them inside $S$ and the path inside $T$ must coincide: two different paths would form a cycle in $S\cup T$. That common path lies in the intersection, so the intersection is connected as well.

For the second clause, fix $A$. Given a switching $\sigma$, if the formula-tree edge immediately above $A$ occurs in $G_{\sigma }(N)$, delete it and let $C_{\sigma }(A)$ be the component containing $A$. If that edge is absent or $A$ is already a conclusion, put $C_{\sigma }(A)=G_{\sigma }(N)$. Intersect these components over every switching, retaining the axiom matching and restoring a formula-tree edge whenever both endpoints and its link remain. Call the resulting substructure $S_A$.

First, $A$ is a door of $S_A$. Suppose instead that an ancestor $B$ of $A$ survived. Choose a switching $\hat{\sigma }$ which, at every par on the formula-tree path from $A$ to $B$, retains the edge on that path. The edge immediately above $A$ is therefore present and is deleted in $C_{\hat{\sigma }}(A)$. Since $B$ nevertheless lies in that component, there is an alternative path from $A$ to $B$ avoiding the deleted edge. Compare it with the formula-tree path in the original correction graph. At a first re-entry into that tree path, a par cannot supply the off-path edge, because $\hat{\sigma }$ deleted it. Thus the re-entry uses the sibling edge of an intervening tensor. Choose the uppermost such tensor. The alternative path below it and the retained formula-tree segment give two distinct paths between the tensor’s path child and $A$. This contradicts the unique-path property of the tree $G_{\hat{\sigma }}(N)$.

On the running two-axiom net this check is completely concrete. Put $A=p$ and let its ancestor $B$ be the tensor root $T=p\otimes q$. Choose the switching that retains the $p^{⟂}$-edge at the par root and delete the edge $p-T$. One component is the path $p-p^{⟂}-P$, while the other contains $T-q-q^{⟂}$; there is no alternative path back to $T$. Choosing the other par premise only shortens the first component to $p-p^{⟂}$. The schematic figure describes the only hypothetical way a larger net could reconnect those components: its first re-entry would have to use the sibling of an intervening tensor, and the retained tree segment would then give the forbidden second path. Thus the abstract “uppermost tensor” is a contradiction witness, not an unlabeled vertex hidden in this small example.

The intersection also satisfies the two structural closure conditions in definition 40.10. Axiom closure is immediate: an axiom edge occurs in every switching and is never the deleted formula-tree edge, so its endpoints always lie in the same component. For downward closure, fix a surviving formula vertex $X$. Both child edges of a tensor occur in every switching, so both tensor children survive. At a par, compare two switchings that agree away from $X$ and select opposite children there. If one child left the $A$-component, the unique path from that child to $X$ would cross the deleted edge. Flipping the par choice makes the other child leave instead. The two paths from $X$ to the deleted edge then first diverge along the two par branches and later meet. Choosing the uppermost meeting point gives two distinct paths between that point and $X$ in one of the two correction trees, a contradiction. Hence both par children survive. Induction down the formula tree proves downward closure. Restoring a formula-tree edge when its two endpoints survive therefore changes only the presentation of the induced subforest; it adds no vertex.

It remains to check connectedness rather than assume it from the intersection. Let $\tau$ be a switching of $S_A$, and extend its par choices arbitrarily to a switching $\tilde{\tau }$ of $N$. Axiom closure and the definition of the restored formula edges make $G_{\tau }(S_A)$ the restriction of $C_{\tilde{\tau }}(A)$ to $S_A$. For any $X\in S_A$, the unique path from $A$ to $X$ in $C_{\tilde{\tau }}(A)$ cannot leave and re-enter $S_A$: at the first missing vertex, choose a switching whose $A$-component omitted it; the path in that component and the retained segment of the $\tilde{\tau }$-path would, by the same uppermost-tensor argument, give two paths in one correction tree. Hence the unique path lies in $S_A$. Thus every $G_{\tau }(S_A)$ is connected. It is acyclic as a subgraph of a correction tree, so $S_A$ is a subnet with door $A$.

The family of subnets with door $A$ is finite and nonempty. Repeated nonempty intersection gives its least member, while repeated union gives its greatest member, by the first clause. These are $k(A)$ and $e(A)$. ◻

Proof. The occurrence $B^{\prime }$ belongs to both $e(A^{\prime })$ and $k(B)$. Subnet algebra says that their intersection and union are subnets. If $B\notin e(A^{\prime })$ and $A\notin k(B)$, their union is a subnet with door $A^{\prime }$ strictly larger than $e(A^{\prime })$, a contradiction. Conversely, if $B\in e(A^{\prime })$ and $A\in k(B)$, their intersection is a subnet with door $B$ strictly smaller than $k(B)$, again a contradiction. ◻

Proof. The two premise kingdoms are disjoint. If they intersected, subnet algebra would make their union a subnet; a correction path inside that union would join $A_1$ to $A_2$, and adding the two tensor edges would form a cycle. Their disjoint union, joined through the tensor root, is therefore a proof net with door $A_1\otimes A_2$. Minimality gives $$k(A_1\otimes A_2)\subseteq k(A_1)\cup k(A_2)\cup \{A_1\otimes A_2\}.$$ Conversely, intersect $k(A_i)$ with $k(A_1\otimes A_2)$. The intersection is nonempty at $A_i$, is a subnet by lemma 40.11, and still has $A_i$ as a door. Minimality of $k(A_i)$ forces $k(A_i)\subseteq k(A_1\otimes A_2)$ for $i=1,2$. The tensor root and its edges also belong to its kingdom. This proves the reverse inclusion. ◻

Proof. The intersection $k(A)\cap k(B)$ is nonempty at $A$, so lemma 40.11 makes it a subnet. Occurrence $A$ remains a door of the intersection. Minimality of $k(A)$ gives $$k(A)=k(A)\cap k(B),$$ which is the required inclusion. ◻

Proof. Reflexivity follows because $B$ is a door of $k(B)$. Two applications of lemma 40.14 prove transitivity.

For antisymmetry, suppose distinct nonliteral $A,B$ satisfy $A\in k(B)$ and $B\in k(A)$. Then the two minimal subnets coincide. Call the common subnet $K$. Both $A$ and $B$ are doors of $K$. If $A=A_1\mathrm{\wp }{A}_2$, delete the par root and promote $A_1,A_2$ to doors. In every switching of $K$, the par root was a leaf attached by the one selected premise edge, because $A$ was a door. Deleting that leaf therefore leaves a tree. The resulting smaller subnet still has $B$ as a door, contradicting minimality of $k(B)$. If $A=A_1\otimes A_2$, lemma 40.13 says that its kingdom is the union of the kingdoms of its two premises together with the tensor root. Occurrence $B$ therefore lies in, say, $k(A_1)$. Since $B$ is nonliteral, one of its immediate subformulas $B^{\prime }$ also lies in $k(A_1)\subseteq e(A_1)$. The mutual-containment assumption includes $A\in k(B)$. The boundary calculation of lemma 40.12, applied to $A_1$ below $A$ and $B^{\prime }$ below $B$, now gives $B\notin e(A_1)$. This contradicts $B\in k(A_1)\subseteq e(A_1)$. Thus $A=B$. ◻

Proof. There is a tensor conclusion. Otherwise all conclusions would be literals, so the structure would be a disjoint union of axiom edges; connectedness and more than one axiom link are incompatible. Choose a tensor conclusion $A\otimes B$ maximal among the nonliteral conclusions in the finite kingdom order of lemma 40.15. We show that $$N=\{A\otimes B\}\cup e(A)\cup e(B),$$ with the two empires disjoint.

The two empires cannot intersect. Otherwise their union would be a subnet containing a path from $A$ to $B$; adding the two tensor edges would create a cycle in every switching. In particular, an ancestor chain starting in $e(A)$ cannot reach the selected tensor through its $B$-premise.

By definition 40.10, every subnet having a conclusion $D$ as door contains every descendant occurrence of $D$; in particular, if $C$ is below $D$, then $C\in k(D)$. This is the only ancestor-to-kingdom implication used next.

Besides the selected edge $A\to A\otimes B$, suppose that $e(A)$ had a formula-tree edge crossing its boundary. Choose the first such edge $C^{\prime }\to C$, with $C^{\prime }\in e(A)$ and $C\notin e(A)$. Following ancestors from the nonliteral occurrence $C$ reaches a nonliteral conclusion. It is not the selected tensor, because its selected edge was excluded, and it cannot be par by hypothesis; write it as $D\otimes E$. Downward closure gives $C\in k(D\otimes E)$. By lemma 40.12, $A\otimes B\in k(C)\subseteq k(D\otimes E)$, where the inclusion is lemma 40.14; this contradicts maximality. Thus no formula-tree edge escapes either empire except through the selected tensor root.

The coverage now follows from connectedness, not from the boundary statement alone. Fix a switching and suppose a vertex $X$ lay outside $e(A)\cup e(B)\cup \{A\otimes B\}$. A correction path from $X$ to the selected tensor must enter that union for the first time. It cannot cross an axiom edge, because each empire is closed under axiom matching. It cannot cross a formula-tree edge, because the only boundary edges are the two edges from the selected tensor to $A$ and $B$, and the selected tensor has no edge toward the outside. This contradicts connectedness. Hence the displayed union covers $N$, including all literal conclusions.

Therefore deleting the root leaves the two disjoint proof nets $e(A)$ and $e(B)$, as claimed. ◻

Proof. If the structure is a translation, correctness follows from theorem 40.9. Conversely, suppose that the structure is correct and induct on the number of logical links. With none, connectedness forces a single axiom link, which is Ax.

If a conclusion has par root, delete that root. In every switching the root was a leaf, so its deletion leaves a tree. The smaller net sequentializes by the induction hypothesis; append Par.

Otherwise no conclusion has par root. By correctness, this branch has at least two axiom links: with only one axiom, any logical link would be a tensor joining its two literal branches and would create a cycle in the unique switching. By lemma 40.16, choose a splitting conclusion $A\otimes B$. Its deletion produces two smaller proof nets and distributes every literal side conclusion between them. Sequentialize them independently and append Tensor. The reconstructed derivation translates to the original occurrence graph at each step. ◻

Proof. The bit vectors enumerate each switching exactly once. Depth-first search accepts a finite undirected graph exactly when it is connected and acyclic. This proves functional correctness. One adjacency representation and the search arrays are linear. There are $2^k$ searches, each linear in the size of a correction graph. On an accepted input no search stops early, so the stated family realizes the lower bound for this implementation. ◻

Proof. Guerrini’s sequential-unification algorithm proves this bound. Definitions 1–4 and Theorem 5, proceedings pp. 455–456, identify the structure and the Danos–Regnier/sequentialization problem. Section 5.5 and Theorem 15, proceedings p. 463, prove the linear bound for sequential unification, including the ordered special case of disjoint-set union used by the algorithm [Gue99]. The source explicitly excludes multiplicative constants; it notes that adding them changes the complexity boundary. We use the theorem only for the signature in definition 40.1. ◻

Proof. For an atomic step, every correction graph replaces one path by one edge. Path contraction preserves connectedness and acyclicity.

Consider a multiplicative step and fix a switching outside its redex. Delete the tensor root, the par root, the cut link, and all their incident edges; call the remaining forest $R$. Its four boundary vertices are $A,B,A^{⟂},B^{⟂}$. Switching the old par to $A^{⟂}$ gives a tree; therefore the components of $R$ containing $A,B,A^{⟂}$ must be pairwise distinct. Every component of $R$ must contain one of those three vertices, since the old redex connects no other component. Switching instead to $B^{⟂}$ shows that the components containing $A,B,B^{⟂}$ are pairwise distinct. The only possible partition is therefore $$\{A\},\{B\},\{A^{⟂},B^{⟂}\},$$ where braces name components, not necessarily singleton vertex sets. The reduct adds two cut vertices and their four incident edges. Suppressing each degree-two cut vertex leaves the two connections $A-A^{⟂}$ and $B-B^{⟂}$; they join the three tree components without a cycle, so the result is a tree. The argument applies to every outside switching. ◻

Proof. Let $|p|=|p^{⟂}|=0$ and $|A\otimes B|=|A\mathrm{\wp }B|=1+|A|+|B|$. Order nets lexicographically by $$(\sum _{c\text{ a cut}}|A_c|,\mathrm{\#}\{c\mid c\text{ is an atomic cut}\}),$$ where $A_c$ is either side of cut $c$. A multiplicative step decreases the first coordinate by one; it may increase the second. An atomic redex contributes zero to the first sum, so its contraction leaves that sum unchanged and decreases the second coordinate by one. Hence every step decreases this pair lexicographically. ◻

Proof. Each multiplicative step lowers the connective-size sum by exactly one, so there are at most $m$ such steps. It replaces one cut by two and hence increases the cut count by one. After those steps, at most $c+m$ atomic cuts remain, each removed in one step. Thus the total is at most $m+(c+m)=c+2m$. ◻

Proof. Two multiplicative redexes are disjoint formula occurrences and their steps commute. A multiplicative and an atomic redex are likewise disjoint. Two atomic redexes either are disjoint or occupy adjacent cut edges of one alternating axiom–cut path. In the adjacent case, either contraction shortens that path; contracting the remaining cut produces the same single spliced axiom edge. These are all overlaps because a formula occurrence is the premise of at most one logical or cut link and belongs to exactly one axiom link when literal. ◻

Proof. Use well-founded induction on the source $x$ under the transitive reduction order. Suppose $x{⟶}^{\ast }y$ and $x{⟶}^{\ast }z$. If one path is empty, the other endpoint is already a common reduct. Otherwise write the first steps as $x⟶y_1{⟶}^{\ast }y$ and $x⟶z_1{⟶}^{\ast }z$. Local confluence gives $w$ with $y_1{⟶}^{\ast }w$ and $z_1{⟶}^{\ast }w$ (one-step joins are allowed to be reflexive on either side). Apply the induction hypothesis at $y_1$ to join $y$ with $w$, and at $z_1$ to join $z$ with $w$. The two resulting reducts of $w$ are joined by one final induction application at $w$. All three sources are strict reducts of $x$, so the induction is well founded. ◻

Proof. Preservation and strong normalization are lemma 40.23, lemma 40.24. Local confluence is lemma 40.26. Lemma 40.27 applies to a strongly normalizing, locally confluent relation and yields confluence. Normal forms contain no cut: a cut formula is either literal, when the atomic rule applies, or has dual tensor/par roots, when the multiplicative rule applies. Confluence then gives uniqueness. ◻

Proof. Translate the derivation with the cut clause above. Normalize its cut vertices by theorem 40.28; correctness and the external conclusion multiset are preserved. The normal net is cut free, so sequentialize it by theorem 40.17. The resulting cut-free derivation has exactly the original conclusions. ◻

Proof. By corollary 40.29, choose a cut-free derivation. Read it from conclusion to premises. Rule Par replaces its principal formula by its two immediate subformulas, rule Tensor does the same while partitioning the side conclusions, and Ax contains only its two literal conclusions. Induction on the derivation therefore gives the subformula property. A one-literal sequent cannot end in Ax, Par, or Tensor, so it has no cut-free derivation and hence no derivation. ◻

Proof. Count pairs consisting of a Par above an independent Tensor that can be exchanged. Commuting the par downward decreases this inversion count and creates no new inversion below it. Repetition terminates at a phase-ordered derivation. In the translated structure, the exchanged rules add the same two logical vertices and the same incidence edges; only their heights in the derivation tree changed. Thus $\mathcal{N}$ is invariant. ◻

Proof. Count the rules below the rule that introduced the selected conclusion occurrence. For a par conclusion, every lower rule has an incomparable principal occurrence. If that rule is a tensor, the selected par and all of its side conclusions lie wholly in one tensor premise. The two rules are therefore independent by definition 40.31; commute the par one step downward. The count decreases, so repetition makes it last.

For a splitting tensor, deleting its root partitions the translated net into two components. Every lower rule acts wholly inside one component. A lower tensor joining occurrences from both components would leave a logical edge between them after the selected root was deleted, contradicting the splitting hypothesis. Hence each lower rule satisfies the whole-premise condition of definition 40.31 and commutes upward past the selected tensor. Again the number of lower rules decreases. When the selected tensor is last, its premise occurrence graphs are exactly the two components, because translation is unchanged by every commute. ◻

Proof. By lemma 40.32, every equivalence class has a phase-ordered representative and translation is constant on a class. Surjectivity is theorem 40.17. For injectivity, run sequentialization on the common net. At a par conclusion, apply lemma 40.33 to put that par last in both proofs. Delete it and apply induction to the common smaller net. When no par conclusion remains, choose the same maximal splitting tensor among the nonliteral conclusions by lemma 40.16. Apply lemma 40.33 to put that tensor last in both proofs and identify their two premise graphs with the same two subnet components. Literal conclusions lie on the unique component fixed by the occurrence graph. Induction on each smaller component transforms the two pairs of premise derivations into the same reconstructed premises. Reapplying the common last rule shows that the original derivations differ only by permitted permutations. ◻