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

Zoltan A. Kocsis (Z.A.K.) (Feb 12 2026 at 12:30):

I guess a change of notation and a bit of formality could make things clearer. :fingers_crossed:

Let $G$ denote some countably infinite set (the set of _variables_). We can inductively define the set $\mathrm{Form}(G)$ of Boolean formulae with variables in $G$, using clauses

1. if $X \in G$ then $X$ is a formula,
2. if $\varphi$ and $\psi$ are formulae, then so is $\varphi \vee \psi$,
3. if $\varphi$ and $\psi$ are formulae, then so is $\varphi \wedge \psi$,

and so on.

Given any Heyting algebra $(H, \sqcup, \sqcap, \Rightarrow, \bot_H, \top_H)$ and any map $v : G \rightarrow H$, we can obtain a map $v \models \bullet : \mathrm{Form}(G) \rightarrow H$ given inductively by cases

1. $(v \models X) = v(X)$ for every $X \in G$,
2. $(v \models \varphi \vee \psi) = (v \models \varphi) \sqcup (v \models \psi)$,
3. $(v \models \varphi \wedge \psi) = (v \models \varphi) \sqcap (v \models \psi)$

and so on.

We notice that if we quotient the set $\mathrm{Form}(G)$ with the relation of provable equivalence $\sim$ in any of the usual deductive systems of classical logic, we get that the syntactic operations $(\varphi,\psi) \mapsto \varphi \vee \psi$, $(\varphi,\psi) \mapsto \varphi \wedge \psi$ etc. respect $\sim$ and thus extend to the quotient, and $(\mathrm{Form}(G)/_\sim, \vee, \wedge, \rightarrow, \bot, \top)$ actually forms a free Boolean algebra on the generating set $G$.

Thus, when $(H, \sqcup, \sqcap, \Rightarrow, \bot_H, \top_H)$ is some other Boolean algebra, then for any map $v: G \rightarrow H$ the corresponding $v \models \bullet : \mathrm{Form}(G) \rightarrow H$ respects $\sim$, and we can lift it to a homomorphism of Heyting algebras $\mathrm{Form}(G)/_\sim \rightarrow H$ and vice versa. This is the usual free/underlying adjunction.

However, any non-Boolean $(H, \sqcup, \sqcap, \Rightarrow, \bot_H, \top_H)$ will contain some element $h \in H$ so that $h \sqcup (h \Rightarrow \bot_H) \neq \top_H$$. If you take the valuation $w : G \rightarrow H$ that sends everything to $h$, you will get a map under which

$(w \models X \vee \neg X) = (w \models X) \sqcup (w \models \neg X) = h \sqcup (h \Rightarrow \bot_H) \neq \top_H$

and

$(w \models X \rightarrow X) = (w \models X) \Rightarrow (w \models X) = h \Rightarrow h = \top_H$.

Since $(X \vee \neg X) \sim (X \rightarrow X)$, but $h \sqcup (h \Rightarrow \bot_H) \neq \top$, this map $w \models \bullet : \mathrm{Form}(G) \rightarrow H$ does not lift to a homomorphism of Heyting algebras $\mathrm{Form}(G)/_\sim \rightarrow H$.

John Onstead (Feb 12 2026 at 21:03):

That's really interesting! So it's when you try to quotient by provable equivalence that things go awry. Because the quotient happens with respect to classical logic rather than intuitionistic logic, maps into Boolean algebras work fine, but things break down with intuitionistic logic since the quotient is "too strong".

John Onstead (Feb 12 2026 at 22:30):

Ok, let me recap. My whole question was to explain the contradiction between there existing unsound theories whose models don't "preserve truth", and the idea that a model must "preserve truth" due to it being a functor. Symbolically, a way to rephrase this is that I presented the definition $\mathrm{Mod}_A(T) := \mathrm{Doc}[\mathrm{Syn}(T), A]$, so therefore Mod can never fail to be equal to the category/set of structure preserving maps from the syntactic category. But the analysis with Boolean algebras above implies $\mathrm{Mod}_A(F(G)) \ncong \mathrm{HeyAlg}[F(G), A]$ for $A$ a Heyting algebra. Hence, the contradiction.

John Onstead (Feb 12 2026 at 22:32):

The question is, how does the above contradiction get resolved?
Here's my attempt. Usually when dealing with these kinds of contradiction, we try to separate things out. So perhaps we're simply dealing with two different levels/kinds of "model" which converge in the sound case, but which diverge in the unsound case. There's one notion of model which remains identical to the functorial one by definition, and then there's another kind of "model" which in unsound cases wouldn't correspond to functors precisely because they don't "preserve truth".

Matteo Capucci (he/him) (Feb 13 2026 at 15:01):

