Natural Deduction: An unusual presentation?

Question

1. Context
On page 241 of their paper Natural deduction and coherence for weakly distributive categories Blute et al give the right- and left-introduction rules of multiplicative conjunction for (multiplicative) linear logic as follows:

\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}

They then write:

Thinking in terms of natural deduction, these rules induct a (bijective, once we have the right equations) correspondence indicated by these “rules”: \begin{equation} \dfrac{{\Gamma_1,A \otimes B, \Gamma_2 \vdash \Delta}}{\Gamma_1,A,B,\Gamma_2\vdash \Delta}(\otimes -intro), \end{equation} \begin{equation} \dfrac{{\Gamma_1,A, B, \Gamma_2 \vdash \Delta}}{\Gamma_1, A \otimes B,\Gamma_2\vdash \Delta}(\otimes -elim) \end{equation}

2. Question
I am familiar with the Fitch notation for natural deduction as well as the presentation given in Girard's Proofs and Types. However, the sequent-like (?) notation used here eludes me.

• How is it read? How does one translate this presentation into the one given by Girard say?
• Are there any texts that introduce/explain this notation?

EDIT:
In the comments it was suggested that this is a typo and that the (-elim) and (-intro) names should be swapped. However, the authors repeat the "typo" on the same page leaving me to believe that they read the inference rules of natural deduction bottom-up:

A curiosity is the apparent lack of symmetry between unit introduction and elimination links. Logically they correspond to the (again bijective) correspondence: \begin{equation} \dfrac{{\Gamma_1, \top, \Gamma_2 \vdash \Delta}}{\Gamma_1, \Gamma_2\vdash \Delta}(\top -intro), \end{equation} \begin{equation} \dfrac{{\Gamma_1, \Gamma_2 \vdash \Delta}}{\Gamma_1,\top, \Gamma_2\vdash \Delta}(\top -elim) \end{equation}

Answer 1

Long comment

Based on the previous Def.1.1 the tensor $⊗$ "works like" AND: $A ⊗ \top \to A$, and thus the pair of rules above are exactly those for $∧$ in Sequent Calculus.

The first one reads (simplifying contexts) "from premises 'if $C$ then $A$' and 'if $C$ then $B$', the conclusion 'if $C$ then $A⊗B$' follows".

And the second one reads: "from premises 'if $A$ then $C$' and 'if $B$ then $C$', the conclusion 'if $A⊗B$' then $C$' follows".

Now about the main issue: the text of the paper is right. The "standard" translation from SC to ND maps e.g. $(\text L \land)$ to $(\land \text E)$ and so on (see Negri & von Plato, Structural Proof Theory, page 173).

Why so? You are right: the "mapping" works bottom-up:

$(\text L \land) \text { rule } \dfrac {A,B \vdash C}{A \land B \vdash C} \text { will be } (\land \text E) \text { rule } \dfrac {A \land B \ \ [A], [B] \vdash C}{C}$

---

Note from this point of view, the $\top$ rules are not very useful: they amounts to specifying the trivial fact that adding or removing $\top$ from the set of premises does not affect the validity of the inference.