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: Classical model theory in the language of hyperdoctrines

James Hanson (Feb 18 2024 at 17:53):

I'm trying to understand the hyperdoctrinal approach to logic partially by relating various ideas back to things that I already understand in classical model theory. To be precise I'm going to try to use nLab's definition of Boolean hyperdoctrine, which says that it's a certain kind of contravariant functor from a category $C$ to the category of Boolean algebras satisfying certain coherence conditions relating to the behavior of quantifiers.

My understanding (and let me know if I'm misunderstanding something) is that one of the conceptual achievements of the concept of hyperdoctrines is putting theories and models on the same conceptual footing, analogously to the idea in model theory of sort of identifying a structure with its elementary diagram. The objects in $C$ are like contexts (i.e., collections of free variables) and also correspond to what model theorists call 'imaginary sorts' (i.e., sorts in the many-sorted theory $T^{\mathrm{eq}}$ associated to a first-order theory $T$). And functors between hyperdoctrines are like interpretations.

Assuming I've got those things right, how would one recover various basic notions in model theory? For instance how do you identify which hyperdoctrines are actually the elementary diagram of a model? The 'syntactic' characterization of this is that the theory is complete and 'term-complete' (i.e., has explicit terms witnessing existential statements). Obviously it's possible to translate this characterization verbatim, but is there a more natural way to say it?

How would you talk about elementary embeddings between models of the same theory? An elementary embedding is a special kind of interpretation. Elementary maps from $M$ to $N$ (models of $T$) are interpretations of the elementary diagram of $M$ in the elementary diagram of $N$ that satisfy a certain commutative diagram involving the canonical interpretation of $T$ (i.e., the interpretation of $T$ in $\mathrm{eldiag}(N)$ is the same as the interpretation of $T$ in $\mathrm{eldiag}(M)$ composed with the interpretation of $\mathrm{eldiag}(M)$ in $\mathrm{eldiag}(N)$), but these are also fairly special interpretations as they are required to preserve sorts (in that they are reduct maps where you're throwing away symbols in the language).

Also, how would you talk about non-elementary maps between structures? While these aren't as central as elementary maps, they are actually pretty important both historically and in the modern practice of model theory. A lot of big results in early model theory are about preservation theories, i.e., syntactically characterizing sentences and formulas that are preserved under various non-elementary operations on structures. In modern model theory, they still show up in talking about model companions of theories, which are often pretty important in getting any kind of reasonable quantifier elimination result. Again, I can clearly see that it is possible to state these things in terms of the translation back into classical first-order logic, but is there a more natural way to work with these ideas in the language of hyperdoctrines?

John Baez (Feb 18 2024 at 18:10):

I was fascinated by these questions and wrote a bunch of blog articles as a warmup to more serious work, but I got distracted before making real progress:

• John Baez and Michael Weiss, First-order categorical logic.

One problem was that I don't know enough model theory to make this easy for me. If anyone has tackled any of the questions you raise, I'd love to hear about it!

My understanding (and let me know if I'm misunderstanding something) is that one of the conceptual achievements of the concept of hyperdoctrines is putting theories and models on the same conceptual footing,

That sounds right - at least that's what excites me about hyperdoctrines.

analogously to the idea in model theory of sort of identifying a structure with its elementary diagram.

Alas, I don't even know what an "elementary diagram" is. :cry:

James Hanson (Feb 18 2024 at 18:19):

John Baez said:

Alas, I don't even know what an "elementary diagram" is. :cry:

Let $M$ be an $L$-structure. Let $L_M$ be $L$ extended with new constant symbols corresponding to each element of $M$. We interpret $M$ as an $L_M$-structure in the obvious way (with each new constant symbol interpreted as the corresponding element of $M$). The elementary diagram of $M$ is the theory of $M$ as an $L_M$-structure, i.e., the set of all $L_M$-sentences satisfied by $M$.

Evan Washington (Feb 18 2024 at 21:40):

James Hanson said:

The objects in $C$ are like contexts (i.e., collections of free variables) and also correspond to what model theorists call 'imaginary sorts' (i.e., sorts in the many-sorted theory $T^{\mathrm{eq}}$ associated to a first-order theory $T$). And functors between hyperdoctrines are like interpretations.

Objects in the category of contexts $C$ do not correspond to imaginaries in general. You can think of $T^\mathrm{eq}$ as the (many-sorted) theory you get by closing the basic sorts under (definable) products, subobjects, and quotients (and coproducts if the theory proves some sort has at least two objects). The objects of the category of contexts, on the other hand, are just products of sorts (and the morphisms are tuples of terms). I believe it will be true, though, if the theory eliminates imaginaries (i.e. is already equivalent to its pretopos completion/$T^\mathrm{eq}$).

Evan Washington (Feb 18 2024 at 22:35):

I don't know how to answer your other questions right away, so I'd also really like to see all these details written down explicitly (maybe that means I should try to do it sometime?). But I can say that one viewpoint that has made hyperdoctrines "click" for me is viewing their main benefit as "algebraicizing" first-order logic.

Theories of propositional logic can be presented algebraically as boolean algebras. Models of a propositional theory are boolean algebra homomorphisms to $2$. Via the Grothendieck construction, (syntactic) hyperdoctrines are certain fibrations $T: B \to C$ where each fiber (over a tuple of sorts) is a boolean algebra: the boolean algebra of definable sets (in that tuple of sorts). (Classical) $T$-models should be maps of fibrations from $T$ to the subobject fibration over $\mathsf{Set}$.

Then the trick would be figuring out which flavors of morphism between functors of fibered boolean algebras correspond to which flavors of model-theoretic homomorphism. I wonder which the usual notion corresponds to (are these elementary or not?)

John Baez (Feb 18 2024 at 22:54):

James Hanson said:

John Baez said:

Alas, I don't even know what an "elementary diagram" is. :cry:

Let $M$ be an $L$-structure. Let $L_M$ be $L$ extended with new constant symbols corresponding to each element of $M$. We interpret $M$ as an $L_M$-structure in the obvious way (with each new constant symbol interpreted as the corresponding element of $M$). The elementary diagram of $M$ is the theory of $M$ as an $L_M$-structure, i.e., the set of all $L_M$-sentences satisfied by $M$.

Thanks! This should be a very natural concept in hyperdoctrine theory. Since you were talking about Boolean hyperdoctrines let's assume our hyperdoctrines are Boolean. I'll think of a Boolean hyperdoctrine as a functor $H: \mathrm{FinSet} \to \mathrm{BoolAlg}$ obeying some properties. Heuristically, $H$ of an $n$-element set can be thought of as a Boolean algebra of $n$-ary predicates, or formulae with $n$ free variables.

John Baez (Feb 18 2024 at 22:57):

Here are my guesses:

1) Any language $L$ of the sort you're talking about should give a hyperdoctrine $H(L)$ where the elements of $H(L)(n)$ are formulae in the language $L$ having $n$ free variables $x_1, \dots, x_n$.

2) any set $V$ should give a hyperdoctrine $B(V)$ where the elements of $B(V)(n)$ are subsets of $V^n$.

3) Any $L$-structure $M$ with universe $V$ should give a map of hyperdoctrines which I'll call