One thing that hasn't been touched on is initiality/freeness. $Syn(T)$ is an object in some given (2-)category $D$ but you have to prove it has a particular status, usually that it is initial, i.e. there is a unique model (a map $Syn(T) \to X$) into every other theory $X \in D$. Indeed, that is usually what is meant by soundness: syntactic/logical judgments imply their semantical counterparts, i.e. if $\Gamma \vdash \varphi$ is derivable in $T$, then there is a unique way to interpret such tautology in every model $X$, and it holds there. That is, there are no countermodels to tautologies, nor there is ambiguity in interpreting them.

Often this is also combined with the presence of propositional variables: let $Syn(T, A)$ be the syntactic object with $A$-many constants freely adjoined, then you want to prove that a model $Syn(T,A) \to X$ corresponds to a valuation $v:A \to X$ of the propositional variables. This is freeness of $Syn(T,A)$ over $A$, and thus categorically corresponds to realizing $Syn$ as the left adjoint to a forgetful functor $D \to K$ where $K$ is some base category (usually $\bf Set$).

Thus soundness is rather initiality, more than functoriality, and in fact freeness (since initial is equivalent to 'free on no generators'). This is made unnecessarily confusing by the widespread habit of not really making explicit the fact that soundness and completeness are always relative notions, i.e. depend on the class (category) of models one talks about. So one has also to reconstruct this in the categorical treatment.

There is a subtle point here which I kind of glossed over, concerning the notions of theory, model, and doctrine. Namely note that $T$, your theory, can be understood in two ways: it's an instance of a particular logical doctrine, and it can be itself instanced to models. To ground this, think: doctrine = (a certain fragment of) first-order logic, theory = monoids, and models = a specific monoid. Thus a 'theory' can both be seen as a model and as having models. You can start to see how model, theory, and doctrine are really the same concept in increasing dimensionality ([[microcosm principle]]).

Again, there is a tendency in logic to be very informal about these subtleties (in fact these are rather metamathematical points, and heard no one raising them outside of categorical logic or adjacent subjects). Specifically, the notion of doctrine is usually just called 'logic' (think: first-order, classical propositional, geometric, linear, etc.), but people will not be very clear about what exactly a logic is. The tell-tale sign that one is dealing with a doctrine rather than a theory is that a theory will have clear-cut languages, by which I mean not just which connectives are around but also which constants. For a doctrine, it is tacitly understood there is going to be an unspecified set of propositional variables around that however you can't use in the axioms. Remembering the soundness-as-freeness bit from before, one can then realize that this is because a doctrine is in fact defining a (2-)monad on a category of propositional variables, so that any specific instance $TX$ has propositional variables around, but clearly $T$ is not exhausted by any given choice (there's reasons not to consider doctrines = (2-)monads though, so take this with a grain of salt).

John Baez (Feb 13 2026 at 23:28):

Very helpful, @Matteo Capucci (he/him)!

John Onstead (Feb 14 2026 at 23:27):

Matteo Capucci (he/him) said:

Often this is also combined with the presence of propositional variables: let $Syn(T, A)$ be the syntactic object with $A$-many constants freely adjoined, then you want to prove that a model $Syn(T,A) \to X$ corresponds to a valuation $v:A \to X$ of the propositional variables. This is freeness of $Syn(T,A)$ over $A$, and thus categorically corresponds to realizing $Syn$ as the left adjoint to a forgetful functor $D \to K$ where $K$ is some base category (usually $\bf Set$).

Thus soundness is rather initiality, more than functoriality, and in fact freeness (since initial is equivalent to 'free on no generators').

Ok, I think I understand. The point Zoltan Kocsis was making above was that, for a Boolean algebra $B$, every valuation $v: G \to B$ lifts to a Boolean algebra homomorphism $FB(G) \to B$. This is because $FB(G)$ is the free Boolean algebra on the set $G$. But when we go to the category of Heyting algebras instead, $FB(G)$ is no longer the free object on $G$. Thus, not every valuation $v: G \to H$ would extend to a Heyting algebra homomorphism $FB(G) \to H$ (where here $FB(-)$ isn't the free Heyting algebra but rather the composition of the free Boolean algebra with the embedding of Boolean algebras into Heyting algebras). So indeed in this example, soundness fails when the object whose homomorphisms/models you want to represent valuations, is no longer the free object.

Although, this would imply an easy "fix" to the unsoundness issue covered above. This would be to stop interpreting $FB(G)$ to be the theory of valuations on $G$ in Heyting algebras, and to instead consider $FH(G)$ to be that theory, where $FH(G)$ is the free Heyting algebra on $G$. Now, we have a more "sound" idea: every model/homomorphism $FH(G) \to H$ is indeed a valuation on $G$.

Kevin Carlson (Feb 16 2026 at 20:06):

Yes, that’s right. But the free Heyting algebra on $G$ is not the syntactic model of classical logic in $G$-many variables, so you will have switched to intuitionistic logic to repair soundness, which is as it should be.

Matteo Capucci (he/him) (Feb 18 2026 at 17:24):

Exactly!