chrisamaphone was interested in since it came up on twitter.As far as I got was the following paging-back-in of what I remembered of it: (which may be redundant with stuff you already know, chris?)
If we want to have a three-way connective A -[c]o B pronounced "A linearly implies B contingent on positive atom c being in the context right now", then a candidate shibboleth sequent for whether we've done it right is the nonprovability of
a -[c]o 0, c, c -o a |- 0
where a is also a positive atom. The sequent is attainable (by focusing on a -[c]o n) if at the same time we can (1) consume a and (2) non-destructively observe c. But we can only continue observing c if we don't depend on consuming it in the process of using c -o a.
This sequent suffices to tell us that the "consume c and give it back immediately" strategy
A -[c]o B = c -o c * (A -o B)
is no good, since
c -o c * (a -o 0), c, c -o a |- 0
is easily provable. But also we can see even the "consume c and give it back at the next focusing blur" strategy I tried to propose here is not right. For in that case we get something like
a -[c]o 0 = [c](a -o 0)
= c -o {c}(a -o 0)
= c -o ({c}a -o 0 & a -o {c}0)
= c -o ((c -o a) -o 0 & a -o (c * 0))
and it is possible to prove
c -o ((c -o a) -o 0 & a -o (c * 0)), c, c -o a |- 0
(c -o a) -o 0 & a -o (c * 0), c -o a |- 0
(c -o a) -o 0, c -o a |- 0
Except come to think of it I may have done the translation wrong, because a is a positive atom and shouldn't actually be the locus of a "give-c-back" action. Hmmm.
---
Actually, the left rule I imagine for A -[c]o B is
Δ |- A Γ, B |- D c ∈ Δ, Γ ------------------------------------------- Δ, Γ, A -[c]o |- D
which doesn't preclude
c, c -o a |- a 0 |- 0 ------------------------- a -[c]o 0, c, c -o a |- 0
at all, unless we imagine a focusing discipline where we keep focus on a:
c, c -o a |- [a] 0 |- 0 ------------------------- [a -[c]o 0], c, c -o a |- 0
but then this would mean a failure of completeness of focusing; a sequent that's provable if we don't do focusing, but isn't if we do. This seems to imply that A -[c]o B can't be a negative proposition that allows focusing to flow through to a positive first argument A.
