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: Functoriality vs Soundness

John Onstead (Feb 10 2026 at 12:08):

A theory/formal system in logic is considered "sound" if a proven statement in the theory is true in all models of the theory. To be honest, this was one of those things I thought was true by default, yet it seems it needs to be proven.

In any case, an inference or proof in a theory $T$ often corresponds to a morphism in $\mathrm{Syn}(T)$. A model is just a structure preserving functor $\mathrm{Syn}(T) \to \mathrm{Set}$. So if a proof is indeed a morphism, functoriality carries it over to be a morphism in $\mathrm{Set}$, and since all models are functors with functoriality, it seems the proof carries over in all models. So it seems that functoriality of models implies soundness. The above argument only fails if not all proofs are morphisms in the syntactic category, or if somehow a morphism can "lose truth" even while being transported by the functor.

John Onstead (Feb 10 2026 at 12:09):

But here's where my confusion is. If functoriality of models implies soundness, then by definition of "model" as a functor, all theories are automatically sound, no proof needed. Yet this is clearly contradicted by the fact that soundness needs to be proven, and potentially the existence of non-sound formal systems. This implies that there is something about "soundness" that I am not understanding.

John Onstead (Feb 10 2026 at 12:09):

My question is: true/false, does functoriality of models in functorial semantics imply soundness, and if not, why not?

Ryan Wisnesky (Feb 10 2026 at 15:52):

A co-pre-sheaf F : C -> Set will obey the axioms of C as an easy consequence of functoriality. But often we want to consider properties of F not encoded in C. For example in CQL, our C's can only encode equational constraints. If we want to talk about products, limits, etc, we thus can't encode those in C. We construct a 'lifting problem' instead, for which we ask if there is a solution. So that's how I see it: functorial semantics lets you start from a nice base - a nice C - but you don't have to put all your semantics into it (C).

Matt Earnshaw (Feb 10 2026 at 16:00):

We talk of soundness 1. of a system of syntax and inference rules (theory), 2. with respect to a class of models (semantics), which is specified independently. These are what make you work.

If models of T are defined to be functors out of a given Syn(T), then yes, soundness with respect to the class of models given by all such functors is tautological in the sense you mention.

For certain meanings of theory, there are well established constructions $\mathsf{Syn}$, producing a category (or other gadget) Syn(T) from T. But this is work that has been done, and needs to be done in general: to show how to build a gadget out of the syntax (a notion which has various formal counterparts, but I think is preformal in general).

The second bit of work is showing that for every thing in your class of models (something that generally exists in the wild independently of your theory), there is indeed a functor (or other kind of morphism) from Syn(T) corresponding to it.

Kevin Carlson (Feb 10 2026 at 17:46):

To give a concrete example: consider classical propositional logic, with semantics in Heyting algebras. This is an unsound system! You might really tell a story where a mathematician notices that opens in a topological space really behave a bit like elements of a Boolean algebra, and tries to give them the semantics of this syntax, and is led as a result of failing to prove a soundness theorem to develop intuitionistic propositional logic.

John Baez (Feb 10 2026 at 20:53):

To repeat what @Matt Earnshaw said: yes, the functoriality of models in functorial semantics implies a kind of soundness as @John Onstead wanted, and proving this functoriality can be highly nontrivial, since proving soundness is in general nontrivial.

John Onstead (Feb 10 2026 at 20:58):

Ryan Wisnesky said:

A co-pre-sheaf F : C -> Set will obey the axioms of C as an easy consequence of functoriality

Matt Earnshaw said:

If models of T are defined to be functors out of a given Syn(T), then yes, soundness with respect to the class of models given by all such functors is tautological in the sense you mention

John Baez said:

To repeat what Matt Earnshaw said: yes, the functoriality of models in functorial semantics implies a kind of soundness as John Onstead wanted, and proving this functoriality can be highly nontrivial, since proving soundness is in general nontrivial.

Ok, so functoriality of models does imply soundness. My reasoning above was sound (pun intended!)

John Onstead (Feb 10 2026 at 21:01):

But if all that's true, then I'm still a little confused about how models from an unsound system can work. For instance, take Kevin Carlson's example:

Kevin Carlson said:

