Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

July 14, 2010

What is a Theory?

Posted by Mike Shulman

Over at the nForum John just asked me an interesting question, which I think deserves a wider discussion. It’s about the relationship between logical theories and their walking models, a.k.a. “syntactic categories.” In particular, which is more deserving of the name “theory”? I’m going to present my point of view, but I’d love to hear others as well.

Traditionally, logicians have spoken of a (first-order, many-sorted, logical) “theory” in terms of types, operations, relations, and axioms. For instance, the theory of a group has one type, denoted GG, a binary operation m:(G,G)Gm\colon (G, G)\to G, a nullary operation e:()Ge\colon () \to G, a unary operation i:GGi\colon G\to G, and axioms m(m(x,y),z)=m(x,m(y,z))m(m(x,y),z) = m(x,m(y,z)), m(x,e)=x=m(e,x)m(x,e) = x = m(e,x), and m(x,i(x))=em(x,i(x)) = e. A model of such a theory, in the classical sense, consists of a set GG and functions m:G×GGm\colon G\times G\to G and e:1Ge\colon 1\to G satisfying the axioms, i.e. a group.

It’s easy to generalize this to define a model of a theory internal to a category with sufficient structure; for instance we can define a “group object” in any category with finite products. The level of structure required on the category is called the doctrine (or 2-theory) in which the theory is written; thus the theory of groups is written in the doctrine of finite-products categories. Moreover, for practically any doctrine DD and theory TT in it, there exists a DD-category that is the walking TT-model (also called the syntactic category or category of contexts of TT). This sort of yoga has been discussed here many times before; I know it came up here, and the notion of “walking thing” came up here. I know there are lots more links; anyone want to add some?

