On the correspondence between proof nets and sequents

Question

1. Context
While trying to answer my question on the existence of a (useful) graphical calculus for star-autonomous categories, I came across the paper Natural deduction and coherence for weakly distributive categories by Blute, Cockett, Seely and Trimble. After having defined circuits (for given types $\mathscr{T}$ and components $\mathscr{C}$) they look at particular typed circuits, namely $(\otimes,\oplus)$-circuits with components $\mathscr{C}$ and atomic types $\mathscr{A}$. Among the components $\mathscr{C}$ are links called $\otimes$-introduction and $\otimes$-elimination:

component links	terminology
[A,B] $\otimes$I [A $\otimes$ B]	$\otimes$-introduction
[A $\otimes$ B] $\otimes$E [A,B]	$\otimes$-elimination

Pictorially they are represented as follows:

Blute et al write on page 241:

Proof theoretically the $\otimes I$ link corresponds to the right-introduction rule for the tensor and $\otimes E$ to the left-introduction rule of the tensor. \begin{equation} \dfrac{{\Gamma_1\vdash \Gamma_2,A,\Gamma_3}\qquad{\Delta_1\vdash \Delta_2,B,\Delta_3}}{\Gamma_1, \Delta_1 \vdash \Gamma_2, \Delta_2, A \otimes B, \Gamma_3, \Delta_3}(\otimes R) \end{equation} \begin{equation} \dfrac{{\Gamma_1,A,B,\Gamma_2\vdash \Gamma_3}}{\Gamma_1,A \otimes B, \Gamma_2 \vdash \Gamma_3}(\otimes L) \end{equation}

2. Questions
I do not see how the above links correspond to the given rules of inference. For instance, the $\otimes$-elimination is an elimination rule while $\otimes L$ is an introduction rule. Furthermore, the two links simply seem a reflection of one another (in their pictorial representation a horizontal reflection) while the rules of inference appear to have a greater structural difference. The right-introduction rule derives from two sequents a third while the left-introduction "only uses one sequent".

• How does the correspondence between the above rules of inference and links look like?
• Does one read the right-hand side of the sequents in the derivation from top to bottom while the left-hand side is read from bottom to top? If so, why?

Answer 1

First, it might be of interest to you to know that Table 1 in this paper by Dominic Hughes compares various diagrammatic presentations of the free *-autonomous category (including the paper you've cited).

As for your concrete questions:

• In these circuits, the inputs at the top correspond to the left of a sequent, while outputs at the bottom correspond to the right of a sequent. The ⊗L sequent calculus rule turns a sequent with A,B on the left into a sequent with A⊗B on the left; this corresponds to taking a circuit with inputs A,B and plugging them into a ⊗E link so that the resulting circuit has an input A⊗B. (There might be some other formulas on the left / inputs of the circuit, which are unchanged.) A similar interpretation can be given for ⊗R: take two circuits, put them next to each other, take the output A from the first and B from the second, and plug them into a ⊗I link with output A⊗B.

• "the two links simply seem a reflection of one another while the rules of inference appear to have a greater structural difference": this is a great point! It is usual in various proof net formalisms — and this applies to Blute et al.'s circuits — that "locally", the link introducing ⊗ and its dual look basically the same (actually, in linear logic the De Morgan dual of ⊗ would be the connective denoted here by ⊕, and you can see here that ⊕I and ⊗I have the same shape). So to distinguish them, one needs to impose an additional condition: a global and combinatorial "correctness criterion", formulated using "switches" which are drawn using arcs in the paper (you can see that there is an arc between the A and B edges of ⊗E, which is not the case for ⊗I).