$\alpha: H(L) \to B(V)$

This takes formula with $n$ free variables in the language $L$ to the subsets of $V^n$ for which those formulae hold in the structure $M$.

John Baez (Feb 18 2024 at 23:03):

4) Given an $L$-structure $M$ with universe $V$ we can define a new language $L_M$ which is $L$ together with new constant symbols for each element of $M$. By 1) this language gives a new hyperdoctrine $H(L_M)$.

John Baez (Feb 18 2024 at 23:04):

In this situation there is a natural map of hyperdoctrines $i: H(L) \to H(L_M)$ and the map $\alpha$ extends to a map of hyperdoctrines

$\tilde{\alpha} : H(L_M) \to B(V)$

where "extends" means

$\tilde{\alpha} \circ i = \alpha$

John Baez (Feb 18 2024 at 23:15):

5) Now, to form the "elementary diagram hyperdoctrine" of $M$, we want to create for each $n$ a Boolean algebra $X(n)$, together with the appropriate maps between these. To do this we start with $H(L_M)(n)$, the Boolean algebra consisting of formulae $P$ with free variables $x_1, \dots, x_n$ in the language $L$ supplemented by constant symbols for each element of $V$. But then we take the image of this Boolean algebra under $\tilde{\alpha}$. This will be a Boolean subalgebra

$X(n) \subseteq B(V)(n)$

and that gives our desired "elementary diagram hyperdoctrine".

John Baez (Feb 18 2024 at 23:15):

Does that sound right?

John Baez (Feb 18 2024 at 23:17):

