(no subject)
Aha! Everything seems to work out very nicely if I try to do that monoid-labelled logic in the style of my previous CPS-ish encodings of substructural logics into first-order logic, where I get all the statefulness I need just by exploiting the linearity of the intuitionistic conclusion.

I'm still having some mysterious trouble encoding BI's multiplicative unit. I'm conjecturing that the difference between BI as such and the logic of the category of graphs has something to do with either that, or imposing commutativity on this operation "+" on the first-order domain. To encode BI, I want it to be noncommutative, because the first-order expressions correspond to paths through the context. But with the intuitions coming from graphs, the first-order expressions are merely 0-1 counts of how many times you've passed from the presheaf bucket that holds all the edges of the graph, to the bucket containing vertices --- and these counts are intrinsically commutative. Mmmmmaybe this has to do with how graph-logic seems to be endowed with all these extra equations on contexts. Then again, they all have to do with the multiplicative unit, also, so it's hard for me to discern what to blame yet.
---
Actually having a lot of trouble figuring out whether this really can model BI even without the multiplicative unit. Might need some noncommutative generalizations of boolean algebras...

I'm still having some mysterious trouble encoding BI's multiplicative unit. I'm conjecturing that the difference between BI as such and the logic of the category of graphs has something to do with either that, or imposing commutativity on this operation "+" on the first-order domain. To encode BI, I want it to be noncommutative, because the first-order expressions correspond to paths through the context. But with the intuitions coming from graphs, the first-order expressions are merely 0-1 counts of how many times you've passed from the presheaf bucket that holds all the edges of the graph, to the bucket containing vertices --- and these counts are intrinsically commutative. Mmmmmaybe this has to do with how graph-logic seems to be endowed with all these extra equations on contexts. Then again, they all have to do with the multiplicative unit, also, so it's hard for me to discern what to blame yet.
---
Actually having a lot of trouble figuring out whether this really can model BI even without the multiplicative unit. Might need some noncommutative generalizations of boolean algebras...