To give a concrete example: consider classical propositional logic, with semantics in Heyting algebras. This is an unsound system!

A Heyting algebra $A$ is a poset, so models can be thought of as structure-preserving functors from a Heyting algebra $A$ to $2$, the poset of truth values. Thus, the class of models of a system of classical propositional logic is given by $[A, 2]$, or at least some subset of it on the structure-preserving maps. If $A$ were to be unsound, then what exactly is implied about the poset $[A, 2]$?

John Baez (Feb 10 2026 at 21:03):

It's not that a given Heyting algebra is unsound. It's that taking trying to take classical propositional logic to have semantics in Heyting algebra would be unsound, since Heyting algebras don't obey the rules of classical propositional logic (in general).

John Baez (Feb 10 2026 at 21:04):

To be more specific: one of the rules of classical propositional logic, $P \vee \neg{P}$, fails in Heyting algebras. You can try to restate this problem as the nonexistence of a functor with some properties from some category to some other category.

John Baez (Feb 10 2026 at 21:05):

To do this, you'd have to make up a category that captures "classical propositional logic".

John Onstead (Feb 10 2026 at 21:10):

John Baez said:

It's not that a given Heyting algebra is unsound. It's that taking trying to take classical propositional logic to have semantics in Heyting algebra would be unsound, since Heyting algebras don't obey the rules of classical propositional logic (in general).

Oh! So unsoundness, at least in this case, seems to be due to a mismatch between some class of theories and some doctrine of syntactic categories for a class of theories. Heyting algebras have the internal language of intuitionistic logic, not always Boolean logic, so it would be unsound to try and reason in a Boolean way within them.

John Baez said:

To do this, you'd have to make up a category that captures "classical propositional logic".

This would be a Boolean algebra, no? If so, then does that mean models of Boolean algebras do correspond to structure-preserving maps from them into $2$?

John Baez (Feb 10 2026 at 21:21):

Kevin and I are not talking about models of a Boolean algebra, though that's something you can do too. We're talking about models of the concept of Boolean algebra. That's what classical propositional calculus describes: the rules that hold in every Boolean algebra. That's why I said it would take some work to capture this concept in a category.

There won't be a unique way to do this. You can try things like this: there's a topos called "the classifying topos of Boolean algebras". Geometric morphisms from this to a topos T are Boolean algebra objects in T, I hope.

Kevin Carlson (Feb 11 2026 at 00:19):

