You Can Only Cross The Same River Once

The formula a \otimes b \multimap a is strange. For example, here’s a small proof fragment, where C is an arbitrary goal formula:

\frac{\frac{\overline{a \vdash a} \qquad \overline{b \vdash b}}{a,b \vdash a \otimes b} \qquad \Delta, a \vdash C}{\Delta, a,b,a \otimes b \multimap a \vdash C}

Is the a in the right premise of the loli-left rule the same as the one we started with in the conclusion?

Read the rest of this entry »