Now, many people, starting with Lawvere and including John Baez and Jim Dolan, have a tendency to identify a theory TT with the walking TT-model T\langle T \rangle. This undoubtedly has certain advantages. For instance, since TT-models in a DD-category CC are equivalent to DD-functors TC\langle T \rangle \to C, knowledge of T\langle T \rangle suffices to recover all the TT-models. Conversely, T\langle T \rangle is determined uniquely as a representing object for the functor CTMod(C)C \mapsto T Mod(C), so there is a nice duality. Moreover, syntactically different theories TT and TT' can give rise to equivalent categories TT\langle T \rangle \simeq \langle T' \rangle, and hence to an equivalent notion of model (we then say that TT and TT' are “Morita equivalent”). Thus, considering walking models to be the theories removes superfluous ambiguity.

Finally, the walking model T\langle T \rangle contains more information than the syntactic version of TT does. For instance, if TT is the theory of groups, then T\langle T \rangle tells you that there is exactly one way to multiply together any number of elements of a group once you fix their ordering. In other words, it is an unbiased presentation of the notion of group, which is arguably the version that we actually tend to use on a day-to-day basis.

Thus, over at the nForum, John remarked to me:

I got the impression from Jim Dolan that going from the “syntactic presentation” of a theory to the corresponding category was mainly a bunch of bureaucratic red tape, and that the really fun starts when we get past that stage and think of theories as being those categories. Sort of like how groups are more fun than group presentations, though of course those presentations are very useful. So, I’m a bit surprised that you seem to be taking more of the viewpoint of the traditional fuddy-duddy logician who likes nothing more than manipulating well-formed formulas according to purely syntactic rules.

So why do I (and some others, like Toby) continue to insist on talking about syntactic presentations, and distinguishing between a (syntactically presented) theory and its walking model?

The analogy with groups and group presentations is fairly compelling, so let’s start there. You won’t find me arguing with the claim that groups are more fun than group presentations, or that our real interest is in a group rather than any particular presentation of it. On the other hand, it is certainly true that a set of generators and relations for a group is a useful thing to have around.

What else can we say about the relationship between groups and group presentations? The fact that every set of generators and relations actually presents a group is fairly easy to see, but in more complicated situations it is a statement with content (Peter Johnstone and Steve Vickers wrote a whole paper about how and why preframes can be presented by generators and relations). Conversely, (a generalization of) the fact that every group can be presented by generators and relations is important to the monadicity theorem. Furthermore, for an arbitrary group presentation, determining facts about the group it presents is hard — not just computationally intractable, but computationally impossible.

For all of these reasons, I think it’s valid to say that there is real mathematics in the correspondence between groups and group presentations. I claim the same is true of theories, but even more so. I agree with all the reasons given above for why the walking model of a theory is good, useful, and lots of fun. However, consider the following.

  1. As I’ve opined before, one of the main things we do when we do mathematics (and especially when we communicate mathematics) is write down symbols on paper and manipulate them according to rules. Traditional logic studies, among other things, the symbols we write down, the rules we manipulate them with, and how those symbols and rules correspond to whatever “objects” we might be studying. The correspondence between syntactic presentations of theories and their walking models is part of this correspondence between symbols and “reality.” That just seems to me like an important thing to understand, from a metamathematical perspective if nothing else.

  2. In the case of groups, it’s fairly uncommon to be simply given a group presentation; usually we’re given a group in some other way and then produce a presentation of it. But giving objects via presentations gets more attractive as the objects get more complicated. For instance, the tensor product of abelian groups is often defined via generators and relations. Similarly, any algebraic extension of a field is naturally so defined. 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.

  3. Determining facts about the walking model of a theory (or, equivalently, about all models of that theory, since the walking model is the initial one), given only a presentation of it, is hard. For instance, let TT be the first-order (syntactically presented) theory ZFC, and let φ\varphi be the statement in the first-order language of ZFC that encodes the Riemann hypothesis. In the walking model ZFC\langle ZFC\rangle, the statement φ\varphi is incarnated by a subterminal object [φ]1[\varphi] \hookrightarrow 1. Showing that this map is an isomorphism is worth a million dollars.

Thus, I wouldn’t describe the passage from a syntactically presentated theory to its walking model as bureaucratic red tape. It’s certainly a purely formal operation, but that doesn’t make it uninteresting, unimportant, or trivial. Point one above says that it’s philosophically interesting; point two says that it’s important in practice, because we do it a lot; point three says that the resulting construction is quite nontrivial, and in fact can be regarded as encoding all of mathematics.

A final question, of course, is even if we grant that the two are both important, why shouldn’t we call them “theory presentations” and “theories” by analogy with “group presentations” and “groups”? I can think of two reasons. One is the traditional and entrenched usage of logicians. The other is that we already have a word for the Morita-invariant notion: namely, a DD-category, for whatever doctrine DD is in use. Thus we have a correspondence between “finite-products theories” and “categories with finite products,” another one between “first-order theories” and “Heyting categories,” another between “geometric theories” and “Grothendieck toposes,” and so on. Why should we define “geometric theory” to mean “Grothendieck topos” and force ourselves to say “presentation of a geometric theory” for the syntactic notion, when we already have the perfectly good term “Grothendieck topos” to refer to the categories in which (walking) models of geometric theories live?

Posted at July 14, 2010 5:34 AM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2242

41 Comments & 0 Trackbacks

Re: What is a Theory?

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.

Posted by: Toby Bartels on July 14, 2010 7:05 AM | Permalink | Reply to this

Re: What is a Theory?

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 TT and a finite-limits theory UU, then (if you think of the theories as the categories) it is natural to think that the question of whether TT and UU are essentially the same theory is the question of whether they are the same category. More precisely, you would apply the inclusion functor i:FinCompCatCartMonCati\colon Fin Comp Cat \to Cart Mon Cat to UU and then ask whether TT and i(U)i(U) are equivalent in the 22-category CartMonCatCart Mon Cat.

But in fact this is the wrong question! In particular, if you start with the theory of groups and define TT and UU each to be that theory in the relevant doctrine, then TT and i(U)i(U) are not equivalent in CartMonCatCart Mon Cat. Indeed, TT is a cartesian monoidal category that does not have all finite limits! (For example, it does not have an equaliser of G 2mGG^2 \overset{m}\to G and G 2bG 2mGG^2 \overset{b}\to G^2 \overset{m}\to G, where GG is the generating object, mm is the walking multiplication map, and bb is the braiding in the cartesian monoidal category. In other words, there is no object {(x,y)|xy=yx}\{(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 ii 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:CartMonCatFinCompCatj\colon Cart Mon Cat \to Fin Comp Cat which is left adjoint to ii. And it is useful to understand ii 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)j(T) is the theory of groups when TT is and not think that i(U)i(U) is the theory of groups when UU is. So the theory is not given consistently across doctrines by a single category, but it is given consistently by a single presentation.

Posted by: Toby Bartels on July 14, 2010 7:34 AM | Permalink | Reply to this

Re: What is a Theory?

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.

Posted by: Peter LeFanu Lumsdaine on July 14, 2010 2:09 PM | Permalink | Reply to this

Re: What is a Theory?

I think you actually just proved my point in (3). What I was trying to say is just that the walking model of a theory is, in general, a complicated object, whereas its syntactic presentation is a simpler one — and therefore something interesting and important (such as, for instance, all of mathematics) must be going on in the passage from one to the other. That is, it’s not just bureaucratic red tape. I think that’s totally in line with everything else you said.

Posted by: Mike Shulman on July 15, 2010 8:03 AM | Permalink | Reply to this

Re: What is a Theory?

I’m still not sure I quite agree. As I think of it, we’re implicitly talking about three categories (for each doctrine), which we could call:

  • SynPres\mathbf{SynPres}, syntactic presentations of theories;
  • SynThy\mathbf{SynThy}, syntactically presented theories;
  • CatThy\mathbf{CatThy}, categorically “embodied” theories.

SynThy\mathbf{SynThy} is typically a Kleisli over SynPres\mathbf{SynPres}, as my terminology suggests; this is where (non-categorial) proof theory starts (and spends much of its time), and this is where (to my eyes) the huge complexity blow-up happens.

On the other hand, SynThy\mathbf{SynThy} and CatThy\mathbf{CatThy} should be connected by… sometimes an equivalence, often just a 2-equivalence (for appropriate higher cells).

I guess I was reading your original question as being about whether a “theory” should mean an object of CatThy\mathbf{CatThy} or of SynThy\mathbf{SynThy}; maybe you were giving SynPres\mathbf{SynPres} more consideration than I was?

Posted by: Peter LeFanu Lumsdaine on July 15, 2010 1:21 PM | Permalink | Reply to this

Re: What is a Theory?

I was not thinking of syntactic presentations of theories as forming any sort of category. But I suppose if you really insisted on making them into a category, you’d get something like SynPresSynPres, and then SynThySynThy is sort of halfway along the construction of walking models from such theories.

Posted by: Mike Shulman on July 16, 2010 4:27 AM | Permalink | Reply to this

Re: What is a Theory?

Mike wrote:

I was not thinking of syntactic presentations of theories as forming any sort of category.

Tut tut! Logic may wish to hold itself over the rest of math, but we category theorists enjoy pulling it off its perch, to see how it fares as an ordinary citizen.

Posted by: John Baez on July 16, 2010 5:36 AM | Permalink | Reply to this

Re: What is a Theory?

And category theory may wish to hold itself over the rest of math, but it’s occasionally useful to be reminded that there are many things in mathematics (not just in logic) which are not categories. (-:

Posted by: Mike Shulman on July 16, 2010 7:57 AM | Permalink | Reply to this

Re: What is a Theory?

For example, objects in categories.

Posted by: John Baez on July 16, 2010 8:45 AM | Permalink | Reply to this

Re: What is a Theory?

Right, those are functors. Functors are not categories, natural transformations are not even functors, etc. So not everything is a category!

Posted by: Toby Bartels on July 24, 2010 10:25 PM | Permalink | Reply to this

Re: What is a Theory?

Mike wrote:

…there are many things in mathematics (not just in logic) which are not categories.

Crikey! Say it ain’t so! :-P

That’s true, of course. But presentations of theories are at least objects of an evident groupoid, and, more to the point, are studied in a way that (implicitly) acknowledges this. The most conservative logician would agree that the theory of groups is “the same theory” whether we use the symbol \cdot or ×\times, and wouldn’t consider studying a property or construction which wasn’t invariant under this sort of renaming, i.e. under isomorphisms in what I was calling SynPres\mathbf{SynPres}. And much of the time, things are also invariant under isomorphisms in SynThy\mathbf{SynThy}. So for a category theorist, it may be helpful, and not inaccurate, to say that by “a theory” logicians mean an object of one of these categories. See next comment for a different continuation of this train of thought.

In “The time and space of Uncle Albert”, Gretchen notices that all the galaxies are moving away from ours, and at first thinks this must mean that ours is at the centre of the universe! But she quickly realises that hubris isn’t really implied: in an expanding universe, this is true of every galaxy.

Similarly, I don’t think it’s categorical chauvinism to point out that everything can (often trivially, but also often profitably) be viewed in terms of category theory. Everything can also be seen (often trivially, often profitably) as logic. Everything can be seen (often trivially, often profitably) as topology. There’s no conflict between these statements! :-)

Posted by: Peter LeFanu Lumsdaine on July 16, 2010 3:23 PM | Permalink | Reply to this

Re: What is a Theory?

The most conservative logician would agree that the theory of groups is “the same theory” whether we use the symbol \cdot or ×\times

A year ago, I would have said the same thing. But apparently that isn’t true: some people would like to actually distinguish between “groups written with \cdot” and “groups written with ×\times”.

I don’t think it’s categorical chauvinism to point out that everything can… be viewed in terms of category theory.

No, I don’t either. And I agree that at least the core of SynPres is important, and it’s a good categorical way to describe a syntactic presentation of a theory modulo renaming of symbols. I just didn’t have it in mind at first.

Posted by: Mike Shulman on July 17, 2010 6:51 AM | Permalink | Reply to this

Re: What is a Theory?

some people would like to actually distinguish between “groups written with \cdot” and “groups written with ×\times

That’s true… And further, I suppose, there are situations where we really do care about things not invariant under a similar sort of renaming: eg parsing issues depending on what kinds of strings/characters are used as identifiers. But I suspect the consensus terminology would be that this is the study of something like the implementation of a (presentation of a) theory, not just the theory itself.

Posted by: Peter LeFanu Lumsdaine on July 18, 2010 10:43 AM | Permalink | Reply to this

Re: What is a Theory?

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 11xx\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).

Posted by: Jacques Carette on July 14, 2010 2:57 PM | Permalink | Reply to this

Re: What is a Theory?

Out of curiosity, what would you classify the type of work people like Zeiberger do as?

Posted by: bane on July 14, 2010 5:40 PM | Permalink | Reply to this

Zeilberger

In general, he does discrete mathematics. A lot of it is of a combinatorial nature, and almost all of it involves finite objects. He expertly and deftly wields tools from quite a few area of mathematics, including Computer Algebra as well as other things often considered computer science (rather than math), to solve all sorts of difficult problems.

He is a user and big fan of mechanized mathematics, although he much prefers the computational aspects over the proof aspects (as he made very clear in a deliberately provocative invited talk at CICM in Paris last week, although he told me he really enjoyed my (also invited) talk on mechanized mathematics).

Posted by: Jacques Carette on July 15, 2010 1:11 AM | Permalink | Reply to this

Re: Zeilberger

Thanks for your thoughts.

I was thinking more in terms of you mentioning that computers can only manipulate syntax: it seems odd to think of his “holonomic ansatz”, or any of the more narrow “frameworks” such as the 2-D Collatz system framework, as syntactic manipulation. But thinking about it maybe that’s just me being unwilling to see the unfolding of the structures as the computation unfolds as syntactic.

(Incidentally, I get the impression that he thinks a computational strategy is a “way” of proving something, so one might say he’s more interested in aspects of computational proof than in other types of proof.)

Posted by: bane on July 15, 2010 3:38 PM | Permalink | Reply to this

Re: What is a Theory?

Most CASes will happily treat this as 0.

Posted by: Toby Bartels on July 15, 2010 1:42 AM | Permalink | Reply to this

Re: What is a Theory?

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.

Posted by: John Baez on July 15, 2010 8:10 AM | Permalink | Reply to this

Re: What is a Theory?

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? ;-)

Posted by: Peter LeFanu Lumsdaine on July 15, 2010 3:54 PM | Permalink | Reply to this

Re: What is a Theory?

If you define words to mean whatever you want them to mean, then of course they mean (to you) whatever you defined them to mean. However, I think that the word “theory” ought to retain some connection with the way it has been used by logicians for the past century or so! In the sentence you quoted I was using the word “theory” in an intuitive sense evoking this sort of meaning. I think that most of the categories with finite limits that we encounter in the wild it does not make sense to call “finite-limit theories.”

Posted by: Mike Shulman on July 16, 2010 4:33 AM | Permalink | Reply to this

Re: What is a Theory?

Mike wrote:

If you define words to mean whatever you want them to mean, then of course they mean (to you) whatever you defined them to mean.

Spoken like a true logician. The parenthetical phrase is a nice touch.

I think that most of the categories with finite limits that we encounter in the wild it does not make sense to call “finite-limit theories.”

Maybe — but I can’t help adding that it’s extremely fun to take categories that typically arise as ‘environments’, reinterpret them as ‘theories’, and see what their models are like.

In case my lingo isn’t clear: if TT and EE are two categories in some doctrine, I call a morphism f:TEf: T \to E a model of the theory TT in the environment EE.

For example, take the doctrine of categories with finite limits. FinSetFinSet is a category with finite limits which we often encounter as an environment. That is, we often look at models of finite limits theories in FinSetFinSet. But we can also turn around and ask questions like “what’s a model of FinSetFinSet in some category with finite limits EE?” — and the answers tend to be enjoyable.

These questions also make good puzzles when you’re trying to learn this stuff. So,what’s the answer to this one? Say if E=SetE = Set, for example. What’s a model of FinSetFinSet in SetSet?

In other words, a bit more formally: what’s the category of finite-limit-preserving functors from FinSetFinSet to SetSet, and natural transformations between these?

The point of the puzzle is to find a category equivalent to this, which we all know and love. And when you find the answer, you get an enjoyable chill running up your spine, because you see a strange new view of something familiar.

Posted by: John Baez on July 16, 2010 5:10 AM | Permalink | Reply to this

Re: What is a Theory?

What’s a model of FinSetFinSet in SetSet?

I know the answer, and it’s a well-chosen problem. A little too well-chosen if you ask me! In other words, if you replaced FinSetFinSet with some other finitely complete category pulled randomly off the shelf and asked the same question, chances are the answer would be an unenlightening mess.

Posted by: Todd Trimble on July 16, 2010 7:26 AM | Permalink | Reply to this

Re: What is a Theory?

I agree with Todd, although there is a particular “well-chosen” shelf off of which one could start pulling other examples where the answer is nice: namely, categories of finitely presented objects in locally finitely presentable categories.

Also, I would argue that the reason such examples are interesting is precisely because of the difference between syntactically presented theories and their walking models. When we pull a category off of some shelf and discover that it’s equivalent to the walking model of some theory, we get an enjoyable chill running up our spine because the formal “bureaucratic” construction of the walking model of that theory, which on its own is very inexplicit, turns out to have magically produced something familiar.

It often seems to me that people (especially category theorists) have a tendency to say that because As can all be interpreted as Bs in some way, there is no need for the notion of A. But if we didn’t have the notion of A, then we wouldn’t be able to talk about how all As are interpreted as Bs! And if even if we only care about Bs in the end, if As occur in nature, then surely that only makes the process by which As are interpreted as Bs more important, since we have to perform it on any A we encounter in order to make it into the B we really care about.

Posted by: Mike Shulman on July 16, 2010 7:54 AM | Permalink | Reply to this

Re: What is a Theory?

Mike wrote:

It often seems to me that people (especially category theorists) have a tendency to say that because As can all be interpreted as Bs in some way, there is no need for the notion of A.

I think this is forgivable as a kind of rhetorical outburst designed to attract people’s attention to concept B. However, it’s often pretty silly when taken literally.

But if we didn’t have the notion of A, then we wouldn’t be able to talk about how all As are interpreted as Bs!

Reminds me of something Pippi Longstocking said:

“This is why we are here,” said Teacher, “to be good and kind to other people.”

Pippi stood on her head on the horse’s back and waved her legs in the air. “Heigh-ho,” said she, “then why are the other people here?”

Posted by: John Baez on July 16, 2010 8:51 AM | Permalink | Reply to this

Re: What is a Theory?

Mike wrote:

people (especially category theorists) have a tendency to say that because As can all be interpreted as Bs in some way, there is no need for the notion of A.

As John says, this is quite silly if taken too seriously.

But what people (especially category theorists) tend to say more often is that because the (something) of A’s is equivalent to the (something) of B’s, we can move freely between A’s and B’s; they’re two ways of looking at the same things!

We know that various different representations of projective space are isomorphic (and by isomorphisms that are, if not quite canonical, at least conventional). If I talk about “a point of projective space”, no-one asks me whether I’m representing it by homogeneous co-ordinates, or as a 1-dimensional subspace, or what; we can work with it as whichever is most convenient, but which it actually “is” is a non-question. (And it’s not just category theorists that do this!)

Why don’t we feel the same way about theories? I must admit — taking my devil’s-advocate hat off — that I am with you on this: I do feel the need to clearly distinguish when I’m talking about a syntactically presented theory from when I’m talking about a categorically embodied one; and I wouldn’t be comfortable defining “theory”, unqualified, to be anything other than the syntactically presented version. But… I can’t quite justify this feeling, on principle! They’re equivalent categories; why does it matter which one we define a theory to be an object of?

Posted by: Peter LeFanu Lumsdaine on July 16, 2010 3:31 PM | Permalink | Reply to this

Re: What is a Theory?

Actually, I guess you’ve talked me nicely into answering my own questions. Viewed categorically, the logicians’ traditional use of “theory” can sometimes be seen as (something like) an object of SynPres\mathbf{SynPres}, and sometimes as (something like) an object of SynThy\mathbf{SynThy}. (And this distinction comes up, in non-categorical terms, in questions like “are Boolean Algebras and Boolean Rings the same theory?”)

Defining a theory to be an object of CatThy\mathbf{CatThy} would fit with the latter, but conflict with the former. So that’s perhaps why it’s both tempting and misleading to call an object of CatThy\mathbf{CatThy} a “theory” — which is why we’re probably better off qualifying it as something like “Lawvere theory” or “Morita-equivalence class of theories” (though that last is really an awful mouthful!)

Posted by: Peter LeFanu Lumsdaine on July 16, 2010 3:52 PM | Permalink | Reply to this

Re: What is a Theory?

Viewed categorically, the logicians’ traditional use of “theory” can sometimes be seen as (something like) an object of SynPres, and sometimes as (something like) an object of SynThy.

Yes, I think I agree. For instance, when people say something like “this description of theory X has infinitely many axioms, but it can also be finitely axiomatized,” clearly “theory” is not denoting an object of SynPres, since in that category changing the axioms would change the object. On the other hand, I think there are definitely ways in which the traditional usage of “theory” is narrower than the objects of SynThy.

In fact, now that I think about it, 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. For instance, I recall in my introductory logic book, at least, a definition of “theory” to mean a collection of sentences, in a fixed signature, closed under implication.

Thanks for helping to isolate what’s going on.

Posted by: Mike Shulman on July 17, 2010 7:41 AM | Permalink | Reply to this

Re: What is a Theory?

Mike wrote:

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

Ah, yes! Yes, I’d agree. So I suppose an object of SynPres would better be called something like an axiomatisation of a theory. Yep, this seems right.

So now that we’re happier about what the traditional use of “theory” means, in categorical terms, we have a better footing from which to make provocative claims that it should mean something else :-P

Posted by: Peter LeFanu Lumsdaine on July 18, 2010 10:55 AM | Permalink | Reply to this

Re: What is a Theory?

So it seems like a theory (in any given doctrine) can be considered at various different levels of “completedness” or “embodiment.” From least to greatest, we have:

  1. An axiomatization in terms of types, operations, and axioms.
  2. The seemingly more traditional notion, with generating types and operations fixed, but the “axioms” are closed under implication.
  3. Something like a (generalized) operad/multicategory, where the generating types are fixed, but the operations are closed under composition and satisfaction of the axioms.
  4. A fully embodied walking model, in which all the type-constructing rules are also fully applied.

Do you see the property, structure, and stuff stratification getting into the game again? Perhaps we should come up with an adjective to describe this continuum and label these four levels with numbers.

Posted by: Mike Shulman on July 18, 2010 10:09 PM | Permalink | Reply to this

Re: What is a Theory?

Perhaps we should come up with an adjective to describe this continuum and label these four levels with numbers.

kk-axiomatised? kk-embodied?

Posted by: Toby Bartels on July 24, 2010 11:42 PM | Permalink | Reply to this

Re: What is a Theory?

Those are possibilities, but neither of them quite flows off of my tongue easily.

Posted by: Mike Shulman on July 26, 2010 12:14 AM | Permalink | Reply to this

Kaxiomatised and Kembodied; Re: What is a Theory?

Kaxiomatised and Kembodied flow easily enough off the tongue.

The first more or less rhymes with Taxi Home Goodbyes, and the second with Them Shoddied.

But nobody who wasn’t here first will have any idea what we’re babbling about.

Posted by: Jonathan Vos Post on July 26, 2010 10:08 PM | Permalink | Reply to this

Re: What is a Theory?

Mike wrote:

Do you see the property, structure, and stuff stratification getting into the game again?

Umm, yeah — especially after you shoved it right into our face.

Seriously, I think it’s brilliant:

In 1 you’re handing us the stuff, structure and properties syntactically.

In 2 you’re handing us the stuff and structure syntactically and taking some sort of closure of the properties.

In 3 you’re handing us the stuff syntatically and taking some sort of closure of the structure and properties.

In 4 you’re taking some sort of closure of the stuff, structure and properties.

Clearly this process will have more steps when we go from theories to doctrines to metadoctrines etc.

I keep saying the word “syntactically” above, but I don’t have any comparable word for the opposite, the thing where take some sort of closure that eliminates dependence on a specific presentation. What’s the right word? I don’t think “semantically” is it. Or is it?

Lawvere has some stuff about “concrete general” versus “abstract general”. Is that it?

Posted by: John Baez on July 19, 2010 10:17 AM | Permalink | Reply to this

some sort of closure of the stuff, structure and properties; Re: What is a Theory?

That’s so cool that I just linked again to that page, on Facebook, quoted Mike Shulman (with attribution and timestamp), and quoted John Baez’s enthusiatic response (with attribution and timestamp). What my 1,047 “friends” will think of it is up for grabs, as many are writers, teachers, artists, musicians, and not necessarily Mathematicians or Scientists. But really cool, to me. Thanks!

Posted by: Jonathan Vos Post on July 21, 2010 9:38 AM | Permalink | Reply to this

Re: What is a Theory?

Sorry, that was supposed to be a rhetorical question, not a patronizing one. Maybe I should stick to using simple sentences. (-: Or stick on more emoticons. (-:

I keep saying the word “syntactically” above, but I don’t have any comparable word for the opposite, the thing where take some sort of closure that eliminates dependence on a specific presentation. What’s the right word? I don’t think “semantically” is it. Or is it?

To me “semantics” refers to the process of talking about models of a given theory T in some category C (in some doctrine). So there’s at least some relationship between “semantics” and this “closure” process: the walking model of a theory is the target of its “universal semantics.” But it’s probably not the right word to use as a general descriptor.

Lawvere has some stuff about “concrete general” versus “abstract general”. Is that it?

Beats me. Is there anyone here who can explain what that’s about?

Posted by: Mike Shulman on July 19, 2010 6:28 PM | Permalink | Reply to this

Re: What is a Theory?

Mike wrote:

Sorry, that was supposed to be a rhetorical question, not a patronizing one.

Don’t mind me… I was just joking around.

John wrote:

Lawvere has some stuff about “concrete general” versus “abstract general”. Is that it?

Beats me. Is there anyone here who can explain what that’s about?

Maybe I used to know: in my summary of Lawvere’s ideas in week200, I wrote:

And this gives me an excuse to explain another bit of Lawvere’s jargon: while a theory is an “abstract general”, and particular model of it is a “concrete particular”, he calls the category of all its models in some category a “concrete general”. For example, Th(Grp) is an abstract general, and any particular group is a concrete particular, but Grp is a concrete general. I mention this mainly because Lawvere flings around this trio of terms quite a bit, and some people find them off-putting. There are lots of reasons to find his work daunting, but this need not be one.

In short, we have this kind of setup:

ABSTRACT GENERAL        CONCRETE GENERAL
theory                  models
syntax                  semantics

and a precise duality between the two columns!

So I don’t think these terms address the distinction we’re talking about here…

Posted by: John Baez on July 22, 2010 1:00 PM | Permalink | Reply to this

Re: What is a Theory?

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.

Posted by: Hamid on July 21, 2010 4:20 PM | Permalink | Reply to this

Re: What is a Theory?

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

Posted by: William Boshuck on July 25, 2010 5:24 PM | Permalink | Reply to this

Re: What is a Theory?

This was the sort of thing I had in mind earlier when I was thinking of SynThy\mathbf{SynThy} as the category of theories. But while this category certainly is considered classically, I don’t think this is where theories are basically thought of as living.

In particular, isomorphism in this category fails to preserve many logically interesting properties, so theories that are isomorphic in this category are often not thought of as “the same theory” – there’s a discussion somewhere back on the FOM archive about whether Boolean lattices and Boolean rings are “the same theory”, and iirc the majority view was that they aren’t — just inter-interpretable, with mutually inverse interpretations.

On the other hand, there were certainly proponents of both points of view… I think this question may depend very much on what field of logic people come from: a model theorist might be more likely to consider them the same theory than a proof theorist?

Posted by: Peter LeFanu Lumsdaine on July 25, 2010 7:27 PM | Permalink | Reply to this

Re: What is a Theory?

Thanks for pointing that out. Perhaps the conclusion to draw is that there is no one “traditional” notion of morphism of theories; we have (at least) four possible categories of theories (per doctrine) and they are all potentially interesting. All the more reason to have good systematic names for them.

Posted by: Mike Shulman on July 25, 2010 11:55 PM | Permalink | Reply to this

Post a New Comment