Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: category theory

Topic: Linear ultrafilters?

Alexander Gietelink Oldenziel (May 04 2023 at 16:52):

It is well-known that ultrafilters (or maximal ideals) correspond to Boolean algebra morphisms $B \to 2$. I don't know exactly what Heyting algebra morphisms $$H \to \mathbb{S}$ where $\mathbb{S}$$ denotes the Sierpinski Heyting algebra correspond to but frame morphisms $F \to \mathbb{S}$ correspond to prime filters on $F$ I think.

Boolean algebras and Heyting algebras are the proof-irrelevant truncated syntactic categories of propositional classical, respectively intuitionistic, theories.

Apart from classical logic and intuitionistic logic there is the very natural linear logic.
I suppose the analog for Boolean algebras and Heyting algebras here would be *-autonomous posets, probably with products and coproducts (i.e. joins and meets) + distributivity laws relating tensor and plus $\otimes,\oplus$ and similarly for par and with.

Does anybody know if the maps $G \to Free(\emptyset), G\to Free(\bullet)$ where $Free(-)$ denotes the free *-autonomous poset (or the free *-autonomous posets with meets, joins) and $G$ is a *-autonomous poset (possibly with meets and joints) have been described somewhere?

Additionally one could ask the same questions for: monoidal closed posets, possibly with meet and joins (i.e. intuitionistic multiplicative-additive linear logic) and linear distributive posets.

Valeria de Paiva (May 06 2023 at 19:12):

Hi Alexander,

I suppose the analog for Boolean algebras and Heyting algebras here would be *-autonomous posets, probably with products and coproducts (i.e. joins and meets) + distributivity laws relating tensor and plus ⊗,⊕⊗,⊕ and similarly for par and with.

the algebraic models of Linear Logic had lots of discussion in the 90s. I am particularly fond of what I call "lineales" which are just the symmetric monoidal closed posets. no involution, as I wanted to discuss Full Intuitionistic Linear Logic, which has tensor, par, product and coproduct (as you described them), but a non-involutive negation, just like Intuitionistic Logic, so negated A is the same as A linear implication into \bot . You can read about it in Lineales: Algebras and Categories in the Semantics of Linear Logic, In “Words, Proofs and Diagrams", CSLI Publications, Stanford 2002. Troelstra had his algebras in his book, and many other people played with different notions. I also worked with Andrea Schalk on Poset-valued sets or how to build models for linear logics, where we describe answers to similar questions to yours, but not exactly what you ask.

Alexander Gietelink Oldenziel (May 15 2023 at 15:14):

Thank you Valeria, I will take a look!