Currently I am back in moderately pleased state. I think I may have finally sussed out the solution to three issues I've been confusedly equivocating over for so long:
- whether variables in the context are each labelled with arbitrary world expressions, or labelled with distinct fresh worlds
- whether weakening of labels is a principle that must be satisfied by all rules, or is a rule itself
- whether the context includes hypothetical inequalities, or does not
I believe the answer is that taking the first option of all three choices as I've listed them works, and so does taking the second option of all three.
I formerly thought these lined up with the distinction between bunched and linear logic, but now that claim is very shaky. So far both of these systems seem to be expressing bunched logic perfectly well, and linear logic is just inexpressible. That part is still very frustrating.
The theorem that ought to relate the two systems is:
For all sets of inequalities L, and propositions Ai, C, and world-expressions pi,
L, A1[p1], ... An[pn] |- C[r]
there exists q over the variables a1, ..., an such that
A1[a1], ... An[an] |- C[q]
and L |- r ≥ [p1/a1]...[pn/an]q
The thing is I really need to get off my ass and dig into the literature like I've been promising myself to and find what everyone else has done about these choice-points, 'cause I know for a fact that there's a shit-ton of stuff out there that at least has a great chance of being relevant. It's troubling that so much of it is classical --- I don't know what, if any, of their results apply to my effort, and even if they did, how to translate them.
Ugh, just kidding, found yet another problem with that proof. God dammit.