The most elementary thing to do, I think, would be to build the "syntactic model" of classical propositional logic by taking some fixed, say, countably infinite set, of generating propositions, then taking the model to be all formulas in those propositions expressible in classical propositional logic up to provable equivalence. Then the "functorial" semantics for this notion of model is "Heyting algebra homomorphism", and indeed there is no such homomorphism from the syntactic model to an arbitrary Heyting algebra (equipped with an at-most-countable set of generators, I guess, I'm not sure how most easily to get rid of that annoyance) since the syntactic is of course the free Boolean algebra on countably many generators.

Kevin Carlson (Feb 11 2026 at 00:20):

It's possible to look for a vibe here where unsoundness means that you have a mismatch where you're trying to allow too many models of your language, while incompleteness means that you're allowing too few.

John Onstead (Feb 11 2026 at 00:55):

Kevin Carlson said:

The most elementary thing to do, I think, would be to build the "syntactic model" of classical propositional logic by taking some fixed, say, countably infinite set, of generating propositions, then taking the model to be all formulas in those propositions expressible in classical propositional logic up to provable equivalence. Then the "functorial" semantics for this notion of model is "Heyting algebra homomorphism", and indeed there is no such homomorphism from the syntactic model to an arbitrary Heyting algebra since the syntactic is of course the free Boolean algebra on countably many generators.

Let me see if I'm understanding. There exists a theory $T$ of "formulas in propositions expressible in classical propositional logic up to provable equivalence". Then $\mathrm{Syn}(T)$ is the free Boolean algebra on countably many generators. The argument is that $T$ should be satisfiable in that there should exist at least one model, with each model being those formulas. On the other hand, the category $\mathrm{Bool}[\mathrm{Syn}(T), 2]$ of structure-preserving maps is empty.
So then the inconsistency is that we are expecting models of $T$ to exist, but when we actually try generating them with functorial semantics, we don't end up finding any models. Do I have this right?

Kevin Carlson (Feb 11 2026 at 00:59):

No, I don't think so. I was proposing to try to make the category of Heyting algebras into a semantic category for classical propositional logic. The syntactic model is a particular Heyting algebra, that is, the free Boolean algebra on countably many generators. There are many Heyting algebras to which this guy does not map, so my interpretation is not sound.

Kevin Carlson (Feb 11 2026 at 00:59):

There are lots of structure preserving maps from free Boolean algebras to $2$, and to any other Boolean algebra, because of how free things work.

John Onstead (Feb 11 2026 at 03:16):

Kevin Carlson said:

No, I don't think so. I was proposing to try to make the category of Heyting algebras into a semantic category for classical propositional logic. The syntactic model is a particular Heyting algebra, that is, the free Boolean algebra on countably many generators. There are many Heyting algebras to which this guy does not map, so my interpretation is not sound.

Ok, let me try again. So let $F(G)$ be our free Boolean algebra on countably many generators. This is obviously an object in $\mathrm{BoolAlg}$, but we want to also realize it as an object in $\mathrm{HeyAlg}$ due to the embedding from the former to the latter. Then it seems you are saying that for many Heyting algebras $A$, the hom $\mathrm{HeyAlg}[F(G), A]$ is empty.

John Onstead (Feb 11 2026 at 03:20):

This might be completely off the mark, but this almost feels analogous to if we took a finite limits category and only considered finite product preserving functors from it into a finite products category (since finite limits is stronger logically than finite products, just as Boolean is stronger than Heyting). But in this case, the finite product functors would still be models, just of whatever the underlying algebraic theory is rather than of the full finite limits theory.

Zoltan A. Kocsis (Z.A.K.) (Feb 11 2026 at 03:57):

John Onstead said:

Then it seems you are saying that for many Heyting algebras $A$, the hom $\mathrm{HeyAlg}[F(G), A]$ is empty.

Every Heyting algebra admits a homomorphism from the two-element Boolean algebra (which one?).

Under standard set theoretic assumptions every Heyting algebra (except the one where $\top=\bot$ if you consider that a Heyting algebra) also admits a morphism to the two-element Boolean algebra. Composing these, you get that such homsets are never empty.

Kevin Carlson (Feb 11 2026 at 19:27):

Yes, thanks, I was sloppy, there--many Heyting algebras don't admit any nontrivial homomorphisms from any Boolean algebra, but there is a trivial one.

John Onstead (Feb 11 2026 at 21:20):

Zoltan A. Kocsis (Z.A.K.) said:

Every Heyting algebra admits a homomorphism from the two-element Boolean algebra (which one?).

Under standard set theoretic assumptions every Heyting algebra (except the one where $\top=\bot$ if you consider that a Heyting algebra) also admits a morphism to the two-element Boolean algebra. Composing these, you get that such homsets are never empty.

Thanks for the clarification!

John Onstead (Feb 11 2026 at 21:21):

Kevin Carlson said:

Yes, thanks, I was sloppy, there--many Heyting algebras don't admit any nontrivial homomorphisms from any Boolean algebra, but there is a trivial one.

So with this in mind, $F(G)$ would map to $A$, but only trivially. But to get back to the original point of this discussion, I'm still confused by why I should be surprised by this. $F(G)$ was defined to be the theory whose models were "formulas expressible in classical propositional logic up to provable equivalence". But if $A$ is a Heyting and not a Boolean algebra, then we shouldn't really expect any formulas (perhaps besides trivial ones) to be expressible in classical propositional logic internally to it, precisely because the internal language of $A$ isn't classical propositional logic. So from this we'd already expect there to be only trivial models at best, which perfectly aligns with the functorial analysis. Is there something I'm mistaken about here?

Zoltan A. Kocsis (Z.A.K.) (Feb 11 2026 at 21:28):

@Kevin Carlson, every Heyting algebra admits many homomorphisms from Booleqn algebras, continuum-many from $F(G)$ above.

Pick any subset $S$ of the generators $G$ and consider the indicator function $s: G\rightarrow \{\bot,\top\}$.

By the universal property of the free Boolean algebra $s$ extends to a unique homomorphism from $F(G)$ to the two-element Boolean algebra.

Since Boolean homomorphisms between Boolean algebras are Heyting homomorphisms, and the two-element Boolean algebra is a subalgebra of any Heyting algebra, this construction gives uncountably many different homomorphisms from the free Boolean algebra on countably many generators to any Heyting algebra.

Kevin Carlson (Feb 11 2026 at 22:01):

A collection of trivial ones*... :face_with_peeking_eye:

Zoltan A. Kocsis (Z.A.K.) (Feb 11 2026 at 22:04):

Well, perhaps trivial, but they witness that this unsound semantics is nonetheless complete!

Kevin Carlson (Feb 11 2026 at 22:04):

John Onstead said:

Kevin Carlson said:

Yes, thanks, I was sloppy, there--many Heyting algebras don't admit any nontrivial homomorphisms from any Boolean algebra, but there is a trivial one.

So with this in mind, $F(G)$ would map to $A$, but only trivially. But to get back to the original point of this discussion, I'm still confused by why I should be surprised by this. $F(G)$ was defined to be the theory whose models were "formulas expressible in classical propositional logic up to provable equivalence". But if $A$ is a Heyting and not a Boolean algebra, then we shouldn't really expect any formulas (perhaps besides trivial ones) to be expressible in classical propositional logic internally to it, precisely because the internal language of $A$ isn't classical propositional logic. So from this we'd already expect there to be only trivial models at best, which perfectly aligns with the functorial analysis. Is there something I'm mistaken about here?

I'm not sure why you say we shouldn't expect any formulas to be expressible internally to it. That sentence doesn't really parse to me. I can write any formula of classical propositional logic in a Heyting algebra, and many of them are even true, such as $a\wedge \neg a\implies \bot.$ It's just that not all tautologies of classical logic will hold!

Kevin Carlson (Feb 11 2026 at 22:09):

Zoltan A. Kocsis (Z.A.K.) said:

Well, perhaps trivial, but they witness that this unsound semantics is nonetheless complete!

Ah, interesting, let's see...Actually, I'm not sure I follow this--I would have said something like "if a formula $\varphi(a_i)$ is true in every model then it's true in the syntactic model, where truth is provability by definition." What do you use the other models for in your completeness argument?

Zoltan A. Kocsis (Z.A.K.) (Feb 11 2026 at 22:17):

@Kevin Carlson Consider the semantics you get by evaluation into any one fixed Heyting algebra $H$. This semantics is unsound when $H$ is not Boolean, but is always complete for classical propositional logic. If a formula is not provable, it evaluates to $\bot$ under some assignment in the 2-valued semantics. Such an assignment is a precisely a Heyting homomorphism from $F(G)$ to $\{\bot, \top\}$. Extend it to a homomorphism $F(G) \rightarrow H$, and use the fact that homomorphisms preserve $\bot$, and you're done.

Kevin Carlson (Feb 11 2026 at 22:18):

Ah, I see, you mean that the semantics is complete in any particular Heyting algebra. Very cool, thank you.

John Onstead (Feb 11 2026 at 22:58):

Kevin Carlson said:

I'm not sure why you say we shouldn't expect any formulas to be expressible internally to it. That sentence doesn't really parse to me. I can write any formula of classical propositional logic in a Heyting algebra, and many of them are even true, such as $a\wedge \neg a\implies \bot.$ It's just that not all tautologies of classical logic will hold!

Ok, I think I'm finally getting close to diagnosing the issue, as long as my understanding is good: You can rewrite a formula of classical propositional logic in a Heyting algebra, but it won't extend to a homomorphism $F(G) \to A$ unless this rewriting process also preserves all tautologies of classical logic. Since these don't need to hold in the intuitionistic Heyting algebra, then not every formula rewriting will extend to such a homomorphism. Do I have that right?

Kevin Carlson (Feb 12 2026 at 06:49):

That's about right, although I'm still a little unsure about this "rewriting." A formula like $a \vee (b\wedge \neg c)$ is directly interpretable in a Heyting algebra for any choice of $a,b,c.$