chrisamaphone expressed her preference for naming it, the "contingent transition problem") that she and taus were discussing so fruitfully is really fascinating. It was a topic that came up frequently back in early stages of my thesis discussions with Frank, since we kind of thought having first-class labels for state might provide a solution. But I think they don't provide as strong a solution as can be hoped for.My digestion of their thoughts goes as follows: (which, incidentally, is meant to repudiate all the comments I left on that post, which are a broken semi-solution, I now think)
Suppose c is a positive atom. P and N will stand for general positive and negative propositions. I'd like to add to the logic a propositional notation [c]N, which, when it's on the left of the turnstile, means "you can focus on N as long as c is in the context right now".
Ok, fine, [c]N = c -o N, bam, done. PROBLEM: c is consumed, and N wanted to use that delicious, succulent positive atom. Ok, fine, [c]N = c -o c * N. PROBLEM: switching back to positive polarity means that by the time you're focusing on N again, the c may no longer be around. Like, the beginning (bottom) of my proof might look like this:
N |- P
--------------------------
c, N, c -o 1 |- P
--------------------------
c, c -o c * N, c -o 1 |- P
now I'm able to choose to focus on N --- or wait until later! --- even though c is gone. This is not the intended semantics of [c]N.
Ok, so what I'll try is defining [c]N = c -o {c}N and defining {c}N recursively in N.
{c}(^P) = ^(c * P)
{c}(N & N) = {c}N1 & {c}N2
{c}(top) = top
{c}(P -o N) = ({c}P -o N) & (P -o {c}N)
{c}(vN) = v(c -o N)
{c}(P1 + P2) = {c}P1 + {c}P2
{c}(0) = 0
{c}(P1 * P2) = ({c}P1 * P2) + (P1 * {c}P2)
{c}(1) = 0
This threads the c down through the synchronous meat of N down to wherever the shifts are, and whenever they happen, it "gives c back". The & in the case for -o (and the + in the case for *) expresses the choice involved in the multiplicative context-split between two contexts: we can send the c (the one that we're eventually going to stick in some context, but not until we find a shift) to either side, our choice.
Then we can extend [c]N to more general positive propositions by saying
[P1 + P2]N = [P1]N & [P2]N
[P1 * P2]N = [P1][P2]N
[0]N = top
[1]N = N
---
Anyway I am again intrigued whenever something kinda like the product rule for derivatives (aka "Leibniz Law" from first-year calculus, d/dx (fg) = (df/dx) g + f (dg/dx)) shows up in logic (like it did in that graph-logic stuff).
I never had occasion above to define a dual [c]P = c * {c}P, but it almost smells suspiciously (If I'm allowed to imagine {c}P to be "a P with a c-shaped hole" just because {c} is slightly derivative-like, and derivatives of types are types with holes) like "a c together with a P with a c-shaped hole", which is a satisfying pair of things to have.
---
Huh! Indeed by an easy induction I can show that always [c]P |- P and N |- [c]N. This kind of makes sense, I guess? If [c]N on the left means "you can use N as long as you can verify c is present without really consuming it" then [c]N on the right must mean something like "you must make N, but you are provided with the assumption that c is present, without really producing it". So if you already have an N in the context, you should be able to make a [c]N, ignoring the assumption of c's presence.
