In a picture, here is what went wrong:

And here is a new attempt at doing the right thing:

The x that I'm quantifying over is a boolean variable drawn from a language of boolean expressions, that counts how many circles (zero or one) are meant to be shoved in front of a proposition. The language of boolean expressions looks like this:

What I did was pushed the disjunction over where the circle went

*into*this choice variable, which I'm existentially (disjunctively) quantifying over. Now if I take the rules

and try to prove

A ⊗ A = ∃x.◯

_{x}A ∧ ◯

_{~x}A) ⊢ A

then I find, as is desired, that I can't! I have a constructive hypothesis x that's governing which way the ◯ goes, and I can't do any case-analysis or LEM-like reasoning to consider all the cases. So I think there's something about this that is on the right track. I can also still prove commutativity and associativity of ⊗. Commutativity requires that ~~x = x, (I get a fresh variable x in the existential quantifier on the left, and then I instantiate the one on the right with ~x) and associativity requires a little bit more careful synchronous-quantifier-instantiation and reasoning about boolean functions, but I think it all works out just fine.

However, I run into trouble trying to define the right adjoint. I'm pressured inconsistently from different considerations into making lollipop one of the two following forms:

for (maybe) filled-circle being some kind of slightly different modality. Secretly I am rooting for a different modality to be required, since it seems fancier, and potentially has a better focusing story, since filled-circle could be negative, and hollow-circle positive.

The unit is also unclear; I think I probably have to introduce a new proposition that interacts with the bit-label machinery, something like this:

(full image here)

Anyway I am pretty excited by this whole line of thinking! It tantalizingly suggests there is a

**purely equational**(i.e. no inequalities on context structures are required, as they are in the resource semantics paper I worked on with Frank) way of reducing the logic of BI to first-order logic. It separately looks like it would have the nice property that it's essentially the identity on all the additive structure.