The n-Category Café

One reason why I want to use ‘theory’ for the syntactic notion (the presentation) is to make sure that I'm using that term for the right thing.

I see categorial logic as a form of applied mathematics, in fact applied metamathematics. First, we have these people, mathematicians, engaged in a social activity, and we wish to understand what they are doing. So we develop mathematical logic to study some aspects of this. And now we are applying category theory to that endeavour.

All well and good so far. But the danger in any applied mathematics is that, once you have a mathematical model in mind, you may forget that your job is to fit your model to the data and instead try to start fitting your data to the model. Then you start saying crazy things, such as that glass is not solid because it doesn't have a crystalline structure, or that shellfish are not fish because they don't have spinal cords. (I have picked one example where the current terminological consensus among scientists in the relevant field is with me and one where it is against me, but I'm prepared to defend either.)

In particular, I noticed that you left out something in your description of the theory of groups; among its types, operations, relations, and axioms, you listed only the types, operations, and axioms, even though the axioms cannot be stated without the relation: equality. Of course, you did this because you were implicitly working in a doctrine (presumably the doctrine of finite-products theories) in which every type is automatically equipped with such a relation. But of course, there are other doctrines.

This could be important, since most of the doctrines that are well understood in categorial logic have this property, yet there are doctrines that do not, which include important theories such as the theory of categories (up to equivalence, that is non-strict categories) themselves. It would be easy to fall into the trap of thinking that any theory (in any doctrine) must have equality relations on all of its types, or it's not really a theory.

Fortunately, this particular mistake is unlikely, since we do have some idea of how to deal with such theories in categorial logic (even if it's not as well understood). But we make this attempt in the first place because we meet such theories in practice and want to understand them. If we ever start thinking that the categories are the theories, especially if we fix a particular meaning of ‘doctrine’ and define ‘theory’ to mean an object of a doctrine, then we are liable to define away part of the matter that we were trying to study in the first place.

Sometimes this is the right thing to do, eventually. It proved useful to fix a definition of ‘group’ and develop group theory, even though this relegates some potential examples to the status of ‘semigroup’ or ‘quasigroup’. (Or ‘groupoid’, but now perhaps we are thinking that the definition was not fixed in the right way after all?) A fixed definition of ‘doctrine’ might very well be useful too. But categorial logic is a minority position, and a too restricted definition of ‘theory’ would make us unable to communicate with other logicians. We should leave that word to refer directly to the object of study, and use other words for our mathematical models of those objects.

Here is another reason to call the syntactic presentation the ‘theory’, which is more mathematical and less philosophical than my last one.

If you start thinking that a theory is a category, then you could easily confuse yourself when looking at two theories in different doctrines. Consider: the doctrine of finite-products theories consists of the cartesian monoidal categories, while the doctrine of finite-limits theories consists of the finitely complete categories. Every finitely complete category is cartesian monoidal, so if you have a finite-products theory $T$ and a finite-limits theory $U$, then (if you think of the theories as the categories) it is natural to think that the question of whether $T$ and $U$ are essentially the same theory is the question of whether they are the same category. More precisely, you would apply the inclusion functor $i\colon Fin Comp Cat \to Cart Mon Cat$ to $U$ and then ask whether $T$ and $i(U)$ are equivalent in the $2$-category $Cart Mon Cat$.

But in fact this is the wrong question! In particular, if you start with the theory of groups and define $T$ and $U$ each to be that theory in the relevant doctrine, then $T$ and $i(U)$ are not equivalent in $Cart Mon Cat$. Indeed, $T$ is a cartesian monoidal category that does not have all finite limits! (For example, it does not have an equaliser of $G^2 \overset{m}\to G$ and $G^2 \overset{b}\to G^2 \overset{m}\to G$, where $G$ is the generating object, $m$ is the walking multiplication map, and $b$ is the braiding in the cartesian monoidal category. In other words, there is no object $\{(x,y) \;|\; x y = y x\}$.)

In fact, it is not correct to interpret a finite-limits theory as a finite-products theory, as the functor $i$ would suggest. On the contrary, every finite-products theory is a finite-limits theory! (It is in this sense that the theory of groups, described by Mike above as a finite-products theory, is also a finite-limits theory.) It is very useful to understand this categorially; what we have is a functor $j\colon Cart Mon Cat \to Fin Comp Cat$ which is left adjoint to $i$. And it is useful to understand $i$ too, although it is complicated syntactically, which perhaps just makes the categorial approach even more inviting. Nevertheless, in order to understand ‘the theory of groups’ in several different doctrines, we need to know that $j(T)$ is the theory of groups when $T$ is and not think that $i(U)$ is the theory of groups when $U$ is. So the theory is not given consistently across doctrines by a single category, but it is given consistently by a single presentation.

Amen to all that! I’m interested to see you posting on this as it’s an issue that’s been exercising me a fair bit recently (writing up my thesis, deliberating over how to present a “category of theories”). In particular, your reasons (1) and (2) are the ones that seem most powerful to me.

Your reason (3) (“determining facts about the walking model of a theory is hard”) I’m somewhat less convinced by. It’s true; but I don’t think it’s coming particularly from the non-triviality of the syntax-to-model construction. Determining facts about complicated objects is often hard however they’re constructed!

Indeed, the presentations given by logic can often help prove things that are hard to get at by categorial means. (And also vice versa, of course, but that hardly needs saying around here.) I’m often tempted to think of logic, at least the proof-theoretic side, as the study of (powerful) presentations.

Extremely exciting. My work is best described as mechanized mathematics, i.e. teaching computers to do classical mathematics. There are others who concentrate on the constructive fragment of mathematics, but I don’t.

What should be patently obvious is that, on a computer, syntax is the only thing that can be manipulated. Unfortunately, this is generally ignored by practioners because all too often the morphisms between the logical theory and the walking models are ‘essentially’ isomorphisms. That and they tend to fix a doctrine in which to work [whatever ZFC categorifies to].

This is especially problematic when one tries to do “analysis with formulas”, in other words, find closed-forms for limits, integrals, differential equations, and so forth. The problem is most obvious here because the interpretation function is partial, in that many well-formed terms are undefined. My personal favourite being $\frac{1}{\frac{1}{x-x}}$. Most CASes will happily treat this as 0. Of course, if that term denotes anything at all, it has to be 0, but does it really denote?

All of this becomes extremely topical when you try to implement it all.

The other issue is that, once you have a syntactic representation of your theories, you can manipulate that representation. This is extremely useful to automatically derive new theories, as well as augmenting one’s theory with all sorts of additional tools (as long as they form conservative extensions, this is all fine). Unsurprisingly, (meta)mathematics is also highly structured, so that from small ‘specifications’ one can automatically generate large, rich theories which are much more convenient to work in. Right now, this has allowed me a factor of 10 reduction in my code base, as compared to the same features in say Axiom or Aldor (and a factor of 100 over Maple in some cases).

The ‘secret sauce’ starts with the fact that in the usual doctrines, finite colimits of theory presentations exist - and almost all algebraic structures (bigger list) can be fit into a clean (and rather small) network of colimits. Further operating on this network of theories, one can generate useful definitions like homomorphism, sub-theory, and so on; this, however, is best done ‘syntactically’, and in general requires inspection of the source theory’s syntactic structure [as, in some cases, the result might exist in the model but not be finitely presentable]. The most fun is recognizing the isomorphic theories that arise naturally from such a process (in particular, the theory of Group shows up 3 times with 3 different axiomatizations).

I’m glad Mike took my deliberately inflammatory remark and used it to ignite a discussion. I should add that there’s another side to my personality, the would-be proof theorist, who loves the idea of proofs as purely syntactic manipulations — in part because these proofs are analogous in many ways to processes in quantum physics! But I’m quite happy to take a one-sided view in order to stir up an interesting conversation.

Incidentally, re:

…and in the case of theories encountered in the wild, being given a presentation in terms of types, operations, and axioms is the rule rather than the exception.

isn’t this begging the question a little? If we take the full Lawverian view and define “theory” as “model of some categorical doctrine” (eg “finite product category”, “(l)ccc”, “cocomplete topos”…) then surely the ones we meet as syntactic presentations are by far in the minority? ;-)

Reading your post and some of the comments was really illuminating in my troubles with understanding some of the more physical theories and their categorical counterparts. The immediate example that I still have troubles with is Seiberg-Witten theory both categorically and physically as e.g. in Fuchs et al and Marcolli. n-Category cafe, I like to think and indulge myself, shed some light on why that is so although magnetic monopoles and spin manifolds seem so hard to learn in any language.

Michael Shulman said:

perhaps the closest thing to the traditional logician’s usage of “theory” would be a category intermediate between SynPres and SynThy, where the morphisms are required to preserve operations and relations as in SynPres, but to preserve axioms only as in SynThy

The traditional notion of morphism would be a little wider than this. For example—although it would not be put in these terms—for classical first order theories a morphism (interpretation) in the traditional sense corresponds to a presentation of a (coherent) morphism from the conceptual (Boolean) category of the domain theory to the conceptual (Boolean) pretopos of the codomain theory. This goes back at least to Robinson in the early 1950s. (Because of the kinds of theories of interest to model theorists, probably disjoint sums would not be mentioned explictly, but quotients of definable sets by definable equivalence relations certainly were.)