Notes from a Medium-Sized Island

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...

Just skimming through all the statements (starting on page 11 or so) of the form
Category A is isomorphic to category B^op
in Very Basic Noncommutative Geometry (ahahahaha "very basic") is blowing my mind.

Okay first of all it gave me an answer to what noncommutative geometry is, which I never knew, though I'd heard about it a lot. There's a theorem, the Gelfand-Naimark theorem, that says that the category of every nice (i.e. locally compact hausdorff) topological space is equivalent to the dual of the category of some commutative algebraic gadgets (namely, C* algebras, which I don't really understand at all). But also there's lots of noncommutative C* algebras. What are the topological things that correspond to those? Welllll, not locally compact hausdorff topological spaces, that's for sure. They're all "commutative".

So noncommutative geometry seems to be just... the study of noncommutative C* algebras. But since Gelfand-Naimark is true, this is viewed as if it's the study of a "noncommutative" generalization of topological spaces.

---

Separately, a Lovecraftian shiver tickles my brain upon seeing
(affine schemes) = (commutative rings)^op
on page 19, because, like, commutative rings are so garden variety I think I have a half-dozen growing in my backyard amongst the weeds, but schemes are naked gibbering madness that drive mathematicians crazy for their hubris, or so I hear.