Jason (jcreed) wrote,
Jason
jcreed

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
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 0 comments