Thinking about this, I feel I should be setting up some basic constructions on hyperdoctrines before diving into this special case. For example in 5) I want to say that if you have a map of Boolean hyperdoctrines it has an "image" which is a Boolean hyperdoctrine.

James Hanson (Feb 18 2024 at 23:28):

John Baez said:

Does that sound right?

Yes that sounds reasonable to me. $B(V)$ also should correspond to a concept in some older model theory literature. Occasionally the idea of adding a predicate for every subset of every $V^n$ shows up, and it's sometimes called the 'complete expansion' or something. In Chang and Keisler section 6.4 they just call it the 'completion' of the structure.

This idea doesn't show up so much anymore though because the theory of such a structure is quite combinatorially wild, so modern model theory doesn't have much to say about it.

John Baez (Feb 18 2024 at 23:41):

Thanks! I don't know the model theory literature, but this 'completion' idea is necessary if we want to treat syntax and semantics on an equal footing, even if the idea of adding an n-ary predicate for every subset of the universe to the nth power sounds sort of insanely grandiose from a syntactic viewpoint.

John Baez (Feb 18 2024 at 23:42):

The idea of treating semantics as syntax lets you do lots of fun tricks in categorical logic, e.g. you can take something like the category of sets and ask "what is this the theory of?"

John Baez (Feb 18 2024 at 23:44):

But basically, hyperdoctrines will fall on the 'syntax' end of the spectrum if it's easier to describe maps out of them, and on the 'semantics' end if it's easier to describe in maps into them.

John Onstead (Feb 19 2024 at 00:00):

As someone learning hyperdoctrines this has been helpful!
I do wonder something: there's an equivalence of categories between that of first order theories and hyperdoctrines, meaning every hyperdoctrine corresponds to some first order theory and vice versa. In addition, there is a functor from the category of categories to that of hyperdoctrines that sends a category to its subobject hyperdoctrine. That is, the hyperdoctrine Sub(-) that assigns every object c of that category to the poset corresponding to that object's subobject poset Sub(c), and is meant to represent the internal logic of that category phrased in terms of hyperdoctrines. I'm wondering if this functor also constitutes an equivalence of categories. Just as it's true that every category has this canonical hyperdoctrine associated to it, is it also true that every hyperdoctrine has some corresponding category?

Spencer Breiner (Feb 19 2024 at 15:19):

I believe that a model of the elementary diagram on $M$ is an elementary embedding out of $M$ into some other model $M'$. That suggests your $\bar{\alpha}$ might be a left Kan extension.

James Hanson (Feb 20 2024 at 23:47):

Spencer Breiner said:

I believe that a model of the elementary diagram on $M$ is an elementary embedding out of $M$ into some other model $M'$. That suggests your $\bar{\alpha}$ might be a left Kan extension.

Yes, models of the elementary diagram of $M$ are elementary extensions of $M$.

What would be the significance of that map being a Kan extension? I've seen the term but I don't really understand what they are.

John Baez (Feb 21 2024 at 00:27):

Basically it means the thing I called $\tilde{\alpha}$ is the "obvious" or "canonical" way to extend $\alpha$ to the hyperdoctrine having a constant for each element of the universe of $M$.

John Baez (Feb 21 2024 at 00:33):

It's a good thing, to be sure! It's a "universal property", sort of like that of a colimit. I bet it means

models of the elementary diagram of $M$ are elementary extensions of $M$

but I'd have to think harder to be sure.

Morgan Rogers (he/him) (Feb 21 2024 at 21:51):

@Joshua Wrigley defended his thesis last week which was partly on doctrinal presentations of classifying toposes; maybe he has something to add to this discussion?

Joshua Wrigley (Feb 22 2024 at 14:58):

John Onstead said:

As someone learning hyperdoctrines this has been helpful!
I do wonder something: there's an equivalence of categories between that of first order theories and hyperdoctrines, meaning every hyperdoctrine corresponds to some first order theory and vice versa. In addition, there is a functor from the category of categories to that of hyperdoctrines that sends a category to its subobject hyperdoctrine. That is, the hyperdoctrine Sub(-) that assigns every object c of that category to the poset corresponding to that object's subobject poset Sub(c), and is meant to represent the internal logic of that category phrased in terms of hyperdoctrines. I'm wondering if this functor also constitutes an equivalence of categories. Just as it's true that every category has this canonical hyperdoctrine associated to it, is it also true that every hyperdoctrine has some corresponding category?

