ch:proof-nets: ch:proof-nets

Let $P=p^{⟂}\mathrm{\wp }{q}^{⟂}$ and $R=r^{⟂}\mathrm{\wp }{s}^{⟂}$. The second schedule is $$\frac{{\displaystyle \frac{\mathrm{\Pi }}{⊢p^{⟂},q^{⟂},R,T}}\mathrm{Par}}{⊢P,R,T}\mathrm{Par}.$$ The first principal pair consists of the displayed $r^{⟂}$ and $s^{⟂}$ occurrences; the second consists of $p^{⟂}$ and $q^{⟂}$. Neither pair contains an occurrence from the other pair, so neither principal formula is a subformula of the other. Erasing heights in either schedule leaves the same four axiom edges, the same three tensor roots forming $T$, and the same two par roots forming $P,R$. Thus the incidence graphs coincide occurrence for occurrence.

For the running net, left selection at the par gives the path $$q^{⟂}-q-\otimes -p-p^{⟂}-\mathrm{\wp },$$ so the path between the conclusion roots is its whole reversal from $\mathrm{\wp }$ to $\otimes$. Right selection gives $$p^{⟂}-p-\otimes -q-q^{⟂}-\mathrm{\wp }.$$ Each is a path through all six vertices and hence a tree.

The cyclic example has six vertices and six edges: two axiom and four tensor premise edges. A tree on six vertices would have five edges. More directly, $$p^{⟂}-\otimes -q^{⟂}-q-\otimes -p-p^{⟂}$$ is a cycle.

For the disconnected example write the par roots $P,Q$. In par order $(P,Q)$, the four vectors and selected edges are In every row the two component vertex sets are $$\{P,p,p^{⟂}\},\{Q,q,q^{⟂}\}.$$ Only the selected edge inside each component changes. All four switchings fail connectedness.

The structure of example 40.5 satisfies every local arity and duality condition, yet its unique switching contains the displayed six-edge cycle. The structure of example 40.6 also satisfies those conditions, yet every switching has two components. For any fixed inspection radius, insert equally many tensor/par layers along the paths between the links. The radius-(r) neighbourhood of each link is unchanged while closing the two distant paths creates a cycle, or keeping them apart creates disconnection. Local incidence therefore cannot decide either global property.

Retaining both par premises in the running example produces the cycle $$p^{⟂}-\mathrm{\wp }-q^{⟂}-q-\otimes -p-p^{⟂}.$$ The false sentence in the Par case of lemma 40.8 is that the new par vertex is attached by exactly one selected edge. With both edges retained it is not a leaf, and the second attachment closes the cycle.

Delete the conclusion par root first. The remaining conclusions are $p^{⟂},q^{⟂},p\otimes q$. The tensor root is splitting: one component has conclusions $p^{⟂},p$, the other $q,q^{⟂}$. Both are axioms. Reversing these deletions reconstructs $$\frac{{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{\phantom{X}}{⊢p^{⟂},p}}\mathrm{Ax}\\ {\displaystyle \frac{\phantom{X}}{⊢q,q^{⟂}}}\mathrm{Ax}\end{array}}{⊢p^{⟂},p\otimes q,q^{⟂}}}\mathrm{Tensor}}{⊢p^{⟂}\mathrm{\wp }{q}^{⟂},p\otimes q}\mathrm{Par}.$$ Translation restores exactly the deleted roots and incidence edges.

Immediately after deleting the two par roots, the only conclusion tensor is $T=((p\otimes q)\otimes r)\otimes s$, and it is splitting. Its two premise nets have conclusion multisets $$\{((p\otimes q)\otimes r),p^{⟂},q^{⟂},r^{⟂}\},\{s,s^{⟂}\}.$$ The first recursive call exposes the splitting conclusion $(p\otimes q)\otimes r$, and the next exposes $p\otimes q$. Thus the three tensor conclusions encountered successively are $p\otimes q$, $(p\otimes q)\otimes r$, and $T$ when read in reconstruction order. The corresponding last three tensor rules combine the $p,q$ axioms, then that result with the $r$ axiom, then that result with the $s$ axiom. The side conclusions are respectively the unused dual literals, so every premise multiset is exactly the one forced by the two subnet components.

Order par roots from the left conclusion to the right and visit integer-labeled vertices increasingly whenever the representation offers a choice. The running net examines vectors $0,1$, visits all six vertices in each, and accepts after two switchings. The cyclic net has no par bit; its first and only correction graph revisits a nonparent vertex on the six-edge cycle, so it rejects switching 1 for a cycle. The disconnected net first examines $00$. Depth-first search finishes the $p$-component with the three $q$-component vertices unvisited, so it rejects switching 1 for disconnection. These are the counts and reasons printed by corpus cases PN-CORRECT-2, PN-CYCLIC-1, and PN-DISCONNECTED-4.

