You Can Only Cross The Same River Once

by ivoysey

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?

I think that there’s no difference in terms of what can be proven, so as far as the logic is concerned no: any a is the same resource. Intuitively, though, there is a sense in which they’re different. Abusing the resource metaphor quite badly, one instance of a has been through the loli machine and the other has never been used.

In this particular case we could tell them apart in the logic by looking at the larger context in which they appear, since the machine is also consumed but in the presence of bang that’s not the case. I could imagine, also, subscripting each atom or formula with a counter that keeps track of how many rules have been applied in a given proof that use that atom.

What would a logic that distinguishes between these two as look like? What would it be good for, if anything? Does it already exist?