You Can Only Cross The Same River Once
The formula is strange. For example, here’s a small proof fragment, where is an arbitrary goal formula:
Is the 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 is the same resource. Intuitively, though, there is a sense in which they’re different. Abusing the resource metaphor quite badly, one instance of 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 s look like? What would it be good for, if anything? Does it already exist?