Write $\alpha =p^{⟂}\mathrm{\wp }{q}^{⟂}$, $\beta =\alpha \mathrm{\wp }{r}^{⟂}$, $\tau =p\otimes q$, and $\rho =\tau \otimes r$. All switchings contain the three equal-name axiom edges and the four tensor edges $p-\tau ,q-\tau ,\tau -\rho ,r-\rho$. In par order $(\alpha ,\beta )$, their additional edges are There are ten vertices and nine retained edges. In each row every negative literal reaches its positive mate, the positive tensor tree reaches $\rho$, the selected inner-par edge attaches $\alpha$, and the selected outer-par edge attaches $\beta$. Hence the graph is connected; with nine edges on ten vertices it is a tree. This uses no sequentialization theorem.

Backward sequentialization deletes $\beta$, giving $⊢\alpha ,r^{⟂},\rho$, then deletes $\alpha$, giving $⊢p^{⟂},q^{⟂},r^{⟂},\rho$. Tensor $\rho$ splits this into $⊢p^{⟂},q^{⟂},\tau$ and $⊢r^{⟂},r$. Tensor $\tau$ splits the first premise into the $p$- and $q$-axioms.

One reconstruction first builds $\tau$, applies Par to $p^{⟂},q^{⟂}$, combines $\tau$ with the $r$-axiom by Tensor, and finally builds $\beta$. A second first builds $\tau$, immediately combines it with the $r$-axiom to build $\rho$, then builds $\alpha$ and $\beta$. The first Par and the Tensor building $\rho$ act on disjoint occurrences, so commuting them transforms one derivation into the other. Both translations contain the same three axiom, two tensor, and two par links with the same incidences.

After the outer contraction, the cuts are $p_0\otimes q_0$ against $p_1^{⟂}\mathrm{\wp }{q}_1^{⟂}$, and $r_0$ against $r_1^{⟂}$. After the inner contraction, the three atomic cuts are $p_0/p_1^{⟂}$, $q_0/q_1^{⟂}$, and $r_0/r_1^{⟂}$. Their splices join the indexed exterior axiom endpoints $$p_0^{⟂}-p_1,q_0^{⟂}-q_1,r_0^{⟂}-r_1.$$ Schedule 1 has measures $$(2,0)\to (1,1)\to (0,3)\stackrel{p}{\to }(0,2)\stackrel{q}{\to }(0,1)\stackrel{r}{\to }(0,0).$$ Schedule 2 has measures $$(2,0)\to (1,1)\stackrel{r}{\to }(1,0)\to (0,2)\stackrel{q}{\to }(0,1)\stackrel{p}{\to }(0,0).$$ Both endpoints are therefore the expanded cut-free identity net with conclusions $A_0^{⟂},A_1$, and the three displayed axiom splices name every atomic contraction.

For $i\in \mathbb{Z}/k\mathbb{Z}$, take outer conclusions $(L_i\mathrm{\wp }{R}_i)\otimes S_i$ and one tensor tree whose leaves are the $U_i$ (for $k=1$, its conclusion is just $U_0$). Link $L_i$ by an axiom to $U_i$, and link $R_i$ to $S_{i+1}$. Choose names and polarities so that each displayed pair is dual.

Contract each connected fixed-edge component. The all-left vector $00\cdots 0$ becomes a star: every outer component is joined once to the central $U$-component. It is a tree, and expanding the contracted tree components preserves that fact. The all-right vector $11\cdots 1$ leaves the central component isolated and joins the outer components in a cycle. For $k=1$, that quotient loop expands to the cycle through the par root, $R_0$, its axiom mate $S_0$, and the outer tensor root. Thus one explicit switching passes and one fails for every $k\ge 1$; a distinguished single switching cannot be a correctness criterion.

The derivation is $$\frac{{\displaystyle \frac{\phantom{X}}{⊢1_{\mathsf{u}}}}\mathrm{One}}{⊢1_{\mathsf{u}},{\mathrm{\perp }}_{\mathsf{u}}}\mathrm{Bottom}.$$ Under the proposed translation it has two nullary vertices and no edge, so its correction graph is disconnected. The missing case of lemma 40.8 is Bottom: the old leaf argument has no edge by which to attach the new ${\mathrm{\perp }}_{\mathsf{u}}$ vertex. Hence the old criterion is not sound for the extended signature, without deciding what the repaired unit criterion should be.