The equivalence between hyperdoctrines and theories depends on what notion one takes for a morphism of theories, but yes - given the correct definitions, this can be turned into a 2-equivalence (see for instance here).

To answer your question, the embedding ${\bf Lex} \xhookrightarrow{\rm Sub} {\bf PrimDoc}$ of left exact categories into what are called primary doctrines (doctrines that interpret the symbols $\land, \top$) is not essentially surjective. To immediately see why, there are special properties satisfied by ${\rm Sub}_C \colon C^{op} \to {\bf MSLat}$ which are not satisfied by all doctrines. For example, note that, given a category $C$, for each $d \in {\rm Sub}_C(c)$ there is an object in the base category (namely $d \in C$) for which ${\rm Sub}_C(d) \cong \downarrow \! d \subseteq {\rm Sub}_C(c)$.

If I'm not mistaken, this gets called something like comprehension. Questions on that are best directed to people like @Jacopo Emmenegger.

Instead of forming an equivalence, there is an adjunction: the restricted embedding ${\bf Reg} \hookrightarrow {\bf RegDoc}$ of regular categories into regular doctrines has a left adjoint - this is just the syntactic category of the theory associated to the doctrine!

Joshua Wrigley (Feb 22 2024 at 15:36):

James Hanson said:

How would you talk about elementary embeddings between models of the same theory?

Also, how would you talk about non-elementary maps between structures?

Here's an idea, though not necessarily what you were searching for:

Just to recall some standard definitions: given two Boolean hyperdoctrines $P \colon C^{op} \to {\bf Bool}$ and $Q \colon D^{op} \to {\bf Bool}$, a homomorphism of Boolean hyperdoctrines is a left exact functor $F \colon C \to D$ and a natural transformation $a \colon P \to Q \circ F^{op}$ that also preserves the adjoints, i.e. the square

$$\begin{CD} P(c) @>{\exists_f}>> P(d) \\ @V{a_c}VV @V{a_d}VV\\ Q(F(c)) @>{\exists_f}>> Q(F(d)) \end{CD}$$

commutes (note that, in the Boolean case, it suffices to only show that $a$ respects the left adjoints because $\forall = \neg \exists \neg$), while a transformation between a pair $(F,a),(F',a')$ is a natural transformation $\alpha \colon F \to F'$ and a modification $a \to a'$, i.e. $a_c(x) \leqslant Q(\alpha_c)(a_d(x))$ for all $x \in P(c)$.

The category of models of $P$ can now be recovered by simply taking ${\bf Mod}(P) \simeq {\bf BoolDoc}(P,\mathcal{P})$, where $\mathcal{P} \colon {\bf Set}^{op} \to {\bf Bool}$ is the powerset doctrine.

Joshua Wrigley (Feb 22 2024 at 15:37):

Note that every homomorphism $M \xrightarrow{f} N$ between two such models of a Boolean hyperdoctrine is elementary in the sense that

$$M \vDash \phi(b) \iff N \vDash \phi(f(b))$$

(where $M \vDash \phi(b)$ is read as $b \in M(c)$, $\phi \in P(c)$ and $b \in M(\phi)$). One direction $M \vDash \phi(b)\implies N \vDash \phi(f(b))$ follows from the definition of a homomorphism of models. The other direction is because $M$ also preserves the interpretation of negation.

Non-elementary maps come into play if we instead consider coherent hyperdoctrines (i.e. valued in ${\bf DLat}$ and only requiring left adjoints). In this case, the above trick does not work and we are left with the implication that $M \vDash \phi(b)\implies N \vDash \phi(f(b))$ and not the converse.

Of course, we can say that a homomorphism of models of a coherent hyperdoctrine is elementary if the square

$$\begin{CD} M(\phi) @>>> N(\phi) \\ @VVV @VVV\\ M(c) @>{f}>> N(c) \end{CD}$$

is a pullback in ${\bf Set}$ for each $\phi \in M(c)$.

It turns out that such homomorphisms of models can be expressed topos-theoretically (I haven't talked about the classifying topos theory for doctrines here, but you can imagine a definition) and have very interesting topological properties attached to them. I am currently working with Mark Kamsma on this very topic - so keep an eye out!

John Baez (Feb 22 2024 at 16:19):

Great stuff! By the way, what's $\mathbf{MSLat}$?

Frank Tsai (Feb 22 2024 at 17:39):

Suplattice with a top element I think

Joshua Wrigley (Feb 22 2024 at 17:59):

Meet-semilattices, so posets with all finite limits.