Return to 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:

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 correpondence 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?

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:

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?

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:

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. Question
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 correpondence 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?

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:

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 correpondence 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?