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.
I started a thread at the nCafe a while ago (16 years!) on the perception of a gap between Category Theory and Model Theory.
Good then to see Samson Abramsky's discussion of his research program reconciling the two wings of computer science, 'structure' and 'power', cast in terms of narrowing this gap:
This is a topic that I've wondered about from time to time and I haven't really seen what I would consider to be a comprehensive attempt at trying to see how these ideas could interact (apart from maybe the work on the relationship between AECs and accessible categories, but AECs are already not a huge part of model theory). For instance, Abramsky's paper is really focusing on finitary model theory, which is well known to have a fairly different character from 'Model Theory' model theory (i.e., model theory involving typically infinite models).
To me part of the issue is that Hodges' aphorism, 'model theory = algebraic geometry - fields', was never entirely true and arguably has been mostly untrue since the advent of stability theory in the 70s. I think that a fair amount of model theorists would agree that the content of modern model theory is far more 'combinatorial' than 'algebraic' in character. Most of the really prominent applications of model theory (e.g., Hrushovski's proof of the Mordell-Lang conjecture for function fields and various applications of o-minimality) are applications of the kinds of combinatorial tameness conditions modern model theory studies and less so applications of earlier model theory that was intentionally based on trying to generalize algebraic geometry (like Robinson's notion of model companions).
I feel like this is part of the reason not many tools of categorical logic (e.g., hyperdoctrines, classifying topoi, scheme-theoretic approaches to first-order logic, etc.) seem to have found applications in modern classical model theory. Those tools are most useful when you want to think about certain categories that show up naturally in model theory (like the category of imaginary sorts in a theory or the category of theories with interpretations), but this is a bit like trying to apply various nice properties of the category of groups to the study of amenable groups. Amenability is a fairly delicate combinatorial property that is only compatible with a handful of categorically natural operations on groups, so you don't get things like a good category of amenable groups.
Thanks @James E Hanson.
I was interested for a time in the 'two cultures of mathematics' idea of Tim Gowers, which distringuishes the Erdősian 'combinatorial' from the Grothendieckian 'structural', and in any indication of crossover, e.g., indications that measurability and category theory might get on better here.
James E Hanson said:
Amenability is a fairly delicate combinatorial property that is only compatible with a handful of categorically natural operations on groups, so you don't get things like a good category of amenable groups.
The quoted MO answer just shows that there isn't an adjoint to the forgetful functor from amenable groups to groups. It doesn't really make any claims about a category of amenable groups. That said, it would certainly be more natural for a category theorist to consider a category of "groups equipped with a left-invariant mean" rather than a category of "amenable groups", since being amenable is the propositional truncation of that structure. Similarly, to the extent that one would try to treat partitions of unity with category theory, one would consider a category of spaces equipped with partitions of unity rather than the spaces where we merely have existence, even though the mere existence is what is mostly used in practice.
I don't know how relevant to the discussion amenable groups specifically are; I presume it was just an analogy, although I did dig up at least one study of this property when searching.
However, on the general topic, I would like to point out that there are continuing developments in developing category theory towards model theory. Just last month, I attended talks in Manchester by @Mark Kamsma and Mike Lieberman on model-theoretic stable independence. Caramello has several papers on Fraisse theory and other model-theory-based work, and there were developments by Kubis too. There is no reason that I have seen to suppose that there couldn't be a far greater interaction between CT and model theory; it's only held back by the small population of people working on it.
Morgan Rogers (he/him) said:
There is no reason that I have seen to suppose that there couldn't be a far greater interaction between CT and model theory; it's only held back by the small population of people working on it.
Whenever someone argues CT can't be useful in topic X, I think exactly this thing. I don't think I've ever seen a technical (even informal) argument given to motivate such a claim (which may very well be true!), and often the state of affairs is simply that nobody tried, or that comparatively very few people work on that side of the tunnel.
Instead, there are many successful stories of areas where CT has proven useful when a community put their mind to do it. So I grew weary of such bold statements, which seem to me quite overconfident...
I wonder how traditional model theorists would view the work in
It is indeed true that not many people are working on the intersection of model theory and category theory, but it is a growing number and is gaining interest from the model-theoretic side as well. I know very little about finite model theory and the stuff in Abramsky's research programme. As @James E Hanson already pointed out, this is a different flavour from the model theory that considers infinite structures, which often claims the name "Model Theory". The famous stability theory takes place in the latter setting (although, it has made its way into finite model theory).
Quite recently, great progress has been made by approaching stability-theoretic ideas using accessible categories. This is very close to the setting of AECs, as James mentions as well, but more general (and, of course, category-theoretic). This was all kicked off by the paper Forking independence from the categorical point of view, by Lieberman, Rosický and Vasey (2019, https://doi.org/10.1016/j.aim.2019.02.018). This, and a series of follow-up papers, develop theory concering independence relations in a category-theoretic fashion. Independence relations are a central tool in stability theory. Examples of these things are really what the name suggests: linear independence (in vector spaces), algebraic independence (in algebraically closed fields) and probabilistic independence (in probability algebras). If you have ever heard the words "forking" or "dividing" in model-theoretic context, these are the abstract notions that give rise to such independence relations. I could go on, but this post would get too long, but if people are interested or want to know more then please ask!
As for the final post, referring to @Ivan Di Liberti's thesis: I am not sure if I qualify as a "traditional model theorist". I am definitely interested in that, and similar, work. However, it is a very different flavour from the accessible category stuff I just talked about. What I just talked about can be seen as a more semantical approach: we study something like the category of models of a theory, and do not care too much about how this was axiomatised. Ivan's work, and a lot of categorical logic, focuses more on the logical structure of the definable sets. This will be harder to sell to many (very) traditional model theorists. However, the community has recently become more and more interested in what we call "positive logic", which category theorists call "coherent logic", so who knows what connections can be made...
Matteo Capucci (he/him) said:
Morgan Rogers (he/him) said:
There is no reason that I have seen to suppose that there couldn't be a far greater interaction between CT and model theory; it's only held back by the small population of people working on it.
Whenever someone argues CT can't be useful in topic X, I think exactly this thing. I don't think I've ever seen a technical (even informal) argument given to motivate such a claim (which may very well be true!), and often the state of affairs is simply that nobody tried, or that comparatively very few people work on that side of the tunnel.
Instead, there are many successful stories of areas where CT has proven useful when a community put their mind to do it. So I grew weary of such bold statements, which seem to me quite overconfident...
For me the problem is that there are two rhetorical modes that different people commonly employ when talking about the broad applicability of category theory:
There are people who make extremely broad claims about the fundamental role category theory plays in virtually all of mathematics. This often goes hand-in-hand with a certain degree of derision directed towards people who don't tend to see categorical tools as useful in the mathematics they do.
There are people who make more mannered statements about how category theory is useful for things like unifying perspectives in different parts of math and suggesting generalizations and so on.
The second is very reasonable and I'm not trying to argue against that. I agree that you shouldn't make extremely broad claims about the inapplicability of category theory, but I also feel like there's a point with the first mode where a certain amount of push-back is warranted. For example, William Lawvere spent his entire career telling people that set theorists were doing set theory incorrectly because they weren't using topos theory, and I think his position is just completely unsustainable and frankly a bit ridiculous. I know how to prove far more about topos theory using uniquely set-theoretic tools than I know how to prove about set theory using uniquely topos-theoretic tools.
Model theory (and classical mathematical logic more broadly) does have a degree of cultural hostility towards category theory, but I think some of this comes from weariness of interacting with people like Lawvere. For example, model theory frequently uses the concept of 'monster models,' which are analogous to Weil's universal domain approach to algebraic geometry. Because universal domains have been completely obviated by the language of schemes in algebraic geometry, it's sometimes suggested that model theory is being backwards and would somehow be revolutionized by a shift to scheme-theoretic language, but I've talked to several model theorists who know category theory and/or algebraic geometry fairly well and there's just no clear picture of what that would really even mean. I (and other people in the field) know that there are papers about a scheme theoretic approach to model theory, but the point is that there isn't a clear benefit of the formalism. Schemes demonstrated themselves to be so useful in algebraic geometry that they're regarded as completely fundamental to the field now. In that context, they have easily passed the 'can you use this to prove something you would have cared about before becoming invested in the formalism' test.
I do wish that model theorists would get over this hostility. I've seen talks where people spend 5 minutes explaining that something is a functor, for instance. I also recently learned that a certain important fact in the study of -categorical theories was originally shown by Coquand (specifically that you can reconstruct the theory up to biinterpretability from the automorphism group of its unique countable model). Model theorists don't phrase it this way, but I'm guessing that Coquand originally conceived of the fact in terms of the equivalence of the classifying topos of an -categorical theory and the topos of continuous -sets, where is the unique countable model. I wish that people would talk about this connection more.
That said, I also think that it's reasonable for people to not bother spending time learning things that haven't yet demonstrated themselves to be especially useful in the context of topics they care about. Aside from Espíndola's claimed proof of the eventual categoricity conjecture, almost all of the work on applications of category theory to model theory I've seen have been in the vein of generalization, which is perfectly valid in and of itself, but it's not nearly as compelling as the kind of revolutionary role category theory played in algebraic topology and algebraic geometry. It doesn't need to groundbreaking work, but I haven't even seen what I would consider to be fundamental improvements in the difficulty of classic model theory results using things like the language of hyperdoctrines or classifying toposes.
Mark Kamsma said:
However, the community has recently become more and more interested in what we call "positive logic", which category theorists call "coherent logic", so who knows what connections can be made...
I noticed the fact that model theorists rediscovered coherent logic myself, and I've talked to some people about the connection. I also spent some time trying to see what could feasibly come of it, but I wasn't able to really come up with much that I was really confident in. How would you explain to a skeptical person what specifically is interesting or potentially useful about that connection?
The best I was able to come up with was that potentially you could repeat the story of stability theory in the context of Set-models of an arbitrary coherent theory. In other words, maybe you could show that the category of such models has a stable forking relation in the sense of Lieberman-Rosický-Vasey (i.e., a canonical notion of 'approximate pushouts' analogous to the compositum of fields) if and only if formulas in the language are all stable in the finitary combinatorial sense (i.e., not having the order property or having finite Littlestone dimension or however you want to phrase it). This could be interesting because coherent theories admit richer categories of models than ordinary first-order theories, but I don't know whether it actually works and I don't know what you would really be able to do with this.
Part of why I'm a little skeptical about how general of a picture you would get is that the model-theoretic work on this stuff seems to really need to talk about 'positively closed models' which are somewhat special in the general class of model of the theory (see for instance Haykazyan's work here). One natural example of a coherent theory with a rich category of models is of course the equational theory of groups, but the postively closed groups are the existentially closed groups, which have been known about for decades but rarely seem to show up naturally in group-theoretic contexts.
James E Hanson said:
I (and other people in the field) know that there are papers about a scheme theoretic approach to model theory
Such as @Spencer Breiner's Scheme representation for first-order logic. Has anyone tried more of a 'functor-of-points' approach to model theory, rather than the locally ringed space approach?
Let's see how that would work. I guess the idea would be that a 'theory' is nothing but a functorial assignment to each 'context' the category of models of that theory in that context. Sounds workable. Of course there are many choices of what we mean by 'context'. A 'kind of context' is often called a doctrine, but let's just do the familiar doctrine of categories with finite products. In this case a theory (in the approach we're dreaming of) would be a 2-functor
sending each finite products category the category of models of that theory in . To get things to work well, we may want to require that be better than a mere category: maybe it should have limits, colimits, etc. We probably also want to have some good properties.
All this is categorifying the functor of points approach where a scheme is a well-behaved functor
We get affine schemes from commutative rings by setting
but the fun starts when we consider more general ones that look 'locally' like affine schemes. Similarly, we get some functors
by taking a finite products category and letting
but the fun would start when we consider more general ones.