Jason (jcreed) wrote,

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.
Monoid Logic -> FOL

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...
Tags: bunched, logic, math

  • (no subject)

    Something that's bugged me for a long time is this: How many paths, starting at the origin, taking N steps either up, down, left or right, end up at…

  • (no subject)

    Still sad that SAC seems to end up being as complicated as it is. Surely there's some deeper duality between…

  • (no subject)

    I had already been meaning to dig into JaneSt's "Incremental" library, which bills itself as a practical implementation (in ocaml) of the ideas in…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded