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: learning: questions

Topic: Boolean algebras and propositional theories

Leopold Schlicht (Jul 04 2021 at 19:26):

The category of Boolean algebras is equivalent to the category of theories in propositional logic (as witnessed by the functor sending a propositional theory to its Lindenbaum--Tarski algebra). Is there a (standard) reference for this theorem? It astonishes me a bit that such a reference is hard to find (and that the theorem seems to be only rarely stated at all!), as both topics (propositional logic and Boolean algebras) have the same motivation/origin: to investigate logical operations such as "and", "or", and "not" (for some people, the words "propositional logic" and "Boolean algebra" are even synonyms). So I would think it is natural to explicitly state the connection...

John Baez (Jul 04 2021 at 19:32):

I don't know much about this, but I'll just guess:

It sounds like a category theorist might state a version of this result by saying Boolean algebras are algebras of a finitary monad on Set, since then every Boolean algebra has a "presentation" in terms of free Boolean algebras (i.e. it's a coequalizer of free Boolean algebras, where one describes the "generators" and the other describes the "relations", i.e. axioms). From this you can get an equivalence of categories between Boolean algebras and "presented Boolean algebras".

This idea works equally well if you replace the word "Boolean algebra" by "group", "ring", "complex vector space", etc.

John Baez (Jul 04 2021 at 19:34):

But I imagine propositional logic experts have some special hand-crafted concept of "propositional theory", which is a different way of saying "presented Boolean algebra".

Fawzi Hreiki (Jul 04 2021 at 20:49):

There's some of this in Mike Shulman's 'Categorical logic from a categorical point of view'

Fawzi Hreiki (Jul 04 2021 at 20:51):

The categorical approach though isn't that there is an 'equivalence between propositional theories and Boolean algebras' but that propositional theories are Boolean algebras and models are valuations (maps to the Boolean algebra of truth values).

Fawzi Hreiki (Jul 04 2021 at 20:53):

Awodey's category theory book also has a subsection on (constructive) propositional logic via Heyting algebras.

John Baez (Jul 04 2021 at 20:59):

The categorical approach though isn't that there is an 'equivalence between propositional theories and Boolean algebras' but that propositional theories are Boolean algebras [....]

That sounds like an equivalence to me! :upside_down:

Mike Shulman (Jul 05 2021 at 05:49):

As always with this sort of thing, I would phrase it as an adjunction between (classical) propositional theories and Boolean algebras.

Mike Shulman (Jul 05 2021 at 05:51):

It's more natural to me for a "morphism of theories" to act on syntactic presentations, sending generators to generators, than to be an arbitrary morphism between the Lindenbaum-Tarski algebras.

Fawzi Hreiki (Jul 05 2021 at 10:40):

That's true. I guess it's just a notational difference whether 'theory' refers to the algebra or to the presentation. Either way, a morphism of presentations will be more fine than a morphism of algebras.

Jon Sterling (Jul 05 2021 at 18:37):

Mike Shulman said:

It's more natural to me for a "morphism of theories" to act on syntactic presentations, sending generators to generators, than to be an arbitrary morphism between the Lindenbaum-Tarski algebras.

My experience is that morphisms of this kind (sending generators to generators) are not too common in practice, but maybe I've been looking in the wrong places. At least in computer science, most examples that come up in practice are sending generators to compound expressions. Do you have any examples that show the usefulness of the "generators-to-generates" version?

Nathanael Arkor (Jul 05 2021 at 18:41):

One point is that the generators-to-terms morphisms (which are often called translations) arise from the generators-to-generators morphisms as Kleisli morphisms. So in this sense it is natural to take the latter as fundamental.

Mike Shulman (Jul 05 2021 at 19:23):

Suppose $T$ is a theory (e.g. in propositional logic) and $C$ is the corresponding categorical structure (e.g. a Boolean algebra). Let $UC$ be its underlying theory (= internal language), whose types are the objects of $C$, and whose (generating!) function symbols are the morphisms of $C$. The adjunction picture tells us that structured functors $FT \to C$ from the Lindenbaum-Tarski algebra (syntactic category) of $T$ to $C$ are equivalent to generator-preserving morphisms of theories $T\to UC$, i.e. "labelings" of the types and symbols of $T$ by objects and morphisms of $C$. The latter is exactly what we expect to use when using syntax to reason about the categorical structure $C$. The alternative notion of "morphism of theories" from $T$ to $U C$ would label each symbol of $T$ by a formal composite of morphisms in $C$, which isn't usually what we want.

Mike Shulman (Jul 05 2021 at 19:27):

In addition, with generators-to-generators morphisms of theories, and sufficiently strict morphisms of categorical structures, the adjunction can be a strict 1-adjunction. As far as I know, the other approach can at best produce a biequivalence, since (for instance) $C$ is only equivalent, not isomorphic, to $F U C$. Thus, in particular, it also requires defining 2-cells of theories by lifting them from the categories. So the generators-to-generators version is formally significantly simpler, and as Nathanael says we can always recover the other version with a Kleisli construction.

Leopold Schlicht (Jul 29 2021 at 15:27):

Thanks for the comments. I still wonder whether there's a standard reference for the "connection" (be it an equivalence or an adjunction) between Boolean algebras and propositional theories. Awodey's book talks about Stone duality, but it doesn't seem to make the connection to propositional theories precise.

Leopold Schlicht (Sep 08 2021 at 17:00):

Mike Shulman said:

The latter is exactly what we expect to use when using syntax to reason about the categorical structure $C$.

What do you mean by that?

The alternative notion of "morphism of theories" from $T$ to $U C$ would label each symbol of $T$ by a formal composite of morphisms in $C$, which isn't usually what we want.

In fact, in the book Categorical Logic and Type Theory, Jacobs says quite the opposite (on page 131):

The category $\mathbf{Sign}_{\textrm{tr}}$ is in fact more useful than $\mathbf{Sign}$: translations occur
more naturally than morphisms of signatures, as the following examples illustrate.

Somewhat related to the first question: I found slides by @Tom Hirschowitz (https://www.lama.univ-savoie.fr/pagesmembres/hirschowitz/talks/cours.pdf) in which it is claimed (on page 59) that the adjunction between algebraic theories and cartesian categories is both a completeness theorem and a soundness theorem. I know that the fact that the syntactic category of an algebraic theory is cartesian implies completeness, since it admits a generic model of the theory, but I don't understand why that (and soundness) should follow from the adjunction.

Mike Shulman (Sep 08 2021 at 17:29):

I mean that when I reason about a category $C$ in type theory, I expect each type $A$ to represent an object of $C$, not a formal product of objects of $C$. Jacobs' examples are about translations between syntactic signatures, and doesn't address this point.

Mike Shulman (Sep 08 2021 at 17:30):

The fact that the syntactic category of an algebraic theory is cartesian is part of the existence of the adjunction: it says that the left adjoint lands in the right place.

Leopold Schlicht (Sep 08 2021 at 18:05):

Mike Shulman said:

I mean that when I reason about a category $C$ in type theory, I expect each type $A$ to represent an object of $C$, not a formal product of objects of $C$.

Yes, I also think that that's the right way to define the notion of a model. But we were talking about the notion of a translation. :-)

The fact that the syntactic category of an algebraic theory is cartesian is part of the existence of the adjunction: it says that the left adjoint lands in the right place.

Fair enough!

Mike Shulman (Sep 08 2021 at 18:10):

The point is that a model is a translation, or at least, a morphism of theories, from some theory to the underlying/internal theory of a category.

Leopold Schlicht (Sep 08 2021 at 18:49):

OK. I agree that if one desperately wants translations to precisely match with models in that way, then one should define translation as you suggest (sending generators to generators). But maybe one doesn't want that too much, since such translations don't occur that much. And if one works in a 2-categorical setting, then I think one gets the best of both worlds: since $FUC$ is equivalent to $C$, generators-to-generators translations from a theory $\mathbb T$ to $UC$ correspond up to isomorphism to generators-to-expressions translations from $\mathbb T$ to $UC$. So using the generators-to-expressions approach one can still say that the hom-category $\hom(\mathbb T, UC)$ is equivalent to the category of models of $\mathbb T$ in $C$. (The generators-to-generators approach yields an honest bijection, but I think its more natural to consider models up to isomorphism rather than up to equality.)

Mike Shulman (Sep 08 2021 at 19:18):

Well, I disagree. (-:

Leopold Schlicht (Sep 08 2021 at 21:04):

Mike Shulman said:

The fact that the syntactic category of an algebraic theory is cartesian is part of the existence of the adjunction: it says that the left adjoint lands in the right place.

But what about soundness?

Mike Shulman (Sep 08 2021 at 23:46):

Soundness roughly refers to the map $\hom(\mathbb{T}, UC) \to \hom(F\mathbb{T},C)$. Given an interpretation of the generators in $C$, it follows that you can interpret any derivation or proof into $C$ as well. I.e. "everything provable is true in any model".

Leopold Schlicht (Sep 09 2021 at 10:18):

Ah, right, thanks! Also, when proving that for each translation $J\colon\mathbb T\to\mathbb U$, the construction $FJ\colon F\mathbb T\to F\mathbb U$ is a functor, one needs to verify that it preserves composition, i.e., substitution of terms, and that argument essentially repeats the proof of the soundness of the substitution rule, which is the most "non-trivial" step in the proof of the soundness theorem of equational logic, I think.

Leopold Schlicht (Sep 09 2021 at 11:25):

Mike Shulman said:

As far as I know, the other approach can at best produce a biequivalence, since (for instance) $C$ is only equivalent, not isomorphic, to $F U C$. Thus, in particular, it also requires defining 2-cells of theories by lifting them from the categories. So the generators-to-generators version is formally significantly simpler, and as Nathanael says we can always recover the other version with a Kleisli construction.

But if $C$ is only equivalent and not isomorphic to $FUC$, then even though there's 1-adjunction between $F$ and $U$, the Kleisli construction won't yield a 1-equivalence because $F$ isn't essentially surjective, right? (Or is there another theory $T$ such that $FT$ is isomorphic to $C$?)

Leopold Schlicht (Sep 09 2021 at 11:27):

By the way I think also $UFT$ is, in general, not isomorphic to $T$ - one has to introduce 2-cells and state that they are equivalent.

Mike Shulman (Sep 09 2021 at 14:39):

Not sure exactly what you're asking. What do you want a 1-equivalence between?

Leopold Schlicht (Sep 11 2021 at 10:40):

Mike Shulman said:

Soundness roughly refers to the map $\hom(\mathbb{T}, UC) \to \hom(F\mathbb{T},C)$. Given an interpretation of the generators in $C$, it follows that you can interpret any derivation or proof into $C$ as well. I.e. "everything provable is true in any model".

The situation still confuses me a lot: each translation $\mathbb T\to UC$ induces a functor $F\mathbb T\to FUC$, which in turn induces a functor $F\mathbb T\to C$. Despite what I said in https://categorytheory.zulipchat.com/#narrow/stream/229199-learning.3A-questions/topic/Boolean.20algebras.20and.20propositional.20theories/near/252601974 I have the feeling that this argument doesn't really use the soundness theorem. How can that be? Where does the soundness theorem hide?

Leopold Schlicht (Sep 11 2021 at 14:37):

Mike Shulman said:

Not sure exactly what you're asking. What do you want a 1-equivalence between?

Let $\mathbf{Cart}$ be the category of cartesian categories equipped with specified products and functors preserving these specified products on the nose, and $\mathbf{AlgTh}$ the category of many-sorted algebraic theories and generators-to-generators translations. Consider the two functors $F\colon\mathbf{AlgTh}\to\mathbf{Cart}$ (syntactic category) and $U\colon\mathbf{Cart}\to\mathbf{AlgTh}$ (internal language). Then $F\dashv U$. I was just pointing out that you can't obtain an equivalence from that adjunction using a Kleisli construction, because $F$ is (probably) not essentially surjective, since, as you said, $C$ is in general only equivalent to $FUC$ and not isomorphic to it. (Except one uses a Lambek–Scott-style definition of "theory", in which the types are not freely generated from a collection of basic types. But this is artificial to my mind.)

Now, let $\mathbf{Cart'}$ be the 2-category of cartesian categories, product-preserving functors (up to isomorphism), and natural transformations, and $\mathbf{AlgTh'}$ the 2-category of many-sorted algebraic theories, generators-to-generators translations, and 2-cells defined "like natural transformations". Also, consider the two 2-functors $F'\colon\mathbf{AlgTh'}\to\mathbf{Cart'}$ (syntactic category) and $U'\colon\mathbf{Cart'}\to\mathbf{AlgTh'}$ (internal language). Then $F'\vdash U'$. Now, only in the 2-categorical setting, I think one can use a Kleisli construction to turn $F'\vdash U'$ into a biequivalence between the 2-category of cartesian functors and the 2-category of algebraic theories and generators-to-expressions translations. Right?

Question: Is there a mechanical process that tells us how to build the 2-adjunction $F'\vdash U'$ from the adjunction $F\dashv U$?

I think answering that question in a precise way could improve the section 1.7 (especially 1.7.3 after Theorem 1.7.12 and 1.7.4 after "(g)") of your book draft Categorical logic from a categorical point of view, because there you are briefly mentioning the Kleisli construction several times without telling the full story. This might help readers who have seen presentations like Lambek–Scott, Pitt's Categorical Logic, or Crole's Categories for Types, in which the emphasis is quite on formulating logic-category correspondences as equivalences (in some form) rather than adjunctions. (Or, if that would take too much space, I suggest adding references concisely explaining that cofibrant stuff.)

I guess the mechanical process that turns $F\dashv U$ into $F'\vdash U'$ would define the 1-cells of $\mathbf{Cart'}$ as functors preserving products on the nose (and the objects, cartesian categories, as being equipped with specified products), as in $\mathbf{Cart}$. That one can define them as functors preserving products up to isomorphism is probably because every functor $F\mathbb T\to C$ preserving products up to isomorphism is isomorphic to a functor $F\mathbb T\to C$ preserving products on the nose. Is this just a coincidence or does it happen in other settings too that one can define the 1-cells as up-to-isomorphism-preserving functors?

Mike Shulman (Sep 11 2021 at 15:40):

I have the feeling that this argument doesn't really use the soundness theorem.

Why do you have that feeling? I explained why it does.

Leopold Schlicht (Sep 11 2021 at 16:54):

Mike Shulman said:

I have the feeling that this argument doesn't really use the soundness theorem.

Why do you have that feeling? I explained why it does.

You sketched one argument using the soundness theorem. I sketched another argument:

The situation still confuses me a lot: each translation $\mathbb T\to UC$ induces a functor $F\mathbb T\to FUC$, which in turn induces a functor $F\mathbb T\to C$.

I can't see where this specific argument uses the soundness theorem.

Mike Shulman (Sep 11 2021 at 17:18):

Your argument is the same as mine: applying $F$ and then composing with the counit is precisely how you construct the adjunction isomorphism from a unit-and-counit adjunction.

Leopold Schlicht (Sep 12 2021 at 13:42):

Ah, only now I'm able to spot where the soundness theorem is used. It's used in the second step, when constructing $FUC\to C$. To check that this functor is well-defined one needs to verify that each syntactic consequence of the internal language of $C$ is satisfied by (the canonical structure in) $C$.

Mike Shulman (Sep 15 2021 at 19:31):

Leopold Schlicht said:

Question: Is there a mechanical process that tells us how to build the 2-adjunction $F'\vdash U'$ from the adjunction $F\dashv U$?

There is a 2-monad $T$ on the 2-category $\rm Cat$ whose strict algebras are categories equipped with specified products. As for any 2-monad $T$, we can then define the 2-categories $T\text{-Alg}_s$, resp. $T\text{-Alg}_p$, of $T$-algebras and strict morphisms, resp. pseudo morphisms. Then $T\text{-Alg}_p$ is your $\bf Cart'$, while $T\text{-Alg}_s$ is an enhancement of your $\bf Cart$ with 2-cells.

There is a forgetful functor $T\text{-Alg}_s \to T\text{-Alg}_p$, and since $T$ is accessible this functor has a left adjoint. Moreover, since $T$ satisfies the "general coherence theorem", this 2-adjunction is a biequivalence. Thus, once one has an adjunction between $\bf AlgTh'$ and $T\text{-Alg}_s$, one can compose it with this biequivalence to get a new biadjunction.

I'm not sure offhand if I know a general abstract way to enhance the 1-adjunction $\bf AlgTh \rightleftarrows Cart$ to a 2-adjunction $\bf AlgTh' \rightleftarrows T\text{-Alg}_s$. Of course the 2-cells in $\bf AlgTh'$ are just defined via the functor $F$, but it's not immediately obvious that $U$ lifts to a 2-functor with this definition. Let me know if you think of something.

I do certainly intend to say something along these lines in the final book.